[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"
(modes: i => o => bool)
[show_steps, show_intermediate_results, show_mode_inference]
. (* 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?
Karlsruher Institut für Technologie
Dr. Andreas Lochbihler
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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