121 done |
121 done |
122 |
122 |
123 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})]))) *} |
123 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})]))) *} |
124 print_theorems |
124 print_theorems |
125 |
125 |
126 lemma alpha_rbv_rsp_pre: |
126 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)) *} |
127 "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z" |
127 thm alpha_bn_rsp |
128 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
128 |
129 apply (simp_all add: alpha_dis alpha5_inj) |
|
130 apply clarify |
|
131 apply (case_tac [!] z) |
|
132 apply (simp_all add: alpha_dis alpha5_inj) |
|
133 apply clarify |
|
134 apply auto |
|
135 apply (meson alpha5_symp alpha5_transp) |
|
136 apply (meson alpha5_symp alpha5_transp) |
|
137 done |
|
138 |
|
139 lemma alpha_rbv_rsp_pre2: |
|
140 "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y" |
|
141 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
|
142 apply (simp_all add: alpha_dis alpha5_inj) |
|
143 apply clarify |
|
144 apply (case_tac [!] z) |
|
145 apply (simp_all add: alpha_dis alpha5_inj) |
|
146 apply clarify |
|
147 apply auto |
|
148 apply (meson alpha5_symp alpha5_transp) |
|
149 apply (meson alpha5_symp alpha5_transp) |
|
150 done |
|
151 |
129 |
152 lemma [quot_respect]: |
130 lemma [quot_respect]: |
153 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
131 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
154 "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5" |
132 "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5" |
155 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
133 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
159 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
137 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
160 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
138 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
161 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
139 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
162 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
140 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
163 "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
141 "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
164 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv_rsp_pre alpha_rbv_rsp_pre2 alpha5_reflp) |
142 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha5_reflp alpha_bn_rsp) |
165 apply (clarify) |
143 apply (clarify) |
166 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
144 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
167 done |
145 done |
168 |
146 |
169 lemma |
147 lemma |