# HG changeset patch # User Cezary Kaliszyk # Date 1256923866 -3600 # Node ID c770f36f9459e15ea7578f44fc67e7a9435485cd # Parent 1dd7f7f9804045a87fc2eeb1d327c8876a280e40 Regularization diff -r 1dd7f7f98040 -r c770f36f9459 FSet.thy --- a/FSet.thy Fri Oct 30 16:37:09 2009 +0100 +++ b/FSet.thy Fri Oct 30 18:31:06 2009 +0100 @@ -316,22 +316,33 @@ ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} ML {* lift_thm_fset @{context} @{thm card1_suc} *} ML {* lift_thm_fset @{context} @{thm map_append} *} -ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *} +ML {* lift_thm_fset @{context} @{thm append_assoc} *} thm fold1.simps(2) thm list.recs(2) thm list.cases -ML {* val ind_r_a = atomize_thm @{thm list.induct} *} -(*prove {* build_regularize_goal ind_r_a rty rel @{context} *} +ML {* val ind_r_a = atomize_thm @{thm m2} *} +prove {* build_regularize_goal ind_r_a rty rel @{context} *} ML_prf {* fun tac ctxt = - (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps + (FIRST' [ + rtac rel_refl, + atac, + (rtac @{thm allI} THEN' dtac @{thm spec}), + (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{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 ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *} - apply (tactic {* tac @{context} 1 *})*) + (@{thm equiv_res_exists} OF [rel_eqv])]) i)), + MetisTools.metis_tac ctxt [], + rtac (@{thm eq_rr} OF [rel_refl]), + ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) + ]); + *} + apply (tactic {* tac @{context} 1 *}) + apply (tactic {* tac @{context} 1 *}) + apply (tactic {* tac @{context} 1 *}) + + ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *} ML {* val rt = build_repabs_term @{context} ind_r_r consts rty qty diff -r 1dd7f7f98040 -r c770f36f9459 LamEx.thy --- a/LamEx.thy Fri Oct 30 16:37:09 2009 +0100 +++ b/LamEx.thy Fri Oct 30 18:31:06 2009 +0100 @@ -179,7 +179,6 @@ ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} - local_setup {* Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> @@ -219,6 +218,112 @@ +lemma get_rid: "(\x. (P x \ Q x)) \ ((\x. P x) \ (\x. Q x))" +apply (auto) +done + +lemma get_rid2: "(c \ a) \ (a \ b \ d) \ (a \ b) \ (c \ d)" +apply (auto) +done + +ML {* val t_a = atomize_thm @{thm alpha.cases} *} +prove {* build_regularize_goal t_a rty rel @{context} *} + ML_prf {* fun tac ctxt = + (FIRST' [ + rtac rel_refl, + atac, + rtac @{thm get_rid}, + rtac @{thm get_rid2}, + (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps + [(@{thm equiv_res_forall} OF [rel_eqv]), + (@{thm equiv_res_exists} OF [rel_eqv])]) i)), + (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl) + ]); + *} + apply (atomize(full)) + apply (tactic {* tac @{context} 1 *}) + apply (rule get_rid) + apply (rule get_rid) + apply (rule get_rid2) + apply (simp) + apply (rule get_rid) + apply (rule get_rid2) + apply (rule get_rid) + apply (rule get_rid2) + apply (rule impI) + apply (simp) + apply (tactic {* tac @{context} 1 *}) + apply (rule get_rid2) + apply (rule impI) + apply (simp) + apply (tactic {* tac @{context} 1 *}) + apply (simp) + apply (rule get_rid2) + apply (rule get_rid) + apply (rule get_rid) + apply (rule get_rid) + apply (rule get_rid2) + apply (rule impI) + apply (simp) + apply (tactic {* tac @{context} 1 *}) + apply (rule get_rid) + apply (rule get_rid2) + + + apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *}) +ML_prf {* +fun focus_compose t = Subgoal.FOCUS (fn {concl, ...} => + rtac t 1) +*} +thm spec[of _ "x"] + apply (rule allI) + apply (drule_tac x="a2" in spec) + apply (rule impI) + apply (erule impE) + apply (assumption) + apply (rule allI) + apply (drule_tac x="P" in spec) + apply (atomize(full)) + apply (rule allI) + apply (rule allI) + apply (rule allI) + apply (rule impI) + apply (rule get_rid2) + + thm get_rid2 + apply (tactic {* compose_tac (false, @{thm get_rid2}, 0) 1 *}) + + thm spec + + ML_prf {* val t = snd (Subgoal.focus @{context} 1 (Isar.goal ())) *} +ML_prf {* Seq.pull (compose_tac (false, @{thm get_rid}, 2) 1 t) *} + + + thm get_rid + apply (rule allI) + apply (drule spec) + + thm spec + apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *}) + + apply (tactic {* tac @{context} 1 *}) + apply (tactic {* tac @{context} 1 *}) + apply (rule impI) + apply (erule impE) + apply (assumption) + apply (tactic {* tac @{context} 1 *}) + apply (rule impI) + apply (erule impE) + apply (tactic {* tac @{context} 1 *}) + apply (tactic {* tac @{context} 1 *}) + apply (tactic {* tac @{context} 1 *}) + apply (tactic {* tac @{context} 1 *}) + +ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} +ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} +ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} +ML {* val t_a = simp_allex_prs @{context} quot t_l *} +ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym diff -r 1dd7f7f98040 -r c770f36f9459 QuotMain.thy --- a/QuotMain.thy Fri Oct 30 16:37:09 2009 +0100 +++ b/QuotMain.thy Fri Oct 30 18:31:06 2009 +0100 @@ -501,6 +501,10 @@ else Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t end + | Const (@{const_name "op ="}, ty) $ t => + if needs_lift rty (fastype_of t) then + (tyRel (fastype_of t) rty rel lthy) $ t + else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) | _ => trm *} @@ -513,16 +517,25 @@ (my_reg lthy rel rty (prop_of thm))) *} +lemma eq_rr: "(\x. R x x) \ a = b \ R a b" +by (auto) + ML {* -fun regularize thm rty rel rel_eqv lthy = +fun regularize thm rty rel rel_eqv rel_refl lthy = let val g = build_regularize_goal thm rty rel lthy; fun tac ctxt = - (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps + REPEAT_ALL_NEW (FIRST' [ + rtac rel_refl, + atac, + (rtac @{thm allI} THEN' dtac @{thm spec}), + (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{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 ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); + (@{thm equiv_res_exists} OF [rel_eqv])]) i)), + MetisTools.metis_tac ctxt [], + rtac (@{thm eq_rr} OF [rel_refl]), + ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) + ]); val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); in cthm OF [thm] @@ -907,7 +920,7 @@ val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; val consts = lookup_quot_consts defs; val t_a = atomize_thm t; - val t_r = regularize t_a rty rel rel_eqv lthy; + val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; val abs = findabs rty (prop_of t_a); val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;