# HG changeset patch
# User popescua
# Date 1369415396 -7200
# Node ID 667961fa6a605a5627c2e4261adb7c0166ab55f3
# Parent  57b4fdc59d3b09194036f73bd1b696b5959201c8
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)

diff -r 57b4fdc59d3b -r 667961fa6a60 src/HOL/Cardinals/Constructions_on_Wellorders.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Fri May 24 18:11:57 2013 +0200
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Fri May 24 19:09:56 2013 +0200
@@ -441,7 +441,7 @@
      moreover
      {assume "a \<in> Field r \<and> a' \<in> Field r'"
       hence "a \<in> Field(r - Id) \<and> a' \<in> Field (r' - Id)"
-      using assms rel.Total_Id_Field by blast
+      using assms Total_Id_Field by blast
       hence ?thesis unfolding Osum_def by auto
      }
      ultimately show ?thesis using * unfolding Osum_def by blast
diff -r 57b4fdc59d3b -r 667961fa6a60 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Fri May 24 18:11:57 2013 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Fri May 24 19:09:56 2013 +0200
@@ -71,7 +71,7 @@
   from E have F: "vectorspace F" ..
   note FE = `F \<unlhd> E`
   {
-    fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
+    fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
     have "\<Union>c \<in> M"
       -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *}
       -- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *}
@@ -103,7 +103,7 @@
           \<and> (\<forall>x \<in> H. h x \<le> p x)" by blast
     qed
   }
-  then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x"
+  then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
   -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *}
   proof (rule Zorn's_Lemma)
       -- {* We show that @{text M} is non-empty: *}
diff -r 57b4fdc59d3b -r 667961fa6a60 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Fri May 24 18:11:57 2013 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Fri May 24 19:09:56 2013 +0200
@@ -23,12 +23,12 @@
   of @{text c}.  Every element in @{text H} is member of one of the
   elements of the chain.
 *}
-lemmas [dest?] = chainD
-lemmas chainE2 [elim?] = chainD2 [elim_format]
+lemmas [dest?] = chainsD
+lemmas chainsE2 [elim?] = chainsD2 [elim_format]
 
 lemma some_H'h't:
   assumes M: "M = norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
     and u: "graph H h = \<Union>c"
     and x: "x \<in> H"
   shows "\<exists>H' h'. graph H' h' \<in> c
@@ -63,7 +63,7 @@
 
 lemma some_H'h':
   assumes M: "M = norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
     and u: "graph H h = \<Union>c"
     and x: "x \<in> H"
   shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
@@ -77,8 +77,7 @@
       "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
     by (rule some_H'h't [elim_format]) blast
   from x_hx have "x \<in> H'" ..
-  moreover from cM u c have "graph H' h' \<subseteq> graph H h"
-    by (simp only: chain_ball_Union_upper)
+  moreover from cM u c have "graph H' h' \<subseteq> graph H h" by blast
   ultimately show ?thesis using * by blast
 qed
 
@@ -91,7 +90,7 @@
 
 lemma some_H'h'2:
   assumes M: "M = norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
     and u: "graph H h = \<Union>c"
     and x: "x \<in> H"
     and y: "y \<in> H"
@@ -137,8 +136,7 @@
     finally have xh:"(x, h x) \<in> graph H' h'" .
     then have "x \<in> H'" ..
     moreover from y_hy have "y \<in> H'" ..
-    moreover from cM u and c' have "graph H' h' \<subseteq> graph H h"
-      by (simp only: chain_ball_Union_upper)
+    moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast
     ultimately show ?thesis using * by blast
   next
     assume ?case2
@@ -148,8 +146,7 @@
       also have "\<dots> \<subseteq> graph H'' h''" by fact
       finally have "(y, h y) \<in> graph H'' h''" .
     } then have "y \<in> H''" ..
-    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"
-      by (simp only: chain_ball_Union_upper)
+    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h" by blast
     ultimately show ?thesis using ** by blast
   qed
 qed
@@ -161,7 +158,7 @@
 
 lemma sup_definite:
   assumes M_def: "M \<equiv> norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
     and xy: "(x, y) \<in> \<Union>c"
     and xz: "(x, z) \<in> \<Union>c"
   shows "z = y"
