--- a/src/HOLCF/Cprod.thy Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/Cprod.thy Wed Jan 14 17:11:29 2009 -0800
@@ -12,23 +12,6 @@
subsection {* Type @{typ unit} is a pcpo *}
-instantiation unit :: sq_ord
-begin
-
-definition
- less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
-
-instance ..
-end
-
-instance unit :: discrete_cpo
-by intro_classes simp
-
-instance unit :: finite_po ..
-
-instance unit :: pcpo
-by intro_classes simp
-
definition
unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
"unit_when = (\<Lambda> a _. a)"
@@ -39,165 +22,6 @@
lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
by (simp add: unit_when_def)
-
-subsection {* Product type is a partial order *}
-
-instantiation "*" :: (sq_ord, sq_ord) sq_ord
-begin
-
-definition
- less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
-
-instance ..
-end
-
-instance "*" :: (po, po) po
-proof
- fix x :: "'a \<times> 'b"
- show "x \<sqsubseteq> x"
- unfolding less_cprod_def by simp
-next
- fix x y :: "'a \<times> 'b"
- assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
- unfolding less_cprod_def Pair_fst_snd_eq
- by (fast intro: antisym_less)
-next
- fix x y z :: "'a \<times> 'b"
- assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- unfolding less_cprod_def
- by (fast intro: trans_less)
-qed
-
-subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-
-lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
-unfolding less_cprod_def by simp
-
-lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) = (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"
-unfolding less_cprod_def by simp
-
-text {* Pair @{text "(_,_)"} is monotone in both arguments *}
-
-lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
-by (simp add: monofun_def)
-
-lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
-by (simp add: monofun_def)
-
-lemma monofun_pair:
- "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
-by simp
-
-text {* @{term fst} and @{term snd} are monotone *}
-
-lemma monofun_fst: "monofun fst"
-by (simp add: monofun_def less_cprod_def)
-
-lemma monofun_snd: "monofun snd"
-by (simp add: monofun_def less_cprod_def)
-
-subsection {* Product type is a cpo *}
-
-lemma is_lub_Pair:
- "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
-apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: less_cprod_def is_ub_lub)
-apply (frule ub2ub_monofun [OF monofun_fst])
-apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: less_cprod_def is_lub_lub)
-done
-
-lemma lub_cprod:
- fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
- assumes S: "chain S"
- shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-proof -
- have "chain (\<lambda>i. fst (S i))"
- using monofun_fst S by (rule ch2ch_monofun)
- hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
- by (rule cpo_lubI)
- have "chain (\<lambda>i. snd (S i))"
- using monofun_snd S by (rule ch2ch_monofun)
- hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
- by (rule cpo_lubI)
- show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
- using is_lub_Pair [OF 1 2] by simp
-qed
-
-lemma thelub_cprod:
- "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
- \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-by (rule lub_cprod [THEN thelubI])
-
-instance "*" :: (cpo, cpo) cpo
-proof
- fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
- assume "chain S"
- hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
- by (rule lub_cprod)
- thus "\<exists>x. range S <<| x" ..
-qed
-
-instance "*" :: (finite_po, finite_po) finite_po ..
-
-instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
-proof
- fix x y :: "'a \<times> 'b"
- show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
- unfolding less_cprod_def Pair_fst_snd_eq
- by simp
-qed
-
-subsection {* Product type is pointed *}
-
-lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
-by (simp add: less_cprod_def)
-
-instance "*" :: (pcpo, pcpo) pcpo
-by intro_classes (fast intro: minimal_cprod)
-
-lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_cprod [THEN UU_I, symmetric])
-
-
-subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-
-lemma cont_pair1: "cont (\<lambda>x. (x, y))"
-apply (rule contI)
-apply (rule is_lub_Pair)
-apply (erule cpo_lubI)
-apply (rule lub_const)
-done
-
-lemma cont_pair2: "cont (\<lambda>y. (x, y))"
-apply (rule contI)
-apply (rule is_lub_Pair)
-apply (rule lub_const)
-apply (erule cpo_lubI)
-done
-
-lemma contlub_fst: "contlub fst"
-apply (rule contlubI)
-apply (simp add: thelub_cprod)
-done
-
-lemma contlub_snd: "contlub snd"
-apply (rule contlubI)
-apply (simp add: thelub_cprod)
-done
-
-lemma cont_fst: "cont fst"
-apply (rule monocontlub2cont)
-apply (rule monofun_fst)
-apply (rule contlub_fst)
-done
-
-lemma cont_snd: "cont snd"
-apply (rule monocontlub2cont)
-apply (rule monofun_snd)
-apply (rule contlub_snd)
-done
-
subsection {* Continuous versions of constants *}
definition