# HG changeset patch # User paulson # Date 1131640304 -3600 # Node ID fe14f0282c60dd698baa85617f49e50cf76558a1 # Parent a51ab415209752e02b1db1762b8c2f19ddf150e1 tidying diff -r a51ab4152097 -r fe14f0282c60 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Thu Nov 10 00:36:26 2005 +0100 +++ b/src/HOL/Library/Zorn.thy Thu Nov 10 17:31:44 2005 +0100 @@ -43,7 +43,7 @@ subsection{*Mathematical Preamble*} lemma Union_lemma0: - "(\x \ C. x \ A | B \ x) ==> Union(C)<=A | B \ Union(C)" + "(\x \ C. x \ A | B \ x) ==> Union(C) \ A | B \ Union(C)" by blast @@ -129,8 +129,8 @@ lemma equal_succ_Union: "m \ TFin S ==> (m = succ S m) = (m = Union(TFin S))" apply (rule iffI) apply (rule Union_upper [THEN equalityI]) - apply (rule_tac [2] eq_succ_upper [THEN Union_least]) - apply (assumption+) + apply assumption + apply (rule eq_succ_upper [THEN Union_least], assumption+) apply (erule ssubst) apply (rule Abrial_axiom1 [THEN equalityI]) apply (blast del: subsetI intro: subsetI TFin_UnionI TFin.succI) @@ -153,14 +153,14 @@ lemma mem_super_Ex: "c \ chain S - maxchain S ==> ? d. d \ super S c" by (unfold super_def maxchain_def) auto -lemma select_super: "c \ chain S - maxchain S ==> - (\c'. c': super S c): super S c" +lemma select_super: + "c \ chain S - maxchain S ==> (\c'. c': super S c): super S c" apply (erule mem_super_Ex [THEN exE]) apply (rule someI2, auto) done -lemma select_not_equals: "c \ chain S - maxchain S ==> - (\c'. c': super S c) \ c" +lemma select_not_equals: + "c \ chain S - maxchain S ==> (\c'. c': super S c) \ c" apply (rule notI) apply (drule select_super) apply (simp add: super_def psubset_def) @@ -186,7 +186,7 @@ done theorem Hausdorff: "\c. (c :: 'a set set): maxchain S" - apply (rule_tac x = "Union (TFin S) " in exI) + apply (rule_tac x = "Union (TFin S)" in exI) apply (rule classical) apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ") prefer 2 @@ -201,7 +201,7 @@ lemma chain_extend: "[| c \ chain S; z \ S; - \x \ c. x<=(z:: 'a set) |] ==> {z} Un c \ chain S" + \x \ c. x \ (z:: 'a set) |] ==> {z} Un c \ chain S" by (unfold chain_def) blast lemma chain_Union_upper: "[| c \ chain S; x \ c |] ==> x \ Union(c)" @@ -215,7 +215,7 @@ apply (rule ccontr) apply (simp add: maxchain_def) apply (erule conjE) - apply (subgoal_tac " ({u} Un c) \ super S c") + apply (subgoal_tac "({u} Un c) \ super S c") apply simp apply (unfold super_def psubset_def) apply (blast intro: chain_extend dest: chain_Union_upper) @@ -227,7 +227,7 @@ apply (erule exE) apply (drule subsetD, assumption) apply (drule bspec, assumption) - apply (rule_tac x = "Union (c) " in bexI) + apply (rule_tac x = "Union(c)" in bexI) apply (rule ballI, rule impI) apply (blast dest!: maxchain_Zorn, assumption) done