# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260208154 -3600
# Node ID 38aa6b67a80b66942d461d396e2a10bd92fea91f
# Parent  120e479ed3670001e3e9fd86eeecb7ba71ad5ebf
clarified the function examples

diff -r 120e479ed367 -r 38aa6b67a80b Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Dec 07 17:57:33 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 18:49:14 2009 +0100
@@ -164,6 +164,7 @@
 
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
+apply(rule impI)
 apply(rule ballI)
 apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
 apply(simp only: in_respects)
@@ -177,6 +178,7 @@
 
 lemma "PLUS = PLUS"
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
+apply(rule impI)
 apply(rule plus_rsp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
@@ -271,7 +273,7 @@
 (*========================*)
 
 (* 0. preliminary simplification step *)
-thm ball_reg_eqv bex_reg_eqv babs_reg_eqv
+thm ball_reg_eqv bex_reg_eqv (* of no use: babs_reg_eqv *)
     ball_reg_eqv_range bex_reg_eqv_range
 (* 1. first two rtacs *)
 thm ball_reg_right bex_reg_left
@@ -303,22 +305,36 @@
 apply(tactic {* equiv_tac @{context} 1 *})?
 oops
 
-
-lemma
-  "(\<lambda>y. y) = (\<lambda>x. x) \<longrightarrow>
-    (op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))"
-apply(tactic {* simp_tac simpset  1 *})
-sorry
-
-lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
+lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
 by auto
 
-lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *})
-apply(tactic {* regularize_tac @{context} 1*})?
+lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
+apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
 defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
+apply(subst babs_rsp)
+apply(tactic {* clean_tac  @{context} 1 *})
+apply(simp)
+apply(tactic {* regularize_tac @{context} 1*})?
+apply(subst babs_reg_eqv)
+apply(tactic {* equiv_tac @{context} 1*})
+apply(subst babs_reg_eqv)
+apply(tactic {* equiv_tac @{context} 1*})
+sorry
+
+lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
+by auto
+
+lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
+apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})
+defer
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* clean_tac  @{context} 1 *})
+apply(subst babs_rsp)
+apply(tactic {* clean_tac  @{context} 1 *})
+apply(simp)
+apply(tactic {* regularize_tac @{context} 1*})?
 sorry
 
 end
\ No newline at end of file
diff -r 120e479ed367 -r 38aa6b67a80b Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 17:57:33 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 18:49:14 2009 +0100
@@ -588,7 +588,6 @@
   (* can this cause loops in equiv_tac ? *)
   val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 in
-  ObjectLogic.full_atomize_tac THEN'
   simp_tac simpset THEN'
   REPEAT_ALL_NEW (CHANGED o FIRST' [
     rtac @{thm ball_reg_right},
@@ -597,8 +596,9 @@
     rtac @{thm ball_all_comm},
     rtac @{thm bex_ex_comm},
     resolve_tac eq_eqvs,  
-    (* should be equivalent to the above, but causes loops: *) 
+    (* should be equivalent to the above, but causes loops:   *) 
     (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *)
+    (* the culprit is aslread rtac @{thm eq_imp_rel}          *)
     simp_tac simpset])
 end
 *}
@@ -1133,7 +1133,7 @@
 
 lemma lifting_procedure:
   assumes a: "A"
-  and     b: "A \<Longrightarrow> B"
+  and     b: "A \<longrightarrow> B"
   and     c: "B = C"
   and     d: "C = D"
   shows   "D"