src/HOL/NSA/Filter.thy
changeset 52183 667961fa6a60
parent 47486 4d49f3ffe97e
child 52198 849cf98e03c3
     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)