# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260268084 -3600
# Node ID faab2540f13e4b8fbfd7e13f3ed6fc9db1bbc05a
# Parent  8dfae5d97387e035e0524663afdd962c39eff52d
inj_repabs also works.

diff -r 8dfae5d97387 -r faab2540f13e Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 11:20:01 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 11:28:04 2009 +0100
@@ -305,14 +305,25 @@
      ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) (
        ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y))))))))
       = ((\<lambda>(y::my_int). y) = (\<lambda>x. x))"
-apply(subst babs_prs[OF Quotient_my_int Quotient_my_int])
-apply(subst babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int])
 apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int])
 apply(subst Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
+apply(subst babs_prs[OF Quotient_my_int Quotient_my_int])
+apply(subst babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(rule refl)
 done
 
+lemma lam_tst3a_inj: "QUOT_TRUE ((\<lambda>(y::my_int). y) = (\<lambda>x. x)) \<Longrightarrow>
+    (op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x)) =
+(op \<approx> ===> op \<approx>)
+     ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) (
+       ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y))))))))
+     ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) (
+       ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y))))))))"
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
+done
+
+
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
 defer