src/HOL/Library/Complete_Partial_Order2.thy
changeset 63243 1bc6816fd525
parent 63170 eae6549dbea2
child 63343 fb5d8a50c641
equal deleted inserted replaced
63241:f59fd6cc935e 63243:1bc6816fd525
  1699 lemma mcont2mcont_snd [cont_intro, simp]:
  1699 lemma mcont2mcont_snd [cont_intro, simp]:
  1700   "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
  1700   "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
  1701   \<Longrightarrow> mcont lub ord lubb ordb (\<lambda>x. snd (t x))"
  1701   \<Longrightarrow> mcont lub ord lubb ordb (\<lambda>x. snd (t x))"
  1702 by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
  1702 by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
  1703 
  1703 
       
  1704 lemma monotone_Pair:
       
  1705   "\<lbrakk> monotone ord orda f; monotone ord ordb g \<rbrakk>
       
  1706   \<Longrightarrow> monotone ord (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
       
  1707 by(simp add: monotone_def)
       
  1708 
       
  1709 lemma cont_Pair:
       
  1710   "\<lbrakk> cont lub ord luba orda f; cont lub ord lubb ordb g \<rbrakk>
       
  1711   \<Longrightarrow> cont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
       
  1712 by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
       
  1713 
       
  1714 lemma mcont_Pair:
       
  1715   "\<lbrakk> mcont lub ord luba orda f; mcont lub ord lubb ordb g \<rbrakk>
       
  1716   \<Longrightarrow> mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
       
  1717 by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
       
  1718 
  1704 context partial_function_definitions begin
  1719 context partial_function_definitions begin
  1705 text \<open>Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\<close>
  1720 text \<open>Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\<close>
  1706 lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
  1721 lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
  1707 lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
  1722 lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
  1708 end
  1723 end
  1709 
  1724 
  1710 end
  1725 lemma map_option_mono [partial_function_mono]:
       
  1726   "mono_option B \<Longrightarrow> mono_option (\<lambda>f. map_option g (B f))"
       
  1727 unfolding map_conv_bind_option by(rule bind_mono) simp_all
       
  1728 
       
  1729 lemma compact_flat_lub [cont_intro]: "compact (flat_lub x) (flat_ord x) y"
       
  1730 using flat_interpretation[THEN ccpo]
       
  1731 proof(rule ccpo.compactI[OF _ ccpo.admissibleI])
       
  1732   fix A
       
  1733   assume chain: "Complete_Partial_Order.chain (flat_ord x) A"
       
  1734     and A: "A \<noteq> {}"
       
  1735     and *: "\<forall>z\<in>A. \<not> flat_ord x y z"
       
  1736   from A obtain z where "z \<in> A" by blast
       
  1737   with * have z: "\<not> flat_ord x y z" ..
       
  1738   hence y: "x \<noteq> y" "y \<noteq> z" by(auto simp add: flat_ord_def)
       
  1739   { assume "\<not> A \<subseteq> {x}"
       
  1740     then obtain z' where "z' \<in> A" "z' \<noteq> x" by auto
       
  1741     then have "(THE z. z \<in> A - {x}) = z'"
       
  1742       by(intro the_equality)(auto dest: chainD[OF chain] simp add: flat_ord_def)
       
  1743     moreover have "z' \<noteq> y" using \<open>z' \<in> A\<close> * by(auto simp add: flat_ord_def)
       
  1744     ultimately have "y \<noteq> (THE z. z \<in> A - {x})" by simp }
       
  1745   with z show "\<not> flat_ord x y (flat_lub x A)" by(simp add: flat_ord_def flat_lub_def)
       
  1746 qed
       
  1747 
       
  1748 end