diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Sat Oct 17 01:05:59 2009 +0200 +++ b/src/HOL/Library/Zorn.thy Sat Oct 17 14:43:18 2009 +0200 @@ -1,7 +1,8 @@ -(* Title : HOL/Library/Zorn.thy - Author : Jacques D. Fleuriot, Tobias Nipkow - Description : Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF) - The well-ordering theorem +(* Title: HOL/Library/Zorn.thy + Author: Jacques D. Fleuriot, Tobias Nipkow + +Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF). +The well-ordering theorem. *) header {* Zorn's Lemma *} @@ -289,7 +290,7 @@ assume "a \ Field r" "?B a \ C" "b \ Field r" "?B b \ C" hence "?B a \ ?B b \ ?B b \ ?B a" using 2 by auto thus "(a, b) \ r \ (b, a) \ r" using `Preorder r` `a:Field r` `b:Field r` - by(simp add:subset_Image1_Image1_iff) + by (simp add:subset_Image1_Image1_iff) qed then obtain u where uA: "u:Field r" "\a\?A. (a,u) : r" using u by auto have "\A\C. A \ r^-1 `` {u}" (is "?P u") @@ -297,7 +298,7 @@ fix a B assume aB: "B:C" "a:B" with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto thus "(a,u) : r" using uA aB `Preorder r` - by (auto simp add: preorder_on_def refl_on_def) (metis transD) + by (auto simp add: preorder_on_def refl_on_def) (metis transD) qed thus "EX u:Field r. ?P u" using `u:Field r` by blast qed @@ -381,9 +382,9 @@ next case (Suc i) moreover obtain s where "s\R" and "(f(Suc(Suc i)), f(Suc i)) \ s" - using 1 by auto + using 1 by auto moreover hence "s initial_segment_of r \ r initial_segment_of s" - using assms(1) `r:R` by(simp add: Chain_def) + using assms(1) `r:R` by(simp add: Chain_def) ultimately show ?case by(simp add:init_seg_of_def) blast qed } @@ -452,9 +453,9 @@ proof assume "m={}" moreover have "Well_order {(x,x)}" - by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def) + by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def) ultimately show False using max - by (auto simp:I_def init_seg_of_def simp del:Field_insert) + by (auto simp:I_def init_seg_of_def simp del:Field_insert) qed hence "Field m \ {}" by(auto simp:Field_def) moreover have "wf(m-Id)" using `Well_order m` @@ -476,10 +477,10 @@ moreover have "wf(?m-Id)" proof- have "wf ?s" using `x \ Field m` - by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis + by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis thus ?thesis using `wf(m-Id)` `x \ Field m` - wf_subset[OF `wf ?s` Diff_subset] - by (fastsimp intro!: wf_Un simp add: Un_Diff Field_def) + wf_subset[OF `wf ?s` Diff_subset] + by (fastsimp intro!: wf_Un simp add: Un_Diff Field_def) qed ultimately have "Well_order ?m" by(simp add:order_on_defs) --{*We show that the extension is above m*}