# Theory Product_Cpo

Up to index of Isabelle/HOL/HOLCF

theory Product_Cpo
(*  Title:      HOL/HOLCF/Product_Cpo.thy    Author:     Franz Regensburger*)header {* The cpo of cartesian products *}theory Product_Cpoimports Admbegindefault_sort cposubsection {* Unit type is a pcpo *}instantiation unit :: discrete_cpobegindefinition  below_unit_def [simp]: "x \<sqsubseteq> (y::unit) <-> True"instance proofqed simpendinstance unit :: pcpoby intro_classes simpsubsection {* Product type is a partial order *}instantiation prod :: (below, below) belowbegindefinition  below_prod_def: "(op \<sqsubseteq>) ≡ λp1 p2. (fst p1 \<sqsubseteq> fst p2 ∧ snd p1 \<sqsubseteq> snd p2)"instance ..endinstance prod :: (po, po) poproof  fix x :: "'a × 'b"  show "x \<sqsubseteq> x"    unfolding below_prod_def by simpnext  fix x y :: "'a × 'b"  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"    unfolding below_prod_def prod_eq_iff    by (fast intro: below_antisym)next  fix x y z :: "'a × 'b"  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"    unfolding below_prod_def    by (fast intro: below_trans)qedsubsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}lemma prod_belowI: "[|fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q|] ==> p \<sqsubseteq> q"unfolding below_prod_def by simplemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) <-> a \<sqsubseteq> c ∧ b \<sqsubseteq> d"unfolding below_prod_def by simptext {* Pair @{text "(_,_)"}  is monotone in both arguments *}lemma monofun_pair1: "monofun (λx. (x, y))"by (simp add: monofun_def)lemma monofun_pair2: "monofun (λy. (x, y))"by (simp add: monofun_def)lemma monofun_pair:  "[|x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2|] ==> (x1, y1) \<sqsubseteq> (x2, y2)"by simplemma ch2ch_Pair [simp]:  "chain X ==> chain Y ==> chain (λi. (X i, Y i))"by (rule chainI, simp add: chainE)text {* @{term fst} and @{term snd} are monotone *}lemma fst_monofun: "x \<sqsubseteq> y ==> fst x \<sqsubseteq> fst y"unfolding below_prod_def by simplemma snd_monofun: "x \<sqsubseteq> y ==> snd x \<sqsubseteq> snd y"unfolding below_prod_def by simplemma monofun_fst: "monofun fst"by (simp add: monofun_def below_prod_def)lemma monofun_snd: "monofun snd"by (simp add: monofun_def below_prod_def)lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]lemma prod_chain_cases:  assumes "chain Y"  obtains A B  where "chain A" and "chain B" and "Y = (λi. (A i, B i))"proof  from chain Y show "chain (λi. fst (Y i))" by (rule ch2ch_fst)  from chain Y show "chain (λi. snd (Y i))" by (rule ch2ch_snd)  show "Y = (λi. (fst (Y i), snd (Y i)))" by simpqedsubsection {* Product type is a cpo *}lemma is_lub_Pair:  "[|range A <<| x; range B <<| y|] ==> range (λi. (A i, B i)) <<| (x, y)"unfolding is_lub_def is_ub_def ball_simps below_prod_def by simplemma lub_Pair:  "[|chain (A::nat => 'a::cpo); chain (B::nat => 'b::cpo)|]    ==> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"by (fast intro: lub_eqI is_lub_Pair elim: thelubE)lemma is_lub_prod:  fixes S :: "nat => ('a::cpo × 'b::cpo)"  assumes S: "chain S"  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)lemma lub_prod:  "chain (S::nat => 'a::cpo × 'b::cpo)    ==> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"by (rule is_lub_prod [THEN lub_eqI])instance prod :: (cpo, cpo) cpoproof  fix S :: "nat => ('a × 'b)"  assume "chain S"  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"    by (rule is_lub_prod)  thus "∃x. range S <<| x" ..qedinstance prod :: (discrete_cpo, discrete_cpo) discrete_cpoproof  fix x y :: "'a × 'b"  show "x \<sqsubseteq> y <-> x = y"    unfolding below_prod_def prod_eq_iff    by simpqedsubsection {* Product type is pointed *}lemma minimal_prod: "(⊥, ⊥) \<sqsubseteq> p"by (simp add: below_prod_def)instance prod :: (pcpo, pcpo) pcpoby intro_classes (fast intro: minimal_prod)lemma inst_prod_pcpo: "⊥ = (⊥, ⊥)"by (rule minimal_prod [THEN bottomI, symmetric])lemma Pair_bottom_iff [simp]: "(x, y) = ⊥ <-> x = ⊥ ∧ y = ⊥"unfolding inst_prod_pcpo by simplemma fst_strict [simp]: "fst ⊥ = ⊥"unfolding inst_prod_pcpo by (rule fst_conv)lemma snd_strict [simp]: "snd ⊥ = ⊥"unfolding inst_prod_pcpo by (rule snd_conv)lemma Pair_strict [simp]: "(⊥, ⊥) = ⊥"by simplemma split_strict [simp]: "split f ⊥ = f ⊥ ⊥"unfolding split_def by simpsubsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}lemma cont_pair1: "cont (λx. (x, y))"apply (rule contI)apply (rule is_lub_Pair)apply (erule cpo_lubI)apply (rule is_lub_const)donelemma cont_pair2: "cont (λy. (x, y))"apply (rule contI)apply (rule is_lub_Pair)apply (rule is_lub_const)apply (erule cpo_lubI)donelemma cont_fst: "cont fst"apply (rule contI)apply (simp add: lub_prod)apply (erule cpo_lubI [OF ch2ch_fst])donelemma cont_snd: "cont snd"apply (rule contI)apply (simp add: lub_prod)apply (erule cpo_lubI [OF ch2ch_snd])donelemma cont2cont_Pair [simp, cont2cont]:  assumes f: "cont (λx. f x)"  assumes g: "cont (λx. g x)"  shows "cont (λx. (f x, g x))"apply (rule cont_apply [OF f cont_pair1])apply (rule cont_apply [OF g cont_pair2])apply (rule cont_const)donelemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]lemma cont2cont_prod_case:  assumes f1: "!!a b. cont (λx. f x a b)"  assumes f2: "!!x b. cont (λa. f x a b)"  assumes f3: "!!x a. cont (λb. f x a b)"  assumes g: "cont (λx. g x)"  shows "cont (λx. case g x of (a, b) => f x a b)"unfolding split_defapply (rule cont_apply [OF g])apply (rule cont_apply [OF cont_fst f2])apply (rule cont_apply [OF cont_snd f3])apply (rule cont_const)apply (rule f1)donelemma prod_contI:  assumes f1: "!!y. cont (λx. f (x, y))"  assumes f2: "!!x. cont (λy. f (x, y))"  shows "cont f"proof -  have "cont (λ(x, y). f (x, y))"    by (intro cont2cont_prod_case f1 f2 cont2cont)  thus "cont f"    by (simp only: split_eta)qedlemma prod_cont_iff:  "cont f <-> (∀y. cont (λx. f (x, y))) ∧ (∀x. cont (λy. f (x, y)))"apply safeapply (erule cont_compose [OF _ cont_pair1])apply (erule cont_compose [OF _ cont_pair2])apply (simp only: prod_contI)donelemma cont2cont_prod_case' [simp, cont2cont]:  assumes f: "cont (λp. f (fst p) (fst (snd p)) (snd (snd p)))"  assumes g: "cont (λx. g x)"  shows "cont (λx. prod_case (f x) (g x))"using assms by (simp add: cont2cont_prod_case prod_cont_iff)text {* The simple version (due to Joachim Breitner) is needed if  either element type of the pair is not a cpo. *}lemma cont2cont_split_simple [simp, cont2cont]: assumes "!!a b. cont (λx. f x a b)" shows "cont (λx. case p of (a, b) => f x a b)"using assms by (cases p) autotext {* Admissibility of predicates on product types. *}lemma adm_prod_case [simp]:  assumes "adm (λx. P x (fst (f x)) (snd (f x)))"  shows "adm (λx. case f x of (a, b) => P x a b)"unfolding prod_case_beta using assms .subsection {* Compactness and chain-finiteness *}lemma fst_below_iff: "fst (x::'a × 'b) \<sqsubseteq> y <-> x \<sqsubseteq> (y, snd x)"unfolding below_prod_def by simplemma snd_below_iff: "snd (x::'a × 'b) \<sqsubseteq> y <-> x \<sqsubseteq> (fst x, y)"unfolding below_prod_def by simplemma compact_fst: "compact x ==> compact (fst x)"by (rule compactI, simp add: fst_below_iff)lemma compact_snd: "compact x ==> compact (snd x)"by (rule compactI, simp add: snd_below_iff)lemma compact_Pair: "[|compact x; compact y|] ==> compact (x, y)"by (rule compactI, simp add: below_prod_def)lemma compact_Pair_iff [simp]: "compact (x, y) <-> compact x ∧ compact y"apply (safe intro!: compact_Pair)apply (drule compact_fst, simp)apply (drule compact_snd, simp)doneinstance prod :: (chfin, chfin) chfinapply intro_classesapply (erule compact_imp_max_in_chain)apply (case_tac "\<Squnion>i. Y i", simp)doneend