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