# [isabelle] Preprocessor for code_pred

`I'm currently trying to reactivate the Execute theory of CoreC++ in the AFP. For
``historical reasons, it defines many inductive predicates as sets, which the
``predicate compiler cannot handle, but I do not want to change their definitions.
``Instead, I tried to use the predicate that inductive_set internally generates.
``Unfortunately, I do not know how to instruct the predicate compiler to use the
``compiled predicates instead of the sets when it compiles subsequent predicates.
``I have found three attributes (code_pred_inline, code_pred_def, and
``code_pred_simp), but none of them seems to do the preprocessing that I want.
`
Here is a small fictitious example of what happens frequently in CoreC++:
inductive_set minus2 :: "(nat * nat) set"
where "n ≥ 2 ==> (n, n - 2) : minus2"
code_pred (modes: i => o => bool) minus2p .
abbreviation (input) minus_even :: "nat => nat => bool"
where "minus_even n m == (n, m) : minus2^*"
lemma [code_pred_def, code_pred_inline, code_pred_simp]:
"((n, m) : minus2^*) = minus2p^** n m" sorry
inductive test :: "nat => nat => bool"
where "minus_even n m ==> test n m"
code_pred
(modes: i => o => bool)
[show_steps, show_intermediate_results, show_mode_inference]
test
. (* Fails to infer the specified mode *)

`Obviously, I could derive an introduction rule for test that does not go through
``the sets. But then, I have to prove the corresponding elimination rule, which
``can become very tedious. Is there any way I can instruct the predicate compiler
``to remove such detours via sets?
`
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Dr. Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
``in der Helmholtz-Gemeinschaft
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*