(* Title: Nominal2_Supp+ −
Authors: Brian Huffman, Christian Urban+ −
+ −
Supplementary Lemmas and Definitions for + −
Nominal Isabelle. + −
*)+ −
theory Nominal2_Supp+ −
imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms+ −
begin+ −
+ −
+ −
section {* Fresh-Star *}+ −
+ −
+ −
text {* The fresh-star generalisation of fresh is used in strong+ −
induction principles. *}+ −
+ −
definition + −
fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)+ −
where + −
"as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"+ −
+ −
lemma fresh_star_prod:+ −
fixes as::"atom set"+ −
shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" + −
by (auto simp add: fresh_star_def fresh_Pair)+ −
+ −
lemma fresh_star_union:+ −
shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"+ −
by (auto simp add: fresh_star_def)+ −
+ −
lemma fresh_star_insert:+ −
shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"+ −
by (auto simp add: fresh_star_def)+ −
+ −
lemma fresh_star_Un_elim:+ −
"((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"+ −
unfolding fresh_star_def+ −
apply(rule)+ −
apply(erule meta_mp)+ −
apply(auto)+ −
done+ −
+ −
lemma fresh_star_insert_elim:+ −
"(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"+ −
unfolding fresh_star_def+ −
by rule (simp_all add: fresh_star_def)+ −
+ −
lemma fresh_star_empty_elim:+ −
"({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"+ −
by (simp add: fresh_star_def)+ −
+ −
lemma fresh_star_unit_elim: + −
shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"+ −
by (simp add: fresh_star_def fresh_unit) + −
+ −
lemma fresh_star_prod_elim: + −
shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"+ −
by (rule, simp_all add: fresh_star_prod)+ −
+ −
lemma fresh_star_plus:+ −
fixes p q::perm+ −
shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"+ −
unfolding fresh_star_def+ −
by (simp add: fresh_plus_perm)+ −
+ −
lemma fresh_star_permute_iff:+ −
shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"+ −
unfolding fresh_star_def+ −
by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)+ −
+ −
lemma fresh_star_eqvt[eqvt]:+ −
shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"+ −
unfolding fresh_star_def+ −
unfolding Ball_def+ −
apply(simp add: all_eqvt)+ −
apply(subst permute_fun_def)+ −
apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)+ −
done+ −
+ −
section {* Avoiding of atom sets *}+ −
+ −
text {* + −
For every set of atoms, there is another set of atoms+ −
avoiding a finitely supported c and there is a permutation+ −
which 'translates' between both sets.+ −
*}+ −
+ −
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))"+ −
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)+ −
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+ −
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)"+ −
using `finite As` `finite Xs`+ −
by (simp add: permute_set_eq_image)+ −
then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "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"+ −
by simp_all+ −
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"+ −
using p2 unfolding q+ −
by (intro subset_trans [OF supp_plus_perm])+ −
(auto simp add: supp_swap)+ −
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))"+ −
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_avoiding2:+ −
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"+ −
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_prod)+ −
apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")+ −
apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]+ −
apply(auto simp add: fresh_star_def fresh_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"+ −
proof -+ −
have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)+ −
obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"+ −
using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast+ −
have c: "(p \<bullet> a) \<sharp> c" using p1+ −
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 {* The freshness lemma according to Andy Pitts *}+ −
+ −
lemma freshness_lemma:+ −
fixes h :: "'a::at \<Rightarrow> 'b::pt"+ −
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"+ −
shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"+ −
proof -+ −
from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"+ −
by (auto simp add: fresh_Pair)+ −
show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"+ −
proof (intro exI allI impI)+ −
fix a :: 'a+ −
assume a3: "atom a \<sharp> h"+ −
show "h a = h b"+ −
proof (cases "a = b")+ −
assume "a = b"+ −
thus "h a = h b" by simp+ −
next+ −
assume "a \<noteq> b"+ −
hence "atom a \<sharp> b" by (simp add: fresh_at_base)+ −
with a3 have "atom a \<sharp> h b" + −
by (rule fresh_fun_app)+ −
with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"+ −
by (rule swap_fresh_fresh)+ −
from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"+ −
by (rule swap_fresh_fresh)+ −
from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp+ −
also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"+ −
by (rule permute_fun_app_eq)+ −
also have "\<dots> = h a"+ −
using d2 by simp+ −
finally show "h a = h b" by simp+ −
qed+ −
qed+ −
qed+ −
+ −
lemma freshness_lemma_unique:+ −
fixes h :: "'a::at \<Rightarrow> 'b::pt"+ −
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"+ −
shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"+ −
proof (rule ex_ex1I)+ −
from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"+ −
by (rule freshness_lemma)+ −
next+ −
fix x y+ −
assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"+ −
assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"+ −
from a x y show "x = y"+ −
by (auto simp add: fresh_Pair)+ −
qed+ −
+ −
text {* packaging the freshness lemma into a function *}+ −
+ −
definition+ −
fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"+ −
where+ −
"fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"+ −
+ −
lemma fresh_fun_app:+ −
fixes h :: "'a::at \<Rightarrow> 'b::pt"+ −
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"+ −
assumes b: "atom a \<sharp> h"+ −
shows "fresh_fun h = h a"+ −
unfolding fresh_fun_def+ −
proof (rule the_equality)+ −
show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"+ −
proof (intro strip)+ −
fix a':: 'a+ −
assume c: "atom a' \<sharp> h"+ −
from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)+ −
with b c show "h a' = h a" by auto+ −
qed+ −
next+ −
fix fr :: 'b+ −
assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"+ −
with b show "fr = h a" by auto+ −
qed+ −
+ −
lemma fresh_fun_app':+ −
fixes h :: "'a::at \<Rightarrow> 'b::pt"+ −
assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"+ −
shows "fresh_fun h = h a"+ −
apply (rule fresh_fun_app)+ −
apply (auto simp add: fresh_Pair intro: a)+ −
done+ −
+ −
lemma fresh_fun_eqvt:+ −
fixes h :: "'a::at \<Rightarrow> 'b::pt"+ −
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"+ −
shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"+ −
using a+ −
apply (clarsimp simp add: fresh_Pair)+ −
apply (subst fresh_fun_app', assumption+)+ −
apply (drule fresh_permute_iff [where p=p, THEN iffD2])+ −
apply (drule fresh_permute_iff [where p=p, THEN iffD2])+ −
apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])+ −
apply (erule (1) fresh_fun_app' [symmetric])+ −
done+ −
+ −
lemma fresh_fun_supports:+ −
fixes h :: "'a::at \<Rightarrow> 'b::pt"+ −
assumes a: "\<exists>a. atom a \<sharp> (h, h a)"+ −
shows "(supp h) supports (fresh_fun h)"+ −
apply (simp add: supports_def fresh_def [symmetric])+ −
apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)+ −
done+ −
+ −
notation fresh_fun (binder "FRESH " 10)+ −
+ −
lemma FRESH_f_iff:+ −
fixes P :: "'a::at \<Rightarrow> 'b::pure"+ −
fixes f :: "'b \<Rightarrow> 'c::pure"+ −
assumes P: "finite (supp P)"+ −
shows "(FRESH x. f (P x)) = f (FRESH x. P x)"+ −
proof -+ −
obtain a::'a where "atom a \<notin> supp P"+ −
using P by (rule obtain_at_base)+ −
hence "atom a \<sharp> P"+ −
by (simp add: fresh_def)+ −
show "(FRESH x. f (P x)) = f (FRESH x. P x)"+ −
apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])+ −
apply (cut_tac `atom a \<sharp> P`)+ −
apply (simp add: fresh_conv_MOST)+ −
apply (elim MOST_rev_mp, rule MOST_I, clarify)+ −
apply (simp add: permute_fun_def permute_pure expand_fun_eq)+ −
apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])+ −
apply (rule refl)+ −
done+ −
qed+ −
+ −
lemma FRESH_binop_iff:+ −
fixes P :: "'a::at \<Rightarrow> 'b::pure"+ −
fixes Q :: "'a::at \<Rightarrow> 'c::pure"+ −
fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"+ −
assumes P: "finite (supp P)" + −
and Q: "finite (supp Q)"+ −
shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"+ −
proof -+ −
from assms have "finite (supp P \<union> supp Q)" by simp+ −
then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"+ −
by (rule obtain_at_base)+ −
hence "atom a \<sharp> P" and "atom a \<sharp> Q"+ −
by (simp_all add: fresh_def)+ −
show ?thesis+ −
apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])+ −
apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)+ −
apply (simp add: fresh_conv_MOST)+ −
apply (elim MOST_rev_mp, rule MOST_I, clarify)+ −
apply (simp add: permute_fun_def permute_pure expand_fun_eq)+ −
apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])+ −
apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> Q` pure_fresh])+ −
apply (rule refl)+ −
done+ −
qed+ −
+ −
lemma FRESH_conj_iff:+ −
fixes P Q :: "'a::at \<Rightarrow> bool"+ −
assumes P: "finite (supp P)" and Q: "finite (supp Q)"+ −
shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"+ −
using P Q by (rule FRESH_binop_iff)+ −
+ −
lemma FRESH_disj_iff:+ −
fixes P Q :: "'a::at \<Rightarrow> bool"+ −
assumes P: "finite (supp P)" and Q: "finite (supp Q)"+ −
shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"+ −
using P Q by (rule FRESH_binop_iff)+ −
+ −
+ −
section {* @{const nat_of} is an example of a function + −
without finite support *}+ −
+ −
+ −
lemma not_fresh_nat_of:+ −
shows "\<not> a \<sharp> nat_of"+ −
unfolding fresh_def supp_def+ −
proof (clarsimp)+ −
assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"+ −
hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"+ −
by simp+ −
then obtain b where+ −
b1: "b \<noteq> a" and+ −
b2: "sort_of b = sort_of a" and+ −
b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"+ −
by (rule obtain_atom) auto+ −
have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)+ −
also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)+ −
also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp+ −
also have "\<dots> = nat_of b" using b2 by simp+ −
finally have "nat_of a = nat_of b" by simp+ −
with b2 have "a = b" by (simp add: atom_components_eq_iff)+ −
with b1 show "False" by simp+ −
qed+ −
+ −
lemma supp_nat_of:+ −
shows "supp nat_of = UNIV"+ −
using not_fresh_nat_of [unfolded fresh_def] by auto+ −
+ −
+ −
section {* Induction principle for permutations *}+ −
+ −
+ −
lemma perm_struct_induct[consumes 1, case_names zero swap]:+ −
assumes S: "supp p \<subseteq> S"+ −
and zero: "P 0"+ −
and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"+ −
shows "P p"+ −
proof -+ −
have "finite (supp p)" by (simp add: finite_supp)+ −
then show "P p" using S+ −
proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)+ −
case (psubset p)+ −
then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto+ −
have as: "supp p \<subseteq> S" by fact+ −
{ assume "supp p = {}"+ −
then have "p = 0" by (simp add: supp_perm expand_perm_eq)+ −
then have "P p" using zero by simp+ −
}+ −
moreover+ −
{ assume "supp p \<noteq> {}"+ −
then obtain a where a0: "a \<in> supp p" by blast+ −
then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as+ −
by (auto simp add: supp_atom supp_perm swap_atom)+ −
let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"+ −
have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)+ −
moreover+ −
have "a \<notin> supp ?q" by (simp add: supp_perm)+ −
then have "supp ?q \<noteq> supp p" using a0 by auto+ −
ultimately have "supp ?q \<subset> supp p" using a2 by auto+ −
then have "P ?q" using ih by simp+ −
moreover+ −
have "supp ?q \<subseteq> S" using as a2 by simp+ −
ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp + −
moreover + −
have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)+ −
ultimately have "P p" by simp+ −
}+ −
ultimately show "P p" by blast+ −
qed+ −
qed+ −
+ −
lemma perm_simple_struct_induct[case_names zero swap]:+ −
assumes zero: "P 0"+ −
and swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"+ −
shows "P p"+ −
by (rule_tac S="supp p" in perm_struct_induct)+ −
(auto intro: zero swap)+ −
+ −
lemma perm_subset_induct[consumes 1, case_names zero swap plus]:+ −
assumes S: "supp p \<subseteq> S"+ −
assumes zero: "P 0"+ −
assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"+ −
assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"+ −
shows "P p"+ −
using S+ −
by (induct p rule: perm_struct_induct)+ −
(auto intro: zero plus swap simp add: supp_swap)+ −
+ −
lemma supp_perm_eq:+ −
assumes "(supp x) \<sharp>* p"+ −
shows "p \<bullet> x = x"+ −
proof -+ −
from assms have "supp p \<subseteq> {a. a \<sharp> x}"+ −
unfolding supp_perm fresh_star_def fresh_def by auto+ −
then show "p \<bullet> x = x"+ −
proof (induct p rule: perm_struct_induct)+ −
case zero+ −
show "0 \<bullet> x = x" by simp+ −
next+ −
case (swap p a b)+ −
then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all+ −
then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)+ −
qed+ −
qed+ −
+ −
lemma supp_perm_eq_test:+ −
assumes "(supp x) \<sharp>* p"+ −
shows "p \<bullet> x = x"+ −
proof -+ −
from assms have "supp p \<subseteq> {a. a \<sharp> x}"+ −
unfolding supp_perm fresh_star_def fresh_def by auto+ −
then show "p \<bullet> x = x"+ −
proof (induct p rule: perm_subset_induct)+ −
case zero+ −
show "0 \<bullet> x = x" by simp+ −
next+ −
case (swap a b)+ −
then have "a \<sharp> x" "b \<sharp> x" by simp_all+ −
then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)+ −
next+ −
case (plus p1 p2)+ −
have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact++ −
then show "(p1 + p2) \<bullet> x = x" by simp+ −
qed+ −
qed+ −
+ −
+ −
section {* Support of Finite Sets of Finitely Supported Elements *}+ −
+ −
lemma Union_fresh:+ −
shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"+ −
unfolding Union_image_eq[symmetric]+ −
apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)+ −
apply(perm_simp)+ −
apply(rule refl)+ −
apply(assumption)+ −
done+ −
+ −
lemma Union_supports_set:+ −
shows "(\<Union>x \<in> S. supp x) supports S"+ −
proof -+ −
{ fix a b+ −
have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"+ −
unfolding permute_set_eq by force+ −
}+ −
then show "(\<Union>x \<in> S. supp x) supports S"+ −
unfolding supports_def + −
by (simp add: fresh_def[symmetric] swap_fresh_fresh)+ −
qed+ −
+ −
lemma Union_of_fin_supp_sets:+ −
fixes S::"('a::fs set)"+ −
assumes fin: "finite S" + −
shows "finite (\<Union>x\<in>S. supp x)"+ −
using fin by (induct) (auto simp add: finite_supp)+ −
+ −
lemma Union_included_in_supp:+ −
fixes S::"('a::fs set)"+ −
assumes fin: "finite S"+ −
shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"+ −
proof -+ −
have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"+ −
apply(rule supp_finite_atom_set[symmetric])+ −
apply(rule Union_of_fin_supp_sets[OF fin])+ −
done+ −
also have "\<dots> \<subseteq> supp S"+ −
apply(rule supp_subset_fresh)+ −
apply(simp add: Union_fresh)+ −
done+ −
finally show ?thesis .+ −
qed+ −
+ −
lemma supp_of_fin_sets:+ −
fixes S::"('a::fs set)"+ −
assumes fin: "finite S"+ −
shows "(supp S) = (\<Union>x\<in>S. supp x)"+ −
apply(rule subset_antisym)+ −
apply(rule supp_is_subset)+ −
apply(rule Union_supports_set)+ −
apply(rule Union_of_fin_supp_sets[OF fin])+ −
apply(rule Union_included_in_supp[OF fin])+ −
done+ −
+ −
lemma supp_of_fin_union:+ −
fixes S T::"('a::fs) set"+ −
assumes fin1: "finite S"+ −
and fin2: "finite T"+ −
shows "supp (S \<union> T) = supp S \<union> supp T"+ −
using fin1 fin2+ −
by (simp add: supp_of_fin_sets)+ −
+ −
lemma supp_of_fin_insert:+ −
fixes S::"('a::fs) set"+ −
assumes fin: "finite S"+ −
shows "supp (insert x S) = supp x \<union> supp S"+ −
using fin+ −
by (simp add: supp_of_fin_sets)+ −
+ −
+ −
end+ −