diff -r de9e5faf1f03 -r 46cc6708c3b3 Quot/Examples/SigmaEx.thy --- a/Quot/Examples/SigmaEx.thy Tue Jan 26 15:59:04 2010 +0100 +++ b/Quot/Examples/SigmaEx.thy Tue Jan 26 16:30:51 2010 +0100 @@ -85,14 +85,14 @@ \ fpar\Respects (op = ===> op = ===> alpha_method ===> op =). \ fsgm\Respects (op = ===> (op = ===> alpha_obj) ===> op =). - Bexeq - (prod_rel (alpha_obj ===> op =) + Bex1 + (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 =) ) ) - ) + )) (\ (hom_o\robj \ 'a, hom_d\(char list \ rmethod) list \ 'b, hom_e\char list \ rmethod \ 'c, hom_m\rmethod \ 'd). @@ -128,6 +128,16 @@ sorry +lemma bex1_bex1reg: "(\!x\Respects R. P x) \ (Bexeq R (\x. P x))" +apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects) +apply clarify +apply auto +apply (rule bexI) +apply assumption +apply (simp add: in_respects) +apply (simp add: in_respects) +apply auto +done lemma liftd: " Ex1 (\(hom_o, hom_d, hom_e, hom_m).