--- 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 \<longrightarrow>"]}) 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)
+
+
+
+
--- 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 *: "\<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 *}
@@ -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) (\<lambda>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
*}