# HG changeset patch # User Christian Urban # Date 1259383756 -3600 # Node ID d1aa26ecfecdaeaa6392b2bf9a37e67b856aa065 # Parent 3359033eff798b5789c767308d98147d762ca9bb# Parent 1c245f6911ddae9b97aa475c5d449983f24786c2 merged diff -r 3359033eff79 -r d1aa26ecfecd FSet.thy --- a/FSet.thy Sat Nov 28 05:47:13 2009 +0100 +++ b/FSet.thy Sat Nov 28 05:49:16 2009 +0100 @@ -322,7 +322,7 @@ lemma "CARD x = Suc n \ (\a b. \ IN a b & x = INSERT a b)" apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *}) -oops +done lemma "(\ IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) @@ -347,7 +347,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 *) @@ -450,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 3359033eff79 -r d1aa26ecfecd IntEx.thy --- a/IntEx.thy Sat Nov 28 05:47:13 2009 +0100 +++ b/IntEx.thy Sat Nov 28 05:49:16 2009 +0100 @@ -149,7 +149,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) *} @@ -189,8 +189,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 *}) @@ -226,7 +226,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 3359033eff79 -r d1aa26ecfecd LFex.thy --- a/LFex.thy Sat Nov 28 05:47:13 2009 +0100 +++ b/LFex.thy Sat Nov 28 05:49:16 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 3359033eff79 -r d1aa26ecfecd QuotMain.thy --- a/QuotMain.thy Sat Nov 28 05:47:13 2009 +0100 +++ b/QuotMain.thy Sat Nov 28 05:49:16 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 *} @@ -773,6 +871,62 @@ *} ML {* +<<<<<<< variant A +>>>>>>> variant B +val ball_rsp_tac = + Subgoal.FOCUS (fn {concl, context = ctxt, ...} => + case (term_of concl) of + (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => + ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) + THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} + THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' + (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 + |_ => no_tac) +*} + +ML {* +val bex_rsp_tac = + Subgoal.FOCUS (fn {concl, context = ctxt, ...} => + case (term_of concl) of + (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => + ((simp_tac (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 (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 + | _ => no_tac) +*} + +ML {* +fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) +*} + +ML {* +####### Ancestor +val ball_rsp_tac = + Subgoal.FOCUS (fn {concl, context = ctxt, ...} => + case (term_of concl) of + (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => + ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) + THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} + THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' + (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 + |_ => no_tac) +*} + +ML {* +val bex_rsp_tac = + Subgoal.FOCUS (fn {concl, context = ctxt, ...} => + case (term_of concl) of + (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => + ((simp_tac (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 (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 + | _ => no_tac) +*} + +ML {* +======= end fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = (FIRST' [resolve_tac trans2, LAMBDA_RES_TAC ctxt, @@ -880,6 +1034,31 @@ REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) *} +ML {* +fun get_inj_repabs_tac ctxt rel lhs rhs = +let + val _ = tracing "input" + val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel) + val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs) + val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs) +in + case (rel, lhs, rhs) of + (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *) + => rtac @{thm REP_ABS_RSP(1)} + | (_, Const (@{const_name "Ball"}, _) $ _, + Const (@{const_name "Ball"}, _) $ _) + => rtac @{thm RES_FORALL_RSP} + | _ => K no_tac +end +*} + +ML {* +fun inj_repabs_tac ctxt = + SUBGOAL (fn (goal, i) => + (case (HOLogic.dest_Trueprop goal) of + (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs + | _ => K no_tac) i) +*} section {* Cleaning of the theorem *} @@ -931,26 +1110,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))) @@ -1136,12 +1295,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 3359033eff79 -r d1aa26ecfecd QuotScript.thy --- a/QuotScript.thy Sat Nov 28 05:47:13 2009 +0100 +++ b/QuotScript.thy Sat Nov 28 05:49:16 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