author | nipkow |
Wed, 03 Oct 2018 20:55:59 +0200 | |
changeset 69115 | 919a1b23c192 |
parent 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
24895 | 1 |
theory Support |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
2 |
imports "HOL-Nominal.Nominal" |
24895 | 3 |
begin |
4 |
||
63167 | 5 |
text \<open> |
24895 | 6 |
An example showing that in general |
7 |
||
8 |
x\<sharp>(A \<union> B) does not imply x\<sharp>A and x\<sharp>B |
|
9 |
||
26262 | 10 |
For this we set A to the set of even atoms and B to |
11 |
the set of odd atoms. Then A \<union> B, that is the set of |
|
12 |
all atoms, has empty support. The sets A, respectively B, |
|
13 |
however have the set of all atoms as their support. |
|
63167 | 14 |
\<close> |
24895 | 15 |
|
16 |
atom_decl atom |
|
17 |
||
63167 | 18 |
text \<open>The set of even atoms.\<close> |
24895 | 19 |
abbreviation |
20 |
EVEN :: "atom set" |
|
21 |
where |
|
22 |
"EVEN \<equiv> {atom n | n. \<exists>i. n=2*i}" |
|
23 |
||
63167 | 24 |
text \<open>The set of odd atoms:\<close> |
24895 | 25 |
abbreviation |
26 |
ODD :: "atom set" |
|
27 |
where |
|
28 |
"ODD \<equiv> {atom n | n. \<exists>i. n=2*i+1}" |
|
29 |
||
63167 | 30 |
text \<open>An atom is either even or odd.\<close> |
24895 | 31 |
lemma even_or_odd: |
37388 | 32 |
fixes n :: nat |
24895 | 33 |
shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)" |
34 |
by (induct n) (presburger)+ |
|
35 |
||
63167 | 36 |
text \<open> |
26055 | 37 |
The union of even and odd atoms is the set of all atoms. |
63167 | 38 |
(Unfortunately I do not know a simpler proof of this fact.)\<close> |
24895 | 39 |
lemma EVEN_union_ODD: |
40 |
shows "EVEN \<union> ODD = UNIV" |
|
25139 | 41 |
using even_or_odd |
24895 | 42 |
proof - |
43 |
have "EVEN \<union> ODD = (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i} \<union> (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i+1}" by auto |
|
44 |
also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i} \<union> {n. \<exists>i. n = 2*i+1})" by auto |
|
45 |
also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto |
|
46 |
also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto |
|
47 |
also have "\<dots> = (UNIV::atom set)" using atom.exhaust |
|
40702 | 48 |
by (auto simp add: surj_def) |
24895 | 49 |
finally show "EVEN \<union> ODD = UNIV" by simp |
50 |
qed |
|
51 |
||
63167 | 52 |
text \<open>The sets of even and odd atoms are disjunct.\<close> |
24895 | 53 |
lemma EVEN_intersect_ODD: |
54 |
shows "EVEN \<inter> ODD = {}" |
|
55 |
using even_or_odd |
|
56 |
by (auto) (presburger) |
|
57 |
||
63167 | 58 |
text \<open> |
25751 | 59 |
The preceeding two lemmas help us to prove |
63167 | 60 |
the following two useful equalities:\<close> |
26055 | 61 |
|
24895 | 62 |
lemma UNIV_subtract: |
63 |
shows "UNIV - EVEN = ODD" |
|
64 |
and "UNIV - ODD = EVEN" |
|
65 |
using EVEN_union_ODD EVEN_intersect_ODD |
|
66 |
by (blast)+ |
|
67 |
||
63167 | 68 |
text \<open>The sets EVEN and ODD are infinite.\<close> |
24895 | 69 |
lemma EVEN_ODD_infinite: |
70 |
shows "infinite EVEN" |
|
71 |
and "infinite ODD" |
|
25751 | 72 |
unfolding infinite_iff_countable_subset |
73 |
proof - |
|
74 |
let ?f = "\<lambda>n. atom (2*n)" |
|
75 |
have "inj ?f \<and> range ?f \<subseteq> EVEN" by (auto simp add: inj_on_def) |
|
76 |
then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> EVEN" by (rule_tac exI) |
|
77 |
next |
|
78 |
let ?f = "\<lambda>n. atom (2*n+1)" |
|
79 |
have "inj ?f \<and> range ?f \<subseteq> ODD" by (auto simp add: inj_on_def) |
|
80 |
then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> ODD" by (rule_tac exI) |
|
81 |
qed |
|
24895 | 82 |
|
63167 | 83 |
text \<open> |
26262 | 84 |
A general fact about a set S of atoms that is both infinite and |
27360 | 85 |
coinfinite. Then S has all atoms as its support. Steve Zdancewic |
63167 | 86 |
helped with proving this fact.\<close> |
26055 | 87 |
|
24895 | 88 |
lemma supp_infinite_coinfinite: |
89 |
fixes S::"atom set" |
|
25867 | 90 |
assumes asm1: "infinite S" |
91 |
and asm2: "infinite (UNIV-S)" |
|
24895 | 92 |
shows "(supp S) = (UNIV::atom set)" |
93 |
proof - |
|
94 |
have "\<forall>(x::atom). x\<in>(supp S)" |
|
95 |
proof |
|
96 |
fix x::"atom" |
|
97 |
show "x\<in>(supp S)" |
|
98 |
proof (cases "x\<in>S") |
|
99 |
case True |
|
100 |
have "x\<in>S" by fact |
|
46181 | 101 |
hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm) |
25867 | 102 |
with asm2 have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection) |
24895 | 103 |
hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto) |
104 |
then show "x\<in>(supp S)" by (simp add: supp_def) |
|
105 |
next |
|
106 |
case False |
|
107 |
have "x\<notin>S" by fact |
|
46181 | 108 |
hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm) |
25867 | 109 |
with asm1 have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection) |
24895 | 110 |
hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto) |
111 |
then show "x\<in>(supp S)" by (simp add: supp_def) |
|
112 |
qed |
|
113 |
qed |
|
114 |
then show "(supp S) = (UNIV::atom set)" by auto |
|
115 |
qed |
|
116 |
||
63167 | 117 |
text \<open>As a corollary we get that EVEN and ODD have infinite support.\<close> |
24895 | 118 |
lemma EVEN_ODD_supp: |
119 |
shows "supp EVEN = (UNIV::atom set)" |
|
120 |
and "supp ODD = (UNIV::atom set)" |
|
121 |
using supp_infinite_coinfinite UNIV_subtract EVEN_ODD_infinite |
|
122 |
by simp_all |
|
123 |
||
63167 | 124 |
text \<open> |
25751 | 125 |
The set of all atoms has empty support, since any swappings leaves |
63167 | 126 |
this set unchanged.\<close> |
26055 | 127 |
|
24895 | 128 |
lemma UNIV_supp: |
129 |
shows "supp (UNIV::atom set) = ({}::atom set)" |
|
130 |
proof - |
|
131 |
have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)" |
|
46181 | 132 |
by (auto simp add: perm_set_def calc_atm) |
25751 | 133 |
then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def) |
24895 | 134 |
qed |
135 |
||
63167 | 136 |
text \<open>Putting everything together.\<close> |
24895 | 137 |
theorem EVEN_ODD_freshness: |
138 |
fixes x::"atom" |
|
139 |
shows "x\<sharp>(EVEN \<union> ODD)" |
|
140 |
and "\<not>x\<sharp>EVEN" |
|
141 |
and "\<not>x\<sharp>ODD" |
|
142 |
by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp) |
|
143 |
||
63167 | 144 |
text \<open>Moral: support is a sublte notion.\<close> |
26055 | 145 |
|
62390 | 146 |
end |