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"`