diff -r 8ca1150f34d0 -r 1e227c9ee915 FSet.thy
--- a/FSet.thy	Tue Oct 27 12:20:57 2009 +0100
+++ b/FSet.thy	Tue Oct 27 14:59:00 2009 +0100
@@ -292,7 +292,7 @@
 (* The all_prs and ex_prs should be proved for the instance... *)
 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}
+  r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
   (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
 *}
 
@@ -301,6 +301,15 @@
 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
+ML {* val rty = @{typ "'a list"} *}
+
+ML {*
+fun r_mk_comb_tac_fset ctxt =
+  r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+  (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
+*}
+
+
 ML {* trm_r *}
 prove list_induct_tr: trm_r
 apply (atomize(full))
@@ -336,27 +345,6 @@
 lemma id_apply2 [simp]: "id x \<equiv> x"
   by (simp add: id_def)
 
-ML {*
-   val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}];
-   val lpist = @{thm "HOL.sym"} OF [lpis];
-   val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist
-*}
-
-text {* the proper way to do it *}
-ML {*
-  fun findabs rty tm =
-    case tm of
-      Abs(_, T, b) =>
-        let
-          val b' = subst_bound ((Free ("x", T)), b);
-          val tys = findabs rty b'
-          val ty = fastype_of tm
-        in if needs_lift rty ty then (ty :: tys) else tys
-        end
-    | f $ a => (findabs rty f) @ (findabs rty a)
-    | _ => []
-*}
-
 ML {* val quot = @{thm QUOTIENT_fset} *}
 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *}
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
@@ -367,10 +355,9 @@
     handle _ => thm
 *}
 
-ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *}
+ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *}
 
 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *}
-ML fset_defs_sym
 
 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* ObjectLogic.rulify rthm *}
@@ -405,8 +392,9 @@
 
 thm fold1.simps(2)
 thm list.recs(2)
+thm map_append
 
-ML {* val ind_r_a = atomize_thm @{thm map_append} *}
+ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}
 (*  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
@@ -420,10 +408,10 @@
   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
 apply(atomize(full))
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (auto)
 done
 
 ML {* val (g, thm, othm) =
@@ -433,6 +421,7 @@
    (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
   )
 *}
+
 ML {*
     fun tac2 ctxt =
      (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
@@ -455,12 +444,9 @@
 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *}
 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}
 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}
-ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *}
+ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *}
 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
-
-
-ML {* hd fset_defs_sym *}
 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 ML {* ObjectLogic.rulify ind_r_s *}
@@ -476,7 +462,7 @@
      (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs});
   val ind_r_t = repabs_eq2 @{context} (g, t, ot);
   val ind_r_l = simp_lam_prs @{context} ind_r_t;
-  val ind_r_a = simp_allex_prs @{context} ind_r_l;
+  val ind_r_a = simp_allex_prs @{context} quot ind_r_l;
   val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;
   val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d
 in