# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264513705 -3600
# Node ID 6267ad688ea8101abe7f50e078efa09180815b2c
# Parent  0aaeea9255f34eea518bf3812dd835701cb4b32a
2 cases for regularize with split, lemmas with split now lift.

diff -r 0aaeea9255f3 -r 6267ad688ea8 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 14:08:47 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 14:48:25 2010 +0100
@@ -409,12 +409,20 @@
 
 lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y) \<in> Respects(
   prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>)
-). x = y"
+). (op \<approx> ===> op \<approx>) x y"
 sorry
 
 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y). x = y)"
 apply (lifting test5)
+done
+
+lemma test6: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects(
+  prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>))
+). (op \<approx> ===> op \<approx>) x y \<and> (op \<approx> ===> op \<approx>) y z"
 sorry
 
+lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)"
+apply (lifting test6)
+done
 
 end
diff -r 0aaeea9255f3 -r 6267ad688ea8 Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 14:08:47 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 14:48:25 2010 +0100
@@ -130,7 +130,7 @@
   
 
 lemma liftd: "
-\<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))).
+\<exists>\<exists>(hom_o, hom_d, hom_e, hom_m).
 (
  (\<forall>x. hom_o (Var x) = fvar x) \<and>
  (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and>
@@ -142,9 +142,7 @@
  (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
 )"
 apply (lifting tolift)
-apply (regularize)
-apply (simp)
-sorry
+done
 
 lemma tolift':
 "\<forall> fvar.
diff -r 0aaeea9255f3 -r 6267ad688ea8 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Tue Jan 26 14:08:47 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Jan 26 14:48:25 2010 +0100
@@ -511,6 +511,14 @@
            end
        end 
 
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, Abs(v1', ty', s1))),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , Abs(v2', _  , s2)))) =>
+       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, Abs(v1', ty', regularize_trm ctxt (s1, s2)))
+
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, s1)),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , s2))) =>
+       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, regularize_trm ctxt (s1, s2))
+
   | (t1 $ t2, t1' $ t2') =>
        (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2'))