@@ -214,7 +211,7 @@
 
 lemma sup_lf:
   assumes M: "M = norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
     and u: "graph H h = \<Union>c"
   shows "linearform H h"
 proof
@@ -268,7 +265,7 @@
 lemma sup_ext:
   assumes graph: "graph H h = \<Union>c"
     and M: "M = norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
     and ex: "\<exists>x. x \<in> c"
   shows "graph F f \<subseteq> graph H h"
 proof -
@@ -294,7 +291,7 @@
 lemma sup_supF:
   assumes graph: "graph H h = \<Union>c"
     and M: "M = norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
     and ex: "\<exists>x. x \<in> c"
     and FE: "F \<unlhd> E"
   shows "F \<unlhd> H"
@@ -317,7 +314,7 @@
 lemma sup_subE:
   assumes graph: "graph H h = \<Union>c"
     and M: "M = norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
     and ex: "\<exists>x. x \<in> c"
     and FE: "F \<unlhd> E"
     and E: "vectorspace E"
@@ -373,7 +370,7 @@
 lemma sup_norm_pres:
   assumes graph: "graph H h = \<Union>c"
     and M: "M = norm_pres_extensions E p F f"
-    and cM: "c \<in> chain M"
+    and cM: "c \<in> chains M"
   shows "\<forall>x \<in> H. h x \<le> p x"
 proof
   fix x assume "x \<in> H"
diff -r 57b4fdc59d3b -r 667961fa6a60 src/HOL/Hahn_Banach/Zorn_Lemma.thy
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Fri May 24 18:11:57 2013 +0200
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Fri May 24 19:09:56 2013 +0200
@@ -20,13 +20,13 @@
 *}
 
 theorem Zorn's_Lemma:
-  assumes r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
+  assumes r: "\<And>c. c \<in> chains S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"
     and aS: "a \<in> S"
-  shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
+  shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> z = y"
 proof (rule Zorn_Lemma2)
-  show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
+  show "\<forall>c \<in> chains S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
   proof
-    fix c assume "c \<in> chain S"
+    fix c assume "c \<in> chains S"
     show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
     proof cases
 
@@ -47,7 +47,7 @@
         show "\<Union>c \<in> S"
         proof (rule r)
           from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
-          show "c \<in> chain S" by fact
+          show "c \<in> chains S" by fact
         qed
       qed
     qed
diff -r 57b4fdc59d3b -r 667961fa6a60 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Fri May 24 18:11:57 2013 +0200
+++ b/src/HOL/Library/Zorn.thy	Fri May 24 19:09:56 2013 +0200
@@ -414,6 +414,10 @@
 definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set" where
   "Chains r = {C. \<forall>a\<in>C. \<forall>b\<in>C. (a, b) \<in> r \<or> (b, a) \<in> r}"
 
+lemma chains_extend:
+  "[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"
+  by (unfold chains_def chain_subset_def) blast
+
 lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
   unfolding Chains_def by blast
 
@@ -441,12 +445,20 @@
 
 lemma Zorn_Lemma:
   "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
-  using subset_Zorn' [of A] by (auto simp: chains_alt_def)
+  using subset_Zorn' [of A] by (force simp: chains_alt_def)
 
 lemma Zorn_Lemma2:
   "\<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"
   using subset_Zorn [of A] by (auto simp: chains_alt_def)
 
+text{*Various other lemmas*}
+
+lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
+by (unfold chains_def chain_subset_def) blast
+
+lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"
+by (unfold chains_def) blast
+
 lemma Zorns_po_lemma:
   assumes po: "Partial_order r"
     and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r"
diff -r 57b4fdc59d3b -r 667961fa6a60 src/HOL/NSA/Filter.thy
--- a/src/HOL/NSA/Filter.thy	Fri May 24 18:11:57 2013 +0200
+++ b/src/HOL/NSA/Filter.thy	Fri May 24 19:09:56 2013 +0200
@@ -256,23 +256,23 @@
 by (rule superfrechetI [OF filter_frechet subset_refl])
 
 lemma lemma_mem_chain_filter:
