diff -r f2094906e491 -r e44d86131648 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Zorn.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -12,27 +12,27 @@
 
 definition
   Subset_rel :: "i=>i"  where
-   "Subset_rel(A) == {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}"
+   "Subset_rel(A) \<equiv> {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}"
 
 definition
   chain      :: "i=>i"  where
-   "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
+   "chain(A)      \<equiv> {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
 
 definition
   super      :: "[i,i]=>i"  where
-   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
+   "super(A,c)    \<equiv> {d \<in> chain(A). c<=d & c\<noteq>d}"
 
 definition
   maxchain   :: "i=>i"  where
-   "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
+   "maxchain(A)   \<equiv> {c \<in> chain(A). super(A,c)=0}"
 
 definition
   increasing :: "i=>i"  where
-    "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A \<longrightarrow> x<=f`x}"
+    "increasing(A) \<equiv> {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A \<longrightarrow> x<=f`x}"
 
 
 text\<open>Lemma for the inductive definition below\<close>
-lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> \<Union>(Y) \<in> Pow(A)"
+lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) \<Longrightarrow> \<Union>(Y) \<in> Pow(A)"
 by blast
 
 
@@ -47,10 +47,10 @@
 inductive
   domains       "TFin(S,next)" \<subseteq> "Pow(S)"
   intros
-    nextI:       "[| x \<in> TFin(S,next);  next \<in> increasing(S) |]
-                  ==> next`x \<in> TFin(S,next)"
+    nextI:       "\<lbrakk>x \<in> TFin(S,next);  next \<in> increasing(S)\<rbrakk>
+                  \<Longrightarrow> next`x \<in> TFin(S,next)"
 
-    Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> \<Union>(Y) \<in> TFin(S,next)"
+    Pow_UnionI: "Y \<in> Pow(TFin(S,next)) \<Longrightarrow> \<Union>(Y) \<in> TFin(S,next)"
 
   monos         Pow_mono
   con_defs      increasing_def
@@ -59,22 +59,22 @@
 
 subsection\<open>Mathematical Preamble\<close>
 
-lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> \<Union>(C)<=A | B<=\<Union>(C)"
+lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) \<Longrightarrow> \<Union>(C)<=A | B<=\<Union>(C)"
 by blast
 
 lemma Inter_lemma0:
-     "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A \<subseteq> \<Inter>(C) | \<Inter>(C) \<subseteq> B"
+     "\<lbrakk>c \<in> C; \<forall>x\<in>C. A<=x | x<=B\<rbrakk> \<Longrightarrow> A \<subseteq> \<Inter>(C) | \<Inter>(C) \<subseteq> B"
 by blast
 
 
 subsection\<open>The Transfinite Construction\<close>
 
-lemma increasingD1: "f \<in> increasing(A) ==> f \<in> Pow(A)->Pow(A)"
+lemma increasingD1: "f \<in> increasing(A) \<Longrightarrow> f \<in> Pow(A)->Pow(A)"
 apply (unfold increasing_def)
 apply (erule CollectD1)
 done
 
-lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x \<subseteq> f`x"
+lemma increasingD2: "\<lbrakk>f \<in> increasing(A); x<=A\<rbrakk> \<Longrightarrow> x \<subseteq> f`x"
 by (unfold increasing_def, blast)
 
 lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]
@@ -84,10 +84,10 @@
 
 text\<open>Structural induction on \<^term>\<open>TFin(S,next)\<close>\<close>
 lemma TFin_induct:
-  "[| n \<in> TFin(S,next);
-      !!x. [| x \<in> TFin(S,next);  P(x);  next \<in> increasing(S) |] ==> P(next`x);
-      !!Y. [| Y \<subseteq> TFin(S,next);  \<forall>y\<in>Y. P(y) |] ==> P(\<Union>(Y))
-   |] ==> P(n)"
+  "\<lbrakk>n \<in> TFin(S,next);
+      \<And>x. \<lbrakk>x \<in> TFin(S,next);  P(x);  next \<in> increasing(S)\<rbrakk> \<Longrightarrow> P(next`x);
+      \<And>Y. \<lbrakk>Y \<subseteq> TFin(S,next);  \<forall>y\<in>Y. P(y)\<rbrakk> \<Longrightarrow> P(\<Union>(Y))
+\<rbrakk> \<Longrightarrow> P(n)"
 by (erule TFin.induct, blast+)
 
 
@@ -98,9 +98,9 @@
 
 text\<open>Lemma 1 of section 3.1\<close>
 lemma TFin_linear_lemma1:
-     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);
-         \<forall>x \<in> TFin(S,next) . x<=m \<longrightarrow> x=m | next`x<=m |]
-      ==> n<=m | next`m<=n"
+     "\<lbrakk>n \<in> TFin(S,next);  m \<in> TFin(S,next);
+         \<forall>x \<in> TFin(S,next) . x<=m \<longrightarrow> x=m | next`x<=m\<rbrakk>
+      \<Longrightarrow> n<=m | next`m<=n"
 apply (erule TFin_induct)
 apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)
 (*downgrade subsetI from intro! to intro*)
