--- a/FSet.thy	Thu Nov 05 13:47:41 2009 +0100
+++ b/FSet.thy	Thu Nov 05 16:43:57 2009 +0100
@@ -175,8 +175,6 @@
 ML {* prop_of @{thm fmap_def} *}
 
 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
-ML {* val consts = lookup_quot_consts defs *}
-ML {* val defs_sym = add_lower_defs @{context} defs *}
 
 lemma memb_rsp:
   fixes z
@@ -272,40 +270,18 @@
   apply(auto intro: list_eq.intros)
   done
 
-lemma fun_rel_id:
-  "(op = ===> op =) \<equiv> op ="
-  apply (rule eq_reflection)
-  apply (rule ext)
-  apply (rule ext)
-  apply (simp)
-  apply (auto)
-  apply (rule ext)
-  apply (simp)
-  done
-
 lemma ho_map_rsp:
   "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map"
-  by (simp add: fun_rel_id map_rsp)
+  by (simp add: FUN_REL_EQ map_rsp)
 
 lemma map_append :
   "(map f (a @ b)) \<approx>
   (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
-lemma op_eq_twice: "(op = ===> op =) = (op =)"
-  apply (rule ext)
-  apply (rule ext)
-  apply (simp add: FUN_REL.simps)
-  apply auto
-  apply (rule ext)
-  apply simp
-done
-
-
-
 lemma ho_fold_rsp:
   "((op = ===> op = ===> op =) ===> (op = ===> op =) ===> op = ===> op \<approx> ===> op =) fold1 fold1"
-  apply (auto simp add: op_eq_twice)
+  apply (auto simp add: FUN_REL_EQ)
 sorry
 
 print_quotients
@@ -329,45 +305,51 @@
 ML {* lift_thm_fset @{context} @{thm list.induct} *}
 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
 
-term list_rec
-
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
   "fset_rec \<equiv> list_rec"
 
-(* ML {* Toplevel.program (fn () => lift_thm_fset @{context} @{thm list.recs(2)}) *} *)
+quotient_def
+  fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+where
+  "fset_case \<equiv> list_case"
+
+lemma list_rec_rsp:
+  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
+  apply (auto simp add: FUN_REL_EQ)
+  sorry
 
-thm list.recs(2)
-thm list.cases
+lemma list_case_rsp:
+  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
+  apply (auto simp add: FUN_REL_EQ)
+  sorry
+
+
+ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
+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 {* map (lift_thm_fset @{context}) @{thms list.recs} *}
+ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}
 
 
 
 
 
 
+
+(* Construction site starts here *)
+
+
 ML {* val consts = lookup_quot_consts defs *}
-ML {* val defs_sym = add_lower_defs @{context} defs *}
+ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
 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 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,
@@ -385,7 +367,6 @@
   apply (atomize(full))
   apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
   done*)
-
 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
@@ -400,10 +381,6 @@
 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 () =>
@@ -411,17 +388,20 @@
   )
 *}
 
-ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
+ML {* val abs = findabs rty (prop_of (t_a)) *}
+ML {* val aps = findaps rty (prop_of (t_a)) *}
 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 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 {* t_t *}
+ML {* val t_l0 = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *}
+ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms) t_l0 *}
 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 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 defs_sym = flat (map (add_lower_defs @{context}) defs) *}
+ML {* val t_id = simp_ids @{context} t_a *}
+ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *}
 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *}
 ML {* ObjectLogic.rulify t_s *}
 

--- a/LamEx.thy	Thu Nov 05 13:47:41 2009 +0100
+++ b/LamEx.thy	Thu Nov 05 16:43:57 2009 +0100
@@ -259,7 +259,7 @@
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
 
-ML {* val t_a = atomize_thm @{thm alpha.induct} *}
+ML {* val t_a = atomize_thm @{thm alpha.cases} *}
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
 ML_prf {*  fun tac ctxt =
      (FIRST' [
@@ -278,13 +278,13 @@
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 
-(*ML {*
+ML {*
   val rt = build_repabs_term @{context} t_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 *}
 prove rg
 apply(atomize(full))
-ML_prf {*
+(*ML_prf {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
     rtac trans_thm,
@@ -308,10 +308,37 @@
     ),
     WEAK_LAMBDA_RES_TAC ctxt
     ]);
+*}*)
+ML_prf {*
   fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
 *}
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+
+
+
+
+
+
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
-*)
+
 
 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}

--- a/QuotMain.thy	Thu Nov 05 13:47:41 2009 +0100
+++ b/QuotMain.thy	Thu Nov 05 16:43:57 2009 +0100
@@ -669,14 +669,13 @@
 )
 *}
 
-
-
 ML {*
 fun quotient_tac quot_thm =
   REPEAT_ALL_NEW (FIRST' [
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
-    rtac @{thm IDENTITY_QUOTIENT}
+    rtac @{thm IDENTITY_QUOTIENT},
+    (fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN rtac @{thm IDENTITY_QUOTIENT} i)
   ])
 *}
 
@@ -766,7 +765,8 @@
      (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
      THEN_ALL_NEW (fn _ => no_tac)
     ),
-    WEAK_LAMBDA_RES_TAC ctxt
+    WEAK_LAMBDA_RES_TAC ctxt,
+    (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i))
     ])
 *}
 
@@ -793,26 +793,32 @@
   apply (simp_all add: map.simps)
 done
 
+ML {*
+fun simp_ids lthy thm =
+  thm
+  |> MetaSimplifier.rewrite_rule @{thms id_def_sym}
+  |> repeat_eqsubst_thm lthy @{thms FUN_MAP_I id_apply prod_fun_id map_id}
+*}
+
 text {* expects atomized definition *}
 ML {*
-  fun add_lower_defs_aux ctxt thm =
+  fun add_lower_defs_aux lthy thm =
     let
       val e1 = @{thm fun_cong} OF [thm];
-      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;
-      val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;
-      val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g
+      val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
+      val g = simp_ids lthy f
     in
-      thm :: (add_lower_defs_aux ctxt h)
+      (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
     end
-    handle _ => [thm]
+    handle _ => [simp_ids lthy thm]
 *}
 
 ML {*
-fun add_lower_defs ctxt defs =
+fun add_lower_defs lthy def =
   let
-    val defs_pre_sym = map symmetric defs
-    val defs_atom = map atomize_thm defs_pre_sym
-    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
+    val def_pre_sym = symmetric def
+    val def_atom = atomize_thm def_pre_sym
+    val defs_all = add_lower_defs_aux lthy def_atom
   in
     map Thm.varifyT defs_all
   end
@@ -1012,9 +1018,10 @@
   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 = add_lower_defs lthy defs;
+  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_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;
+  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