--- a/src/HOLCF/Bifinite.thy Mon May 11 20:09:03 2009 +0200
+++ b/src/HOLCF/Bifinite.thy Mon May 11 21:55:30 2009 -0700
@@ -104,6 +104,46 @@
apply (rule lub_mono, simp, simp, simp)
done
+subsection {* Instance for product type *}
+
+instantiation "*" :: (profinite, profinite) profinite
+begin
+
+definition approx_prod_def:
+ "approx = (\<lambda>n. \<Lambda> x. (approx n\<cdot>(fst x), approx n\<cdot>(snd x)))"
+
+instance proof
+ fix i :: nat and x :: "'a \<times> 'b"
+ show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
+ unfolding approx_prod_def by simp
+ show "(\<Squnion>i. approx i\<cdot>x) = x"
+ unfolding approx_prod_def
+ by (simp add: lub_distribs thelub_Pair)
+ show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+ unfolding approx_prod_def by simp
+ have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
+ {x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
+ unfolding approx_prod_def by clarsimp
+ thus "finite {x::'a \<times> 'b. approx i\<cdot>x = x}"
+ by (rule finite_subset,
+ intro finite_cartesian_product finite_fixes_approx)
+qed
+
+end
+
+instance "*" :: (bifinite, bifinite) bifinite ..
+
+lemma approx_Pair [simp]:
+ "approx i\<cdot>(x, y) = (approx i\<cdot>x, approx i\<cdot>y)"
+unfolding approx_prod_def by simp
+
+lemma fst_approx: "fst (approx i\<cdot>p) = approx i\<cdot>(fst p)"
+by (induct p, simp)
+
+lemma snd_approx: "snd (approx i\<cdot>p) = approx i\<cdot>(snd p)"
+by (induct p, simp)
+
+
subsection {* Instance for continuous function space *}
lemma finite_range_cfun_lemma:
--- a/src/HOLCF/Cprod.thy Mon May 11 20:09:03 2009 +0200
+++ b/src/HOLCF/Cprod.thy Mon May 11 21:55:30 2009 -0700
@@ -91,10 +91,10 @@
by (cut_tac Exh_Cprod2, auto)
lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x"
-by (simp add: cpair_eq_pair cfst_def cont_fst)
+by (simp add: cpair_eq_pair cfst_def)
lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y"
-by (simp add: cpair_eq_pair csnd_def cont_snd)
+by (simp add: cpair_eq_pair csnd_def)
lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
by (simp add: cfst_def)
@@ -108,7 +108,7 @@
lemmas surjective_pairing_Cprod2 = cpair_cfst_csnd
lemma below_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
-by (simp add: below_prod_def cfst_def csnd_def cont_fst cont_snd)
+by (simp add: below_prod_def cfst_def csnd_def)
lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
by (auto simp add: po_eq_conv below_cprod)
@@ -133,7 +133,7 @@
lemma lub_cprod2:
"chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
-apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
+apply (simp add: cpair_eq_pair cfst_def csnd_def)
apply (erule lub_cprod)
done
@@ -154,38 +154,9 @@
subsection {* Product type is a bifinite domain *}
-instantiation "*" :: (profinite, profinite) profinite
-begin
-
-definition
- approx_cprod_def:
- "approx = (\<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>)"
-
-instance proof
- fix i :: nat and x :: "'a \<times> 'b"
- show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
- unfolding approx_cprod_def by simp
- show "(\<Squnion>i. approx i\<cdot>x) = x"
- unfolding approx_cprod_def
- by (simp add: lub_distribs eta_cfun)
- show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
- unfolding approx_cprod_def csplit_def by simp
- have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
- {x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
- unfolding approx_cprod_def
- by (clarsimp simp add: pair_eq_cpair)
- thus "finite {x::'a \<times> 'b. approx i\<cdot>x = x}"
- by (rule finite_subset,
- intro finite_cartesian_product finite_fixes_approx)
-qed
-
-end
-
-instance "*" :: (bifinite, bifinite) bifinite ..
-
lemma approx_cpair [simp]:
"approx i\<cdot>\<langle>x, y\<rangle> = \<langle>approx i\<cdot>x, approx i\<cdot>y\<rangle>"
-unfolding approx_cprod_def by simp
+by (simp add: cpair_eq_pair)
lemma cfst_approx: "cfst\<cdot>(approx i\<cdot>p) = approx i\<cdot>(cfst\<cdot>p)"
by (cases p rule: cprodE, simp)
--- a/src/HOLCF/Product_Cpo.thy Mon May 11 20:09:03 2009 +0200
+++ b/src/HOLCF/Product_Cpo.thy Mon May 11 21:55:30 2009 -0700
@@ -78,6 +78,10 @@
"\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
by simp
+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 *}
lemma monofun_fst: "monofun fst"
@@ -86,28 +90,47 @@
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 = (\<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)
+ show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
+qed
+
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)"
+ "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: below_prod_def is_ub_lub)
+apply (simp add: is_ub_lub)
apply (frule ub2ub_monofun [OF monofun_fst])
apply (drule ub2ub_monofun [OF monofun_snd])
apply (simp add: below_prod_def is_lub_lub)
done
+lemma thelub_Pair:
+ "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
+ \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
+by (fast intro: thelubI is_lub_Pair elim: thelubE)
+
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)
+ from `chain S` have "chain (\<lambda>i. fst (S i))"
+ by (rule ch2ch_fst)
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)
+ from `chain S` have "chain (\<lambda>i. snd (S i))"
+ by (rule ch2ch_snd)
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))"
--- a/src/HOLCF/Sprod.thy Mon May 11 20:09:03 2009 +0200
+++ b/src/HOLCF/Sprod.thy Mon May 11 21:55:30 2009 -0700
@@ -5,7 +5,7 @@
header {* The type of strict products *}
theory Sprod
-imports Cprod
+imports Bifinite
begin
defaultsort pcpo
@@ -13,7 +13,7 @@
subsection {* Definition of strict product type *}
pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) =
- "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
+ "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
by simp_all
instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
@@ -28,23 +28,23 @@
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
lemma spair_lemma:
- "<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
+ "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
by (simp add: Sprod_def strictify_conv_if)
subsection {* Definitions of constants *}
definition
sfst :: "('a ** 'b) \<rightarrow> 'a" where
- "sfst = (\<Lambda> p. cfst\<cdot>(Rep_Sprod p))"
+ "sfst = (\<Lambda> p. fst (Rep_Sprod p))"
definition
ssnd :: "('a ** 'b) \<rightarrow> 'b" where
- "ssnd = (\<Lambda> p. csnd\<cdot>(Rep_Sprod p))"
+ "ssnd = (\<Lambda> p. snd (Rep_Sprod p))"
definition
spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
"spair = (\<Lambda> a b. Abs_Sprod
- <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>)"
+ (strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a))"
definition
ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
@@ -62,7 +62,7 @@
subsection {* Case analysis *}
lemma Rep_Sprod_spair:
- "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
+ "Rep_Sprod (:a, b:) = (strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a)"
unfolding spair_def
by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
@@ -73,7 +73,7 @@
lemma Exh_Sprod:
"z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
apply (insert Rep_Sprod [of z])
-apply (simp add: Rep_Sprod_simps eq_cprod)
+apply (simp add: Rep_Sprod_simps Pair_fst_snd_eq)
apply (simp add: Sprod_def)
apply (erule disjE, simp)
apply (simp add: strictify_conv_if)
@@ -162,7 +162,7 @@
lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
-apply (rule below_cprod)
+apply (simp only: below_prod_def)
done
lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
--- a/src/HOLCF/Ssum.thy Mon May 11 20:09:03 2009 +0200
+++ b/src/HOLCF/Ssum.thy Mon May 11 21:55:30 2009 -0700
@@ -5,7 +5,7 @@
header {* The type of strict sums *}
theory Ssum
-imports Cprod Tr
+imports Tr
begin
defaultsort pcpo
@@ -14,8 +14,8 @@
pcpodef (Ssum) ('a, 'b) "++" (infixr "++" 10) =
"{p :: tr \<times> ('a \<times> 'b).
- (cfst\<cdot>p \<sqsubseteq> TT \<longleftrightarrow> csnd\<cdot>(csnd\<cdot>p) = \<bottom>) \<and>
- (cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
+ (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
+ (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
by simp_all
instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
@@ -33,28 +33,28 @@
definition
sinl :: "'a \<rightarrow> ('a ++ 'b)" where
- "sinl = (\<Lambda> a. Abs_Ssum <strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>>)"
+ "sinl = (\<Lambda> a. Abs_Ssum (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>))"
definition
sinr :: "'b \<rightarrow> ('a ++ 'b)" where
- "sinr = (\<Lambda> b. Abs_Ssum <strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b>)"
+ "sinr = (\<Lambda> b. Abs_Ssum (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b))"
-lemma sinl_Ssum: "<strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>> \<in> Ssum"
+lemma sinl_Ssum: "(strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>) \<in> Ssum"
by (simp add: Ssum_def strictify_conv_if)
-lemma sinr_Ssum: "<strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b> \<in> Ssum"
+lemma sinr_Ssum: "(strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b) \<in> Ssum"
by (simp add: Ssum_def strictify_conv_if)
-lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum <strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>>"
+lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>)"
by (unfold sinl_def, simp add: cont_Abs_Ssum sinl_Ssum)
-lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum <strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b>"
+lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"
by (unfold sinr_def, simp add: cont_Abs_Ssum sinr_Ssum)
-lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = <strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>>"
+lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>)"
by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum)
-lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b>"
+lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"
by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
subsection {* Properties of @{term sinl} and @{term sinr} *}
@@ -139,12 +139,11 @@
lemma Exh_Ssum:
"z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)"
-apply (rule_tac x=z in Abs_Ssum_induct)
-apply (rule_tac p=y in cprodE, rename_tac t x)
-apply (rule_tac p=x in cprodE, rename_tac a b)
-apply (rule_tac p=t in trE)
+apply (induct z rule: Abs_Ssum_induct)
+apply (case_tac y, rename_tac t a b)
+apply (case_tac t rule: trE)
apply (rule disjI1)
-apply (simp add: Ssum_def cpair_strict Abs_Ssum_strict)
+apply (simp add: Ssum_def Abs_Ssum_strict)
apply (rule disjI2, rule disjI1, rule_tac x=a in exI)
apply (simp add: sinl_Abs_Ssum Ssum_def)
apply (rule disjI2, rule disjI2, rule_tac x=b in exI)
@@ -177,7 +176,7 @@
definition
sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
- "sscase = (\<Lambda> f g s. (\<Lambda><t, x, y>. If t then f\<cdot>x else g\<cdot>y fi)\<cdot>(Rep_Ssum s))"
+ "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_Ssum s))"
translations
"case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
@@ -187,8 +186,8 @@
"\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
lemma beta_sscase:
- "sscase\<cdot>f\<cdot>g\<cdot>s = (\<Lambda><t, x, y>. If t then f\<cdot>x else g\<cdot>y fi)\<cdot>(Rep_Ssum s)"
-unfolding sscase_def by (simp add: cont_Rep_Ssum cont2cont_LAM)
+ "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_Ssum s)"
+unfolding sscase_def by (simp add: cont_Rep_Ssum [THEN cont_compose])
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
unfolding beta_sscase by (simp add: Rep_Ssum_strict)
@@ -206,9 +205,9 @@
instance "++" :: (flat, flat) flat
apply (intro_classes, clarify)
-apply (rule_tac p=x in ssumE, simp)
-apply (rule_tac p=y in ssumE, simp_all add: flat_below_iff)
-apply (rule_tac p=y in ssumE, simp_all add: flat_below_iff)
+apply (case_tac x, simp)
+apply (case_tac y, simp_all add: flat_below_iff)
+apply (case_tac y, simp_all add: flat_below_iff)
done
subsection {* Strict sum is a bifinite domain *}