# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264517944 -3600
# Node ID de9e5faf1f03ff12d15ed90c5150df6d3ad490c6
# Parent  6267ad688ea8101abe7f50e078efa09180815b2c
Hom Theorem with exists unique

diff -r 6267ad688ea8 -r de9e5faf1f03 Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 14:48:25 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 15:59:04 2010 +0100
@@ -85,17 +85,17 @@
  \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
  \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
 
- \<exists> (hom_o\<Colon>robj \<Rightarrow> 'a, hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b, hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c, hom_m\<Colon>rmethod \<Rightarrow> 'd)
- \<in> Respects
+ Bexeq
    (prod_rel (alpha_obj ===> op =)
      (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =)
        (prod_rel ((prod_rel (op =) alpha_method) ===> op =)
          (alpha_method ===> op =)
        )
      )
-   ).
+   )
+(\<lambda> (hom_o\<Colon>robj \<Rightarrow> 'a, hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b, hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c, hom_m\<Colon>rmethod \<Rightarrow> 'd).
 
-(
+
  (\<forall>x. hom_o (rVar x) = fvar x) \<and>
  (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and>
  (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and>
@@ -130,8 +130,8 @@
   
 
 lemma liftd: "
-\<exists>\<exists>(hom_o, hom_d, hom_e, hom_m).
-(
+Ex1 (\<lambda>(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>
  (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and>
@@ -144,6 +144,8 @@
 apply (lifting tolift)
 done
 
+done
+
 lemma tolift':
 "\<forall> fvar.
  \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).