173 apply(auto) |
173 apply(auto) |
174 apply(perm_simp) |
174 apply(perm_simp) |
175 apply(simp add: swap_fresh_fresh) |
175 apply(simp add: swap_fresh_fresh) |
176 done |
176 done |
177 |
177 |
|
178 lemma rep_qlam_inverse: |
|
179 "abs_qlam (rep_qlam t) = t" |
|
180 by (metis Quotient_abs_rep Quotient_qlam) |
|
181 |
|
182 lemma supports_rep_qlam: |
|
183 "supp (rep_qlam t) supports t" |
|
184 apply(subst (2) rep_qlam_inverse[symmetric]) |
|
185 apply(rule supports_abs_qlam) |
|
186 done |
|
187 |
|
188 lemma supports_qvar: |
|
189 "{atom x} supports (QVar x)" |
|
190 apply(subgoal_tac "supp (Var x) supports (abs_qlam (Var x))") |
|
191 apply(simp add: lam.supp supp_at_base) |
|
192 defer |
|
193 apply(rule supports_abs_qlam) |
|
194 apply(simp add: QVar_def) |
|
195 done |
|
196 |
|
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 |
178 lemma "(p \<bullet> rep_qlam t) \<approx> rep_qlam (p \<bullet> t)" |
207 lemma "(p \<bullet> rep_qlam t) \<approx> rep_qlam (p \<bullet> t)" |
179 apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) |
208 apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) |
180 apply (rule rep_abs_rsp[OF Quotient_qlam]) |
209 apply (rule rep_abs_rsp[OF Quotient_qlam]) |
181 apply (rule equ_refl) |
210 apply (rule equ_refl) |
182 done |
211 done |
201 is "Supp::lam \<Rightarrow> atom set" |
230 is "Supp::lam \<Rightarrow> atom set" |
202 |
231 |
203 |
232 |
204 lemma |
233 lemma |
205 fixes t::"qlam" |
234 fixes t::"qlam" |
206 shows "supp t = supp_qlam t" |
235 shows "(supp x) supports (QVar x)" |
|
236 apply(rule_tac x="QVar x" in Abs_qlam_cases) |
|
237 apply(auto) |
|
238 thm QVar_def |
207 apply(descending) |
239 apply(descending) |
208 oops |
240 oops |
209 |
241 |
210 |
242 |
211 |
243 |
|
244 section {* Size *} |
|
245 |
|
246 definition |
|
247 "Size t = Least {size s | s. s \<approx> t}" |
212 |
248 |
213 lemma [quot_respect]: |
249 lemma [quot_respect]: |
214 shows "(equ ===> op=) Size Size" |
250 shows "(equ ===> op=) Size Size" |
215 unfolding fun_rel_def |
251 unfolding fun_rel_def |
216 unfolding Size_def |
252 unfolding Size_def |
218 apply(rule_tac f="Least" in arg_cong) |
254 apply(rule_tac f="Least" in arg_cong) |
219 apply(auto) |
255 apply(auto) |
220 apply (metis equ_trans) |
256 apply (metis equ_trans) |
221 by (metis equivp_def qlam_equivp) |
257 by (metis equivp_def qlam_equivp) |
222 |
258 |
223 |
|
224 section {* Size *} |
|
225 |
|
226 definition |
|
227 "Size t = Least {size s | s. s \<approx> t}" |
|
228 |
|
229 lemma [quot_respect]: |
|
230 shows "(equ ===> op=) Size Size" |
|
231 unfolding fun_rel_def |
|
232 unfolding Size_def |
|
233 apply(auto) |
|
234 apply(rule_tac f="Least" in arg_cong) |
|
235 apply(auto) |
|
236 apply (metis equ_trans) |
|
237 by (metis equivp_def qlam_equivp) |
|
238 |
|
239 instantiation qlam :: size |
259 instantiation qlam :: size |
240 begin |
260 begin |
241 |
261 |
242 quotient_definition "size_qlam::qlam \<Rightarrow> nat" |
262 quotient_definition "size_qlam::qlam \<Rightarrow> nat" |
243 is "Size::lam \<Rightarrow> nat" |
263 is "Size::lam \<Rightarrow> nat" |
263 |
283 |
264 lemma |
284 lemma |
265 "size (QLam [x].t) = Suc (size t)" |
285 "size (QLam [x].t) = Suc (size t)" |
266 apply(descending) |
286 apply(descending) |
267 apply(simp add: Size_def) |
287 apply(simp add: Size_def) |
268 apply(auto) |
|
269 apply(rule_tac n="Suc (size t)" and m="size t" in Least_Suc2) |
288 apply(rule_tac n="Suc (size t)" and m="size t" in Least_Suc2) |
270 apply(simp add: Collect_def) |
289 apply(simp add: Collect_def) |
271 apply(rule_tac x="Lam [x].t" in exI) |
290 apply(rule_tac x="Lam [x].t" in exI) |
272 apply(auto intro: equ_refl)[1] |
291 apply(auto intro: equ_refl)[1] |
273 apply(simp add: Collect_def) |
292 apply(simp add: Collect_def) |
274 apply(rule_tac x="t" in exI) |
293 apply(rule_tac x="t" in exI) |
275 apply(auto intro: equ_refl)[1] |
294 apply(auto intro: equ_refl)[1] |
276 apply(simp add: Collect_def) |
295 apply(simp add: Collect_def) |
277 apply(auto)[1] |
|
278 defer |
296 defer |
279 apply(simp add: Collect_def) |
297 apply(simp add: Collect_def) |
280 apply(auto)[1] |
298 apply(auto)[1] |
281 |
299 |
282 apply(auto) |
300 apply(auto) |