--- a/LFex.thy Thu Nov 26 19:51:31 2009 +0100
+++ b/LFex.thy Thu Nov 26 20:32:33 2009 +0100
@@ -180,15 +180,6 @@
where
"perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
-
-
-
-
-
-
-
-
-
ML {* val defs =
@{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
@@ -197,78 +188,97 @@
thm akind_aty_atrm.induct
+lemma left_ball_regular:
+ assumes a: "EQUIV R"
+ shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
+apply (rule LEFT_RES_FORALL_REGULAR)
+using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
+apply (simp)
+done
+
+lemma right_bex_regular:
+ assumes a: "EQUIV R"
+ shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
+apply (rule RIGHT_RES_EXISTS_REGULAR)
+using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
+apply (simp)
+done
+
+lemma ball_respects_refl:
+ fixes P::"'a \<Rightarrow> bool"
+ and x::"'a"
+ assumes a: "EQUIV R2"
+ shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
+apply(rule iffI)
+apply(rule allI)
+apply(drule_tac x="\<lambda>y. f x" in bspec)
+apply(simp add: Respects_def IN_RESPECTS)
+apply(rule impI)
+using a EQUIV_REFL_SYM_TRANS[of "R2"]
+apply(simp add: REFL_def)
+apply(simp)
+apply(simp)
+done
+
ML {*
-fun regularize_monos_tac lthy eqvs =
- let
- val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) eqvs
- val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) eqvs
+fun ball_simproc rel_eqvs ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val thy = ProofContext.theory_of ctxt
in
- REPEAT_ALL_NEW (FIRST' [
- (rtac @{thm impI} THEN' atac),
- (rtac @{thm my_equiv_res_forallR}),
- (rtac @{thm my_equiv_res_forallL}),
- (rtac @{thm Set.imp_mono}),
- (resolve_tac (Inductive.get_monos lthy)),
- (EqSubst.eqsubst_tac lthy [0] (subs1 @ subs2))
- ])
+ case redex of
+ (ogl as ((Const (@{const_name "Ball"}, _)) $
+ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) =>
+ (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_respects_refl} OF [eqv]]);
+ val R1c = cterm_of @{theory} 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 {*
- val subs1 = map (fn x => @{thm eq_reflection} OF [@{thm equiv_res_forall} OF [x]]) @{thms alpha_EQUIVs}
-*}
-
-ML {*
-fun regularize_tac ctxt rel_eqvs rel_refls =
- 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
+fun regularize_tac ctxt rel_eqvs =
+ 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 pat = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+ val thy = ProofContext.theory_of ctxt
+ val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs))
in
(ObjectLogic.full_atomize_tac) THEN'
+ (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc]))
+ THEN'
REPEAT_ALL_NEW (FIRST' [
- FIRST' (map rtac rel_refls),
- atac,
- rtac @{thm universal_twice},
- rtac @{thm impI} THEN' atac,
- rtac @{thm implication_twice},
- EqSubst.eqsubst_tac ctxt [0] (subs1 @ subs2),
- (* For a = b \<longrightarrow> a \<approx> b *)
- (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+ (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
+ (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
+ (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+ (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+ (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+ (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+ (resolve_tac (Inductive.get_monos ctxt)),
+ rtac @{thm move_forall},
+ rtac @{thm move_exists}
])
end
*}
-thm RIGHT_RES_FORALL_REGULAR
-thm my_equiv_res_forallR
-(*
-lemma "\<And>i j xb\<Colon>trm \<Rightarrow> trm \<Rightarrow> bool. Respects (atrm ===> atrm ===> op =) xb \<Longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm\<in>Respects (atrm ===> atrm). xb (Const i) (m (Const j))) \<longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm. xb (Const i) (m (Const j)))"
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-*)
-
-lemma move_quant: "((\<forall>y. \<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>y. \<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 [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
-apply(auto)
-done
-
-lemma test:
- fixes P Q::"'a \<Rightarrow> bool"
- and x::"'a"
- assumes a: "REFL R2"
- and b: "\<And>f. Q (f x) \<longrightarrow> P (f x)"
- shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))"
-apply(rule impI)
-apply(rule allI)
-apply(drule_tac x="\<lambda>y. f x" in bspec)
-apply(simp add: Respects_def IN_RESPECTS)
-apply(rule impI)
-using a
-apply(simp add: REFL_def)
-using b
-apply(simp)
-done
lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K');
\<And>A A' K x x' K'.
@@ -289,12 +299,15 @@
\<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
+apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+
+apply(rule LEFT_RES_FORALL_REGULAR)
apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *})
apply(atomize (full))
apply(rule RIGHT_RES_FORALL_REGULAR)
apply(rule RIGHT_RES_FORALL_REGULAR)
apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
apply(rule test)
defer
apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+