1090 qed |
1090 qed |
1091 |
1091 |
1092 |
1092 |
1093 subsection {* supp and fresh are equivariant *} |
1093 subsection {* supp and fresh are equivariant *} |
1094 |
1094 |
1095 lemma finite_Collect_bij: |
1095 |
1096 assumes a: "bij f" |
1096 lemma supp_eqvt [eqvt]: |
1097 shows "finite {x. P (f x)} = finite {x. P x}" |
1097 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
1098 by (metis a finite_vimage_iff vimage_Collect_eq) |
1098 unfolding supp_def |
|
1099 by (perm_simp) |
|
1100 (simp only: permute_eqvt[symmetric]) |
|
1101 |
|
1102 lemma fresh_eqvt [eqvt]: |
|
1103 shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)" |
|
1104 unfolding fresh_def |
|
1105 by (perm_simp) (rule refl) |
1099 |
1106 |
1100 lemma fresh_permute_iff: |
1107 lemma fresh_permute_iff: |
1101 shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" |
1108 shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" |
1102 proof - |
1109 by (simp only: fresh_eqvt[symmetric] permute_bool_def) |
1103 have "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> finite {b. (p \<bullet> a \<rightleftharpoons> b) \<bullet> p \<bullet> x \<noteq> p \<bullet> x}" |
|
1104 unfolding fresh_def supp_def by simp |
|
1105 also have "\<dots> \<longleftrightarrow> finite {b. (p \<bullet> a \<rightleftharpoons> p \<bullet> b) \<bullet> p \<bullet> x \<noteq> p \<bullet> x}" |
|
1106 using bij_permute by (rule finite_Collect_bij[symmetric]) |
|
1107 also have "\<dots> \<longleftrightarrow> finite {b. p \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> p \<bullet> x}" |
|
1108 by (simp only: permute_eqvt [of p] swap_eqvt) |
|
1109 also have "\<dots> \<longleftrightarrow> finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" |
|
1110 by (simp only: permute_eq_iff) |
|
1111 also have "\<dots> \<longleftrightarrow> a \<sharp> x" |
|
1112 unfolding fresh_def supp_def by simp |
|
1113 finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" . |
|
1114 qed |
|
1115 |
|
1116 lemma fresh_eqvt [eqvt]: |
|
1117 shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)" |
|
1118 unfolding permute_bool_def |
|
1119 by (simp add: fresh_permute_iff) |
|
1120 |
|
1121 lemma supp_eqvt [eqvt]: |
|
1122 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
|
1123 unfolding supp_conv_fresh |
|
1124 by (perm_simp) (rule refl) |
|
1125 |
1110 |
1126 lemma fresh_permute_left: |
1111 lemma fresh_permute_left: |
1127 shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x" |
1112 shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x" |
1128 proof |
1113 proof |
1129 assume "a \<sharp> p \<bullet> x" |
1114 assume "a \<sharp> p \<bullet> x" |