# HG changeset patch # User Cezary Kaliszyk # Date 1256382054 -7200 # Node ID da38ce2711a607d74b145c60b916cc968d37dce5 # Parent 13aab4c59096d645ea0663e4ad97d91d00f51493 More infrastructure for automatic lifting of theorems lifted before diff -r 13aab4c59096 -r da38ce2711a6 FSet.thy --- a/FSet.thy Sat Oct 24 10:16:53 2009 +0200 +++ b/FSet.thy Sat Oct 24 13:00:54 2009 +0200 @@ -278,11 +278,11 @@ let val g = build_regularize_goal thm rty rel lthy; val tac = - (simp_tac ((Simplifier.context lthy HOL_ss) addsimps + atac ORELSE' (simp_tac ((Simplifier.context lthy HOL_ss) addsimps [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])])) THEN' - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' - (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy []); + (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW + ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' + (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy [])); val cgoal = cterm_of (ProofContext.theory_of lthy) g; val cthm = Goal.prove_internal [] cgoal (fn _ => tac 1); in @@ -392,23 +392,31 @@ ML Goal.prove ML {* -fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = +fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = let val rt = build_repabs_term lthy thm constructors rty qty; val rg = Logic.mk_equals ((Thm.prop_of thm), rt); fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms)); val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); -(* val tac2 = - (simp_tac ((Simplifier.context lthy HOL_ss) addsimps [cthm])) - THEN' (rtac thm); - val cgoal = cterm_of (ProofContext.theory_of lthy) rt; - val cthm = Goal.prove_internal [] cgoal (fn _ => tac2); *) + in + (rt, cthm, thm) + end +*} + +ML {* +fun repabs_eq2 lthy (rt, thm, othm) = + let + fun tac2 ctxt = + (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) + THEN' (rtac othm); + val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1); in cthm end *} + 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} @@ -430,14 +438,6 @@ apply (tactic {* rtac thm 1 *}) done -ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *} -ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \"} @{thm equiv_list_eq} @{context} *} -ML {* 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} -*} - thm list.recs(2) thm m2 @@ -465,21 +465,21 @@ by (simp add: id_def) ML {* - val t = prop_of @{thm LAMBDA_PRS} - val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS} - val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}] - val tttt = @{thm "HOL.sym"} OF [ttt] + 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 {* - val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt - val zzz = @{thm m2_t} + val lpi = Drule.instantiate' + [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS}; *} -prove asdfasdf : {* concl_of tt *} +prove asdfasdf : {* 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 asdfasdf,simplified] ML {* @@ -496,11 +496,31 @@ Simplifier.rewrite_rule [rt] thm end *} -ML ttttt -ML {* val m2_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm m2_t} *} -ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} -ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *} -ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *} + +(* @{thms HOL.sym[OF asdfasdf,simplified]} *) + +ML {* + fun simp_lam_prs lthy thm = + simp_lam_prs lthy (eqsubst_thm lthy [lam_prs] 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 [spec OF [rwf]]; + val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]}; + val rwes = @{thm "HOL.sym"} OF [spec 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 rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} ML {* ObjectLogic.rulify rthm *} @@ -529,101 +549,71 @@ ML {* val card1_suc_t_n = @{thm card1_suc_t} *} ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm card1_suc_t} *} ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} card1_suc_t' *} -ML {* val ithm = eqsubst_thm @{context} [rwrs] card1_suc_t'' *} -ML {* val rwr = @{thm EXISTS_PRS[OF QUOTIENT_fset]} *} -ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *} -ML {* val jthm = eqsubst_thm @{context} [rwrs] ithm *} -ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym jthm *} +ML {* val ithm = simp_allex_prs @{context} 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 *} - -ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} -prove fold1_def_2_r: {* - Logic.mk_implies - ((prop_of li), - (regularise (prop_of li) @{typ "'a List.list"} @{term "op \"} @{context})) *} - apply (simp add: equiv_res_forall[OF equiv_list_eq]) - done - -ML {* @{thm fold1_def_2_r} OF [li] *} +thm fold1.simps(2) -lemma yy: - shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" -unfolding IN_def EMPTY_def -apply(rule_tac f="(op =) False" in arg_cong) -apply(rule memb_rsp) -apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) -apply(rule list_eq.intros) -done - -lemma - shows "IN (x::nat) EMPTY = False" -using m1 -apply - -apply(rule yy[THEN iffD1, symmetric]) -apply(simp) -done - -lemma - shows "((x=y) \ (IN x xs) = (IN (x::nat) (INSERT y xs))) = - ((x=y) \ x memb REP_fset xs = x memb (y # REP_fset xs))" -unfolding IN_def INSERT_def -apply(rule_tac f="(op \) (x=y)" in arg_cong) -apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) -apply(rule memb_rsp) -apply(rule list_eq.intros(3)) -apply(unfold REP_fset_def ABS_fset_def) -apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) -apply(rule list_eq_refl) -done - -lemma yyy: - shows " - ( - (UNION EMPTY s = s) & - ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2))) - ) = ( - ((ABS_fset ([] @ REP_fset s)) = s) & - ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2))) - )" - unfolding UNION_def EMPTY_def INSERT_def - apply(rule_tac f="(op &)" in arg_cong2) - apply(rule_tac f="(op =)" in arg_cong2) - apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) - apply(rule append_respects_fst) - apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) - apply(rule list_eq_refl) - apply(simp) - apply(rule_tac f="(op =)" in arg_cong2) - apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) - apply(rule append_respects_fst) - apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) - apply(rule list_eq_refl) - apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) - apply(rule list_eq.intros(5)) - apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) - apply(rule list_eq_refl) -done - -lemma - shows " - (UNION EMPTY s = s) & - ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))" - apply (simp add: yyy) - apply (simp add: QUOT_TYPE_I_fset.thm10) - done +ML {* val ind_r_a = atomize_thm @{thm fold1.simps(2)} *} +ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \"} @{thm equiv_list_eq} @{context} *} +ML {* + 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 {* (r_mk_comb_tac_fset @{context}) 1 *})*) +ML {* val (g, thm, othm) = + 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} + ) +*} +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 m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) + 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_a = simp_allex_prs @{context} ind_r_l *} +ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *} +ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} ML {* -cterm_of @{theory} (prop_of m1_novars); -cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}); +fun lift thm = +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"} + @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} + @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}; + 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_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 + ObjectLogic.rulify ind_r_s +end *} +ML {* lift @{thm m2} *} +ML {* lift @{thm m1} *} +ML {* lift @{thm list_eq.intros(4)} *} +ML {* lift @{thm list_eq.intros(5)} *} (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) ML {* diff -r 13aab4c59096 -r da38ce2711a6 QuotScript.thy --- a/QuotScript.thy Sat Oct 24 10:16:53 2009 +0200 +++ b/QuotScript.thy Sat Oct 24 13:00:54 2009 +0200 @@ -127,7 +127,7 @@ "FUN_REL E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" abbreviation - FUN_REL_syn ("_ ===> _") + FUN_REL_syn (infixr "===>" 55) where "E1 ===> E2 \ FUN_REL E1 E2" @@ -509,6 +509,7 @@ shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)" sorry +(* Currently fixed, should be general *) lemma ho_all_prs: "op = ===> op = ===> op = All All" apply (auto) done