src/HOL/HOLCF/Product_Cpo.thy

 (*  Title:      HOL/HOLCF/Product_Cpo.thy
     Author:     Franz Regensburger
 *)
 
-section {* The cpo of cartesian products *}
+section \<open>The cpo of cartesian products\<close>
 
 theory Product_Cpo
 imports Adm
 begin
 
 default_sort cpo
 
-subsection {* Unit type is a pcpo *}
+subsection \<open>Unit type is a pcpo\<close>
 
 instantiation unit :: discrete_cpo
 begin
 
 definition

 
 instance unit :: pcpo
 by intro_classes simp
 
 
-subsection {* Product type is a partial order *}
+subsection \<open>Product type is a partial order\<close>
 
 instantiation prod :: (below, below) below
 begin
 
 definition

   assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
     unfolding below_prod_def
     by (fast intro: below_trans)
 qed
 
-subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
+subsection \<open>Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
 
 lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
 unfolding below_prod_def by simp
 
 lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
 unfolding below_prod_def by simp
 
-text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
+text \<open>Pair \<open>(_,_)\<close>  is monotone in both arguments\<close>
 
 lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
 by (simp add: monofun_def)
 
 lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"

 
 lemma ch2ch_Pair [simp]:
   "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
 by (rule chainI, simp add: chainE)
 
-text {* @{term fst} and @{term snd} are monotone *}
+text \<open>@{term fst} and @{term snd} are monotone\<close>
 
 lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
 unfolding below_prod_def by simp
 
 lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y"

 lemma prod_chain_cases:
   assumes "chain Y"
   obtains A B
   where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
 proof
-  from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
-  from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
+  from \<open>chain Y\<close> show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
+  from \<open>chain Y\<close> show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
   show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
 qed
 
-subsection {* Product type is a cpo *}
+subsection \<open>Product type is a cpo\<close>
 
 lemma is_lub_Pair:
   "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
 unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
 

   show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
     unfolding below_prod_def prod_eq_iff
     by simp
 qed
 
-subsection {* Product type is pointed *}
+subsection \<open>Product type is pointed\<close>
 
 lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
 by (simp add: below_prod_def)
 
 instance prod :: (pcpo, pcpo) pcpo

 by simp
 
 lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>"
 unfolding split_def by simp
 
-subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
+subsection \<open>Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
 
 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
 apply (rule contI)
 apply (rule is_lub_Pair)
 apply (erule cpo_lubI)

   assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
   assumes g: "cont (\<lambda>x. g x)"
   shows "cont (\<lambda>x. case_prod (f x) (g x))"
 using assms by (simp add: cont2cont_case_prod prod_cont_iff)
 
-text {* The simple version (due to Joachim Breitner) is needed if
-  either element type of the pair is not a cpo. *}
+text \<open>The simple version (due to Joachim Breitner) is needed if
+  either element type of the pair is not a cpo.\<close>
 
 lemma cont2cont_split_simple [simp, cont2cont]:
  assumes "\<And>a b. cont (\<lambda>x. f x a b)"
  shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
 using assms by (cases p) auto
 
-text {* Admissibility of predicates on product types. *}
+text \<open>Admissibility of predicates on product types.\<close>
 
 lemma adm_case_prod [simp]:
   assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
   shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
 unfolding case_prod_beta using assms .
 
-subsection {* Compactness and chain-finiteness *}
+subsection \<open>Compactness and chain-finiteness\<close>
 
 lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
 unfolding below_prod_def by simp
 
 lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"