# HG changeset patch # User Cezary Kaliszyk # Date 1259382570 -3600 # Node ID 9c33c0809733f8eb40c947fc3e6e51658de44cb4 # Parent 5a3965aa4d8032b0e61e117e5abfab7e5e697566 Finished and tested the new regularize diff -r 5a3965aa4d80 -r 9c33c0809733 FSet.thy --- a/FSet.thy Sat Nov 28 04:02:54 2009 +0100 +++ b/FSet.thy Sat Nov 28 05:29:30 2009 +0100 @@ -307,7 +307,8 @@ ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *} lemma "IN x EMPTY = False" -by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) +apply (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) +done lemma "IN x (INSERT y xa) = (x = y \ IN x xa)" by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) @@ -347,7 +348,7 @@ lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) +apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) prefer 2 apply(rule cheat) apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) @@ -449,7 +450,7 @@ (* Construction site starts here *) lemma "P (x :: 'a list) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *}) -apply (tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) +apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) apply (rule FUN_QUOTIENT) apply (rule FUN_QUOTIENT) diff -r 5a3965aa4d80 -r 9c33c0809733 IntEx.thy --- a/IntEx.thy Sat Nov 28 04:02:54 2009 +0100 +++ b/IntEx.thy Sat Nov 28 05:29:30 2009 +0100 @@ -151,7 +151,7 @@ lemma "PLUS a b = PLUS b a" apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) +apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) prefer 2 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} @@ -191,8 +191,8 @@ lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) -apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) +apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) @@ -228,7 +228,7 @@ lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) +apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} diff -r 5a3965aa4d80 -r 9c33c0809733 LFex.thy --- a/LFex.thy Sat Nov 28 04:02:54 2009 +0100 +++ b/LFex.thy Sat Nov 28 05:29:30 2009 +0100 @@ -182,84 +182,6 @@ thm akind_aty_atrm.induct -ML {* -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"}, _)) $ 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_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 inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl - val _ = tracing "AAA"; - val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); - val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); - in - SOME thm2 - end - handle _ => NONE - - ) - | _ => NONE - end -*} - -ML {* -fun regularize_tac ctxt rel_eqvs = - let - val pat1 = [@{term "Ball (Respects R) P"}]; - val pat2 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; - val thy = ProofContext.theory_of ctxt - 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 ball_reg_right}, - rtac @{thm bex_reg_left}, - resolve_tac (Inductive.get_monos ctxt), - rtac @{thm move_forall}, - rtac @{thm move_exists}, - simp_tac simp_ctxt - ]) - end -*} ML {* val defs = @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def @@ -375,8 +297,24 @@ apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) -apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) 1 *}) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) + + + + diff -r 5a3965aa4d80 -r 9c33c0809733 QuotMain.thy --- a/QuotMain.thy Sat Nov 28 04:02:54 2009 +0100 +++ b/QuotMain.thy Sat Nov 28 05:29:30 2009 +0100 @@ -488,45 +488,6 @@ *) -lemma universal_twice: - assumes *: "\x. (P x \ Q x)" - shows "(\x. P x) \ (\x. Q x)" -using * by auto - -lemma implication_twice: - assumes a: "c \ a" - assumes b: "b \ d" - shows "(a \ b) \ (c \ d)" -using a b by auto - -(* version of regularize_tac including debugging information *) -ML {* -fun regularize_tac ctxt rel_eqv rel_refl = - (ObjectLogic.full_atomize_tac) THEN' - REPEAT_ALL_NEW (FIRST' - [(K (print_tac "start")) THEN' (K no_tac), - DT ctxt "1" (resolve_tac rel_refl), - DT ctxt "2" atac, - DT ctxt "3" (rtac @{thm universal_twice}), - DT ctxt "4" (rtac @{thm impI} THEN' atac), - DT ctxt "5" (rtac @{thm implication_twice}), - DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] - [(@{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 ball_reg_right}) - ]); -*} - -lemma move_forall: - "(\y. (\x\P. A x y) \ (\x. B x y)) \ ((\x\P. \y. A x y) \ (\x. \y. B x y))" -by auto - -lemma move_exists: - "((\y. \x. A x y) \ (\y. \x\P. B x y)) \ ((\x. \y. A x y) \ (\x\P. \y. B x y))" -by auto - lemma [mono]: "(\x. P x \ Q x) \ (Ex P) \ (Ex Q)" by blast @@ -544,32 +505,169 @@ *} ML {* -fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) +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"}, _)) $ 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 bex_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 "Bex"}, _)) $ + ((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 bex_reg_eqv} OF [eqv]]); +(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) + in + SOME thm + end + handle _ => NONE + ) + | _ => NONE + end +*} + +ML {* +fun prep_trm thy (x, (T, t)) = + (cterm_of thy (Var (x, T)), cterm_of thy t) + +fun prep_ty thy (x, (S, ty)) = + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) +*} + +ML {* +fun matching_prs thy pat trm = +let + val univ = Unify.matchers thy [(pat, trm)] + val SOME (env, _) = Seq.pull univ + val tenv = Vartab.dest (Envir.term_env env) + val tyenv = Vartab.dest (Envir.type_env env) +in + (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) +end *} -(* ML {* -fun regularize_tac ctxt rel_eqvs rel_refl = +fun ball_reg_eqv_range_simproc rel_eqvs ss redex = 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 ctxt = Simplifier.the_context ss + val thy = ProofContext.theory_of ctxt in - (ObjectLogic.full_atomize_tac) THEN' - (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs)) - THEN' - REPEAT_ALL_NEW (FIRST' - [(rtac @{thm RIGHT_RES_FORALL_REGULAR}), - (rtac @{thm LEFT_RES_EXISTS_REGULAR}), - (resolve_tac (Inductive.get_monos ctxt)), - (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), - (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), - rtac @{thm move_forall}, - rtac @{thm move_exists}, - (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))]) + 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_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 inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl + val _ = tracing "AAA"; + val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); + val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); + in + SOME thm2 + end + handle _ => NONE + + ) + | _ => NONE end *} -*) + +ML {* +fun bex_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 "Bex"}, _)) $ + ((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 bex_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 inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl + val _ = tracing "AAA"; + val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); + val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); + in + SOME thm2 + end + handle _ => NONE + + ) + | _ => NONE + end +*} + +lemma eq_imp_rel: "EQUIV R \ a = b \ R a b" +by (simp add: EQUIV_REFL) + +ML {* +fun regularize_tac ctxt rel_eqvs = + let + val pat1 = [@{term "Ball (Respects R) P"}]; + val pat2 = [@{term "Bex (Respects R) P"}]; + val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; + val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; + val thy = ProofContext.theory_of ctxt + val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) + val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) + val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) + val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) + val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] + (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *) + val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs + in + ObjectLogic.full_atomize_tac THEN' + simp_tac simp_ctxt THEN' + REPEAT_ALL_NEW (FIRST' [ + rtac @{thm ball_reg_right}, + rtac @{thm bex_reg_left}, + resolve_tac (Inductive.get_monos ctxt), + rtac @{thm ball_all_comm}, + rtac @{thm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simp_ctxt + ]) + end +*} section {* Injections of REP and ABSes *} @@ -741,24 +839,24 @@ *} +(* Doesn't work *) ML {* -fun APPLY_RSP_TAC rty = - CSUBGOAL (fn (concl, i) => +fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} => let val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); val insts = Thm.match (pat, concl) in - if needs_lift rty (type_of f) - then rtac (Drule.instantiate insts @{thm APPLY_RSP}) i + if needs_lift rty (type_of f) then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 else no_tac end handle _ => no_tac) *} + + ML {* -val ball_rsp_tac = - Subgoal.FOCUS (fn {concl, context = ctxt, ...} => +val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => let val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl @@ -772,8 +870,7 @@ *} ML {* -val bex_rsp_tac = - Subgoal.FOCUS (fn {concl, context = ctxt, ...} => +val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => let val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl @@ -787,6 +884,10 @@ *} ML {* +fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) +*} + +ML {* fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = (FIRST' [resolve_tac trans2, LAMBDA_RES_TAC, @@ -796,9 +897,9 @@ bex_rsp_tac ctxt, resolve_tac rsp_thms, rtac @{thm refl}, - (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' + (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thms)])), - (APPLY_RSP_TAC rty THEN' + (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), Cong_Tac.cong_tac @{thm cong}, rtac @{thm ext}, @@ -862,11 +963,11 @@ (* R (\) (Rep (Abs \)) \ R (\) (\) *) (* observe ---> *) - DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt + DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), (* R (t $ \) (t' $ \) \ APPLY_RSP provided type of t needs lifting *) - DT ctxt "A" ((APPLY_RSP_TAC rty THEN' + DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), (* R (t $ \) (t' $ \) \ Cong provided R = (op =) and t does not need lifting *) @@ -965,26 +1066,6 @@ THEN' (quotient_tac quot) *} -ML {* -fun prep_trm thy (x, (T, t)) = - (cterm_of thy (Var (x, T)), cterm_of thy t) - -fun prep_ty thy (x, (S, ty)) = - (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) -*} - -ML {* -fun matching_prs thy pat trm = -let - val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ - val tenv = Vartab.dest (Envir.term_env env) - val tyenv = Vartab.dest (Envir.type_env env) -in - (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) -end -*} - (* Rewrites the term with LAMBDA_PRS thm. Replaces: (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) @@ -1170,12 +1251,12 @@ val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv in - EVERY1 - [rtac rule, + EVERY1 + [rtac rule, RANGE [rtac rthm', - regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *) + regularize_tac lthy rel_eqv, REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), - clean_tac lthy quot defs aps]] + clean_tac lthy quot defs aps]] end) lthy *} diff -r 5a3965aa4d80 -r 9c33c0809733 QuotScript.thy --- a/QuotScript.thy Sat Nov 28 04:02:54 2009 +0100 +++ b/QuotScript.thy Sat Nov 28 05:29:30 2009 +0100 @@ -517,6 +517,13 @@ shows "Bex R Q" using a b by (metis COMBC_def Collect_def Collect_mem_eq) +lemma ball_all_comm: + "(\y. (\x\P. A x y) \ (\x. B x y)) \ ((\x\P. \y. A x y) \ (\x. \y. B x y))" +by auto + +lemma bex_ex_comm: + "((\y. \x. A x y) \ (\y. \x\P. B x y)) \ ((\x. \y. A x y) \ (\x\P. \y. B x y))" +by auto