(* 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 fresh_permute_iff)
lemma fresh_star_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
apply (intro subset_trans [OF supp_plus_perm])
apply (auto simp add: supp_swap)
done
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
section {* The freshness lemma according to Andrew Pitts *}
lemma fresh_conv_MOST:
shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
unfolding fresh_def supp_def MOST_iff_cofinite by simp
lemma fresh_apply:
assumes "a \<sharp> f" and "a \<sharp> x"
shows "a \<sharp> f x"
using assms unfolding fresh_conv_MOST
unfolding permute_fun_app_eq [where f=f]
by (elim MOST_rev_mp, simp)
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_apply)
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 {* An example of a function without finite support *}
primrec
nat_of :: "atom \<Rightarrow> nat"
where
"nat_of (Atom s n) = n"
lemma atom_eq_iff:
fixes a b :: atom
shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
by (induct a, induct b, simp)
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_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 {* Support for sets of atoms *}
lemma supp_finite_atom_set:
fixes S::"atom set"
assumes "finite S"
shows "supp S = S"
apply(rule finite_supp_unique)
apply(simp add: supports_def)
apply(simp add: swap_set_not_in)
apply(rule assms)
apply(simp add: swap_set_in)
done
section {* transpositions of permutations *}
fun
add_perm
where
"add_perm [] = 0"
| "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
lemma add_perm_append:
shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
by (induct xs arbitrary: ys)
(auto simp add: add_assoc)
(* this induction is the fixed version of the one in Finite_Set.thy *)
lemma finite_psubset_induct2[consumes 1, case_names psubset]:
assumes major: "finite A"
and minor: "\<And>A. finite A \<Longrightarrow> (\<And>B. B \<subset> A \<Longrightarrow> P B) \<Longrightarrow> P A"
shows "P A"
using major
proof (induct A taking: card rule: measure_induct_rule)
case (less A)
have fact: "finite A" by fact
have ih: "\<And>B. \<lbrakk>card B < card A; finite B\<rbrakk> \<Longrightarrow> P B" by fact
{ fix B
assume asm: "B \<subset> A"
from asm have "card B < card A" using psubset_card_mono fact by blast
moreover
from asm have "B \<subseteq> A" by auto
then have "finite B" using fact finite_subset by blast
ultimately
have "P B" using ih by simp
}
then show "P A" using minor fact by blast
qed
lemma perm_list_exists:
fixes p::perm
shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
proof -
have "finite (supp p)" by (simp add: finite_supp)
then show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct2)
case (psubset p)
have ih: "\<And>q. (supp q) \<subset> (supp p) \<Longrightarrow> (\<exists>xs. q = add_perm xs \<and> supp xs \<subseteq> supp q)" by fact
{ assume "supp p = {}"
then have "p = 0" by (simp add: supp_perm expand_perm_eq)
then have "p = add_perm [] \<and> supp [] \<subseteq> supp p" by (simp add: supp_Nil)
}
moreover
{ assume "supp p \<noteq> {}"
then obtain a where a0: "a \<in> supp p" by blast
let ?q = "p + (((- p) \<bullet> a) \<rightleftharpoons> a)"
have a1: "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)" by auto
then obtain xs where a: "?q = add_perm xs" and b: "supp xs \<subseteq> supp ?q" using ih by blast
let ?xs' = "xs @ [((- p) \<bullet> a, a)]"
have "supp [(- p \<bullet> a, a)] \<subseteq> supp p" using a0
by (simp add: supp_Cons supp_Nil supp_Pair supp_atom supp_perm) (metis permute_minus_cancel(1))
moreover
have "supp xs \<subseteq> supp p" using b a1 by blast
ultimately
have"supp ?xs' \<subseteq> supp p" by (simp add: supp_append)
moreover
have "p = add_perm ?xs'" using a[symmetric]
by (simp add: add_perm_append expand_perm_eq)
ultimately
have "p = add_perm ?xs' \<and> supp ?xs' \<subseteq> supp p" by simp
then have "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast
}
ultimately show "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p" by blast
qed
qed
section {* Lemma about support and permutations *}
lemma supp_perm_eq:
assumes a: "(supp x) \<sharp>* p"
shows "p \<bullet> x = x"
proof -
obtain xs where eq: "p = add_perm xs" and sub: "supp xs \<subseteq> supp p"
using perm_list_exists by blast
from a have "\<forall>a \<in> supp p. a \<sharp> x"
by (auto simp add: fresh_star_def fresh_def supp_perm)
with eq sub have "\<forall>a \<in> supp xs. a \<sharp> x" by auto
then have "add_perm xs \<bullet> x = x"
by (induct xs rule: add_perm.induct)
(simp_all add: supp_Cons supp_Pair supp_atom swap_fresh_fresh)
then show "p \<bullet> x = x" using eq by simp
qed
section {* at_set_avoiding2 *}
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: "xa \<sharp> x"
shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
proof -
have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
have c: "(p \<bullet> xa) \<sharp> c" using p1
unfolding fresh_star_def Ball_def
by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
then show ?thesis by blast
qed
end