fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
authorpopescua
Fri May 24 19:09:56 2013 +0200 (2013-05-24)
changeset 52183667961fa6a60
parent 52182 57b4fdc59d3b
child 52184 d6627b50b131
child 52185 1b481b490454
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
src/HOL/Cardinals/Constructions_on_Wellorders.thy
src/HOL/Hahn_Banach/Hahn_Banach.thy
src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
src/HOL/Hahn_Banach/Zorn_Lemma.thy
src/HOL/Library/Zorn.thy
src/HOL/NSA/Filter.thy
     1.1 --- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Fri May 24 18:11:57 2013 +0200
     1.2 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Fri May 24 19:09:56 2013 +0200
     1.3 @@ -441,7 +441,7 @@
     1.4       moreover
     1.5       {assume "a \<in> Field r \<and> a' \<in> Field r'"
     1.6        hence "a \<in> Field(r - Id) \<and> a' \<in> Field (r' - Id)"
     1.7 -      using assms rel.Total_Id_Field by blast
     1.8 +      using assms Total_Id_Field by blast
     1.9        hence ?thesis unfolding Osum_def by auto
    1.10       }
    1.11       ultimately show ?thesis using * unfolding Osum_def by blast
     2.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Fri May 24 18:11:57 2013 +0200
     2.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Fri May 24 19:09:56 2013 +0200
     2.3 @@ -71,7 +71,7 @@
     2.4    from E have F: "vectorspace F" ..
     2.5    note FE = `F \<unlhd> E`
     2.6    {
     2.7 -    fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
     2.8 +    fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
     2.9      have "\<Union>c \<in> M"
    2.10        -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *}
    2.11        -- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *}
    2.12 @@ -103,7 +103,7 @@
    2.13            \<and> (\<forall>x \<in> H. h x \<le> p x)" by blast
    2.14      qed
    2.15    }
    2.16 -  then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
    2.17 +  then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
    2.18    -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *}
    2.19    proof (rule Zorn's_Lemma)
    2.20        -- {* We show that @{text M} is non-empty: *}
     3.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Fri May 24 18:11:57 2013 +0200
     3.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Fri May 24 19:09:56 2013 +0200
     3.3 @@ -23,12 +23,12 @@
     3.4    of @{text c}.  Every element in @{text H} is member of one of the
     3.5    elements of the chain.
     3.6  *}
     3.7 -lemmas [dest?] = chainD
     3.8 -lemmas chainE2 [elim?] = chainD2 [elim_format]
     3.9 +lemmas [dest?] = chainsD
    3.10 +lemmas chainsE2 [elim?] = chainsD2 [elim_format]
    3.11  
    3.12  lemma some_H'h't:
    3.13    assumes M: "M = norm_pres_extensions E p F f"
    3.14 -    and cM: "c \<in> chain M"
    3.15 +    and cM: "c \<in> chains M"
    3.16      and u: "graph H h = \<Union>c"
    3.17      and x: "x \<in> H"
    3.18    shows "\<exists>H' h'. graph H' h' \<in> c
    3.19 @@ -63,7 +63,7 @@
    3.20  
    3.21  lemma some_H'h':
    3.22    assumes M: "M = norm_pres_extensions E p F f"
    3.23 -    and cM: "c \<in> chain M"
    3.24 +    and cM: "c \<in> chains M"
    3.25      and u: "graph H h = \<Union>c"
    3.26      and x: "x \<in> H"
    3.27    shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
    3.28 @@ -77,8 +77,7 @@
    3.29        "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
    3.30      by (rule some_H'h't [elim_format]) blast
    3.31    from x_hx have "x \<in> H'" ..
    3.32 -  moreover from cM u c have "graph H' h' \<subseteq> graph H h"
    3.33 -    by (simp only: chain_ball_Union_upper)
    3.34 +  moreover from cM u c have "graph H' h' \<subseteq> graph H h" by blast
    3.35    ultimately show ?thesis using * by blast
    3.36  qed
    3.37  
    3.38 @@ -91,7 +90,7 @@
    3.39  
    3.40  lemma some_H'h'2:
    3.41    assumes M: "M = norm_pres_extensions E p F f"
    3.42 -    and cM: "c \<in> chain M"
    3.43 +    and cM: "c \<in> chains M"
    3.44      and u: "graph H h = \<Union>c"
    3.45      and x: "x \<in> H"
    3.46      and y: "y \<in> H"
    3.47 @@ -137,8 +136,7 @@
    3.48      finally have xh:"(x, h x) \<in> graph H' h'" .
    3.49      then have "x \<in> H'" ..
    3.50      moreover from y_hy have "y \<in> H'" ..
    3.51 -    moreover from cM u and c' have "graph H' h' \<subseteq> graph H h"
    3.52 -      by (simp only: chain_ball_Union_upper)
    3.53 +    moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast
    3.54      ultimately show ?thesis using * by blast
    3.55    next
    3.56      assume ?case2
    3.57 @@ -148,8 +146,7 @@
    3.58        also have "\<dots> \<subseteq> graph H'' h''" by fact
    3.59        finally have "(y, h y) \<in> graph H'' h''" .
    3.60      } then have "y \<in> H''" ..
    3.61 -    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"
    3.62 -      by (simp only: chain_ball_Union_upper)
    3.63 +    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h" by blast
    3.64      ultimately show ?thesis using ** by blast
    3.65    qed
    3.66  qed
    3.67 @@ -161,7 +158,7 @@
    3.68  
    3.69  lemma sup_definite:
    3.70    assumes M_def: "M \<equiv> norm_pres_extensions E p F f"
    3.71 -    and cM: "c \<in> chain M"
    3.72 +    and cM: "c \<in> chains M"
    3.73      and xy: "(x, y) \<in> \<Union>c"
    3.74      and xz: "(x, z) \<in> \<Union>c"
    3.75    shows "z = y"
    3.76 @@ -214,7 +211,7 @@
    3.77  
    3.78  lemma sup_lf:
    3.79    assumes M: "M = norm_pres_extensions E p F f"
    3.80 -    and cM: "c \<in> chain M"
    3.81 +    and cM: "c \<in> chains M"
    3.82      and u: "graph H h = \<Union>c"
    3.83    shows "linearform H h"
    3.84  proof
    3.85 @@ -268,7 +265,7 @@
    3.86  lemma sup_ext:
    3.87    assumes graph: "graph H h = \<Union>c"
    3.88      and M: "M = norm_pres_extensions E p F f"
    3.89 -    and cM: "c \<in> chain M"
    3.90 +    and cM: "c \<in> chains M"
    3.91      and ex: "\<exists>x. x \<in> c"
    3.92    shows "graph F f \<subseteq> graph H h"
    3.93  proof -
    3.94 @@ -294,7 +291,7 @@
    3.95  lemma sup_supF:
    3.96    assumes graph: "graph H h = \<Union>c"
    3.97      and M: "M = norm_pres_extensions E p F f"
    3.98 -    and cM: "c \<in> chain M"
    3.99 +    and cM: "c \<in> chains M"
   3.100      and ex: "\<exists>x. x \<in> c"
   3.101      and FE: "F \<unlhd> E"
   3.102    shows "F \<unlhd> H"
   3.103 @@ -317,7 +314,7 @@
   3.104  lemma sup_subE:
   3.105    assumes graph: "graph H h = \<Union>c"
   3.106      and M: "M = norm_pres_extensions E p F f"
   3.107 -    and cM: "c \<in> chain M"
   3.108 +    and cM: "c \<in> chains M"
   3.109      and ex: "\<exists>x. x \<in> c"
   3.110      and FE: "F \<unlhd> E"
   3.111      and E: "vectorspace E"
   3.112 @@ -373,7 +370,7 @@
   3.113  lemma sup_norm_pres:
   3.114    assumes graph: "graph H h = \<Union>c"
   3.115      and M: "M = norm_pres_extensions E p F f"
   3.116 -    and cM: "c \<in> chain M"
   3.117 +    and cM: "c \<in> chains M"
   3.118    shows "\<forall>x \<in> H. h x \<le> p x"
   3.119  proof
   3.120    fix x assume "x \<in> H"
     4.1 --- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Fri May 24 18:11:57 2013 +0200
     4.2 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Fri May 24 19:09:56 2013 +0200
     4.3 @@ -20,13 +20,13 @@
     4.4  *}
     4.5  
     4.6  theorem Zorn's_Lemma:
     4.7 -  assumes r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
     4.8 +  assumes r: "\<And>c. c \<in> chains S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
     4.9      and aS: "a \<in> S"
    4.10 -  shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
    4.11 +  shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> z = y"
    4.12  proof (rule Zorn_Lemma2)
    4.13 -  show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
    4.14 +  show "\<forall>c \<in> chains S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
    4.15    proof
    4.16 -    fix c assume "c \<in> chain S"
    4.17 +    fix c assume "c \<in> chains S"
    4.18      show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
    4.19      proof cases
    4.20  
    4.21 @@ -47,7 +47,7 @@
    4.22          show "\<Union>c \<in> S"
    4.23          proof (rule r)
    4.24            from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
    4.25 -          show "c \<in> chain S" by fact
    4.26 +          show "c \<in> chains S" by fact
    4.27          qed
    4.28        qed
    4.29      qed
     5.1 --- a/src/HOL/Library/Zorn.thy	Fri May 24 18:11:57 2013 +0200
     5.2 +++ b/src/HOL/Library/Zorn.thy	Fri May 24 19:09:56 2013 +0200
     5.3 @@ -414,6 +414,10 @@
     5.4  definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set" where
     5.5    "Chains r = {C. \<forall>a\<in>C. \<forall>b\<in>C. (a, b) \<in> r \<or> (b, a) \<in> r}"
     5.6  
     5.7 +lemma chains_extend:
     5.8 +  "[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"
     5.9 +  by (unfold chains_def chain_subset_def) blast
    5.10 +
    5.11  lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
    5.12    unfolding Chains_def by blast
    5.13  
    5.14 @@ -441,12 +445,20 @@
    5.15  
    5.16  lemma Zorn_Lemma:
    5.17    "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
    5.18 -  using subset_Zorn' [of A] by (auto simp: chains_alt_def)
    5.19 +  using subset_Zorn' [of A] by (force simp: chains_alt_def)
    5.20  
    5.21  lemma Zorn_Lemma2:
    5.22    "\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
    5.23    using subset_Zorn [of A] by (auto simp: chains_alt_def)
    5.24  
    5.25 +text{*Various other lemmas*}
    5.26 +
    5.27 +lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
    5.28 +by (unfold chains_def chain_subset_def) blast
    5.29 +
    5.30 +lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"
    5.31 +by (unfold chains_def) blast
    5.32 +
    5.33  lemma Zorns_po_lemma:
    5.34    assumes po: "Partial_order r"
    5.35      and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r"
     6.1 --- a/src/HOL/NSA/Filter.thy	Fri May 24 18:11:57 2013 +0200
     6.2 +++ b/src/HOL/NSA/Filter.thy	Fri May 24 19:09:56 2013 +0200
     6.3 @@ -256,23 +256,23 @@
     6.4  by (rule superfrechetI [OF filter_frechet subset_refl])
     6.5  
     6.6  lemma lemma_mem_chain_filter:
     6.7 -  "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
     6.8 -by (unfold chain_def superfrechet_def, blast)
     6.9 +  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
    6.10 +by (unfold chains_def superfrechet_def, blast)
    6.11  
    6.12  
    6.13  subsubsection {* Unions of chains of superfrechets *}
    6.14  
    6.15  text "In this section we prove that superfrechet is closed
    6.16  with respect to unions of non-empty chains. We must show
    6.17 -  1) Union of a chain is a filter,
    6.18 +  1) Union of a chain is afind_theorems name: Union_chain_UNIV filter,
    6.19    2) Union of a chain contains frechet.
    6.20  
    6.21  Number 2 is trivial, but 1 requires us to prove all the filter rules."
    6.22  
    6.23  lemma Union_chain_UNIV:
    6.24 -  "\<lbrakk>c \<in> chain superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
    6.25 +  "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
    6.26  proof -
    6.27 -  assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
    6.28 +  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
    6.29    from 2 obtain x where 3: "x \<in> c" by blast
    6.30    from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
    6.31    hence "UNIV \<in> x" by (rule filter.UNIV)
    6.32 @@ -280,9 +280,9 @@
    6.33  qed
    6.34  
    6.35  lemma Union_chain_empty:
    6.36 -  "c \<in> chain superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
    6.37 +  "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
    6.38  proof
    6.39 -  assume 1: "c \<in> chain superfrechet" and 2: "{} \<in> \<Union>c"
    6.40 +  assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
    6.41    from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
    6.42    from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
    6.43    hence "{} \<notin> x" by (rule filter.empty)
    6.44 @@ -290,14 +290,14 @@
    6.45  qed
    6.46  
    6.47  lemma Union_chain_Int:
    6.48 -  "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
    6.49 +  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
    6.50  proof -
    6.51 -  assume c: "c \<in> chain superfrechet"
    6.52 +  assume c: "c \<in> chains superfrechet"
    6.53    assume "u \<in> \<Union>c"
    6.54      then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
    6.55    assume "v \<in> \<Union>c"
    6.56      then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
    6.57 -  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" by (rule chainD)
    6.58 +  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
    6.59    with xc yc have xyc: "x \<union> y \<in> c"
    6.60      by (auto simp add: Un_absorb1 Un_absorb2)
    6.61    with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
    6.62 @@ -308,9 +308,9 @@
    6.63  qed
    6.64  
    6.65  lemma Union_chain_subset:
    6.66 -  "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
    6.67 +  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
    6.68  proof -
    6.69 -  assume c: "c \<in> chain superfrechet"
    6.70 +  assume c: "c \<in> chains superfrechet"
    6.71       and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
    6.72    from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
    6.73    from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
    6.74 @@ -319,8 +319,8 @@
    6.75  qed
    6.76  
    6.77  lemma Union_chain_filter:
    6.78 -assumes chain: "c \<in> chain superfrechet" and nonempty: "c \<noteq> {}"
    6.79 -shows "filter (\<Union>c)"
    6.80 +assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
    6.81 +shows "filter (\<Union>c)" 
    6.82  proof (rule filter.intro)
    6.83    show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
    6.84  next
    6.85 @@ -334,13 +334,13 @@
    6.86  qed
    6.87  
    6.88  lemma lemma_mem_chain_frechet_subset:
    6.89 -  "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
    6.90 -by (unfold superfrechet_def chain_def, blast)
    6.91 +  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
    6.92 +by (unfold superfrechet_def chains_def, blast)
    6.93  
    6.94  lemma Union_chain_superfrechet:
    6.95 -  "\<lbrakk>c \<noteq> {}; c \<in> chain superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
    6.96 +  "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
    6.97  proof (rule superfrechetI)
    6.98 -  assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
    6.99 +  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   6.100    thus "filter (\<Union>c)" by (rule Union_chain_filter)
   6.101    from 2 obtain x where 3: "x \<in> c" by blast
   6.102    from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
   6.103 @@ -351,9 +351,9 @@
   6.104  subsubsection {* Existence of free ultrafilter *}
   6.105  
   6.106  lemma max_cofinite_filter_Ex:
   6.107 -  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G"
   6.108 -proof (rule Zorn_Lemma2 [rule_format])
   6.109 -  fix c assume c: "c \<in> chain superfrechet"
   6.110 +  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" 
   6.111 +proof (rule Zorn_Lemma2, safe)
   6.112 +  fix c assume c: "c \<in> chains superfrechet"
   6.113    show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
   6.114    proof (cases)
   6.115      assume "c = {}"
   6.116 @@ -385,7 +385,7 @@
   6.117  proof -
   6.118    from max_cofinite_filter_Ex obtain U
   6.119      where U: "U \<in> superfrechet"
   6.120 -      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G" ..
   6.121 +      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
   6.122    from U have fil: "filter U" by (rule superfrechetD1)
   6.123    from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
   6.124    have ultra: "ultrafilter_axioms U"
   6.125 @@ -393,7 +393,7 @@
   6.126      fix G assume G: "filter G" and UG: "U \<subseteq> G"
   6.127      from fre UG have "frechet \<subseteq> G" by simp
   6.128      with G have "G \<in> superfrechet" by (rule superfrechetI)
   6.129 -    from this UG show "U = G" by (rule max)
   6.130 +    from this UG show "U = G" by (rule max[symmetric])
   6.131    qed
   6.132    have free: "freeultrafilter_axioms U"
   6.133    proof (rule freeultrafilter_axioms.intro)