[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.