@@ -110,8 +110,8 @@
 text\<open>Lemma 2 of section 3.2.  Interesting in its own right!
   Requires \<^term>\<open>next \<in> increasing(S)\<close> in the second induction step.\<close>
 lemma TFin_linear_lemma2:
-    "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
-     ==> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m | next`n \<subseteq> m"
+    "\<lbrakk>m \<in> TFin(S,next);  next \<in> increasing(S)\<rbrakk>
+     \<Longrightarrow> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m | next`n \<subseteq> m"
 apply (erule TFin_induct)
 apply (rule impI [THEN ballI])
 txt\<open>case split using \<open>TFin_linear_lemma1\<close>\<close>
@@ -135,14 +135,14 @@
 
 text\<open>a more convenient form for Lemma 2\<close>
 lemma TFin_subsetD:
-     "[| n<=m;  m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
-      ==> n=m | next`n \<subseteq> m"
+     "\<lbrakk>n<=m;  m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S)\<rbrakk>
+      \<Longrightarrow> n=m | next`n \<subseteq> m"
 by (blast dest: TFin_linear_lemma2 [rule_format])
 
 text\<open>Consequences from section 3.3 -- Property 3.2, the ordering is total\<close>
 lemma TFin_subset_linear:
-     "[| m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
-      ==> n \<subseteq> m | m<=n"
+     "\<lbrakk>m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S)\<rbrakk>
+      \<Longrightarrow> n \<subseteq> m | m<=n"
 apply (rule disjE)
 apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
 apply (assumption+, erule disjI2)
@@ -153,7 +153,7 @@
 
 text\<open>Lemma 3 of section 3.3\<close>
 lemma equal_next_upper:
-     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n \<subseteq> m"
+     "\<lbrakk>n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m\<rbrakk> \<Longrightarrow> n \<subseteq> m"
 apply (erule TFin_induct)
 apply (drule TFin_subsetD)
 apply (assumption+, force, blast)
@@ -161,8 +161,8 @@
 
 text\<open>Property 3.3 of section 3.3\<close>
 lemma equal_next_Union:
-     "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
-      ==> m = next`m <-> m = \<Union>(TFin(S,next))"
+     "\<lbrakk>m \<in> TFin(S,next);  next \<in> increasing(S)\<rbrakk>
+      \<Longrightarrow> m = next`m <-> m = \<Union>(TFin(S,next))"
 apply (rule iffI)
 apply (rule Union_upper [THEN equalityI])
 apply (rule_tac [2] equal_next_upper [THEN Union_least])
@@ -197,15 +197,15 @@
 done
 
 lemma choice_super:
-     "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
-      ==> ch ` super(S,X) \<in> super(S,X)"
+     "\<lbrakk>ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S)\<rbrakk>
+      \<Longrightarrow> ch ` super(S,X) \<in> super(S,X)"
 apply (erule apply_type)
 apply (unfold super_def maxchain_def, blast)
 done
 
 lemma choice_not_equals:
-     "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
-      ==> ch ` super(S,X) \<noteq> X"
+     "\<lbrakk>ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S)\<rbrakk>
+      \<Longrightarrow> ch ` super(S,X) \<noteq> X"
 apply (rule notI)
 apply (drule choice_super, assumption, assumption)
 apply (simp add: super_def)
@@ -213,7 +213,7 @@
 
 text\<open>This justifies Definition 4.4\<close>
 lemma Hausdorff_next_exists:
