842 shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)" |
842 shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)" |
843 unfolding permute_bool_def |
843 unfolding permute_bool_def |
844 by (simp add: fresh_permute_iff) |
844 by (simp add: fresh_permute_iff) |
845 |
845 |
846 lemma supp_eqvt: |
846 lemma supp_eqvt: |
847 fixes p :: "perm" |
|
848 and x :: "'a::pt" |
|
849 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
847 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
850 unfolding supp_conv_fresh |
848 unfolding supp_conv_fresh |
851 unfolding Collect_def |
849 unfolding Collect_def |
852 unfolding permute_fun_def |
850 unfolding permute_fun_def |
853 by (simp add: Not_eqvt fresh_eqvt) |
851 by (simp add: Not_eqvt fresh_eqvt) |
|
852 |
|
853 lemma fresh_permute_left: |
|
854 shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x" |
|
855 proof |
|
856 assume "a \<sharp> p \<bullet> x" |
|
857 then have "- p \<bullet> a \<sharp> - p \<bullet> p \<bullet> x" by (simp only: fresh_permute_iff) |
|
858 then show "- p \<bullet> a \<sharp> x" by simp |
|
859 next |
|
860 assume "- p \<bullet> a \<sharp> x" |
|
861 then have "p \<bullet> - p \<bullet> a \<sharp> p \<bullet> x" by (simp only: fresh_permute_iff) |
|
862 then show "a \<sharp> p \<bullet> x" by simp |
|
863 qed |
|
864 |
854 |
865 |
855 subsection {* supports *} |
866 subsection {* supports *} |
856 |
867 |
857 definition |
868 definition |
858 supports :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" (infixl "supports" 80) |
869 supports :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" (infixl "supports" 80) |
2234 apply(subst inj_image_mem_iff) |
2245 apply(subst inj_image_mem_iff) |
2235 apply(simp add: inj_on_def) |
2246 apply(simp add: inj_on_def) |
2236 apply(simp) |
2247 apply(simp) |
2237 done |
2248 done |
2238 |
2249 |
|
2250 lemma fresh_at_base_permute_iff[simp]: |
|
2251 fixes a::"'a::at_base" |
|
2252 shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x" |
|
2253 unfolding atom_eqvt[symmetric] |
|
2254 by (simp add: fresh_permute_iff) |
|
2255 |
2239 |
2256 |
2240 section {* Infrastructure for concrete atom types *} |
2257 section {* Infrastructure for concrete atom types *} |
2241 |
2258 |
2242 section {* A swapping operation for concrete atoms *} |
|
2243 |
|
2244 definition |
2259 definition |
2245 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
2260 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
2246 where |
2261 where |
2247 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
2262 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
2248 |
2263 |
2302 fixes a b::"'a::at_base" |
2317 fixes a b::"'a::at_base" |
2303 assumes "atom a \<sharp> x" "atom b \<sharp> x" |
2318 assumes "atom a \<sharp> x" "atom b \<sharp> x" |
2304 shows "(a \<leftrightarrow> b) \<bullet> x = x" |
2319 shows "(a \<leftrightarrow> b) \<bullet> x = x" |
2305 using assms |
2320 using assms |
2306 by (simp add: flip_def swap_fresh_fresh) |
2321 by (simp add: flip_def swap_fresh_fresh) |
|
2322 |
|
2323 |
2307 |
2324 |
2308 subsection {* Syntax for coercing at-elements to the atom-type *} |
2325 subsection {* Syntax for coercing at-elements to the atom-type *} |
2309 |
2326 |
2310 syntax |
2327 syntax |
2311 "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3) |
2328 "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3) |
2500 using a |
2517 using a |
2501 apply (clarsimp simp add: fresh_Pair) |
2518 apply (clarsimp simp add: fresh_Pair) |
2502 apply (subst fresh_fun_apply', assumption+) |
2519 apply (subst fresh_fun_apply', assumption+) |
2503 apply (drule fresh_permute_iff [where p=p, THEN iffD2]) |
2520 apply (drule fresh_permute_iff [where p=p, THEN iffD2]) |
2504 apply (drule fresh_permute_iff [where p=p, THEN iffD2]) |
2521 apply (drule fresh_permute_iff [where p=p, THEN iffD2]) |
2505 apply (simp add: atom_eqvt permute_fun_app_eq [where f=h]) |
2522 apply (simp only: atom_eqvt permute_fun_app_eq [where f=h]) |
2506 apply (erule (1) fresh_fun_apply' [symmetric]) |
2523 apply (erule (1) fresh_fun_apply' [symmetric]) |
2507 done |
2524 done |
2508 |
2525 |
2509 lemma fresh_fun_supports: |
2526 lemma fresh_fun_supports: |
2510 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
2527 fixes h :: "'a::at \<Rightarrow> 'b::pt" |