186 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
186 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
187 )" |
187 )" |
188 apply (lifting tolift') |
188 apply (lifting tolift') |
189 done |
189 done |
190 |
190 |
|
191 lemma tolift'': |
|
192 "\<forall> fvar. |
|
193 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
194 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
|
195 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =). |
|
196 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
197 \<forall> fnil. |
|
198 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
|
199 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
|
200 |
|
201 Bexeq (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a . |
|
202 Bexeq (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b. |
|
203 Bexeq ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c. |
|
204 Bexeq (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd. |
|
205 ( |
|
206 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
|
207 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
|
208 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
|
209 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
210 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
211 (hom_d [] = fnil) \<and> |
|
212 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
213 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
214 ) |
|
215 ))))" |
|
216 sorry |
|
217 |
|
218 lemma liftd'': " |
|
219 \<exists>!hom_o. \<exists>!hom_d. \<exists>!hom_e. \<exists>!hom_m. |
|
220 ( |
|
221 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
|
222 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and> |
|
223 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and> |
|
224 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
225 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
226 (hom_d [] = fnil) \<and> |
|
227 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
228 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
229 )" |
|
230 apply (lifting tolift'') |
|
231 done |
|
232 |
|
233 |
191 end |
234 end |
192 |
235 |