--- a/FSet.thy	Mon Oct 26 14:16:32 2009 +0100
+++ b/FSet.thy	Mon Oct 26 15:31:53 2009 +0100
@@ -60,7 +60,6 @@
 term UNION
 thm UNION_def
 
-
 thm QUOTIENT_fset
 
 thm QUOT_TYPE_I_fset.thm11
@@ -160,13 +159,31 @@
 term IN
 thm IN_def
 
+local_setup {*
+  make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term fold1
+term fold
+thm fold_def
+
+local_setup {*
+  make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term map
+term fmap
+thm fmap_def
+
+
 ML {*
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
                 @{const_name "membship"}, @{const_name "card1"},
-                @{const_name "append"}, @{const_name "fold1"}];
+                @{const_name "append"}, @{const_name "fold1"},
+                @{const_name "map"}];
 *}
 
-ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
+ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
 lemma memb_rsp:
@@ -220,10 +237,36 @@
   apply(induct a)
   sorry
 
-lemma (* ho_append_rsp: *)
+lemma ho_append_rsp:
   "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
 sorry
 
+lemma map_rsp:
+  assumes a: "a \<approx> b"
+  shows "map f a \<approx> map f b"
+  using a
+  apply (induct)
+  apply(auto intro: list_eq.intros)
+  done
+
+lemma ho_map_rsp:
+  "op = ===> op = ===> op \<approx> ===> op \<approx> map map"
+  apply (simp add: FUN_REL.simps)
+  apply (rule allI)
+  apply (rule allI)
+  apply (rule impI)
+  apply (rule allI)
+  apply (rule allI)
+  apply (rule impI)
+  sorry (* apply (auto simp add: map_rsp[of "xa" "ya"]) *)
+
+lemma map_append :
+  "(map f ((a::'a list) @ b)) \<approx>
+  ((map f a) ::'a list) @ (map f b)"
+ apply simp
+ apply (rule list_eq_refl)
+ done
+
 thm list.induct
 lemma list_induct_hol4:
   fixes P :: "'a list \<Rightarrow> bool"
@@ -250,7 +293,7 @@
 ML {*
 fun r_mk_comb_tac_fset ctxt =
   r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
-  (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs})
+  (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
 *}
 
 
@@ -401,7 +444,7 @@
 thm fold1.simps(2)
 thm list.recs(2)
 
-ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}
+ML {* val ind_r_a = atomize_thm @{thm map_append} *}
 (*  prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
   ML_prf {*  fun tac ctxt =
        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
@@ -415,9 +458,12 @@
   val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
-(*prove rg
+prove rg
 apply(atomize(full))
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})*)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (auto)
+done
+
 ML {* val (g, thm, othm) =
   Toplevel.program (fn () =>
   repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
@@ -485,6 +531,9 @@
 ML {* lift @{thm card1_suc} *}
 (* ML {* lift @{thm append_assoc} *} *)
 
+thm 
+
+
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 

--- a/IntEx.thy	Mon Oct 26 14:16:32 2009 +0100
+++ b/IntEx.thy	Mon Oct 26 15:31:53 2009 +0100
@@ -142,15 +142,6 @@
     repabs_eq2 @{context} (g, thm, othm)
   )
 *}
-ML {*
- val lpi = Drule.instantiate'
-   [SOME @{ctyp "nat \<times> nat"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};
-*}
-prove lambda_prs_mn_b : {* concl_of lpi *}
-apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
-apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-done
 
 ML {*
 fun make_simp_lam_prs_thm lthy quot_thm typ =
@@ -166,26 +157,23 @@
     val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);
     val ts = @{thm HOL.sym} OF [t]
   in
-    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_def}] ts
+    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts
   end
 *}
 
 
-
+thm id_apply
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 thm HOL.sym[OF lambda_prs_mn_b,simplified]
 
 ML {*
   fun simp_lam_prs lthy thm =
-    simp_lam_prs lthy (eqsubst_thm lthy
-      @{thms HOL.sym[OF lambda_prs_mn_b,simplified]}
-    thm)
+    simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
 *}
 ML {* t_t2 *}
 ML {* val t_l = simp_lam_prs @{context} t_t2 *}
-ML {* findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
 
 ML {*
   fun simp_allex_prs lthy thm =