equal
deleted
inserted
replaced
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 Bexeq |
88 Bex1 |
89 (prod_rel (alpha_obj ===> op =) |
89 (Respects (prod_rel (alpha_obj ===> op =) |
90 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) |
90 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) |
91 (prod_rel ((prod_rel (op =) alpha_method) ===> op =) |
91 (prod_rel ((prod_rel (op =) alpha_method) ===> op =) |
92 (alpha_method ===> op =) |
92 (alpha_method ===> op =) |
93 ) |
93 ) |
94 ) |
94 ) |
95 ) |
95 )) |
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). |
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). |
97 |
97 |
98 |
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> |
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))" |
|
132 apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects) |
|
133 apply clarify |
|
134 apply auto |
|
135 apply (rule bexI) |
|
136 apply assumption |
|
137 apply (simp add: in_respects) |
|
138 apply (simp add: in_respects) |
|
139 apply auto |
|
140 done |
131 |
141 |
132 lemma liftd: " |
142 lemma liftd: " |
133 Ex1 (\<lambda>(hom_o, hom_d, hom_e, hom_m). |
143 Ex1 (\<lambda>(hom_o, hom_d, hom_e, hom_m). |
134 |
144 |
135 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
145 (\<forall>x. hom_o (Var x) = fvar x) \<and> |