diff -r ca9eae5bd871 -r 7610d2bbca48 FSet.thy --- a/FSet.thy Wed Oct 28 01:48:45 2009 +0100 +++ b/FSet.thy Wed Oct 28 01:49:31 2009 +0100 @@ -187,8 +187,20 @@ *} ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} + +ML {* +fun add_lower_defs ctxt defs = + let + val defs_pre_sym = map symmetric defs + val defs_atom = map atomize_thm defs_pre_sym + val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) + in + map Thm.varifyT defs_all + end +*} ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} + lemma memb_rsp: fixes z assumes a: "list_eq x y" @@ -295,7 +307,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}) *} @@ -304,6 +316,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)) @@ -339,27 +360,6 @@ lemma id_apply2 [simp]: "id x \ 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 *} @@ -370,10 +370,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 *} @@ -408,8 +407,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} *} (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \"} @{context} *} ML_prf {* fun tac ctxt = (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @@ -423,33 +423,20 @@ 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) = +ML {* val ind_r_t = Toplevel.program (fn () => - repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} + repabs @{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 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])) - THEN' (rtac othm); *} -(* ML {* val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1); -*} *) - -ML {* - val ind_r_t2 = - Toplevel.program (fn () => - repabs_eq2 @{context} (g, thm, othm) - ) -*} -ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} +ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *} lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) done @@ -458,13 +445,10 @@ 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_d = repeat_eqsubst_thm @{context} 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 *} @@ -473,14 +457,13 @@ let val ind_r_a = atomize_thm thm; val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \"} @{thm equiv_list_eq} @{context}; - val (g, t, ot) = - repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} + val ind_r_t = + repabs @{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}); - val ind_r_t = repabs_eq2 @{context} (g, t, ot); + (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}); 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_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a; + val ind_r_a = simp_allex_prs @{context} quot ind_r_l; + val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a; val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d in ObjectLogic.rulify ind_r_s @@ -488,15 +471,19 @@ *} ML fset_defs +lemma eq_r: "a = b \ a \ b" +by (simp add: list_eq_refl) + ML {* lift @{thm m2} *} ML {* lift @{thm m1} *} ML {* lift @{thm list_eq.intros(4)} *} ML {* lift @{thm list_eq.intros(5)} *} ML {* lift @{thm card1_suc} *} -(* ML {* lift @{thm append_assoc} *} *) +ML {* lift @{thm map_append} *} +ML {* lift @{thm eq_r[OF append_assoc]} *} -thm +thm (*notation ( output) "prop" ("#_" [1000] 1000) *)