equal
deleted
inserted
replaced
950 unfolding fresh_def supp_atom by simp |
950 unfolding fresh_def supp_atom by simp |
951 |
951 |
952 instance atom :: fs |
952 instance atom :: fs |
953 by default (simp add: supp_atom) |
953 by default (simp add: supp_atom) |
954 |
954 |
955 section {* Support for finite sets of atoms *} |
|
956 |
|
957 lemma supp_finite_atom_set: |
|
958 fixes S::"atom set" |
|
959 assumes "finite S" |
|
960 shows "supp S = S" |
|
961 apply(rule finite_supp_unique) |
|
962 apply(simp add: supports_def) |
|
963 apply(simp add: swap_set_not_in) |
|
964 apply(rule assms) |
|
965 apply(simp add: swap_set_in) |
|
966 done |
|
967 |
955 |
968 section {* Type @{typ perm} is finitely-supported. *} |
956 section {* Type @{typ perm} is finitely-supported. *} |
969 |
957 |
970 lemma perm_swap_eq: |
958 lemma perm_swap_eq: |
971 shows "(a \<rightleftharpoons> b) \<bullet> p = p \<longleftrightarrow> (p \<bullet> (a \<rightleftharpoons> b)) = (a \<rightleftharpoons> b)" |
959 shows "(a \<rightleftharpoons> b) \<bullet> p = p \<longleftrightarrow> (p \<bullet> (a \<rightleftharpoons> b)) = (a \<rightleftharpoons> b)" |
1263 using supp_fun_app by auto |
1251 using supp_fun_app by auto |
1264 qed |
1252 qed |
1265 |
1253 |
1266 |
1254 |
1267 section {* Support of Finite Sets of Finitely Supported Elements *} |
1255 section {* Support of Finite Sets of Finitely Supported Elements *} |
|
1256 |
|
1257 text {* support and freshness for atom sets *} |
|
1258 |
|
1259 lemma supp_finite_atom_set: |
|
1260 fixes S::"atom set" |
|
1261 assumes "finite S" |
|
1262 shows "supp S = S" |
|
1263 apply(rule finite_supp_unique) |
|
1264 apply(simp add: supports_def) |
|
1265 apply(simp add: swap_set_not_in) |
|
1266 apply(rule assms) |
|
1267 apply(simp add: swap_set_in) |
|
1268 done |
|
1269 |
|
1270 lemma fresh_finite_atom_set: |
|
1271 fixes S::"atom set" |
|
1272 assumes "finite S" |
|
1273 shows "a \<sharp> S \<longleftrightarrow> a \<notin> S" |
|
1274 unfolding fresh_def |
|
1275 by (simp add: supp_finite_atom_set[OF assms]) |
|
1276 |
1268 |
1277 |
1269 lemma Union_fresh: |
1278 lemma Union_fresh: |
1270 shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)" |
1279 shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)" |
1271 unfolding Union_image_eq[symmetric] |
1280 unfolding Union_image_eq[symmetric] |
1272 apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app) |
1281 apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app) |
1975 apply(simp add: supp_of_finite_sets[OF a]) |
1984 apply(simp add: supp_of_finite_sets[OF a]) |
1976 apply(simp add: supp_at_base) |
1985 apply(simp add: supp_at_base) |
1977 apply(auto) |
1986 apply(auto) |
1978 done |
1987 done |
1979 |
1988 |
|
1989 lemma fresh_finite_set_at_base: |
|
1990 fixes a::"'a::at_base" |
|
1991 assumes a: "finite S" |
|
1992 shows "atom a \<sharp> S \<longleftrightarrow> a \<notin> S" |
|
1993 unfolding fresh_def |
|
1994 apply(simp add: supp_finite_set_at_base[OF a]) |
|
1995 apply(subst inj_image_mem_iff) |
|
1996 apply(simp add: inj_on_def) |
|
1997 apply(simp) |
|
1998 done |
|
1999 |
|
2000 |
1980 section {* Infrastructure for concrete atom types *} |
2001 section {* Infrastructure for concrete atom types *} |
1981 |
2002 |
1982 section {* A swapping operation for concrete atoms *} |
2003 section {* A swapping operation for concrete atoms *} |
1983 |
2004 |
1984 definition |
2005 definition |