
diff -r fafcc54e531d -r 7ef153ded7e2 LFex.thy
--- 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 *})+




