--- 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)"