
diff -r 01a0da807f50 -r 66f39908df95 QuotMain.thy
--- a/QuotMain.thy	Mon Dec 07 04:39:42 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 04:41:42 2009 +0100
@@ -170,11 +170,24 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
+section {* Bounded abstraction *}
+
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
+section {* Simset setup *}
+
+(* since HOL_basic_ss is too "big", we need to set up *)
+(* our own minimal simpset                            *)
+ML {*
+fun  mk_minimal_ss ctxt =
+  Simplifier.context ctxt empty_ss
+    setsubgoaler asm_simp_tac
+    setmksimps (mksimps [])
+*}
+
 section {* atomize *}
 
 lemma atomize_eqv[atomize]:
@@ -481,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' 
@@ -508,54 +506,6 @@
 *}
 
 ML {*
-fun ball_reg_eqv_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"}, _)) $ R) $ P1)) =>
-      (let
-        val gl = Const (@{const_name "equivp"}, dummyT) $ R;
-        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
-        val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 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 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 "equivp"}, dummyT) $ R;
-        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
-        val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 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)
 
@@ -576,96 +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)
 
-(* does not work yet
+(* 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 simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
-    val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
-    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 = HOL_basic_ss 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
+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 [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},
@@ -673,37 +601,7 @@
     rtac @{thm ball_all_comm},
     rtac @{thm bex_ex_comm},
     resolve_tac eq_eqvs,
-    simp_tac simp_set
-  ])
-  end
-*}*)
-
-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 simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
-  val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
-  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_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]) (equiv_rules_get ctxt)
-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])
+    simp_tac simpset])
 end
 *}
 
@@ -1083,7 +981,7 @@
 ML {*
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
-   ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+   ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>
      let
        val thy = ProofContext.theory_of ctxt
        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
@@ -1096,9 +994,14 @@
        val tl = Thm.lhs_of ts
        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 _ = tracing "lambda_prs"
-          val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
-          val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
+       val _ = if not (s = @{const_name "id"}) then
+                  (tracing "lambda_prs";
+                   tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+                   tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
+                   tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
+                   tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+                   tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
+               else ()
      in
        Conv.rewr_conv ti ctrm
      end
@@ -1145,8 +1048,7 @@
     val thms1 = @{thms all_prs ex_prs} @ defs
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
-    fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
-      (* FIXME: use of someting smaller than HOL_basic_ss *)
+    fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [lambda_prs_tac lthy,
             simp_tac (simps thms1),




