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 *}