159 apply(rule equ_refl) |
159 apply(rule equ_refl) |
160 done |
160 done |
161 |
161 |
162 end |
162 end |
163 |
163 |
|
164 quotient_definition subst_qlam ("_[_ ::q= _]") |
|
165 where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst |
|
166 |
|
167 lemma |
|
168 "(QVar x)[y ::q= s] = (if x = y then s else (QVar x))" |
|
169 apply(descending) |
|
170 apply(simp) |
|
171 apply(auto intro: equ_refl) |
|
172 done |
|
173 |
|
174 lemma |
|
175 "(QApp t1 t2)[y ::q= s] = QApp (t1[y ::q= s]) (t2[y ::q= s])" |
|
176 apply(descending) |
|
177 apply(simp) |
|
178 apply(rule equ_refl) |
|
179 done |
|
180 |
|
181 lemma |
|
182 "(QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])" |
|
183 apply(descending) |
|
184 apply(subst subst.simps) |
|
185 prefer 3 |
|
186 apply(rule equ_refl) |
|
187 oops |
|
188 |
|
189 |
164 lemma [eqvt]: "(p \<bullet> abs_qlam t) = abs_qlam (p \<bullet> t)" |
190 lemma [eqvt]: "(p \<bullet> abs_qlam t) = abs_qlam (p \<bullet> t)" |
165 apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) |
191 apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) |
166 apply (subst Quotient_rel[OF Quotient_qlam, simplified equivp_reflp[OF qlam_equivp], simplified]) |
192 apply (subst Quotient_rel[OF Quotient_qlam, simplified equivp_reflp[OF qlam_equivp], simplified]) |
167 by (metis Quotient_qlam equ_refl eqvt rep_abs_rsp_left) |
193 by (metis Quotient_qlam equ_refl eqvt rep_abs_rsp_left) |
168 |
194 |
192 defer |
218 defer |
193 apply(rule supports_abs_qlam) |
219 apply(rule supports_abs_qlam) |
194 apply(simp add: QVar_def) |
220 apply(simp add: QVar_def) |
195 done |
221 done |
196 |
222 |
197 lemma supports_qapp: |
|
198 "supp (t, s) supports (QApp t s)" |
|
199 apply(subgoal_tac "supp (t, s) supports (abs_qlam (App (rep_qlam t) (rep_qlam s)))") |
|
200 apply(simp add: QApp_def) |
|
201 apply(subgoal_tac "supp (App (rep_qlam t) (rep_qlam s)) supports (abs_qlam (App (rep_qlam t) (rep_qlam s)))") |
|
202 prefer 2 |
|
203 apply(rule supports_abs_qlam) |
|
204 apply(simp add: lam.supp) |
|
205 oops |
|
206 |
|
207 lemma "(p \<bullet> rep_qlam t) \<approx> rep_qlam (p \<bullet> t)" |
|
208 apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) |
|
209 apply (rule rep_abs_rsp[OF Quotient_qlam]) |
|
210 apply (rule equ_refl) |
|
211 done |
|
212 |
|
213 section {* Supp *} |
223 section {* Supp *} |
214 |
224 |
215 definition |
225 definition |
216 "Supp t = \<Inter>{supp s | s. s \<approx> t}" |
226 "Supp t = \<Inter>{supp s | s. s \<approx> t}" |
217 |
227 |
227 by (metis equivp_def qlam_equivp) |
237 by (metis equivp_def qlam_equivp) |
228 |
238 |
229 quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" |
239 quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" |
230 is "Supp::lam \<Rightarrow> atom set" |
240 is "Supp::lam \<Rightarrow> atom set" |
231 |
241 |
|
242 lemma s: |
|
243 assumes "s \<approx> t" |
|
244 shows "a \<sharp> (abs_qlam s) \<longleftrightarrow> a \<sharp> (abs_qlam t)" |
|
245 using assms |
|
246 by (metis Quotient_qlam Quotient_rel_abs) |
|
247 |
|
248 lemma ss: |
|
249 "Supp t supports (abs_qlam t)" |
|
250 apply(simp only: supports_def) |
|
251 apply(rule allI)+ |
|
252 apply(rule impI) |
|
253 apply(rule swap_fresh_fresh) |
|
254 apply(drule conjunct1) |
|
255 apply(auto)[1] |
|
256 apply(simp add: Supp_def) |
|
257 apply(auto)[1] |
|
258 apply(simp add: s[symmetric]) |
|
259 apply(rule supports_fresh) |
|
260 apply(rule supports_abs_qlam) |
|
261 apply(simp add: finite_supp) |
|
262 apply(simp) |
|
263 apply(drule conjunct2) |
|
264 apply(auto)[1] |
|
265 apply(simp add: Supp_def) |
|
266 apply(auto)[1] |
|
267 apply(simp add: s[symmetric]) |
|
268 apply(rule supports_fresh) |
|
269 apply(rule supports_abs_qlam) |
|
270 apply(simp add: finite_supp) |
|
271 apply(simp) |
|
272 done |
232 |
273 |
233 lemma |
274 lemma |
234 fixes t::"qlam" |
275 fixes t::"qlam" |
235 shows "(supp x) supports (QVar x)" |
276 shows "(supp x) supports (QVar x)" |
236 apply(rule_tac x="QVar x" in Abs_qlam_cases) |
277 apply(rule_tac x="QVar x" in Abs_qlam_cases) |