# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260149664 -3600
# Node ID 951681538e3f37644cfef9155beaefabfd432dfd
# Parent  4e66a18f263bb41f2a1a3122d9f8feecd8c316fa
simplified the regularize simproc

diff -r 4e66a18f263b -r 951681538e3f QuotMain.thy
--- a/QuotMain.thy	Mon Dec 07 01:28:10 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 02:34:24 2009 +0100
@@ -494,21 +494,6 @@
        raise (LIFT_MATCH "regularize (default)")
 *}
 
-(*
-FIXME / TODO: needs to be adapted
-
-To prove that the raw theorem implies the regularised one, 
-we try in order:
-
- - Reflexivity of the relation
- - Assumption
- - Elimnating quantifiers on both sides of toplevel implication
- - Simplifying implications on both sides of toplevel implication
- - Ball (Respects ?E) ?P = All ?P
- - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
-
-*)
-
 ML {*
 fun equiv_tac ctxt =
   REPEAT_ALL_NEW (FIRST' 
@@ -541,94 +526,74 @@
 *}
 
 ML {*
-fun ball_reg_eqv_range_simproc 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 "equivp"}, 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 {context,...} => equiv_tac context 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 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
+fun calculate_instance ctxt thm redex R1 R2 =
+let
+  val thy = ProofContext.theory_of ctxt
+  val goal = Const (@{const_name "equivp"}, dummyT) $ R2  
+             |> Syntax.check_term ctxt
+             |> HOLogic.mk_Trueprop 
+  val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1)
+  val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
+  val R1c = cterm_of thy R1
+  val thmi = Drule.instantiate' [] [SOME R1c] thm
+  val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
+  val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)
+in
+  SOME thm2
+end
+handle _ => NONE
+(* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *)
 *}
 
-
-thm bex_reg_eqv_range
-thm ball_reg_eqv
-thm bex_reg_eqv
-
 ML {*
-fun bex_reg_eqv_range_simproc 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 "equivp"}, 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 {context,...} => equiv_tac context 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 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
-
-      )
+fun ball_bex_range_simproc ss redex =
+let
+  val ctxt = Simplifier.the_context ss
+in 
+ case redex of
+    (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ 
+      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+        calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
+  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ 
+      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>  
+        calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
   | _ => NONE
-  end
+end
 *}
 
-lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+lemma eq_imp_rel: 
+  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 by (simp add: equivp_reflp)
 
+(* FIXME/TODO: How does regularizing work? *)
+(* FIXME/TODO: needs to be adapted
+
+To prove that the raw theorem implies the regularised one, 
+we try in order:
+
+ - Reflexivity of the relation
+ - Assumption
+ - Elimnating quantifiers on both sides of toplevel implication
+ - Simplifying implications on both sides of toplevel implication
+ - Ball (Respects ?E) ?P = All ?P
+ - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+
+*)
 ML {*
 fun regularize_tac ctxt =
-  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 simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
-    val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
-    val simp_set = (mk_minimal_ss ctxt) 
+let
+  val thy = ProofContext.theory_of ctxt
+  val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
+  val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
+  val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
+  val simpset = (mk_minimal_ss ctxt) 
                        addsimps @{thms ball_reg_eqv bex_reg_eqv}
-                       addsimprocs [simproc3, simproc4]
-                       addSolver equiv_solver
-    (* 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]) (equiv_rules_get ctxt)
-  in
+                       addsimprocs [simproc] addSolver equiv_solver
+  (* 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]) (equiv_rules_get ctxt)
+in
   ObjectLogic.full_atomize_tac THEN'
-  simp_tac simp_set THEN'
+  simp_tac simpset THEN'
   REPEAT_ALL_NEW (FIRST' [
     rtac @{thm ball_reg_right},
     rtac @{thm bex_reg_left},
@@ -636,9 +601,8 @@
     rtac @{thm ball_all_comm},
     rtac @{thm bex_ex_comm},
     resolve_tac eq_eqvs,
-    simp_tac simp_set
-  ])
-  end
+    simp_tac simpset])
+end
 *}
 
 section {* Injections of rep and abses *}