--- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
@@ -54,7 +54,8 @@
value [code] "Predicate.the (append_3 ([]::int list))"
subsection {* Tricky case with alternative rules *}
-
+text {* This cannot be handled correctly yet *}
+(*
inductive append2
where
"append2 [] xs xs"
@@ -70,7 +71,7 @@
case append2
from append2.cases[OF append2(1)] append2(2-3) show thesis by blast
qed
-
+*)
subsection {* Tricky cases with tuples *}
inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -370,10 +371,10 @@
code_pred (inductify_all) avl .
thm avl.equation
-
+(*
lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\<lambda>(y::'a::type). False)"
unfolding bot_fun_inst.bot_fun[symmetric] bot_bool_eq[symmetric] bot_fun_eq by simp
-
+*)
fun set_of
where
"set_of ET = {}"
@@ -384,9 +385,31 @@
"is_ord ET = True"
| "is_ord (MKT n l r h) =
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
+(*
+lemma empty_set[code_pred_def]: "{} = (\<lambda>x. False)" unfolding empty_def by simp
+thm set_of.simps[unfolded empty_set Un_def]
+*)
+(*
+declare empty_def[code_pred_def]
+*)
+ML {* prop_of (@{thm set_of.simps(1)}) *}
+thm Un_def
+thm eq_refl
+declare eq_reflection[OF empty_def, code_pred_inline]
+thm Un_def
+definition Un' where "Un' A B == A Un B"
-declare Un_def[code_pred_def]
+lemma [code_pred_intros]: "A x ==> Un' A B x"
+and [code_pred_intros] : "B x ==> Un' A B x"
+sorry
+
+code_pred Un' sorry
+lemmas a = Un'_def[symmetric]
+declare a[code_pred_inline]
+declare set_of.simps
+ML {* prop_of @{thm Un_def} *}
+ML {* tap *}
code_pred (inductify_all) set_of .
thm set_of.equation
(* FIXME *)
@@ -429,6 +452,8 @@
code_pred (inductify_all) List.rev .
thm revP.equation
+section {* Handling set operations *}
+
section {* Context Free Grammar *}