# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259007136 -3600
# Node ID b1f83c7a8674c33b2942af112b739060f2f05c01
# Parent  7e82493c6253c1a2e73892f76cc86112fb83aba1
More theorems lifted in the goal-directed way.

diff -r 7e82493c6253 -r b1f83c7a8674 FSet.thy
--- a/FSet.thy	Mon Nov 23 20:10:39 2009 +0100
+++ b/FSet.thy	Mon Nov 23 21:12:16 2009 +0100
@@ -304,25 +304,46 @@
   @ @{thms ho_all_prs ho_ex_prs} *}
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
-
-thm m2
+ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *}
 
-thm neq_Nil_conv
-term REP_fset
-term "op --->"
-thm INSERT_def
-ML {* val defs_sym = flat (map (add_lower_defs @{context}) @{thms INSERT_def}) *}
-(*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)
+ML {* atomize_thm @{thm m1} *}
+ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *}
 ML {* lift_thm_fset @{context} @{thm m1} *}
+ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
+ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \<or> IN x xa)"} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
+ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
+ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(5)} @{term "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
+ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \<Longrightarrow> \<exists>a b. \<not> IN a b \<and> x = INSERT a b"} *}
+ML {* lift_thm_fset @{context} @{thm not_mem_card1} *}
+ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *}
+ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
+(* Doesn't work with 'a, 'b, but works with 'b, 'a *)
+ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) =
+    (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}
+
+ML {* lift_thm_fset @{context} @{thm append_assoc} *}
+ML {* val goal_a = atomize_goal @{theory} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *}
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+(* Fails *)
+ML {* val reg_trm = mk_REGULARIZE_goal @{context} (prop_of (atomize_thm @{thm append_assoc})) goal_a *}
+
+
+
+
+ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *}
+
+ML {* lift_thm_g_fset @{context} @{thm append_assoc} gl *}
+
+
 ML {* lift_thm_fset @{context} @{thm map_append} *}
-ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 ML {* lift_thm_fset @{context} @{thm list.induct} *}
-ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
-ML {* lift_thm_fset @{context} @{thm not_mem_card1} *}
+ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
+
+(*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
@@ -357,6 +378,12 @@
 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *}
 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}
 
+ML {* atomize_thm @{thm m1} *}
+ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *}
+ML {* lift_thm_fset @{context} @{thm m1} *}
+(* ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"}) *} *)
+
+
 lemma list_induct_part:
   assumes a: "P (x :: 'a list) ([] :: 'a list)"
   assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
diff -r 7e82493c6253 -r b1f83c7a8674 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 20:10:39 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 21:12:16 2009 +0100
@@ -1117,16 +1117,21 @@
 fun atomize_goal thy gl =
   let
     val vars = map Free (Term.add_frees gl []);
-    fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm;
-    val gla = fold lambda_all vars (@{term "Trueprop"} $ gl)
+    val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;
+    fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;
+    val glv = fold lambda_all vars gl
+    val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))
     val glf = Type.legacy_freeze gla
-    val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf))
   in
-    term_of glac
+    if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf
   end
 *}
 
 
+ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
+ML {* atomize_goal @{theory} @{term "x = xa \<Longrightarrow> a # x = a # xa"} *}
+
+
 ML {*
 (* builds the relation for respects *)
  
@@ -1512,6 +1517,16 @@
 end
 *}
 
+ML {*
+fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal =
+  let
+    val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;
+    val (_, lthy2) = note (name, lifted_thm) lthy;
+  in
+    lthy2
+  end
+*}
+
 
 end