src/HOL/Library/Zorn.thy
changeset 32960 69916a850301
parent 30663 0b6aff7451b2
child 35175 61255c81da01
     1.1 --- a/src/HOL/Library/Zorn.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Library/Zorn.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,7 +1,8 @@
     1.4 -(*  Title       : HOL/Library/Zorn.thy
     1.5 -    Author      : Jacques D. Fleuriot, Tobias Nipkow
     1.6 -    Description : Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF)
     1.7 -                  The well-ordering theorem
     1.8 +(*  Title:      HOL/Library/Zorn.thy
     1.9 +    Author:     Jacques D. Fleuriot, Tobias Nipkow
    1.10 +
    1.11 +Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
    1.12 +The well-ordering theorem.
    1.13  *)
    1.14  
    1.15  header {* Zorn's Lemma *}
    1.16 @@ -289,7 +290,7 @@
    1.17        assume "a \<in> Field r" "?B a \<in> C" "b \<in> Field r" "?B b \<in> C"
    1.18        hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto
    1.19        thus "(a, b) \<in> r \<or> (b, a) \<in> r" using `Preorder r` `a:Field r` `b:Field r`
    1.20 -	by(simp add:subset_Image1_Image1_iff)
    1.21 +        by (simp add:subset_Image1_Image1_iff)
    1.22      qed
    1.23      then obtain u where uA: "u:Field r" "\<forall>a\<in>?A. (a,u) : r" using u by auto
    1.24      have "\<forall>A\<in>C. A \<subseteq> r^-1 `` {u}" (is "?P u")
    1.25 @@ -297,7 +298,7 @@
    1.26        fix a B assume aB: "B:C" "a:B"
    1.27        with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto
    1.28        thus "(a,u) : r" using uA aB `Preorder r`
    1.29 -	by (auto simp add: preorder_on_def refl_on_def) (metis transD)
    1.30 +        by (auto simp add: preorder_on_def refl_on_def) (metis transD)
    1.31      qed
    1.32      thus "EX u:Field r. ?P u" using `u:Field r` by blast
    1.33    qed
    1.34 @@ -381,9 +382,9 @@
    1.35      next
    1.36        case (Suc i)
    1.37        moreover obtain s where "s\<in>R" and "(f(Suc(Suc i)), f(Suc i)) \<in> s"
    1.38 -	using 1 by auto
    1.39 +        using 1 by auto
    1.40        moreover hence "s initial_segment_of r \<or> r initial_segment_of s"
    1.41 -	using assms(1) `r:R` by(simp add: Chain_def)
    1.42 +        using assms(1) `r:R` by(simp add: Chain_def)
    1.43        ultimately show ?case by(simp add:init_seg_of_def) blast
    1.44      qed
    1.45    }
    1.46 @@ -452,9 +453,9 @@
    1.47      proof
    1.48        assume "m={}"
    1.49        moreover have "Well_order {(x,x)}"
    1.50 -	by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
    1.51 +        by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
    1.52        ultimately show False using max
    1.53 -	by (auto simp:I_def init_seg_of_def simp del:Field_insert)
    1.54 +        by (auto simp:I_def init_seg_of_def simp del:Field_insert)
    1.55      qed
    1.56      hence "Field m \<noteq> {}" by(auto simp:Field_def)
    1.57      moreover have "wf(m-Id)" using `Well_order m`
    1.58 @@ -476,10 +477,10 @@
    1.59      moreover have "wf(?m-Id)"
    1.60      proof-
    1.61        have "wf ?s" using `x \<notin> Field m`
    1.62 -	by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis
    1.63 +        by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis
    1.64        thus ?thesis using `wf(m-Id)` `x \<notin> Field m`
    1.65 -	wf_subset[OF `wf ?s` Diff_subset]
    1.66 -	by (fastsimp intro!: wf_Un simp add: Un_Diff Field_def)
    1.67 +        wf_subset[OF `wf ?s` Diff_subset]
    1.68 +        by (fastsimp intro!: wf_Un simp add: Un_Diff Field_def)
    1.69      qed
    1.70      ultimately have "Well_order ?m" by(simp add:order_on_defs)
    1.71  --{*We show that the extension is above m*}