replace locale 'UFT' with new un-named context block feature;
authorhuffman
Sun Apr 15 18:55:45 2012 +0200 (2012-04-15)
changeset 474864d49f3ffe97e
parent 47485 0b4698a31e9a
child 47487 54a2f155621b
replace locale 'UFT' with new un-named context block feature;
use locale begin/end instead of 'in';
src/HOL/NSA/Filter.thy
     1.1 --- a/src/HOL/NSA/Filter.thy	Sun Apr 15 14:51:15 2012 +0200
     1.2 +++ b/src/HOL/NSA/Filter.thy	Sun Apr 15 18:55:45 2012 +0200
     1.3 @@ -20,65 +20,73 @@
     1.4    assumes empty [iff]: "{} \<notin> F"
     1.5    assumes Int:         "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
     1.6    assumes subset:      "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
     1.7 +begin
     1.8  
     1.9 -lemma (in filter) memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
    1.10 +lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
    1.11  proof
    1.12    assume "A \<in> F" and "- A \<in> F"
    1.13    hence "A \<inter> (- A) \<in> F" by (rule Int)
    1.14    thus "False" by simp
    1.15  qed
    1.16  
    1.17 -lemma (in filter) not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
    1.18 +lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
    1.19  by (drule memD, simp)
    1.20  
    1.21 -lemma (in filter) Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
    1.22 +lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
    1.23  by (auto elim: subset intro: Int)
    1.24  
    1.25 +end
    1.26 +
    1.27  subsubsection {* Ultrafilters *}
    1.28  
    1.29  locale ultrafilter = filter +
    1.30    assumes ultra: "A \<in> F \<or> - A \<in> F"
    1.31 +begin
    1.32  
    1.33 -lemma (in ultrafilter) memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
    1.34 -by (cut_tac ultra [of A], simp)
    1.35 +lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
    1.36 +using ultra [of A] by simp
    1.37  
    1.38 -lemma (in ultrafilter) not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
    1.39 +lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
    1.40  by (rule memI, simp)
    1.41  
    1.42 -lemma (in ultrafilter) not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
    1.43 +lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
    1.44  by (rule iffI [OF not_memD not_memI])
    1.45  
    1.46 -lemma (in ultrafilter) Compl_iff: "(- A \<in> F) = (A \<notin> F)"
    1.47 +lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)"
    1.48  by (rule iffI [OF not_memI not_memD])
    1.49  
    1.50 -lemma (in ultrafilter) Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
    1.51 +lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
    1.52   apply (rule iffI)
    1.53    apply (erule contrapos_pp)
    1.54    apply (simp add: Int_iff not_mem_iff)
    1.55   apply (auto elim: subset)
    1.56  done
    1.57  
    1.58 +end
    1.59 +
    1.60  subsubsection {* Free Ultrafilters *}
    1.61  
    1.62  locale freeultrafilter = ultrafilter +
    1.63    assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
    1.64 +begin
    1.65  
    1.66 -lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F"
    1.67 +lemma finite: "finite A \<Longrightarrow> A \<notin> F"
    1.68  by (erule contrapos_pn, erule infinite)
    1.69  
    1.70 -lemma (in freeultrafilter) singleton: "{x} \<notin> F"
    1.71 +lemma singleton: "{x} \<notin> F"
    1.72  by (rule finite, simp)
    1.73  
    1.74 -lemma (in freeultrafilter) insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
    1.75 +lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
    1.76  apply (subst insert_is_Un)
    1.77  apply (subst Un_iff)
    1.78  apply (simp add: singleton)
    1.79  done
    1.80  
    1.81 -lemma (in freeultrafilter) filter: "filter F" ..
    1.82 +lemma filter: "filter F" ..
    1.83  
    1.84 -lemma (in freeultrafilter) ultrafilter: "ultrafilter F" ..
    1.85 +lemma ultrafilter: "ultrafilter F" ..
    1.86  
    1.87 +end
    1.88  
    1.89  subsection {* Collect properties *}
    1.90  
    1.91 @@ -192,8 +200,8 @@
    1.92  
    1.93  subsection {* Ultrafilter Theorem *}
    1.94  
    1.95 -text "A locale makes proof of ultrafilter Theorem more modular"
    1.96 -locale UFT =
    1.97 +text "A local context makes proof of ultrafilter Theorem more modular"
    1.98 +context
    1.99    fixes   frechet :: "'a set set"
   1.100    and     superfrechet :: "'a set set set"
   1.101  
   1.102 @@ -201,16 +209,17 @@
   1.103  
   1.104    defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
   1.105    and     superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
   1.106 +begin
   1.107  
   1.108 -lemma (in UFT) superfrechetI:
   1.109 +lemma superfrechetI:
   1.110    "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
   1.111  by (simp add: superfrechet_def)
   1.112  
   1.113 -lemma (in UFT) superfrechetD1:
   1.114 +lemma superfrechetD1:
   1.115    "G \<in> superfrechet \<Longrightarrow> filter G"
   1.116  by (simp add: superfrechet_def)
   1.117  
   1.118 -lemma (in UFT) superfrechetD2:
   1.119 +lemma superfrechetD2:
   1.120    "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
   1.121  by (simp add: superfrechet_def)
   1.122  
   1.123 @@ -240,13 +249,13 @@
   1.124               export main result: The ultrafilter Theorem
   1.125  *}
   1.126  
   1.127 -lemma (in UFT) filter_frechet: "filter frechet"
   1.128 +lemma filter_frechet: "filter frechet"
   1.129  by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
   1.130  
   1.131 -lemma (in UFT) frechet_in_superfrechet: "frechet \<in> superfrechet"
   1.132 +lemma frechet_in_superfrechet: "frechet \<in> superfrechet"
   1.133  by (rule superfrechetI [OF filter_frechet subset_refl])
   1.134  
   1.135 -lemma (in UFT) lemma_mem_chain_filter:
   1.136 +lemma lemma_mem_chain_filter:
   1.137    "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
   1.138  by (unfold chain_def superfrechet_def, blast)
   1.139  
   1.140 @@ -260,8 +269,8 @@
   1.141  
   1.142  Number 2 is trivial, but 1 requires us to prove all the filter rules."
   1.143  
   1.144 -lemma (in UFT) Union_chain_UNIV:
   1.145 -"\<lbrakk>c \<in> chain superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
   1.146 +lemma Union_chain_UNIV:
   1.147 +  "\<lbrakk>c \<in> chain superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
   1.148  proof -
   1.149    assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
   1.150    from 2 obtain x where 3: "x \<in> c" by blast
   1.151 @@ -270,8 +279,8 @@
   1.152    with 3 show "UNIV \<in> \<Union>c" by blast
   1.153  qed
   1.154  
   1.155 -lemma (in UFT) Union_chain_empty:
   1.156 -"c \<in> chain superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
   1.157 +lemma Union_chain_empty:
   1.158 +  "c \<in> chain superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
   1.159  proof
   1.160    assume 1: "c \<in> chain superfrechet" and 2: "{} \<in> \<Union>c"
   1.161    from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
   1.162 @@ -280,8 +289,8 @@
   1.163    with 4 show "False" by simp
   1.164  qed
   1.165  
   1.166 -lemma (in UFT) Union_chain_Int:
   1.167 -"\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
   1.168 +lemma Union_chain_Int:
   1.169 +  "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
   1.170  proof -
   1.171    assume c: "c \<in> chain superfrechet"
   1.172    assume "u \<in> \<Union>c"
   1.173 @@ -298,8 +307,8 @@
   1.174    with xyc show "u \<inter> v \<in> \<Union>c" ..
   1.175  qed
   1.176  
   1.177 -lemma (in UFT) Union_chain_subset:
   1.178 -"\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
   1.179 +lemma Union_chain_subset:
   1.180 +  "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
   1.181  proof -
   1.182    assume c: "c \<in> chain superfrechet"
   1.183       and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
   1.184 @@ -309,7 +318,7 @@
   1.185    with xc show "v \<in> \<Union>c" ..
   1.186  qed
   1.187  
   1.188 -lemma (in UFT) Union_chain_filter:
   1.189 +lemma Union_chain_filter:
   1.190  assumes chain: "c \<in> chain superfrechet" and nonempty: "c \<noteq> {}"
   1.191  shows "filter (\<Union>c)"
   1.192  proof (rule filter.intro)
   1.193 @@ -324,11 +333,11 @@
   1.194    with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
   1.195  qed
   1.196  
   1.197 -lemma (in UFT) lemma_mem_chain_frechet_subset:
   1.198 +lemma lemma_mem_chain_frechet_subset:
   1.199    "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
   1.200  by (unfold superfrechet_def chain_def, blast)
   1.201  
   1.202 -lemma (in UFT) Union_chain_superfrechet:
   1.203 +lemma Union_chain_superfrechet:
   1.204    "\<lbrakk>c \<noteq> {}; c \<in> chain superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
   1.205  proof (rule superfrechetI)
   1.206    assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
   1.207 @@ -341,7 +350,7 @@
   1.208  
   1.209  subsubsection {* Existence of free ultrafilter *}
   1.210  
   1.211 -lemma (in UFT) max_cofinite_filter_Ex:
   1.212 +lemma max_cofinite_filter_Ex:
   1.213    "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G"
   1.214  proof (rule Zorn_Lemma2 [rule_format])
   1.215    fix c assume c: "c \<in> chain superfrechet"
   1.216 @@ -357,7 +366,7 @@
   1.217    qed
   1.218  qed
   1.219  
   1.220 -lemma (in UFT) mem_superfrechet_all_infinite:
   1.221 +lemma mem_superfrechet_all_infinite:
   1.222    "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
   1.223  proof
   1.224    assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
   1.225 @@ -371,7 +380,7 @@
   1.226  
   1.227  text {* There exists a free ultrafilter on any infinite set *}
   1.228  
   1.229 -lemma (in UFT) freeultrafilter_ex:
   1.230 +lemma freeultrafilter_Ex:
   1.231    "\<exists>U::'a set set. freeultrafilter U"
   1.232  proof -
   1.233    from max_cofinite_filter_Ex obtain U
   1.234 @@ -397,7 +406,7 @@
   1.235    then show ?thesis ..
   1.236  qed
   1.237  
   1.238 -lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
   1.239 +end
   1.240  
   1.241  hide_const (open) filter
   1.242