83 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
83 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
84 \<forall> fnil. |
84 \<forall> fnil. |
85 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
85 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
86 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
86 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
87 |
87 |
88 \<exists> (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) |
88 Bexeq |
89 \<in> Respects |
|
90 (prod_rel (alpha_obj ===> op =) |
89 (prod_rel (alpha_obj ===> op =) |
91 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) |
90 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) |
92 (prod_rel ((prod_rel (op =) alpha_method) ===> op =) |
91 (prod_rel ((prod_rel (op =) alpha_method) ===> op =) |
93 (alpha_method ===> op =) |
92 (alpha_method ===> op =) |
94 ) |
93 ) |
95 ) |
94 ) |
96 ). |
95 ) |
97 |
96 (\<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). |
98 ( |
97 |
|
98 |
99 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
99 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
100 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
100 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
101 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
101 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
102 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
102 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
103 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
103 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
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 Ex1 (\<lambda>(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> |
139 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
139 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<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 done |
|
146 |
145 done |
147 done |
146 |
148 |
147 lemma tolift': |
149 lemma tolift': |
148 "\<forall> fvar. |
150 "\<forall> fvar. |
149 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
151 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |