--- a/FSet.thy	Tue Oct 27 14:14:30 2009 +0100
+++ b/FSet.thy	Tue Oct 27 14:15:40 2009 +0100
@@ -357,56 +357,19 @@
     | _ => []
 *}
 
-ML {* findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *}
-
-ML {*
- val lpi = Drule.instantiate'
-   [SOME @{ctyp "'a list"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};
-*}
-prove lambda_prs_l_b : {* concl_of lpi *}
-apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
-apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
-apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
-done
-thm HOL.sym[OF lambda_prs_l_b,simplified]
-ML {*
- val lpi = Drule.instantiate'
-   [SOME @{ctyp "'a list \<Rightarrow> bool"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};
-*}
-prove lambda_prs_lb_b : {* concl_of lpi *}
-apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
-apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
-apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
-done
-thm HOL.sym[OF lambda_prs_lb_b,simplified]
-
-
-
+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 *}
 
 ML {*
   fun simp_lam_prs lthy thm =
-    simp_lam_prs lthy (eqsubst_thm lthy
-      @{thms HOL.sym[OF lambda_prs_lb_b,simplified] HOL.sym[OF lambda_prs_l_b,simplified]}
-    thm)
+    simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
 *}
 
 ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *}
 
-ML {*
-  fun simp_allex_prs lthy thm =
-    let
-      val rwf = @{thm FORALL_PRS[OF QUOTIENT_fset]};
-      val rwfs = @{thm "HOL.sym"} OF [rwf];
-      val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]};
-      val rwes = @{thm "HOL.sym"} OF [rwe]
-    in
-      (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))
-    end
-    handle _ => thm
-*}
-
-ML {* val ithm = simp_allex_prs @{context} 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 *}
@@ -434,9 +397,8 @@
 done
 
 ML {* val card1_suc_t_n = @{thm card1_suc_t} *}
-ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *}
-ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *}
-ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *}
+ML {* val card1_suc_t' = simp_lam_prs @{context} @{thm card1_suc_t} *}
+ML {* val ithm = simp_allex_prs @{context} quot card1_suc_t' *}
 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *}
 ML {* ObjectLogic.rulify qthm *}
@@ -468,7 +430,7 @@
   Toplevel.program (fn () =>
   repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
    @{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})
   )
 *}
 ML {*