# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264074643 -3600
# Node ID aa960d16570fa6f01c3d4199cd1f2f62480aaee4
# Parent  95ee248b3832ce3ae09efd6ffc45c6b4cbaf836a
Lifted Peter's Sigma lemma with Ex1.

diff -r 95ee248b3832 -r aa960d16570f FIXME-TODO
--- a/FIXME-TODO	Thu Jan 21 12:03:47 2010 +0100
+++ b/FIXME-TODO	Thu Jan 21 12:50:43 2010 +0100
@@ -64,4 +64,6 @@
       as "rconst"
 
   That means "qconst :: qty" is not read as a term, but
-  as two entities.
\ No newline at end of file
+  as two entities.
+
+- Add syntax for Bexeq, for example "\<exists>!!"
diff -r 95ee248b3832 -r aa960d16570f Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Thu Jan 21 12:03:47 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Thu Jan 21 12:50:43 2010 +0100
@@ -188,5 +188,48 @@
 apply (lifting tolift')
 done
 
+lemma tolift'':
+"\<forall> fvar.
+ \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
+ \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =).
+ \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =).
+ \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
+ \<forall> fnil.
+ \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
+ \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
+
+ Bexeq (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a .
+ Bexeq (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b.
+ Bexeq ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c.
+ Bexeq (alpha_method ===> op =) (\<lambda>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>
+ (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
+ (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
+ (hom_d [] = fnil) \<and>
+ (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
+ (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
+)
+))))"
+sorry
+
+lemma liftd'': "
+\<exists>!hom_o. \<exists>!hom_d. \<exists>!hom_e. \<exists>!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>
+ (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
+ (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
+ (hom_d [] = fnil) \<and>
+ (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
+ (\<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'')
+done
+
+
 end
 
diff -r 95ee248b3832 -r aa960d16570f Unused.thy
--- a/Unused.thy	Thu Jan 21 12:03:47 2010 +0100
+++ b/Unused.thy	Thu Jan 21 12:50:43 2010 +0100
@@ -5,6 +5,10 @@
   shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
   by(auto simp add: QUOT_TRUE_def)
 
+syntax
+  "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
+translations
+  "\<exists>!!x\<in>A. P"  == "Bexeq A (%x. P)"
 
 
 (* Atomize infrastructure *)