# HG changeset patch # User Cezary Kaliszyk # Date 1256372213 -7200 # Node ID 13aab4c59096d645ea0663e4ad97d91d00f51493 # Parent 22cd68da9ae4cba3ba1553c3c508a93e7ba649f9 More infrastructure for automatic lifting of theorems lifted before diff -r 22cd68da9ae4 -r 13aab4c59096 FSet.thy --- a/FSet.thy Sat Oct 24 08:34:14 2009 +0200 +++ b/FSet.thy Sat Oct 24 10:16:53 2009 +0200 @@ -235,6 +235,11 @@ apply (simp_all add:memb_rsp) done +lemma ho_card1_rsp: "op \ ===> op = card1 card1" + apply (simp add: FUN_REL.simps) + apply (metis card1_rsp) + done + lemma cons_rsp: fixes z assumes a: "xs \ ys" @@ -259,11 +264,32 @@ thm list.induct lemma list_induct_hol4: fixes P :: "'a list \ bool" - assumes "((P []) \ (\t. (P t) \ (\h. (P (h # t)))))" - shows "(\l. (P l))" - sorry + assumes a: "((P []) \ (\t. (P t) \ (\h. (P (h # t)))))" + shows "\l. (P l)" + using a + apply (rule_tac allI) + apply (induct_tac "l") + apply (simp) + apply (metis) + done -ML {* atomize_thm @{thm list_induct_hol4} *} +ML {* +fun regularize thm rty rel rel_eqv lthy = + let + val g = build_regularize_goal thm rty rel lthy; + val tac = + (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 []); + val cgoal = cterm_of (ProofContext.theory_of lthy) g; + val cthm = Goal.prove_internal [] cgoal (fn _ => tac 1); + in + cthm OF [thm] + end +*} + prove list_induct_r: {* build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \"} @{context} *} @@ -295,6 +321,14 @@ (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) *} +ML {* +fun res_exists_rsp_tac ctxt = + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) + THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} + THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) +*} + ML {* fun quotient_tac quot_thm = @@ -314,9 +348,21 @@ | _ => fn _ => no_tac) i st *} +ML {* +fun WEAK_LAMBDA_RES_TAC ctxt i st = + (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of + (_ $ (_ $ _$(Abs(_,_,_)))) => + (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' + (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) + | (_ $ (_ $ (Abs(_,_,_))$_)) => + (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' + (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) + | _ => fn _ => no_tac) i st +*} + ML {* -fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm res_thms = +fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms = (FIRST' [ rtac @{thm FUN_QUOTIENT}, rtac quot_thm, @@ -325,8 +371,9 @@ rtac trans_thm, LAMBDA_RES_TAC ctxt, res_forall_rsp_tac ctxt, + res_exists_rsp_tac ctxt, ( - (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps (res_thms @ @{thms ho_all_prs}))) + (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps (rsp_thms @ @{thms ho_all_prs ho_ex_prs}))) THEN_ALL_NEW (fn _ => no_tac) ), (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), @@ -337,13 +384,34 @@ ( (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac) - ) + ), + WEAK_LAMBDA_RES_TAC ctxt ]) *} +ML Goal.prove + +ML {* +fun repabs 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 + 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} + 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} *} @@ -354,14 +422,6 @@ ML {* trm_r *} prove list_induct_tr: trm_r apply (atomize(full)) -(* APPLY_RSP_TAC *) -ML_prf {* val ctxt = @{context} *} -apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -(* LAMBDA_RES_TAC *) -apply (subst FUN_REL.simps) -apply (rule allI) -apply (rule allI) -apply (rule impI) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) done @@ -370,9 +430,16 @@ apply (tactic {* rtac thm 1 *}) done -ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} +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 ML {* atomize_thm @{thm m2} *} @@ -397,10 +464,9 @@ lemma id_apply2 [simp]: "id x \ x" by (simp add: id_def) -thm LAMBDA_PRS ML {* val t = prop_of @{thm LAMBDA_PRS} - val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{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] *} @@ -408,6 +474,13 @@ val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt val zzz = @{thm m2_t} *} +prove asdfasdf : {* concl_of tt *} +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 {* fun eqsubst_thm ctxt thms thm = @@ -423,9 +496,10 @@ Simplifier.rewrite_rule [rt] thm end *} -ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *} +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 [ObjectLogic.rulify rwr] *} +ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *} ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *} ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} ML {* ObjectLogic.rulify rthm *} @@ -433,14 +507,36 @@ ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} -prove card1_suc_r: {* - Logic.mk_implies - ((prop_of card1_suc_f), - (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \"} @{context})) *} +prove card1_suc_r_p: {* + build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \"} @{context} *} apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) - done +done + +ML {* val card1_suc_r = @{thm card1_suc_r_p} OF [atomize_thm @{thm card1_suc}] *} +ML {* val card1_suc_t_g = build_repabs_goal @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *} +ML {* val card1_suc_t = build_repabs_term @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *} +prove card1_suc_t_p: card1_suc_t_g +apply (atomize(full)) +apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) +done -ML {* @{thm card1_suc_r} OF [card1_suc_f] *} +prove card1_suc_t: card1_suc_t +apply (simp only: card1_suc_t_p[symmetric]) +apply (tactic {* rtac card1_suc_r 1 *}) +done + + +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 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: {* @@ -635,7 +731,6 @@ *} ML {* lift_theorem_fset_aux @{thm m1} @{context} *} - ML {* fun lift_theorem_fset name thm lthy = let diff -r 22cd68da9ae4 -r 13aab4c59096 QuotScript.thy --- a/QuotScript.thy Sat Oct 24 08:34:14 2009 +0200 +++ b/QuotScript.thy Sat Oct 24 10:16:53 2009 +0200 @@ -480,6 +480,12 @@ apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS) done +lemma RES_EXISTS_RSP: + shows "\f g. (R ===> (op =)) f g ==> + (Bex (Respects R) f = Bex (Respects R) g)" + apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS) + done + (* TODO: - [FORALL_PRS, EXISTS_PRS, COND_PRS]; > val it = @@ -498,9 +504,18 @@ shows "!f. All f = Ball (Respects R) ((absf ---> id) f)" sorry +lemma EXISTS_PRS: + assumes a: "QUOTIENT R absf repf" + shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)" + sorry + lemma ho_all_prs: "op = ===> op = ===> op = All All" apply (auto) done +lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex" + apply (auto) + done + end