# HG changeset patch # User Cezary Kaliszyk # Date 1259377374 -3600 # Node ID 5a3965aa4d8032b0e61e117e5abfab7e5e697566 # Parent 98936120ab02a2c02590fe500400e76e7c0c5287 Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox. diff -r 98936120ab02 -r 5a3965aa4d80 LFex.thy --- a/LFex.thy Sat Nov 28 03:17:22 2009 +0100 +++ b/LFex.thy Sat Nov 28 04:02:54 2009 +0100 @@ -182,56 +182,48 @@ thm akind_aty_atrm.induct -lemma left_ball_regular: - assumes a: "EQUIV R" - shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" -apply (rule LEFT_RES_FORALL_REGULAR) -using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"] -apply (simp) -done - -lemma right_bex_regular: - assumes a: "EQUIV R" - shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" -apply (rule RIGHT_RES_EXISTS_REGULAR) -using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"] -apply (simp) -done - -lemma ball_respects_refl: - fixes P::"'a \ bool" - and x::"'a" - assumes a: "EQUIV R2" - shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" -apply(rule iffI) -apply(rule allI) -apply(drule_tac x="\y. f x" in bspec) -apply(simp add: Respects_def IN_RESPECTS) -apply(rule impI) -using a EQUIV_REFL_SYM_TRANS[of "R2"] -apply(simp add: REFL_def) -apply(simp) -apply(simp) -done - ML {* -fun ball_simproc rel_eqvs ss redex = +fun ball_reg_eqv_simproc rel_eqvs ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt in case redex of (ogl as ((Const (@{const_name "Ball"}, _)) $ - ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) => + ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => + (let + val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; + val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); + val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); +(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) + in + SOME thm + end + handle _ => NONE + ) + | _ => NONE + end +*} + +ML {* +fun ball_reg_eqv_range_simproc rel_eqvs ss redex = + let + val ctxt = Simplifier.the_context ss + val thy = ProofContext.theory_of ctxt + in + case redex of + (ogl as ((Const (@{const_name "Ball"}, _)) $ + ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => (let val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); val _ = tracing (Syntax.string_of_term ctxt glc); val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); - val thm = (@{thm eq_reflection} OF [@{thm ball_respects_refl} OF [eqv]]); - val R1c = cterm_of @{theory} R1; + val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); + val R1c = cterm_of thy R1; val thmi = Drule.instantiate' [] [SOME R1c] thm; - val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); +(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl val _ = tracing "AAA"; val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); @@ -249,26 +241,22 @@ ML {* fun regularize_tac ctxt rel_eqvs = let - val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs; - val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs; - val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2); - val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}]; + val pat1 = [@{term "Ball (Respects R) P"}]; + val pat2 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; val thy = ProofContext.theory_of ctxt - val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs)) - in - (ObjectLogic.full_atomize_tac) THEN' - (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) THEN' + val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) + val simproc2 = Simplifier.simproc_i thy "" pat2 (K (ball_reg_eqv_range_simproc rel_eqvs)) + val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2] + in + ObjectLogic.full_atomize_tac THEN' + simp_tac simp_ctxt THEN' REPEAT_ALL_NEW (FIRST' [ - (rtac @{thm RIGHT_RES_FORALL_REGULAR}), - (rtac @{thm LEFT_RES_EXISTS_REGULAR}), - (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), - (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), - (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), - (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), - (resolve_tac (Inductive.get_monos ctxt)), + rtac @{thm ball_reg_right}, + rtac @{thm bex_reg_left}, + resolve_tac (Inductive.get_monos ctxt), rtac @{thm move_forall}, rtac @{thm move_exists}, - (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) + simp_tac simp_ctxt ]) end *} @@ -337,9 +325,6 @@ val te = @{thm eq_reflection} OF [t] val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te val tl = Thm.lhs_of ts; -(* val _ = rrrt := ts; - val _ = rrr1 := ctrm; - val _ = rrr2 := tl;*) val (insp, inst) = make_inst (term_of tl) (term_of ctrm); val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; (* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) @@ -378,12 +363,6 @@ ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *} apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *}) -thm FORALL_PRS[symmetric] -ML_prf {* -fun allex_prs_tac lthy quot = - (EqSubst.eqsubst_tac lthy [1] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) - THEN' (quotient_tac quot); -*} apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} diff -r 98936120ab02 -r 5a3965aa4d80 QuotMain.thy --- a/QuotMain.thy Sat Nov 28 03:17:22 2009 +0100 +++ b/QuotMain.thy Sat Nov 28 04:02:54 2009 +0100 @@ -511,11 +511,11 @@ DT ctxt "4" (rtac @{thm impI} THEN' atac), DT ctxt "5" (rtac @{thm implication_twice}), DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])]), + [(@{thm ball_reg_eqv} OF [rel_eqv]), + (@{thm ball_reg_eqv} OF [rel_eqv])]), (* For a = b \ a \ b *) DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)), - DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) + DT ctxt "8" (rtac @{thm ball_reg_right}) ]); *} @@ -534,41 +534,6 @@ lemma [mono]: "P \ Q \ \Q \ \P" by auto -lemma ball_respects_refl: - fixes P Q::"'a \ bool" - and x::"'a" - assumes a: "EQUIV R2" - and b: "\f. Q (f x) \ P (f x)" - shows "(Ball (Respects (R1 ===> R2)) (\f. Q (f x)) \ All (\f. P (f x)))" -apply(rule impI) -apply(rule allI) -apply(drule_tac x="\y. f x" in bspec) -apply(simp add: Respects_def IN_RESPECTS) -apply(rule impI) -using a EQUIV_REFL_SYM_TRANS[of "R2"] -apply(simp add: REFL_def) -using b -apply(simp) -done - -lemma bex_respects_refl: - fixes P Q::"'a \ bool" - and x::"'a" - assumes a: "EQUIV R2" - and b: "\f. P (f x) \ Q (f x)" - shows "(Ex (\f. P (f x))) \ (Bex (Respects (R1 ===> R2)) (\f. Q (f x)))" -apply(rule impI) -apply(erule exE) -thm bexI -apply(rule_tac x="\y. f x" in bexI) -using b -apply(simp) -apply(simp add: Respects_def IN_RESPECTS) -apply(rule impI) -using a EQUIV_REFL_SYM_TRANS[of "R2"] -apply(simp add: REFL_def) -done - (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) ML {* fun equiv_tac rel_eqvs = @@ -582,6 +547,7 @@ fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) *} +(* ML {* fun regularize_tac ctxt rel_eqvs rel_refl = let @@ -603,6 +569,7 @@ (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))]) end *} +*) section {* Injections of REP and ABSes *} @@ -1206,7 +1173,7 @@ EVERY1 [rtac rule, RANGE [rtac rthm', - regularize_tac lthy rel_eqv rel_refl, + regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *) REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), clean_tac lthy quot defs aps]] end) lthy diff -r 98936120ab02 -r 5a3965aa4d80 QuotScript.thy --- a/QuotScript.thy Sat Nov 28 03:17:22 2009 +0100 +++ b/QuotScript.thy Sat Nov 28 04:02:54 2009 +0100 @@ -429,67 +429,96 @@ by (auto) -(* TODO: Put the following lemmas in proper places *) -lemma equiv_res_forall: +(* Set of lemmas for regularisation of ball and bex *) +lemma ball_reg_eqv: + fixes P :: "'a \ bool" + assumes a: "EQUIV R" + shows "Ball (Respects R) P = (All P)" + by (metis EQUIV_def IN_RESPECTS a) + +lemma bex_reg_eqv: fixes P :: "'a \ bool" - assumes a: "EQUIV E" - shows "Ball (Respects E) P = (All P)" - using a by (metis EQUIV_def IN_RESPECTS a) + assumes a: "EQUIV R" + shows "Bex (Respects R) P = (Ex P)" + by (metis EQUIV_def IN_RESPECTS a) + +lemma ball_reg_right: + assumes a: "\x. R x \ P x \ Q x" + shows "All P \ Ball R Q" + by (metis COMBC_def Collect_def Collect_mem_eq a) + +lemma bex_reg_left: + assumes a: "\x. R x \ Q x \ P x" + shows "Bex R Q \ Ex P" + by (metis COMBC_def Collect_def Collect_mem_eq a) + +lemma ball_reg_left: + assumes a: "EQUIV R" + shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" + by (metis EQUIV_REFL IN_RESPECTS a) -lemma equiv_res_exists: - fixes P :: "'a \ bool" - assumes a: "EQUIV E" - shows "Bex (Respects E) P = (Ex P)" - using a by (metis EQUIV_def IN_RESPECTS a) +lemma bex_reg_right: + assumes a: "EQUIV R" + shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" + by (metis EQUIV_REFL IN_RESPECTS a) -lemma FORALL_REGULAR: +lemma ball_reg_eqv_range: + fixes P::"'a \ bool" + and x::"'a" + assumes a: "EQUIV R2" + shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" + apply(rule iffI) + apply(rule allI) + apply(drule_tac x="\y. f x" in bspec) + apply(simp add: Respects_def IN_RESPECTS) + apply(rule impI) + using a EQUIV_REFL_SYM_TRANS[of "R2"] + apply(simp add: REFL_def) + apply(simp) + apply(simp) + done + +lemma bex_reg_eqv_range: + fixes P::"'a \ bool" + and x::"'a" + assumes a: "EQUIV R2" + shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" + apply(auto) + apply(rule_tac x="\y. f x" in bexI) + apply(simp) + apply(simp add: Respects_def IN_RESPECTS) + apply(rule impI) + using a EQUIV_REFL_SYM_TRANS[of "R2"] + apply(simp add: REFL_def) + done + +lemma all_reg: assumes a: "!x :: 'a. (P x --> Q x)" and b: "All P" shows "All Q" using a b by (metis) -lemma EXISTS_REGULAR: +lemma ex_reg: assumes a: "!x :: 'a. (P x --> Q x)" and b: "Ex P" shows "Ex Q" using a b by (metis) -lemma RES_FORALL_REGULAR: +lemma ball_reg: assumes a: "!x :: 'a. (R x --> P x --> Q x)" and b: "Ball R P" shows "Ball R Q" using a b by (metis COMBC_def Collect_def Collect_mem_eq) -lemma RES_EXISTS_REGULAR: +lemma bex_reg: assumes a: "!x :: 'a. (R x --> P x --> Q x)" and b: "Bex R P" shows "Bex R Q" using a b by (metis COMBC_def Collect_def Collect_mem_eq) -lemma LEFT_RES_FORALL_REGULAR: - assumes a: "\x. (R x \ (Q x \ P x))" - shows "Ball R Q \ All P" - using a - apply (metis COMBC_def Collect_def Collect_mem_eq a) - done -lemma RIGHT_RES_FORALL_REGULAR: - assumes a: "\x. R x \ P x \ Q x" - shows "All P \ Ball R Q" - using a - apply (metis COMBC_def Collect_def Collect_mem_eq a) - done -lemma LEFT_RES_EXISTS_REGULAR: - assumes a: "\x. R x \ Q x \ P x" - shows "Bex R Q \ Ex P" - using a by (metis COMBC_def Collect_def Collect_mem_eq) - -lemma RIGHT_RES_EXISTS_REGULAR: - assumes a: "\x. (R x \ (P x \ Q x))" - shows "Ex P \ Bex R Q" - using a by (metis COMBC_def Collect_def Collect_mem_eq) (* TODO: Add similar *) lemma RES_FORALL_RSP: