--- 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 *}