equal
deleted
inserted
replaced
126 sorry |
126 sorry |
127 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>" |
127 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>" |
128 sorry |
128 sorry |
129 |
129 |
130 |
130 |
131 lemma bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bexeq R (\<lambda>x. P x))" |
131 lemma bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))" |
132 apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects) |
132 apply (simp add: Bex1_def Ex1_def Bex1_rel_def in_respects) |
133 apply clarify |
133 apply clarify |
134 apply auto |
134 apply auto |
135 apply (rule bexI) |
135 apply (rule bexI) |
136 apply assumption |
136 apply assumption |
137 apply (simp add: in_respects) |
137 apply (simp add: in_respects) |
205 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
205 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
206 \<forall> fnil. |
206 \<forall> fnil. |
207 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
207 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
208 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
208 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
209 |
209 |
210 Bexeq (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a . |
210 Bex1_rel (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a . |
211 Bexeq (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b. |
211 Bex1_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b. |
212 Bexeq ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c. |
212 Bex1_rel ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c. |
213 Bexeq (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd. |
213 Bex1_rel (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd. |
214 ( |
214 ( |
215 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
215 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
216 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
216 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
217 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
217 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
218 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
218 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |