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