# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257324751 -3600
# Node ID b82e765ca4645fad1303a8f57938150001be0008
# Parent  ddd2f209d0d29f54a27ce3576e752c1cada76a3c
Lifting 'fold1.simps(2)' and some cleaning.

diff -r ddd2f209d0d2 -r b82e765ca464 FSet.thy
--- a/FSet.thy	Tue Nov 03 18:09:59 2009 +0100
+++ b/FSet.thy	Wed Nov 04 09:52:31 2009 +0100
@@ -178,8 +178,6 @@
 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
@@ -295,21 +293,36 @@
   (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)
+sorry
 
 print_quotients
 
 
 ML {* val qty = @{typ "'a fset"} *}
-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 rsp_thms =
-  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp}
+  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}
   @ @{thms ho_all_prs ho_ex_prs} *}
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
+
+
+
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
@@ -318,12 +331,30 @@
 (*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)} *}
 
-thm fold1.simps(2)
+term list_rec
+
+quotient_def
+  fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'b"
+where
+  "fset_rec \<equiv> list_rec"
+
 thm list.recs(2)
 thm list.cases
 
-ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
+
+
+
+
+
+ML {* val consts = lookup_quot_consts defs *}
+ML {* val defs_sym = 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 ind_r_a = atomize_thm @{thm card1_suc} *}
 (* prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
  ML_prf {*  fun tac ctxt =
      (FIRST' [
@@ -341,7 +372,7 @@
   apply (atomize(full))
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *}
-(*ML {*
+ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
@@ -349,7 +380,7 @@
 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 *})
-done*)
+done
 ML {* val ind_r_t =
   Toplevel.program (fn () =>
   repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms
diff -r ddd2f209d0d2 -r b82e765ca464 LamEx.thy
--- a/LamEx.thy	Tue Nov 03 18:09:59 2009 +0100
+++ b/LamEx.thy	Wed Nov 04 09:52:31 2009 +0100
@@ -38,6 +38,7 @@
   apply (simp_all add:a1 a2)
   apply (rule a3)
   apply (simp_all)
+  (* apply (simp add: pt_swap_bij'') *)
 sorry
 
 quotient lam = rlam / alpha
diff -r ddd2f209d0d2 -r b82e765ca464 QuotMain.thy
--- a/QuotMain.thy	Tue Nov 03 18:09:59 2009 +0100
+++ b/QuotMain.thy	Wed Nov 04 09:52:31 2009 +0100
@@ -1058,6 +1058,16 @@
 end
 *}
 
+ML {*
+  fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
+    let
+      val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
+      val (_, lthy2) = note (name, lifted_thm) lthy;
+    in
+      lthy2
+    end;
+*}
+
 
 end