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