--- a/src/HOL/ex/Predicate_Compile_ex.thy Wed Jun 10 21:04:36 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Jun 11 12:06:13 2009 +0200
@@ -44,13 +44,15 @@
| "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
+(* FIXME: correct handling of parameters *)
+(*
ML {* reset Predicate_Compile.do_proofs *}
-
code_pred partition .
thm partition.equation
+ML {* set Predicate_Compile.do_proofs *}
+*)
-ML {* set Predicate_Compile.do_proofs *}
(* TODO: requires to handle abstractions in parameter positions correctly *)
(*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0)
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" *)
@@ -63,11 +65,11 @@
"r a b ==> tranclp r b c ==> tranclp r a c"
by auto
*)
-
+(*
code_pred tranclp .
thm tranclp.equation
-
+*)
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
--- a/src/HOL/ex/predicate_compile.ML Wed Jun 10 21:04:36 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Thu Jun 11 12:06:13 2009 +0200
@@ -1443,12 +1443,14 @@
(* TODO: must create state to prove multiple cases *)
fun generic_code_pred prep_const raw_const lthy =
let
+
val thy = ProofContext.theory_of lthy
val const = prep_const thy raw_const
+
val lthy' = LocalTheory.theory (PredData.map (Graph.extend (dependencies_of thy) const)) lthy
val thy' = ProofContext.theory_of lthy'
val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
- val _ = Output.tracing ("preds: " ^ commas preds)
+
fun mk_cases const =
let
val nparams = nparams_of thy' const
@@ -1458,7 +1460,8 @@
fun after_qed thms =
LocalTheory.theory (fold set_elim (map the_single thms) #> add_equations const)
in
- Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy'
+ Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy
+ (* FIXME: expected the actual local_theory to be lthy'; but works with lthy ??*)
end;
structure P = OuterParse