diff -r 196aa25daadf -r 199d1ae1401f LFex.thy
--- a/LFex.thy	Thu Nov 26 10:52:24 2009 +0100
+++ b/LFex.thy	Thu Nov 26 12:21:47 2009 +0100
@@ -197,6 +197,58 @@
 
 thm akind_aty_atrm.induct
 
+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
+  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))
+    ])
+  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
+  in
+  (ObjectLogic.full_atomize_tac) 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})
+  ])
+  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 "\<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'.
     \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk>
@@ -216,31 +268,52 @@
 \<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 {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *})
 apply(atomize (full))
-apply(rule my_equiv_res_forallR)
+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(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule my_equiv_res_forallR)
-apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
-apply(rule my_equiv_res_forallR)
-apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
-apply(rule my_equiv_res_forallR)
-apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
-apply(rule my_equiv_res_forallR)
-apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
-apply(rule my_equiv_res_forallR)
-apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
-apply(rule my_equiv_res_forallR)
-apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
-apply(rule my_equiv_res_forallR)
-apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *})
-apply(rule my_equiv_res_forallR)
-apply(tactic {*  (resolve_tac (Inductive.get_monos @{context})) 1 *})
+apply(rule Set.imp_mono)
+apply(rule impI) apply(assumption)
+apply(rule Set.imp_mono)
+apply(rule impI) apply(assumption)
+apply(rule Set.imp_mono)
+apply(rule impI) apply(assumption)
+apply(rule Set.imp_mono)
+apply(rule impI) apply(assumption)
+apply(rule Set.imp_mono)
+apply(rule impI) apply(assumption)
+apply(rule Set.imp_mono)
+apply(rule impI) apply(assumption)
+apply(rule Set.imp_mono)
+apply(rule impI) apply(assumption)
 apply(rule Set.imp_mono)
-apply(rule impI)
-apply(assumption)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (simp add: Ball_def IN_RESPECTS Respects_def)
+apply (metis COMBK_def al_refl(3))
+apply(rule Set.imp_mono)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (simp add: Ball_def IN_RESPECTS Respects_def)
+apply (metis COMBK_def al_refl(3))
 apply(rule Set.imp_mono)
-
-
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(rule move_quant)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(rule move_quant)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(rule move_quant)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (simp add: Ball_def IN_RESPECTS Respects_def)
+apply (metis COMBK_def al_refl(3))
+apply(rule impI) apply(assumption)
 
 ML {*
 val rty_qty_rel =
@@ -251,7 +324,7 @@
 
 print_quotients
 
-ML {* val rty = [@{typ }]
+ML {* val rty = [@{typ }] *}
 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
 ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *}
 prove {* build_regularize_goal t_a rty rel @{context}