nominal2: comparison Nominal/Nominal2

equal deleted inserted replaced

-:1803104d76c9
+:0d7a1703fe28
 }
 ultimately show "(p + q) \<bullet> a = (q + p) \<bullet> a"
 using asm by blast
 qed
 qed
+lemma supp_plus_perm_eq:
+fixes p q::perm
+assumes asm: "supp p \<inter> supp q = {}"
+shows "supp (p + q) = supp p \<union> supp q"
+proof -
+{ fix a::"atom"
+assume "a \<in> supp p"
+then have "a \<notin> supp q" using asm by auto
+then have "a \<in> supp (p + q)" using `a \<in> supp p`
+by (simp add: supp_perm)
+}
+moreover
+{ fix a::"atom"
+assume "a \<in> supp q"
+then have "a \<notin> supp p" using asm by auto
+then have "a \<in> supp (q + p)" using `a \<in> supp q`
+by (simp add: supp_perm)
+then have "a \<in> supp (p + q)" using asm plus_perm_eq
+by metis
+}
+ultimately have "supp p \<union> supp q \<subseteq> supp (p + q)"
+by blast
+then show "supp (p + q) = supp p \<union> supp q" using supp_plus_perm
+by blast
+qed
 section {* Finite Support instances for other types *}
 subsection {* Type @{typ "'a \<times> 'b"} is finitely-supported. *}
 lemma at_set_avoiding_aux:
 fixes Xs::"atom set"
 and   As::"atom set"
 assumes b: "Xs \<subseteq> As"
 and     c: "finite As"
-shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) = (Xs \<union> (p \<bullet> Xs))"
 proof -
 from b c have "finite Xs" by (rule finite_subset)
 then show ?thesis using b
 proof (induct rule: finite_subset_induct)
 case empty
 have "0 \<bullet> {} \<inter> As = {}" by simp
 moreover
-have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
+have "supp (0::perm) = {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
 ultimately show ?case by blast
 next
 case (insert x Xs)
 then obtain p where
 p1: "(p \<bullet> Xs) \<inter> As = {}" and
-p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast
+p2: "supp p = (Xs \<union> (p \<bullet> Xs))" by blast
 from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast
 with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast
 hence px: "p \<bullet> x = x" unfolding supp_perm by simp
-have "finite (As \<union> p \<bullet> Xs)"
+have "finite (As \<union> p \<bullet> Xs \<union> supp p)"
 using `finite As` `finite Xs`
-by (simp add: permute_set_eq_image)
+by (simp add: permute_set_eq_image finite_supp)
-then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"
+then obtain y where "y \<notin> (As \<union> p \<bullet> Xs \<union> supp p)" "sort_of y = sort_of x"
 by (rule obtain_atom)
-hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"
+hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "y \<notin> supp p" "sort_of y = sort_of x"
 by simp_all
+hence py: "p \<bullet> y = y" "x \<noteq> y" using `x \<in> As`
+by (auto simp add: supp_perm)
 let ?q = "(x \<rightleftharpoons> y) + p"
 have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
 unfolding insert_eqvt
 using `p \<bullet> x = x` `sort_of y = sort_of x`
 using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
 by (simp add: swap_atom swap_set_not_in)
 have "?q \<bullet> insert x Xs \<inter> As = {}"
 using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
 unfolding q by simp
 moreover
-have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
+have "supp (x \<rightleftharpoons> y) \<inter> supp p = {}" using px py `sort_of y = sort_of x`
-using p2 unfolding q
+unfolding supp_swap by (simp add: supp_perm)
-by (intro subset_trans [OF supp_plus_perm])
+then have "supp ?q = (supp (x \<rightleftharpoons> y) \<union> supp p)"
-(auto simp add: supp_swap)
+by (simp add: supp_plus_perm_eq)
+then have "supp ?q = insert x Xs \<union> ?q \<bullet> insert x Xs"
+using p2 `sort_of y = sort_of x` `x \<noteq> y` unfolding q supp_swap
+by auto
 ultimately show ?case by blast
 qed
 qed
 lemma at_set_avoiding:
 assumes a: "finite Xs"
 and     b: "finite (supp c)"
-obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) = (Xs \<union> (p \<bullet> Xs))"
 using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
 unfolding fresh_star_def fresh_def by blast
 lemma at_set_avoiding1:
 assumes "finite xs"
 lemma at_set_avoiding3:
 assumes "finite xs"
 and     "finite (supp c)" "finite (supp x)"
 and     "xs \<sharp>* x"
-shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p \<subseteq> xs \<union> (p \<bullet> xs)"
+shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p = xs \<union> (p \<bullet> xs)"
 using assms
 apply(erule_tac c="(c, x)" in at_set_avoiding)
 apply(simp add: supp_Pair)
 apply(rule_tac x="p" in exI)
 apply(simp add: fresh_star_Pair)
 apply(rule fresh_star_supp_conv)
 apply(auto simp add: fresh_star_def)
 done
 lemma at_set_avoiding2_atom:
 assumes "finite (supp c)" "finite (supp x)"
 and     b: "a \<sharp> x"
 shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"
 unfolding fresh_star_def Ball_def
 by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
 hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
 then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
 qed
 section {* Renaming permutations *}
 lemma set_renaming_perm:
 assumes a: "p \<bullet> bs \<inter> bs = {}"

changeset 2614	0d7a1703fe28
parent 2611	3d101f2f817c
child 2632	e8732350a29f