183 and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A" |
183 and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A" |
184 and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M" |
184 and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M" |
185 apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts) |
185 apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts) |
186 apply(simp_all add: akind_aty_atrm.intros) |
186 apply(simp_all add: akind_aty_atrm.intros) |
187 apply (simp_all add: akind_aty_atrm_inj) |
187 apply (simp_all add: akind_aty_atrm_inj) |
188 apply(rule alpha_gen_atom_sym) |
188 apply(erule alpha_gen_compose_sym) |
189 apply(rule alpha_eqvt) |
189 apply(erule alpha_eqvt) |
190 apply(assumption)+ |
190 apply(erule alpha_gen_compose_sym) |
191 apply(rule alpha_gen_atom_sym) |
191 apply(erule alpha_eqvt) |
192 apply(rule alpha_eqvt) |
192 apply(erule alpha_gen_compose_sym) |
193 apply(assumption)+ |
193 apply(erule alpha_eqvt) |
194 apply(rule alpha_gen_atom_sym) |
|
195 apply(rule alpha_eqvt) |
|
196 apply(assumption)+ |
|
197 done |
194 done |
198 |
195 |
199 lemma al_trans: |
196 lemma al_trans: |
200 fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm" |
197 fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm" |
201 shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''" |
198 shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''" |
204 apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts) |
201 apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts) |
205 apply(simp_all add: akind_aty_atrm.intros) |
202 apply(simp_all add: akind_aty_atrm.intros) |
206 apply(erule akind.cases) |
203 apply(erule akind.cases) |
207 apply(simp_all add: akind_aty_atrm.intros) |
204 apply(simp_all add: akind_aty_atrm.intros) |
208 apply(simp add: akind_aty_atrm_inj) |
205 apply(simp add: akind_aty_atrm_inj) |
209 apply(rule alpha_gen_atom_trans) |
206 apply(erule alpha_gen_compose_trans) |
210 apply(rule alpha_eqvt) |
207 apply(assumption) |
211 apply(assumption)+ |
208 apply(erule alpha_eqvt) |
212 apply(rotate_tac 4) |
209 apply(rotate_tac 4) |
213 apply(erule aty.cases) |
210 apply(erule aty.cases) |
214 apply(simp_all add: akind_aty_atrm.intros) |
211 apply(simp_all add: akind_aty_atrm.intros) |
215 apply(rotate_tac 3) |
212 apply(rotate_tac 3) |
216 apply(erule aty.cases) |
213 apply(erule aty.cases) |
217 apply(simp_all add: akind_aty_atrm.intros) |
214 apply(simp_all add: akind_aty_atrm.intros) |
218 apply(simp add: akind_aty_atrm_inj) |
215 apply(simp add: akind_aty_atrm_inj) |
219 apply(rule alpha_gen_atom_trans) |
216 apply(erule alpha_gen_compose_trans) |
220 apply(rule alpha_eqvt) |
217 apply(assumption) |
221 apply(assumption)+ |
218 apply(erule alpha_eqvt) |
222 apply(rotate_tac 4) |
219 apply(rotate_tac 4) |
223 apply(erule atrm.cases) |
220 apply(erule atrm.cases) |
224 apply(simp_all add: akind_aty_atrm.intros) |
221 apply(simp_all add: akind_aty_atrm.intros) |
225 apply(rotate_tac 3) |
222 apply(rotate_tac 3) |
226 apply(erule atrm.cases) |
223 apply(erule atrm.cases) |
227 apply(simp_all add: akind_aty_atrm.intros) |
224 apply(simp_all add: akind_aty_atrm.intros) |
228 apply(simp add: akind_aty_atrm_inj) |
225 apply(simp add: akind_aty_atrm_inj) |
229 apply(rule alpha_gen_atom_trans) |
226 apply(erule alpha_gen_compose_trans) |
230 apply(rule alpha_eqvt) |
227 apply(assumption) |
231 apply(assumption)+ |
228 apply(erule alpha_eqvt) |
232 done |
229 done |
233 |
230 |
234 lemma alpha_equivps: |
231 lemma alpha_equivps: |
235 shows "equivp akind" |
232 shows "equivp akind" |
236 and "equivp aty" |
233 and "equivp aty" |