Email Gateway (Aug 19 2022 at 09:08): Email Gateway (Aug 19 2022 at 09:08):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Last updated: Apr 18 2024 at 16:19 UTC