equal
deleted
inserted
replaced
128 sorry |
128 sorry |
129 |
129 |
130 |
130 |
131 |
131 |
132 lemma liftd: " |
132 lemma liftd: " |
133 \<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))). |
133 \<exists>\<exists>(hom_o, hom_d, hom_e, hom_m). |
134 ( |
134 ( |
135 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
135 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
136 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and> |
136 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and> |
137 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and> |
137 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and> |
138 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
138 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
140 (hom_d [] = fnil) \<and> |
140 (hom_d [] = fnil) \<and> |
141 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
141 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
142 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
142 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
143 )" |
143 )" |
144 apply (lifting tolift) |
144 apply (lifting tolift) |
145 apply (regularize) |
145 done |
146 apply (simp) |
|
147 sorry |
|
148 |
146 |
149 lemma tolift': |
147 lemma tolift': |
150 "\<forall> fvar. |
148 "\<forall> fvar. |
151 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
149 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
152 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
150 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |