# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260157302 -3600
# Node ID 66f39908df953ba55e7c556b0c33a1841218b924
# Parent  01a0da807f50b505957d110f0599a860d0663c8f# Parent  951681538e3f37644cfef9155beaefabfd432dfd
merge

diff -r 01a0da807f50 -r 66f39908df95 IntEx.thy
--- a/IntEx.thy	Mon Dec 07 04:39:42 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 04:41:42 2009 +0100
@@ -149,37 +149,6 @@
 apply(rule refl)
 done
 
-
-(*
-lemma yy:
-  "(REP_my_int ---> id)
- (\<lambda>x. Ball (Respects op \<approx>)
-       ((ABS_my_int ---> id)
-         ((REP_my_int ---> id)
-           (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
-                 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
-                 (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)) \<approx>
-                (ABS_my_int ---> ABS_my_int ---> REP_my_int)
-                 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
-                 (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)))))) =
-(\<lambda>x. Ball (Respects op \<approx>)
-     ((ABS_my_int ---> id)
-       ((REP_my_int ---> id)
-         (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
-               ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
-               (REP_my_int (ABS_my_int b)) \<approx>
-              (ABS_my_int ---> ABS_my_int ---> REP_my_int)
-               ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
-               (REP_my_int (ABS_my_int b))))))"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [lambda_prs2 @{theory}]) 1*})
-
-apply(rule lambda_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(simp add: id_simps)
-apply(tactic {* quotient_tac @{context} 1 *})
-done
-*)
-
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
@@ -187,6 +156,8 @@
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 
+thm lambda_prs
+
 lemma test2: "my_plus a = my_plus a"
 apply(rule refl)
 done
diff -r 01a0da807f50 -r 66f39908df95 IntEx2.thy
--- a/IntEx2.thy	Mon Dec 07 04:39:42 2009 +0100
+++ b/IntEx2.thy	Mon Dec 07 04:41:42 2009 +0100
@@ -389,6 +389,7 @@
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
 use "~~/src/HOL/Tools/numeral_syntax.ML"
+(*
 setup NumeralSyntax.setup
 
 abbreviation
@@ -432,3 +433,4 @@
 
 lemmas normalize_bin_simps =
   Bit0_Pls Bit1_Min
+*)
\ No newline at end of file
diff -r 01a0da807f50 -r 66f39908df95 LFex.thy
--- a/LFex.thy	Mon Dec 07 04:39:42 2009 +0100
+++ b/LFex.thy	Mon Dec 07 04:41:42 2009 +0100
@@ -296,7 +296,7 @@
   \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"
-apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *})
+apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 done
 
 print_quotients
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),