--- 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 *: "\<And>x. (P x \<longrightarrow> Q x)"
- shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
-using * by auto
-
-lemma implication_twice:
- assumes a: "c \<longrightarrow> a"
- assumes b: "b \<longrightarrow> d"
- shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> 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 \<longrightarrow> a \<approx> 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:
- "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
-by auto
-
-lemma move_exists:
- "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
-by auto
-
lemma [mono]:
"(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (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 \<Longrightarrow> a = b \<longrightarrow> 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 (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
(* 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 $ \<dots>) (t' $ \<dots>) \<Longrightarrow> 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 $ \<dots>) (t' $ \<dots>) \<Longrightarrow> 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) (\<lambda>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
*}