# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260141216 -3600
# Node ID 5c1e6b896ff0f979ee9a8b24d2f48ba253764d4c
# Parent  cdc6ae1a4ed2a098ff6921e1aab654743139caa1# Parent  b16cac0b7c884a6b68bc2f52e8b9569dc129f5cd
merged

diff -r b16cac0b7c88 -r 5c1e6b896ff0 IntEx.thy
--- a/IntEx.thy	Mon Dec 07 00:03:12 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 00:13:36 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 *})
diff -r b16cac0b7c88 -r 5c1e6b896ff0 LFex.thy
--- a/LFex.thy	Mon Dec 07 00:03:12 2009 +0100
+++ b/LFex.thy	Mon Dec 07 00:13:36 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 b16cac0b7c88 -r 5c1e6b896ff0 QuotMain.thy
--- a/QuotMain.thy	Mon Dec 07 00:03:12 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 00:13:36 2009 +0100
@@ -1083,7 +1083,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 +1096,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