src/HOL/Library/Zorn.thy
changeset 53374 a14d2a854c02
parent 52821 05eb2d77b195
child 54482 a2874c8b3558
equal deleted 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"