added theory with alternative definitions for the predicate compiler; cleaned up examples

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -129,8 +129,10 @@
 
 fun store_thm_in_table ignore_consts thy th=
   let
-    val th = AxClass.unoverload thy th
+    val th = th
       |> inline_equations thy
+      |> Pred_Compile_Set.unfold_set_notation
+      |> AxClass.unoverload thy
     val (const, th) =
       if is_equationlike th then
         let
@@ -139,9 +141,7 @@
         in
           (defining_const_of_equation eq, eq)
         end
-      else if (is_introlike th) then
-        let val th = Pred_Compile_Set.unfold_set_notation th
-        in (defining_const_of_introrule th, th) end
+      else if (is_introlike th) then (defining_const_of_introrule th, th)
       else error "store_thm: unexpected definition format"
   in
     if not (member (op =) ignore_consts const) then
@@ -191,7 +191,9 @@
 val logic_operator_names =
   [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "op &"}]
 
-val special_cases = member (op =) [@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
+val special_cases = member (op =) [
+    @{const_name "False"},
+    @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
     @{const_name Nat.one_nat_inst.one_nat},
 @{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
 @{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -15,7 +15,8 @@
 structure Pred_Compile_Set : PRED_COMPILE_SET =
 struct
 (*FIXME: unfolding Ball in pretty adhoc here *)
-val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}, @{thm Bex_def}]
+val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
+@{thm Ball_def}, @{thm Bex_def}]
 
 val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
 

--- a/src/HOL/ex/Predicate_Compile.thy	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Sat Oct 24 16:55:42 2009 +0200
@@ -14,52 +14,4 @@
 setup {* Predicate_Compile.setup *}
 setup {* Quickcheck.add_generator ("pred_compile", Pred_Compile_Quickcheck.quickcheck) *}
 
-section {* Alternative rules for set *}
-
-lemma set_ConsI1 [code_pred_intros]:
-  "set (x # xs) x"
-unfolding mem_def[symmetric, of _ x]
-by auto
-
-lemma set_ConsI2 [code_pred_intros]:
-  "set xs x ==> set (x' # xs) x" 
-unfolding mem_def[symmetric, of _ x]
-by auto
-(*
-code_pred set
-proof -
-  case set
-  from this show thesis
-    apply (case_tac a1)
-    apply auto
-    unfolding mem_def[symmetric, of _ a2]
-    apply auto
-    unfolding mem_def
-    apply auto
-    done
-qed
-*)
-
-section {* Alternative rules for list_all2 *}
-
-lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []"
-by auto
-
-lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
-by auto
-
-(*
-code_pred list_all2
-proof -
-  case list_all2
-  from this show thesis
-    apply -
-    apply (case_tac a1)
-    apply (case_tac a2)
-    apply auto
-    apply (case_tac a2)
-    apply auto
-    done
-qed
-*)
 end
\ No newline at end of file

--- 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 *}