181 done |
181 done |
182 |
182 |
183 local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} |
183 local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} |
184 print_theorems |
184 print_theorems |
185 |
185 |
186 |
186 local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} |
187 lemma alpha_rbv_rsp_pre: |
187 thm alpha_bn_rsp |
188 "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z" |
|
189 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
|
190 apply (simp_all add: alpha_dis alpha5_inj) |
|
191 apply clarify |
|
192 apply (case_tac [!] z) |
|
193 apply (simp_all add: alpha_dis alpha5_inj) |
|
194 apply clarify |
|
195 apply auto |
|
196 apply (meson alpha5_symp alpha5_transp) |
|
197 apply (meson alpha5_symp alpha5_transp) |
|
198 done |
|
199 |
|
200 lemma alpha_rbv_rsp_pre2: |
|
201 "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y" |
|
202 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
|
203 apply (simp_all add: alpha_dis alpha5_inj) |
|
204 apply clarify |
|
205 apply (case_tac [!] z) |
|
206 apply (simp_all add: alpha_dis alpha5_inj) |
|
207 apply clarify |
|
208 apply auto |
|
209 apply (meson alpha5_symp alpha5_transp) |
|
210 apply (meson alpha5_symp alpha5_transp) |
|
211 done |
|
212 |
188 |
213 lemma [quot_respect]: |
189 lemma [quot_respect]: |
214 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
190 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
215 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
191 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
216 "(alpha_rlts ===> op =) rbv5 rbv5" |
192 "(alpha_rlts ===> op =) rbv5 rbv5" |
219 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
195 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
220 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
196 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
221 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
197 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
222 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
198 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
223 "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
199 "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
224 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
200 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp) |
225 apply (clarify) |
201 apply (clarify) |
226 apply (rule_tac x="0" in exI) |
202 apply (rule_tac x="0" in exI) |
227 apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
203 apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
228 apply clarify |
|
229 apply (simp add: alpha_rbv_rsp_pre2) |
|
230 apply (simp add: alpha_rbv_rsp_pre) |
|
231 done |
204 done |
232 |
205 |
233 lemma |
206 lemma |
234 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
207 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
235 by (simp add: bv_list_rsp) |
208 by (simp add: bv_list_rsp) |