--- a/FSet.thy	Tue Nov 24 08:35:04 2009 +0100
+++ b/FSet.thy	Tue Nov 24 08:36:28 2009 +0100
@@ -306,51 +306,38 @@
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *}
 
-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_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_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 {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} 
-ML {* lift_thm_fset @{context} @{thm map_append} *}
-ML {* val gl = @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
-
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val rtrm = prop_of (atomize_thm @{thm map_append}) *}
+ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *}
 
-ML {* val qtrm = atomize_goal @{theory} gl *}
-ML {* val a = (REGULARIZE_trm @{context} rtrm qtrm) *}
-
-ML {* val a = Syntax.check_term @{context} 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 map_append} gl *}
-
-
+ML {* lift_thm_fset @{context} @{thm map_append} *}
+ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
 ML {* lift_thm_fset @{context} @{thm list.induct} *}
 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
@@ -381,11 +368,60 @@
 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
+ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *}
+
+thm list.recs(2)
+ML {* lift_thm_fset @{context} @{thm list.recs(2)} *}
+ML {* lift_thm_g_fset @{context} @{thm list.recs(2)} @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *}
+
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
+ML {* val consts = lookup_quot_consts defs *}
+
+ML {* val gl = @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *}
+ML {* val t_a = atomize_thm @{thm list.recs(2)} *}
+ML {* val qtrm = atomize_goal @{theory} gl *}
+ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (REGULARIZE_trm @{context} (prop_of t_a) qtrm)) *}
+ML {* val rg2 = cterm_of @{theory}(my_reg @{context} rel rty (prop_of t_a)) *}
+
+ML {* val t_r = regularize_goal @{context} t_a rel_eqv rel_refl qtrm *}
+ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
+
+ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (inj_REPABS @{context} ((prop_of t_r), qtrm))) *}
+ML {* val rg2 = cterm_of @{theory} (build_repabs_term @{context} t_r consts rty qty) *}
+ML {* val t_t = repabs_goal @{context} t_r rty quot rel_refl trans2 rsp_thms qtrm *}
+ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
+ML {*
+  val lthy = @{context}
+  val (alls, exs) = findallex lthy rty qty (prop_of t_a);
+  val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
+  val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
+  val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
+  val abs = findabs rty (prop_of t_a);
+  val aps = findaps rty (prop_of t_a);
+  val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
+  val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
+  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
+  val defs_sym = flat (map (add_lower_defs lthy) defs);
+  val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
+  val t_id = simp_ids lthy t_l;
+  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
+  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
+  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+  val t_rv = ObjectLogic.rulify t_r
+
+*}
 
 
-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} *}