-  "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
-by (unfold chain_def superfrechet_def, blast)
+  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
+by (unfold chains_def superfrechet_def, blast)
 
 
 subsubsection {* Unions of chains of superfrechets *}
 
 text "In this section we prove that superfrechet is closed
 with respect to unions of non-empty chains. We must show
-  1) Union of a chain is a filter,
+  1) Union of a chain is afind_theorems name: Union_chain_UNIV filter,
   2) Union of a chain contains frechet.
 
 Number 2 is trivial, but 1 requires us to prove all the filter rules."
 
 lemma Union_chain_UNIV:
-  "\<lbrakk>c \<in> chain superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
+  "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
 proof -
-  assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
+  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   from 2 obtain x where 3: "x \<in> c" by blast
   from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   hence "UNIV \<in> x" by (rule filter.UNIV)
@@ -280,9 +280,9 @@
 qed
 
 lemma Union_chain_empty:
-  "c \<in> chain superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
+  "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
 proof
-  assume 1: "c \<in> chain superfrechet" and 2: "{} \<in> \<Union>c"
+  assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
   from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
   from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   hence "{} \<notin> x" by (rule filter.empty)
@@ -290,14 +290,14 @@
 qed
 
 lemma Union_chain_Int:
-  "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
+  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
 proof -
-  assume c: "c \<in> chain superfrechet"
+  assume c: "c \<in> chains superfrechet"
   assume "u \<in> \<Union>c"
     then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   assume "v \<in> \<Union>c"
     then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
-  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" by (rule chainD)
+  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
   with xc yc have xyc: "x \<union> y \<in> c"
     by (auto simp add: Un_absorb1 Un_absorb2)
   with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
@@ -308,9 +308,9 @@
 qed
 
 lemma Union_chain_subset:
-  "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
+  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
 proof -
-  assume c: "c \<in> chain superfrechet"
+  assume c: "c \<in> chains superfrechet"
      and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
   from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
@@ -319,8 +319,8 @@
 qed
 
 lemma Union_chain_filter:
-assumes chain: "c \<in> chain superfrechet" and nonempty: "c \<noteq> {}"
-shows "filter (\<Union>c)"
+assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
+shows "filter (\<Union>c)" 
 proof (rule filter.intro)
   show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
 next
@@ -334,13 +334,13 @@
 qed
 
 lemma lemma_mem_chain_frechet_subset:
-  "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
-by (unfold superfrechet_def chain_def, blast)
+  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
+by (unfold superfrechet_def chains_def, blast)
 
 lemma Union_chain_superfrechet:
-  "\<lbrakk>c \<noteq> {}; c \<in> chain superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
+  "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
 proof (rule superfrechetI)
-  assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
+  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   thus "filter (\<Union>c)" by (rule Union_chain_filter)
   from 2 obtain x where 3: "x \<in> c" by blast
   from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
@@ -351,9 +351,9 @@
 subsubsection {* Existence of free ultrafilter *}
 
 lemma max_cofinite_filter_Ex:
-  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G"
-proof (rule Zorn_Lemma2 [rule_format])
-  fix c assume c: "c \<in> chain superfrechet"
+  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" 
+proof (rule Zorn_Lemma2, safe)
+  fix c assume c: "c \<in> chains superfrechet"
   show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
   proof (cases)
     assume "c = {}"
@@ -385,7 +385,7 @@
 proof -
   from max_cofinite_filter_Ex obtain U
     where U: "U \<in> superfrechet"
-      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G" ..
+      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
   from U have fil: "filter U" by (rule superfrechetD1)
   from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
   have ultra: "ultrafilter_axioms U"
@@ -393,7 +393,7 @@
     fix G assume G: "filter G" and UG: "U \<subseteq> G"
     from fre UG have "frechet \<subseteq> G" by simp
     with G have "G \<in> superfrechet" by (rule superfrechetI)
-    from this UG show "U = G" by (rule max)
+    from this UG show "U = G" by (rule max[symmetric])
   qed
   have free: "freeultrafilter_axioms U"
   proof (rule freeultrafilter_axioms.intro)