1.1 --- a/src/HOL/NSA/Filter.thy Fri May 24 18:11:57 2013 +0200
1.2 +++ b/src/HOL/NSA/Filter.thy Fri May 24 19:09:56 2013 +0200
1.3 @@ -256,23 +256,23 @@
1.4 by (rule superfrechetI [OF filter_frechet subset_refl])
1.5
1.6 lemma lemma_mem_chain_filter:
1.7 - "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
1.8 -by (unfold chain_def superfrechet_def, blast)
1.9 + "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
1.10 +by (unfold chains_def superfrechet_def, blast)
1.11
1.12
1.13 subsubsection {* Unions of chains of superfrechets *}
1.14
1.15 text "In this section we prove that superfrechet is closed
1.16 with respect to unions of non-empty chains. We must show
1.17 - 1) Union of a chain is a filter,
1.18 + 1) Union of a chain is afind_theorems name: Union_chain_UNIV filter,
1.19 2) Union of a chain contains frechet.
1.20
1.21 Number 2 is trivial, but 1 requires us to prove all the filter rules."
1.22
1.23 lemma Union_chain_UNIV:
1.24 - "\<lbrakk>c \<in> chain superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
1.25 + "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
1.26 proof -
1.27 - assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
1.28 + assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
1.29 from 2 obtain x where 3: "x \<in> c" by blast
1.30 from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
1.31 hence "UNIV \<in> x" by (rule filter.UNIV)
1.32 @@ -280,9 +280,9 @@
1.33 qed
1.34
1.35 lemma Union_chain_empty:
1.36 - "c \<in> chain superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
1.37 + "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
1.38 proof
1.39 - assume 1: "c \<in> chain superfrechet" and 2: "{} \<in> \<Union>c"
1.40 + assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
1.41 from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
1.42 from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
1.43 hence "{} \<notin> x" by (rule filter.empty)
1.44 @@ -290,14 +290,14 @@
1.45 qed
1.46
1.47 lemma Union_chain_Int:
1.48 - "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
1.49 + "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
1.50 proof -
1.51 - assume c: "c \<in> chain superfrechet"
1.52 + assume c: "c \<in> chains superfrechet"
1.53 assume "u \<in> \<Union>c"
1.54 then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
1.55 assume "v \<in> \<Union>c"
1.56 then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
1.57 - from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" by (rule chainD)
1.58 + from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
1.59 with xc yc have xyc: "x \<union> y \<in> c"
1.60 by (auto simp add: Un_absorb1 Un_absorb2)
1.61 with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
1.62 @@ -308,9 +308,9 @@
1.63 qed
1.64
1.65 lemma Union_chain_subset:
1.66 - "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
1.67 + "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
1.68 proof -
1.69 - assume c: "c \<in> chain superfrechet"
1.70 + assume c: "c \<in> chains superfrechet"
1.71 and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
1.72 from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
1.73 from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
1.74 @@ -319,8 +319,8 @@
1.75 qed
1.76
1.77 lemma Union_chain_filter:
1.78 -assumes chain: "c \<in> chain superfrechet" and nonempty: "c \<noteq> {}"
1.79 -shows "filter (\<Union>c)"
1.80 +assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
1.81 +shows "filter (\<Union>c)"
1.82 proof (rule filter.intro)
1.83 show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
1.84 next
1.85 @@ -334,13 +334,13 @@
1.86 qed
1.87
1.88 lemma lemma_mem_chain_frechet_subset:
1.89 - "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
1.90 -by (unfold superfrechet_def chain_def, blast)
1.91 + "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
1.92 +by (unfold superfrechet_def chains_def, blast)
1.93
1.94 lemma Union_chain_superfrechet:
1.95 - "\<lbrakk>c \<noteq> {}; c \<in> chain superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
1.96 + "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
1.97 proof (rule superfrechetI)
1.98 - assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
1.99 + assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
1.100 thus "filter (\<Union>c)" by (rule Union_chain_filter)
1.101 from 2 obtain x where 3: "x \<in> c" by blast
1.102 from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
1.103 @@ -351,9 +351,9 @@
1.104 subsubsection {* Existence of free ultrafilter *}
1.105
1.106 lemma max_cofinite_filter_Ex:
1.107 - "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G"
1.108 -proof (rule Zorn_Lemma2 [rule_format])
1.109 - fix c assume c: "c \<in> chain superfrechet"
1.110 + "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U"
1.111 +proof (rule Zorn_Lemma2, safe)
1.112 + fix c assume c: "c \<in> chains superfrechet"
1.113 show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
1.114 proof (cases)
1.115 assume "c = {}"
1.116 @@ -385,7 +385,7 @@
1.117 proof -
1.118 from max_cofinite_filter_Ex obtain U
1.119 where U: "U \<in> superfrechet"
1.120 - and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G" ..
1.121 + and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
1.122 from U have fil: "filter U" by (rule superfrechetD1)
1.123 from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
1.124 have ultra: "ultrafilter_axioms U"
1.125 @@ -393,7 +393,7 @@
1.126 fix G assume G: "filter G" and UG: "U \<subseteq> G"
1.127 from fre UG have "frechet \<subseteq> G" by simp
1.128 with G have "G \<in> superfrechet" by (rule superfrechetI)
1.129 - from this UG show "U = G" by (rule max)
1.130 + from this UG show "U = G" by (rule max[symmetric])
1.131 qed
1.132 have free: "freeultrafilter_axioms U"
1.133 proof (rule freeultrafilter_axioms.intro)