equal
deleted
inserted
replaced
1236 assume "a \<notin> (supp x) \<and> b \<notin> (supp x)" |
1236 assume "a \<notin> (supp x) \<and> b \<notin> (supp x)" |
1237 then have "a \<sharp> x" and "b \<sharp> x" by (simp_all add: fresh_def) |
1237 then have "a \<sharp> x" and "b \<sharp> x" by (simp_all add: fresh_def) |
1238 then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh) |
1238 then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh) |
1239 qed |
1239 qed |
1240 |
1240 |
|
1241 lemma supports_fresh: |
|
1242 fixes x :: "'a::pt" |
|
1243 assumes a1: "S supports x" |
|
1244 and a2: "finite S" |
|
1245 and a3: "a \<notin> S" |
|
1246 shows "a \<sharp> x" |
|
1247 unfolding fresh_def |
|
1248 proof - |
|
1249 have "(supp x) \<subseteq> S" using a1 a2 by (rule supp_is_subset) |
|
1250 then show "a \<notin> (supp x)" using a3 by auto |
|
1251 qed |
|
1252 |
1241 lemma supp_is_least_supports: |
1253 lemma supp_is_least_supports: |
1242 fixes S :: "atom set" |
1254 fixes S :: "atom set" |
1243 and x :: "'a::pt" |
1255 and x :: "'a::pt" |
1244 assumes a1: "S supports x" |
1256 assumes a1: "S supports x" |
1245 and a2: "finite S" |
1257 and a2: "finite S" |
1249 show "(supp x) \<subseteq> S" using a1 a2 by (rule supp_is_subset) |
1261 show "(supp x) \<subseteq> S" using a1 a2 by (rule supp_is_subset) |
1250 with a2 have fin: "finite (supp x)" by (rule rev_finite_subset) |
1262 with a2 have fin: "finite (supp x)" by (rule rev_finite_subset) |
1251 have "(supp x) supports x" by (rule supp_supports) |
1263 have "(supp x) supports x" by (rule supp_supports) |
1252 with fin a3 show "S \<subseteq> supp x" by blast |
1264 with fin a3 show "S \<subseteq> supp x" by blast |
1253 qed |
1265 qed |
|
1266 |
1254 |
1267 |
1255 lemma subsetCI: |
1268 lemma subsetCI: |
1256 shows "(\<And>x. x \<in> A \<Longrightarrow> x \<notin> B \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> B" |
1269 shows "(\<And>x. x \<in> A \<Longrightarrow> x \<notin> B \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> B" |
1257 by auto |
1270 by auto |
1258 |
1271 |
1639 |
1652 |
1640 lemma eqvtI: |
1653 lemma eqvtI: |
1641 shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f" |
1654 shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f" |
1642 unfolding eqvt_def |
1655 unfolding eqvt_def |
1643 by simp |
1656 by simp |
|
1657 |
|
1658 lemma eqvt_at_perm: |
|
1659 assumes "eqvt_at f x" |
|
1660 shows "eqvt_at f (q \<bullet> x)" |
|
1661 proof - |
|
1662 { fix p::"perm" |
|
1663 have "p \<bullet> (f (q \<bullet> x)) = p \<bullet> q \<bullet> (f x)" |
|
1664 using assms by (simp add: eqvt_at_def) |
|
1665 also have "\<dots> = (p + q) \<bullet> (f x)" by simp |
|
1666 also have "\<dots> = f ((p + q) \<bullet> x)" |
|
1667 using assms by (simp add: eqvt_at_def) |
|
1668 finally have "p \<bullet> (f (q \<bullet> x)) = f (p \<bullet> q \<bullet> x)" by simp } |
|
1669 then show "eqvt_at f (q \<bullet> x)" unfolding eqvt_at_def |
|
1670 by simp |
|
1671 qed |
1644 |
1672 |
1645 lemma supp_fun_eqvt: |
1673 lemma supp_fun_eqvt: |
1646 assumes a: "eqvt f" |
1674 assumes a: "eqvt f" |
1647 shows "supp f = {}" |
1675 shows "supp f = {}" |
1648 using a |
1676 using a |