--- a/FSet.thy	Thu Nov 05 10:46:54 2009 +0100
+++ b/FSet.thy	Thu Nov 05 13:36:46 2009 +0100
@@ -322,7 +322,7 @@
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
-(*ML {* lift_thm_fset @{context} @{thm map_append} *}*)
+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)} *}
@@ -334,6 +334,8 @@
 where
   "fset_rec \<equiv> list_rec"
 
+(* ML {* Toplevel.program (fn () => lift_thm_fset @{context} @{thm list.recs(2)}) *} *)
+
 thm list.recs(2)
 thm list.cases
 
@@ -348,7 +350,22 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
 
-ML {* val t_a = atomize_thm @{thm map_append} *}
+ML {* val t_a = atomize_thm @{thm list.recs(2)} *}
+ML {* val p_a = cprop_of t_a *}
+ML {* val pp = (snd o Thm.dest_abs NONE o snd o Thm.dest_comb o snd o Thm.dest_comb) p_a *}
+ML {* needs_lift @{typ "'a list"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} *}
+ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *}
+
+
+ML {* val tt = (my_reg @{context} (@{term list_eq}) ( @{typ "'a list"}) (term_of pp)) *}
+ML {* val (_, [R, _]) = strip_comb tt *}
+ML {* val (_, [R]) = strip_comb R *}
+ML {* val (f, [R1, R2]) = strip_comb R *}
+ML {* val (f, [R1, R2]) = strip_comb R2 *}
+ML {* val (f, [R1, R2]) = strip_comb R2 *}
+
+ML {* cterm_of @{theory} R2 *}
+
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
  ML_prf {*  fun tac ctxt = FIRST' [
       rtac rel_refl,
@@ -367,7 +384,7 @@
   apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
   done*)
 
-ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
+ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *}
 ML {*
   val rt = build_repabs_term @{context} t_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
@@ -380,6 +397,11 @@
 apply(atomize(full))
 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+
+"(op = ===> (op = ===> op \<approx> ===> op = ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
+"QUOTIENT op = (id ---> id) (id ---> id)"
+"(op = ===> op \<approx> ===> op =) x y"
+
 done
 ML {* val t_t =
   Toplevel.program (fn () =>
@@ -391,12 +413,11 @@
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
-ML {* val app_prs_thms = map Thm.freezeT app_prs_thms *}
+ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *}
 ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms @ lam_prs_thms) t_t *}
-ML {* val (alls, exs) = findallex rty qty (prop_of t_a); *}
+ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *}
 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
-ML {* val allthmsv = map Thm.varifyT allthms *}
-ML {* val t_a = MetaSimplifier.rewrite_rule (allthmsv) t_l *}
+ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_l *}
 ML {* val defs_sym = add_lower_defs @{context} defs *}
 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *}
 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *}