diff -r 3664eafcad09 -r 7a42cc191111 Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Thu Feb 04 18:09:20 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Fri Feb 05 10:32:21 2010 +0100
@@ -75,6 +75,8 @@
 
 end
 
+
+
 lemma tolift:
 "\<forall> fvar.
  \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
@@ -85,18 +87,16 @@
  \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
  \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
 
- Bex1
-   (Respects (prod_rel (alpha_obj ===> op =)
+ Ex1 (\<lambda>x.
+(x \<in> (Respects (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 =)
        )
-     )
-   ))
+     )))) \<and>
 (\<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>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>
@@ -104,14 +104,25 @@
  (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))
-)"
+)) x) "
 sorry
 
-syntax
+lemma test_to: "Ex1 (\<lambda>x. (x \<in> (Respects alpha_obj)) \<and> P x)"
+ML_prf {* prop_of (#goal (Isar.goal ())) *}
+sorry
+lemma test_tod: "Ex1 (P :: obj \<Rightarrow> bool)"
+apply (lifting test_to)
+done
+
+
+
+
+(*syntax
   "_expttrn"        :: "pttrn => bool => bool"      ("(3\<exists>\<exists> _./ _)" [0, 10] 10)
 
 translations
   "\<exists>\<exists> x. P"   == "Ex (%x. P)"
+*)
 
 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar"
   by (simp add: a1)
@@ -129,7 +140,7 @@
 
   
 lemma bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
-apply (simp add: Bex1_def Ex1_def Bex1_rel_def in_respects)
+apply (simp add: Ex1_def Bex1_rel_def in_respects)
 apply clarify
 apply auto
 apply (rule bexI)
@@ -154,8 +165,6 @@
 apply (lifting tolift)
 done
 
-done
-
 lemma tolift':
 "\<forall> fvar.
  \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).