--- a/LFex.thy	Sat Nov 28 04:02:54 2009 +0100
+++ b/LFex.thy	Sat Nov 28 05:29:30 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)
+
+
+
+