-     "ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X) ==>
+     "ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X) \<Longrightarrow>
       \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                    next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
 apply (rule_tac x="\<lambda>X\<in>Pow(S).
@@ -236,12 +236,12 @@
 
 text\<open>Lemma 4\<close>
 lemma TFin_chain_lemma4:
-     "[| c \<in> TFin(S,next);
+     "\<lbrakk>c \<in> TFin(S,next);
          ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X);
          next \<in> increasing(S);
          \<forall>X \<in> Pow(S). next`X =
-                          if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
-     ==> c \<in> chain(S)"
+                          if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)\<rbrakk>
+     \<Longrightarrow> c \<in> chain(S)"
 apply (erule TFin_induct)
 apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
             choice_super [THEN super_subset_chain [THEN subsetD]])
@@ -277,10 +277,10 @@
 
 text\<open>Used in the proof of Zorn's Lemma\<close>
 lemma chain_extend:
-    "[| c \<in> chain(A);  z \<in> A;  \<forall>x \<in> c. x<=z |] ==> cons(z,c) \<in> chain(A)"
+    "\<lbrakk>c \<in> chain(A);  z \<in> A;  \<forall>x \<in> c. x<=z\<rbrakk> \<Longrightarrow> cons(z,c) \<in> chain(A)"
 by (unfold chain_def, blast)
 
-lemma Zorn: "\<forall>c \<in> chain(S). \<Union>(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
+lemma Zorn: "\<forall>c \<in> chain(S). \<Union>(c) \<in> S \<Longrightarrow> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
 apply (rule Hausdorff [THEN exE])
 apply (simp add: maxchain_def)
 apply (rename_tac c)
@@ -299,7 +299,7 @@
 text \<open>Alternative version of Zorn's Lemma\<close>
 
 theorem Zorn2:
-  "\<forall>c \<in> chain(S). \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
+  "\<forall>c \<in> chain(S). \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y \<Longrightarrow> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
 apply (cut_tac Hausdorff maxchain_subset_chain)
 apply (erule exE)
 apply (drule subsetD, assumption)
@@ -321,8 +321,8 @@
 
 text\<open>Lemma 5\<close>
 lemma TFin_well_lemma5:
-     "[| n \<in> TFin(S,next);  Z \<subseteq> TFin(S,next);  z:Z;  ~ \<Inter>(Z) \<in> Z |]
-      ==> \<forall>m \<in> Z. n \<subseteq> m"
+     "\<lbrakk>n \<in> TFin(S,next);  Z \<subseteq> TFin(S,next);  z:Z;  \<not> \<Inter>(Z) \<in> Z\<rbrakk>
+      \<Longrightarrow> \<forall>m \<in> Z. n \<subseteq> m"
 apply (erule TFin_induct)
 prefer 2 apply blast txt\<open>second induction step is easy\<close>
 apply (rule ballI)
@@ -332,7 +332,7 @@
 done
 
 text\<open>Well-ordering of \<^term>\<open>TFin(S,next)\<close>\<close>
-lemma well_ord_TFin_lemma: "[| Z \<subseteq> TFin(S,next);  z \<in> Z |] ==> \<Inter>(Z) \<in> Z"
+lemma well_ord_TFin_lemma: "\<lbrakk>Z \<subseteq> TFin(S,next);  z \<in> Z\<rbrakk> \<Longrightarrow> \<Inter>(Z) \<in> Z"
 apply (rule classical)
 apply (subgoal_tac "Z = {\<Union>(TFin (S,next))}")
 apply (simp (no_asm_simp) add: Inter_singleton)
@@ -344,7 +344,7 @@
 text\<open>This theorem just packages the previous result\<close>
 lemma well_ord_TFin:
      "next \<in> increasing(S) 
-      ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
+      \<Longrightarrow> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
 apply (rule well_ordI)
 apply (unfold Subset_rel_def linear_def)
 txt\<open>Prove the well-foundedness goal\<close>
@@ -364,14 +364,14 @@
 text\<open>* Defining the "next" operation for Zermelo's Theorem *\<close>
 
 lemma choice_Diff:
-     "[| ch \<in> (\<Prod>X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
+     "\<lbrakk>ch \<in> (\<Prod>X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S\<rbrakk> \<Longrightarrow> ch ` (S-X) \<in> S-X"
 apply (erule apply_type)
 apply (blast elim!: equalityE)
 done
 
 text\<open>This justifies Definition 6.1\<close>
 lemma Zermelo_next_exists:
-     "ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X) ==>
+     "ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X) \<Longrightarrow>
            \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                       next`X = (if X=S then S else cons(ch`(S-X), X))"
 apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
@@ -391,10 +391,10 @@
 
 text\<open>The construction of the injection\<close>
 lemma choice_imp_injection:
-     "[| ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X);
+     "\<lbrakk>ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X);
          next \<in> increasing(S);
-         \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
-      ==> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))
+         \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X))\<rbrakk>
+      \<Longrightarrow> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))
                \<in> inj(S, TFin(S,next) - {S})"
 apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)
 apply (rule DiffI)
@@ -406,7 +406,7 @@
 prefer 2 apply (blast elim: equalityE)
 txt\<open>For proving \<open>x \<in> next`\<Union>(...)\<close>.
   Abrial and Laffitte's justification appears to be faulty.\<close>
-apply (subgoal_tac "~ next ` Union({y \<in> TFin (S,next) . x \<notin> y}) 
+apply (subgoal_tac "\<not> next ` Union({y \<in> TFin (S,next) . x \<notin> y}) 
                     \<subseteq> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
  prefer 2
  apply (simp del: Union_iff
@@ -439,7 +439,7 @@
   "Chain(r) = {A \<in> Pow(field(r)). \<forall>a\<in>A. \<forall>b\<in>A. <a, b> \<in> r | <b, a> \<in> r}"
 
 lemma mono_Chain:
-  "r \<subseteq> s ==> Chain(r) \<subseteq> Chain(s)"
+  "r \<subseteq> s \<Longrightarrow> Chain(r) \<subseteq> Chain(s)"
   unfolding Chain_def
   by blast