
diff -r 5a3965aa4d80 -r 9c33c0809733 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 04:02:54 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 05:29:30 2009 +0100
@@ -488,45 +488,6 @@
 
 *)
 
-lemma universal_twice:
-  assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
-  shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
-using * by auto
-
-lemma implication_twice:
-  assumes a: "c \<longrightarrow> a"
-  assumes b: "b \<longrightarrow> d"
-  shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-using a b by auto
-
-(* version of regularize_tac including debugging information *)
-ML {*
-fun regularize_tac ctxt rel_eqv rel_refl =
-  (ObjectLogic.full_atomize_tac) THEN'
-  REPEAT_ALL_NEW (FIRST'
-   [(K (print_tac "start")) THEN' (K no_tac),
-    DT ctxt "1" (resolve_tac rel_refl),
-    DT ctxt "2" atac,
-    DT ctxt "3" (rtac @{thm universal_twice}),
-    DT ctxt "4" (rtac @{thm impI} THEN' atac),
-    DT ctxt "5" (rtac @{thm implication_twice}),
-    DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
-      [(@{thm ball_reg_eqv} OF [rel_eqv]),
-       (@{thm ball_reg_eqv} OF [rel_eqv])]),
-    (* For a = b \<longrightarrow> a \<approx> b *)
-    DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)),
-    DT ctxt "8" (rtac @{thm ball_reg_right})
-  ]);
-*}
-
-lemma move_forall: 
-  "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<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 move_exists: 
-  "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
-by auto
-
 lemma [mono]: 
   "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
 by blast
@@ -544,32 +505,169 @@
 *}
 
 ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+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 bex_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 "Bex"}, _)) $
+        ((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 bex_reg_eqv} OF [eqv]]);
+(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
+      in
+        SOME thm
+      end
+      handle _ => NONE
+      )
+  | _ => NONE
+  end
+*}
+
+ML {*
+fun prep_trm thy (x, (T, t)) =
+  (cterm_of thy (Var (x, T)), cterm_of thy t)
+
+fun prep_ty thy (x, (S, ty)) =
+  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+*}
+
+ML {*
+fun matching_prs thy pat trm =
+let
+  val univ = Unify.matchers thy [(pat, trm)]
+  val SOME (env, _) = Seq.pull univ
+  val tenv = Vartab.dest (Envir.term_env env)
+  val tyenv = Vartab.dest (Envir.type_env env)
+in
+  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+end
 *}
 
-(*
 ML {*
-fun regularize_tac ctxt rel_eqvs rel_refl =
+fun ball_reg_eqv_range_simproc rel_eqvs ss redex =
   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 ctxt = Simplifier.the_context ss
+    val thy = ProofContext.theory_of ctxt
   in
-  (ObjectLogic.full_atomize_tac) THEN'
-  (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs))
-  THEN'
-  REPEAT_ALL_NEW (FIRST' 
-    [(rtac @{thm RIGHT_RES_FORALL_REGULAR}),
-     (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
-     (resolve_tac (Inductive.get_monos ctxt)),
-     (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
-     (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
-     rtac @{thm move_forall},
-     rtac @{thm move_exists},
-     (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))])
+  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 bex_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 "Bex"}, _)) $
+        ((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 bex_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
+*}
+
+lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
+by (simp add: EQUIV_REFL)
+
+ML {*
+fun regularize_tac ctxt rel_eqvs =
+  let
+    val pat1 = [@{term "Ball (Respects R) P"}];
+    val pat2 = [@{term "Bex (Respects R) P"}];
+    val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+    val pat4 = [@{term "Bex (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 (bex_reg_eqv_simproc rel_eqvs))
+    val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))
+    val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))
+    val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
+    (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *)
+    val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs
+  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 ball_all_comm},
+    rtac @{thm bex_ex_comm},
+    resolve_tac eq_eqvs,
+    simp_tac simp_ctxt
+  ])
+  end
+*}
 
 section {* Injections of REP and ABSes *}
 
@@ -741,24 +839,24 @@
 
 *}
 
+(* Doesn't work *)
 ML {*
-fun APPLY_RSP_TAC rty = 
-  CSUBGOAL (fn (concl, i) =>
+fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
   let
     val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
     val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
     val insts = Thm.match (pat, concl)
   in
-    if needs_lift rty (type_of f) 
-    then rtac (Drule.instantiate insts @{thm APPLY_RSP}) i
+    if needs_lift rty (type_of f) then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
     else no_tac
   end
   handle _ => no_tac)
 *}
 
+
+
 ML {*
-val ball_rsp_tac = 
-  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
   let
     val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
                  (Const (@{const_name Ball}, _) $ _)) = term_of concl
@@ -772,8 +870,7 @@
 *}
 
 ML {*
-val bex_rsp_tac = 
-  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
   let
     val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
                  (Const (@{const_name Bex}, _) $ _)) = term_of concl
@@ -787,6 +884,10 @@
 *}
 
 ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
            LAMBDA_RES_TAC,
@@ -796,9 +897,9 @@
            bex_rsp_tac ctxt,
            resolve_tac rsp_thms,
            rtac @{thm refl},
-           (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' 
+           (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
               (RANGE [SOLVES' (quotient_tac quot_thms)])),
-           (APPLY_RSP_TAC rty THEN' 
+           (APPLY_RSP_TAC rty ctxt THEN'
               (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
            Cong_Tac.cong_tac @{thm cong},
            rtac @{thm ext},
@@ -862,11 +963,11 @@
 
     (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
-    DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
+    DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP   provided type of t needs lifting *)
-    DT ctxt "A" ((APPLY_RSP_TAC rty THEN' 
+    DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
@@ -965,26 +1066,6 @@
   THEN' (quotient_tac quot)
 *}
 
-ML {* 
-fun prep_trm thy (x, (T, t)) = 
-  (cterm_of thy (Var (x, T)), cterm_of thy t) 
-
-fun prep_ty thy (x, (S, ty)) = 
-  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) 
-*}
-
-ML {*
-fun matching_prs thy pat trm = 
-let
-  val univ = Unify.matchers thy [(pat, trm)] 
-  val SOME (env, _) = Seq.pull univ
-  val tenv = Vartab.dest (Envir.term_env env)
-  val tyenv = Vartab.dest (Envir.type_env env)
-in
-  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
-end 
-*}
-
 (* Rewrites the term with LAMBDA_PRS thm.
 
 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
@@ -1170,12 +1251,12 @@
       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
       val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
     in
-      EVERY1 
-       [rtac rule, 
+      EVERY1
+       [rtac rule,
         RANGE [rtac rthm',
-               regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *)
+               regularize_tac lthy rel_eqv,
                REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
-               clean_tac lthy quot defs aps]] 
+               clean_tac lthy quot defs aps]]
     end) lthy
 *}
 




