# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260190836 -3600
# Node ID 6088fea1c8b1e6aa87d85ae23e4d2694522fc093
# Parent  a2f2214dc88120775c88f5a1ad99f456da5020eb
inj_repabs_tac handles Babs now.

diff -r a2f2214dc881 -r 6088fea1c8b1 IntEx.thy
--- a/IntEx.thy	Mon Dec 07 12:14:25 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 14:00:36 2009 +0100
@@ -246,27 +246,31 @@
 
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
-(*apply(tactic {* regularize_tac @{context} 1 *}) *)
-defer
+apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp add: pair_prs)
-sorry
+done
 
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
 by simp
 
+
+
+
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
-apply(tactic {* gen_frees_tac @{context} 1 *})
-ML_prf {* regularize_trm @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *}
-ML_prf {* print_depth 50 *}
-ML_prf {* Syntax.check_term @{context} it *}
-ML_prf {* procedure_inst @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *}
+apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
+defer
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+(*apply(tactic {* lambda_prs_tac  @{context} 1 *})*)
+sorry
 
-apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
+lemma lam_tst3: "(\<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 \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)"
+apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *})
+defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
-done
-
+apply(tactic {* lambda_prs_tac  @{context} 1 *})
+sorry
diff -r a2f2214dc881 -r 6088fea1c8b1 QuotMain.thy
--- a/QuotMain.thy	Mon Dec 07 12:14:25 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 14:00:36 2009 +0100
@@ -907,6 +907,11 @@
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
+| (_ $
+    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+      => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+
     (* reflexivity of operators arising from Cong_tac *)
 | Const (@{const_name "op ="},_) $ _ $ _ 
       => rtac @{thm refl} ORELSE'
@@ -993,6 +998,7 @@
        val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
        val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
        val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+       val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
        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