
diff -r f62d59cd8e1b -r cd6ce3322b8f LFex.thy
--- a/LFex.thy	Sat Nov 28 04:37:04 2009 +0100
+++ b/LFex.thy	Sat Nov 28 04:37:30 2009 +0100
@@ -182,56 +182,48 @@
 
 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 ball_simproc rel_eqvs ss redex =
+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"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) =>
+        ((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_respects_refl} OF [eqv]]);
-        val R1c = cterm_of @{theory} R1;
+        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 _ = 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);
@@ -249,26 +241,22 @@
 ML {*
 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 pat1 = [@{term "Ball (Respects R) P"}];
+    val pat2 = [@{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'
+    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 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 ball_reg_right},
+    rtac @{thm bex_reg_left},
+    resolve_tac (Inductive.get_monos ctxt),
     rtac @{thm move_forall},
     rtac @{thm move_exists},
-    (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc]))
+    simp_tac simp_ctxt
   ])
   end
 *}
@@ -337,9 +325,6 @@
     val te = @{thm eq_reflection} OF [t]
     val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
     val tl = Thm.lhs_of ts;
-(*    val _ = rrrt := ts;
-    val _ = rrr1 := ctrm;
-    val _ = rrr2 := tl;*)
     val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
     val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
 (*    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
@@ -378,12 +363,6 @@
 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
 ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *}
 apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *})
-thm FORALL_PRS[symmetric]
-ML_prf {*
-fun allex_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [1] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
-  THEN' (quotient_tac quot);
-*}
 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}




