equal
deleted
inserted
replaced
1510 by (simp add: supp_perm) |
1510 by (simp add: supp_perm) |
1511 |
1511 |
1512 lemma supp_swap: |
1512 lemma supp_swap: |
1513 shows "supp (a \<rightleftharpoons> b) = (if a = b \<or> sort_of a \<noteq> sort_of b then {} else {a, b})" |
1513 shows "supp (a \<rightleftharpoons> b) = (if a = b \<or> sort_of a \<noteq> sort_of b then {} else {a, b})" |
1514 by (auto simp add: supp_perm swap_atom) |
1514 by (auto simp add: supp_perm swap_atom) |
|
1515 |
|
1516 lemma fresh_swap: |
|
1517 shows "a \<sharp> (b \<rightleftharpoons> c) \<longleftrightarrow> (sort_of b \<noteq> sort_of c) \<or> b = c \<or> (a \<sharp> b \<and> a \<sharp> c)" |
|
1518 by (simp add: fresh_def supp_swap supp_atom) |
1515 |
1519 |
1516 lemma fresh_zero_perm: |
1520 lemma fresh_zero_perm: |
1517 shows "a \<sharp> (0::perm)" |
1521 shows "a \<sharp> (0::perm)" |
1518 unfolding fresh_perm by simp |
1522 unfolding fresh_perm by simp |
1519 |
1523 |
2064 assumes fin1: "finite S" |
2068 assumes fin1: "finite S" |
2065 and fin2: "finite T" |
2069 and fin2: "finite T" |
2066 shows "supp (S \<union> T) = supp S \<union> supp T" |
2070 shows "supp (S \<union> T) = supp S \<union> supp T" |
2067 using fin1 fin2 |
2071 using fin1 fin2 |
2068 by (simp add: supp_of_finite_sets) |
2072 by (simp add: supp_of_finite_sets) |
|
2073 |
|
2074 lemma fresh_finite_union: |
|
2075 fixes S T::"('a::fs) set" |
|
2076 assumes fin1: "finite S" |
|
2077 and fin2: "finite T" |
|
2078 shows "a \<sharp> (S \<union> T) \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T" |
|
2079 unfolding fresh_def |
|
2080 by (simp add: supp_of_finite_union[OF fin1 fin2]) |
2069 |
2081 |
2070 lemma supp_of_finite_insert: |
2082 lemma supp_of_finite_insert: |
2071 fixes S::"('a::fs) set" |
2083 fixes S::"('a::fs) set" |
2072 assumes fin: "finite S" |
2084 assumes fin: "finite S" |
2073 shows "supp (insert x S) = supp x \<union> supp S" |
2085 shows "supp (insert x S) = supp x \<union> supp S" |
2580 case (plus p1 p2) |
2592 case (plus p1 p2) |
2581 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
2593 have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+ |
2582 then show "(p1 + p2) \<bullet> x = x" by simp |
2594 then show "(p1 + p2) \<bullet> x = x" by simp |
2583 qed |
2595 qed |
2584 qed |
2596 qed |
2585 |
|
2586 |
|
2587 |
|
2588 |
2597 |
2589 lemma supp_perm_perm_eq: |
2598 lemma supp_perm_perm_eq: |
2590 assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a" |
2599 assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a" |
2591 shows "p \<bullet> x = q \<bullet> x" |
2600 shows "p \<bullet> x = q \<bullet> x" |
2592 proof - |
2601 proof - |
3053 fixes a::"'a::at_base" |
3062 fixes a::"'a::at_base" |
3054 shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x" |
3063 shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x" |
3055 unfolding atom_eqvt[symmetric] |
3064 unfolding atom_eqvt[symmetric] |
3056 by (simp only: fresh_permute_iff) |
3065 by (simp only: fresh_permute_iff) |
3057 |
3066 |
|
3067 lemma fresh_at_base_permI: |
|
3068 shows "atom a \<sharp> p \<Longrightarrow> p \<bullet> a = a" |
|
3069 by (simp add: fresh_def supp_perm) |
|
3070 |
3058 |
3071 |
3059 section {* Infrastructure for concrete atom types *} |
3072 section {* Infrastructure for concrete atom types *} |
3060 |
3073 |
3061 definition |
3074 definition |
3062 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
3075 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |