
diff -r 3359033eff79 -r d1aa26ecfecd QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 05:47:13 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 05:49:16 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 *}
 
@@ -773,6 +871,62 @@
 *}
 
 ML {*
+<<<<<<< variant A
+>>>>>>> variant B
+val ball_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) =>
+            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+            THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+      |_ => no_tac)
+*}
+
+ML {*
+val bex_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) =>
+            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+            THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+      | _ => no_tac)
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
+####### Ancestor
+val ball_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) =>
+            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+            THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+      |_ => no_tac)
+*}
+
+ML {*
+val bex_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) =>
+            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+            THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+      | _ => no_tac)
+*}
+
+ML {*
+======= end
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
            LAMBDA_RES_TAC ctxt,
@@ -880,6 +1034,31 @@
   REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
+ML {*
+fun get_inj_repabs_tac ctxt rel lhs rhs =
+let
+  val _ = tracing "input"
+  val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel)
+  val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs)
+  val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs)
+in  
+  case (rel, lhs, rhs) of
+    (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *)
+      => rtac @{thm REP_ABS_RSP(1)}
+  | (_, Const (@{const_name "Ball"}, _) $ _, 
+        Const (@{const_name "Ball"}, _) $ _)
+      => rtac @{thm RES_FORALL_RSP}
+  | _ => K no_tac
+end
+*}
+
+ML {* 
+fun inj_repabs_tac ctxt =
+  SUBGOAL (fn (goal, i) =>
+     (case (HOLogic.dest_Trueprop goal) of
+        (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs
+      | _ => K no_tac) i)
+*}
 
 section {* Cleaning of the theorem *}
 
@@ -931,26 +1110,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)))
@@ -1136,12 +1295,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
 *}
 




