298 apply(simp (no_asm)) |
298 apply(simp (no_asm)) |
299 apply(subst Abs_swap[symmetric]) |
299 apply(subst Abs_swap[symmetric]) |
300 apply(simp_all) |
300 apply(simp_all) |
301 done |
301 done |
302 |
302 |
303 lemma supp_Abs_subset1: |
303 lemma finite_supp_Abs_subset1: |
304 fixes x::"'a::fs" |
304 assumes "finite (supp x)" |
305 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
305 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
306 apply(simp add: supp_conv_fresh) |
306 apply(simp add: supp_conv_fresh) |
307 apply(auto) |
307 apply(auto) |
308 apply(drule_tac supp_Abs_fun_fresh) |
308 apply(drule_tac supp_Abs_fun_fresh) |
309 apply(simp only: supp_Abs_fun_simp) |
309 apply(simp only: supp_Abs_fun_simp) |
310 apply(simp add: fresh_def) |
310 apply(simp add: fresh_def) |
311 apply(simp add: supp_finite_atom_set finite_supp) |
311 apply(simp add: supp_finite_atom_set assms) |
312 done |
312 done |
313 |
313 |
314 lemma supp_Abs_subset2: |
314 lemma finite_supp_Abs_subset2: |
315 fixes x::"'a::fs" |
315 assumes "finite (supp x)" |
316 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
316 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
317 apply(rule supp_is_subset) |
317 apply(rule supp_is_subset) |
318 apply(rule Abs_supports) |
318 apply(rule Abs_supports) |
319 apply(simp add: finite_supp) |
319 apply(simp add: assms) |
|
320 done |
|
321 |
|
322 lemma finite_supp_Abs: |
|
323 assumes "finite (supp x)" |
|
324 shows "supp (Abs as x) = (supp x) - as" |
|
325 apply(rule_tac subset_antisym) |
|
326 apply(rule finite_supp_Abs_subset2[OF assms]) |
|
327 apply(rule finite_supp_Abs_subset1[OF assms]) |
320 done |
328 done |
321 |
329 |
322 lemma supp_Abs: |
330 lemma supp_Abs: |
323 fixes x::"'a::fs" |
331 fixes x::"'a::fs" |
324 shows "supp (Abs as x) = (supp x) - as" |
332 shows "supp (Abs as x) = (supp x) - as" |
325 apply(rule_tac subset_antisym) |
333 apply(rule finite_supp_Abs) |
326 apply(rule supp_Abs_subset2) |
334 apply(simp add: finite_supp) |
327 apply(rule supp_Abs_subset1) |
|
328 done |
335 done |
329 |
336 |
330 instance abs :: (fs) fs |
337 instance abs :: (fs) fs |
331 apply(default) |
338 apply(default) |
332 apply(induct_tac x rule: abs_induct) |
339 apply(induct_tac x rule: abs_induct) |