equal
deleted
inserted
replaced
459 lemma aux_fresh: |
459 lemma aux_fresh: |
460 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)" |
460 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)" |
461 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
461 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
462 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
462 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
463 by (rule_tac [!] fresh_fun_eqvt_app) |
463 by (rule_tac [!] fresh_fun_eqvt_app) |
464 (simp_all add: eqvts_raw) |
464 (simp_all only: eqvts_raw) |
465 |
465 |
466 lemma supp_abs_subset1: |
466 lemma supp_abs_subset1: |
467 assumes a: "finite (supp x)" |
467 assumes a: "finite (supp x)" |
468 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
468 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
469 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
469 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
521 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
521 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
522 unfolding fresh_def |
522 unfolding fresh_def |
523 unfolding supp_abs |
523 unfolding supp_abs |
524 by auto |
524 by auto |
525 |
525 |
|
526 lemma Abs_eq_iff: |
|
527 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
|
528 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
|
529 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
|
530 by (lifting alphas_abs) |
|
531 |
|
532 |
|
533 section {* Infrastructure for building tuples of relations and functions *} |
|
534 |
526 fun |
535 fun |
527 prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set" |
536 prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set" |
528 where |
537 where |
529 "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y" |
538 "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y" |
530 |
539 |
558 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
567 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
559 unfolding prod_fv.simps |
568 unfolding prod_fv.simps |
560 by (perm_simp) (rule refl) |
569 by (perm_simp) (rule refl) |
561 |
570 |
562 |
571 |
563 (* Below seems to be not needed *) |
|
564 |
|
565 (* |
|
566 lemma Abs_eq_iff: |
|
567 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
|
568 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
|
569 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
|
570 by (lifting alphas_abs) |
|
571 *) |
|
572 |
|
573 |
|
574 end |
572 end |
575 |
573 |