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