# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260269956 -3600
# Node ID c10a46fa0de96ecc246dbc130fddf77f564bbebc
# Parent  a98b136fc88aacc38bd455b920b3dbfd508e939b
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.

diff -r a98b136fc88a -r c10a46fa0de9 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 11:38:58 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 11:59:16 2009 +0100
@@ -299,30 +299,6 @@
 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
 by auto
 
-lemma lam_tst3a_clean: "(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))))))))
-      = ((\<lambda>(y::my_int). y) = (\<lambda>x. x))"
-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 id_rsp:
   shows "(R ===> R) id id"
 by simp
@@ -332,34 +308,32 @@
 apply (simp add: id_rsp)
 done
 
-
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
-defer
+apply(rule impI)
+apply(rule lam_tst3a_reg)
 apply(tactic {* all_inj_repabs_tac @{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
+apply(simp add: babs_prs[OF Quotient_my_int Quotient_my_int])
+done
 
 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(rule impI)
+apply (rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
+apply (simp add: id_rsp)
 apply(tactic {* all_inj_repabs_tac @{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
+apply(subst babs_prs)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(subst babs_prs)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(rule refl)
+done
 
 end
diff -r a98b136fc88a -r c10a46fa0de9 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 11:38:58 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 11:59:16 2009 +0100
@@ -602,7 +602,12 @@
        Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
 
   | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
-       Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+      let
+        val rty = fastype_of rtrm
+        val qty = fastype_of qtrm
+      in
+        mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
+      end
 
   | (Abs (x, T, t), Abs (x', T', t')) =>
       let