src/HOL/Library/Zorn.thy
 changeset 53374 a14d2a854c02 parent 52821 05eb2d77b195 child 54482 a2874c8b3558
equal inserted replaced
53373:3ca9e79ac926 53374:a14d2a854c02
117      (force simp: suc_def dest: not_maxchain_Some)+
117      (force simp: suc_def dest: not_maxchain_Some)+
118
118
119 lemma chain_sucD:
119 lemma chain_sucD:
120   assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)"
120   assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)"
121 proof -
121 proof -
122   from `chain X` have "chain (suc X)" by (rule chain_suc)
122   from `chain X` have *: "chain (suc X)" by (rule chain_suc)
123   moreover then have "suc X \<subseteq> A" unfolding chain_def by blast
123   then have "suc X \<subseteq> A" unfolding chain_def by blast
124   ultimately show ?thesis by blast
124   with * show ?thesis by blast
125 qed
125 qed
126
126
127 lemma suc_Union_closed_total':
127 lemma suc_Union_closed_total':
128   assumes "X \<in> \<C>" and "Y \<in> \<C>"
128   assumes "X \<in> \<C>" and "Y \<in> \<C>"
129     and *: "\<And>Z. Z \<in> \<C> \<Longrightarrow> Z \<subseteq> Y \<Longrightarrow> Z = Y \<or> suc Z \<subseteq> Y"
129     and *: "\<And>Z. Z \<in> \<C> \<Longrightarrow> Z \<subseteq> Y \<Longrightarrow> Z = Y \<or> suc Z \<subseteq> Y"
346     and *: "\<And>S. subset.chain A S \<Longrightarrow> \<not> C \<subset> S"
346     and *: "\<And>S. subset.chain A S \<Longrightarrow> \<not> C \<subset> S"
347     by (auto simp: subset.maxchain_def)
347     by (auto simp: subset.maxchain_def)
348   moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto
348   moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto
349   ultimately have "subset.chain A ?C"
349   ultimately have "subset.chain A ?C"
350     using subset.chain_extend [of A C X] and `X \<in> A` by auto
350     using subset.chain_extend [of A C X] and `X \<in> A` by auto
351   moreover assume "\<Union>C \<noteq> X"
351   moreover assume **: "\<Union>C \<noteq> X"
352   moreover then have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
352   moreover from ** have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
353   ultimately show False using * by blast
353   ultimately show False using * by blast
354 qed
354 qed
355
355
356 subsubsection {* Zorn's lemma *}
356 subsubsection {* Zorn's lemma *}
357
357
576   { fix i have "(f (Suc i), f i) \<in> r"
576   { fix i have "(f (Suc i), f i) \<in> r"
577     proof (induct i)
577     proof (induct i)
578       case 0 show ?case by fact
578       case 0 show ?case by fact
579     next
579     next
580       case (Suc i)
580       case (Suc i)
581       moreover obtain s where "s \<in> R" and "(f (Suc (Suc i)), f(Suc i)) \<in> s"
581       then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
582         using 1 by auto
582         using 1 by auto
583       moreover hence "s initial_segment_of r \<or> r initial_segment_of s"
583       then have "s initial_segment_of r \<or> r initial_segment_of s"
584         using assms(1) `r \<in> R` by (simp add: Chains_def)
584         using assms(1) `r \<in> R` by (simp add: Chains_def)
585       ultimately show ?case by (simp add: init_seg_of_def) blast
585       with Suc s show ?case by (simp add: init_seg_of_def) blast
586     qed
586     qed
587   }
587   }
588   thus False using assms(2) and `r \<in> R`
588   thus False using assms(2) and `r \<in> R`
589     by (simp add: wf_iff_no_infinite_down_chain) blast
589     by (simp add: wf_iff_no_infinite_down_chain) blast
590 qed
590 qed
680         wf_subset [OF `wf ?s` Diff_subset]
680         wf_subset [OF `wf ?s` Diff_subset]
681         by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
681         by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
682     qed
682     qed
683     ultimately have "Well_order ?m" by (simp add: order_on_defs)
683     ultimately have "Well_order ?m" by (simp add: order_on_defs)
684 --{*We show that the extension is above m*}
684 --{*We show that the extension is above m*}
685     moreover hence "(m, ?m) \<in> I" using `Well_order m` and `x \<notin> Field m`
685     moreover have "(m, ?m) \<in> I" using `Well_order ?m` and `Well_order m` and `x \<notin> Field m`
686       by (fastforce simp: I_def init_seg_of_def Field_def)
686       by (fastforce simp: I_def init_seg_of_def Field_def)
687     ultimately
687     ultimately
688 --{*This contradicts maximality of m:*}
688 --{*This contradicts maximality of m:*}
689     have False using max and `x \<notin> Field m` unfolding Field_def by blast
689     have False using max and `x \<notin> Field m` unfolding Field_def by blast
690   }
690   }
691   hence "Field m = UNIV" by auto
691   hence "Field m = UNIV" by auto
692   moreover with `Well_order m` have "Well_order m" by simp
692   with `Well_order m` show ?thesis by blast
693   ultimately show ?thesis by blast

694 qed
693 qed
695
694
696 corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"
695 corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"
697 proof -
696 proof -
698   obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"
697   obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"