theory Support
imports "HOL-Nominal.Nominal"
begin
text \<open>
An example showing that in general
x\<sharp>(A \<union> B) does not imply x\<sharp>A and x\<sharp>B
For this we set A to the set of even atoms and B to
the set of odd atoms. Then A \<union> B, that is the set of
all atoms, has empty support. The sets A, respectively B,
however have the set of all atoms as their support.
\<close>
atom_decl atom
text \<open>The set of even atoms.\<close>
abbreviation
EVEN :: "atom set"
where
"EVEN \ {atom n | n. \i. n=2*i}"
text \<open>The set of odd atoms:\<close>
abbreviation
ODD :: "atom set"
where
"ODD \ {atom n | n. \i. n=2*i+1}"
text \<open>An atom is either even or odd.\<close>
lemma even_or_odd:
fixes n :: nat
shows "\i. (n = 2*i) \ (n=2*i+1)"
by (induct n) (presburger)+
text \<open>
The union of even and odd atoms is the set of all atoms.
(Unfortunately I do not know a simpler proof of this fact.)\<close>
lemma EVEN_union_ODD:
shows "EVEN \ ODD = UNIV"
using even_or_odd
proof -
have "EVEN \ ODD = (\n. atom n) ` {n. \i. n = 2*i} \ (\n. atom n) ` {n. \i. n = 2*i+1}" by auto
also have "\ = (\n. atom n) ` ({n. \i. n = 2*i} \ {n. \i. n = 2*i+1})" by auto
also have "\ = (\n. atom n) ` ({n. \i. n = 2*i \ n = 2*i+1})" by auto
also have "\ = (\n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
also have "\ = (UNIV::atom set)" using atom.exhaust
by (auto simp add: surj_def)
finally show "EVEN \ ODD = UNIV" by simp
qed
text \<open>The sets of even and odd atoms are disjunct.\<close>
lemma EVEN_intersect_ODD:
shows "EVEN \ ODD = {}"
using even_or_odd
by (auto) (presburger)
text \<open>
The preceeding two lemmas help us to prove
the following two useful equalities:\<close>
lemma UNIV_subtract:
shows "UNIV - EVEN = ODD"
and "UNIV - ODD = EVEN"
using EVEN_union_ODD EVEN_intersect_ODD
by (blast)+
text \<open>The sets EVEN and ODD are infinite.\<close>
lemma EVEN_ODD_infinite:
shows "infinite EVEN"
and "infinite ODD"
unfolding infinite_iff_countable_subset
proof -
let ?f = "\n. atom (2*n)"
have "inj ?f \ range ?f \ EVEN" by (auto simp add: inj_on_def)
then show "\f::nat\atom. inj f \ range f \ EVEN" by (rule_tac exI)
next
let ?f = "\n. atom (2*n+1)"
have "inj ?f \ range ?f \ ODD" by (auto simp add: inj_on_def)
then show "\f::nat\atom. inj f \ range f \ ODD" by (rule_tac exI)
qed
text \<open>
A general fact about a set S of atoms that is both infinite and
coinfinite. Then S has all atoms as its support. Steve Zdancewic
helped with proving this fact.\<close>
lemma supp_infinite_coinfinite:
fixes S::"atom set"
assumes asm1: "infinite S"
and asm2: "infinite (UNIV-S)"
shows "(supp S) = (UNIV::atom set)"
proof -
have "\(x::atom). x\(supp S)"
proof
fix x::"atom"
show "x\(supp S)"
proof (cases "x\S")
case True
have "x\S" by fact
hence "\b\(UNIV-S). [(x,b)]\S\S" by (auto simp add: perm_set_def calc_atm)
with asm2 have "infinite {b\(UNIV-S). [(x,b)]\S\S}" by (rule infinite_Collection)
hence "infinite {b. [(x,b)]\S\S}" by (rule_tac infinite_super, auto)
then show "x\(supp S)" by (simp add: supp_def)
next
case False
have "x\S" by fact
hence "\b\S. [(x,b)]\S\S" by (auto simp add: perm_set_def calc_atm)
with asm1 have "infinite {b\S. [(x,b)]\S\S}" by (rule infinite_Collection)
hence "infinite {b. [(x,b)]\S\S}" by (rule_tac infinite_super, auto)
then show "x\(supp S)" by (simp add: supp_def)
qed
qed
then show "(supp S) = (UNIV::atom set)" by auto
qed
text \<open>As a corollary we get that EVEN and ODD have infinite support.\<close>
lemma EVEN_ODD_supp:
shows "supp EVEN = (UNIV::atom set)"
and "supp ODD = (UNIV::atom set)"
using supp_infinite_coinfinite UNIV_subtract EVEN_ODD_infinite
by simp_all
text \<open>
The set of all atoms has empty support, since any swappings leaves
this set unchanged.\<close>
lemma UNIV_supp:
shows "supp (UNIV::atom set) = ({}::atom set)"
proof -
have "\(x::atom) (y::atom). [(x,y)]\UNIV = (UNIV::atom set)"
by (auto simp add: perm_set_def calc_atm)
then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def)
qed
text \<open>Putting everything together.\<close>
theorem EVEN_ODD_freshness:
fixes x::"atom"
shows "x\(EVEN \ ODD)"
and "\x\EVEN"
and "\x\ODD"
by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp)
text \<open>Moral: support is a sublte notion.\<close>
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
