--- a/src/HOLCF/Cfun.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Cfun.thy Fri Jan 04 00:01:02 2008 +0100
@@ -103,6 +103,12 @@
lemma UU_CFun: "\<bottom> \<in> CFun"
by (simp add: CFun_def inst_fun_pcpo cont_const)
+instance "->" :: (finite_po, finite_po) finite_po
+by (rule typedef_finite_po [OF type_definition_CFun])
+
+instance "->" :: (finite_po, chfin) chfin
+by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
+
instance "->" :: (cpo, pcpo) pcpo
by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
--- a/src/HOLCF/Cprod.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Cprod.thy Fri Jan 04 00:01:02 2008 +0100
@@ -161,6 +161,31 @@
thus "\<exists>x. S <<| x" ..
qed
+instance "*" :: (finite_po, finite_po) finite_po ..
+
+instance "*" :: (chfin, chfin) chfin
+proof (intro_classes, clarify)
+ fix Y :: "nat \<Rightarrow> 'a \<times> 'b"
+ assume Y: "chain Y"
+ from Y have "chain (\<lambda>i. fst (Y i))"
+ by (rule ch2ch_monofun [OF monofun_fst])
+ hence "\<exists>m. max_in_chain m (\<lambda>i. fst (Y i))"
+ by (rule chfin [rule_format])
+ then obtain m where m: "max_in_chain m (\<lambda>i. fst (Y i))" ..
+ from Y have "chain (\<lambda>i. snd (Y i))"
+ by (rule ch2ch_monofun [OF monofun_snd])
+ hence "\<exists>n. max_in_chain n (\<lambda>i. snd (Y i))"
+ by (rule chfin [rule_format])
+ then obtain n where n: "max_in_chain n (\<lambda>i. snd (Y i))" ..
+ from m have m': "max_in_chain (max m n) (\<lambda>i. fst (Y i))"
+ by (rule maxinch_mono [OF _ le_maxI1])
+ from n have n': "max_in_chain (max m n) (\<lambda>i. snd (Y i))"
+ by (rule maxinch_mono [OF _ le_maxI2])
+ from m' n' have "max_in_chain (max m n) Y"
+ unfolding max_in_chain_def Pair_fst_snd_eq by fast
+ thus "\<exists>n. max_in_chain n Y" ..
+qed
+
subsection {* Product type is pointed *}
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
--- a/src/HOLCF/Discrete.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Discrete.thy Fri Jan 04 00:01:02 2008 +0100
@@ -72,6 +72,22 @@
thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
qed
+instance discr :: (finite) finite_po
+proof
+ have "finite (Discr ` (UNIV :: 'a set))"
+ by (rule finite_imageI [OF finite])
+ also have "(Discr ` (UNIV :: 'a set)) = UNIV"
+ by (auto, case_tac x, auto)
+ finally show "finite (UNIV :: 'a discr set)" .
+qed
+
+instance discr :: (type) chfin
+apply (intro_classes, clarify)
+apply (rule_tac x=0 in exI)
+apply (unfold max_in_chain_def)
+apply (clarify, erule discr_chain0 [symmetric])
+done
+
subsection {* @{term undiscr} *}
definition
@@ -85,9 +101,9 @@
"!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
by (fast dest: discr_chain0 elim: arg_cong)
-lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
-apply (unfold cont_def is_lub_def is_ub_def)
-apply (simp add: discr_chain_f_range0)
+lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
+apply (rule chfindom_monofun2cont)
+apply (rule monofunI, simp)
done
end
--- a/src/HOLCF/Ffun.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Ffun.thy Fri Jan 04 00:01:02 2008 +0100
@@ -62,7 +62,6 @@
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
by (simp add: chain_def less_fun_def)
-
text {* upper bounds of function chains yield upper bound in the po range *}
lemma ub2ub_fun:
@@ -125,6 +124,46 @@
instance "fun" :: (type, dcpo) dcpo
by intro_classes (rule dcpo_fun)
+instance "fun" :: (finite, finite_po) finite_po ..
+
+text {* chain-finite function spaces *}
+
+lemma maxinch2maxinch_lambda:
+ "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
+unfolding max_in_chain_def expand_fun_eq by simp
+
+lemma maxinch_mono:
+ "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
+unfolding max_in_chain_def
+proof (intro allI impI)
+ fix k
+ assume Y: "\<forall>n\<ge>i. Y i = Y n"
+ assume ij: "i \<le> j"
+ assume jk: "j \<le> k"
+ from ij jk have ik: "i \<le> k" by simp
+ from Y ij have Yij: "Y i = Y j" by simp
+ from Y ik have Yik: "Y i = Y k" by simp
+ from Yij Yik show "Y j = Y k" by auto
+qed
+
+instance "fun" :: (finite, chfin) chfin
+proof (intro_classes, clarify)
+ fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
+ let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
+ assume "chain Y"
+ hence "\<And>x. chain (\<lambda>i. Y i x)"
+ by (rule ch2ch_fun)
+ hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
+ by (rule chfin [rule_format])
+ hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
+ by (rule LeastI_ex)
+ hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
+ by (rule maxinch_mono [OF _ Max_ge], simp_all)
+ hence "max_in_chain (Max (range ?n)) Y"
+ by (rule maxinch2maxinch_lambda)
+ thus "\<exists>n. max_in_chain n Y" ..
+qed
+
subsection {* Full function space is pointed *}
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
--- a/src/HOLCF/Lift.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Lift.thy Fri Jan 04 00:01:02 2008 +0100
@@ -14,6 +14,9 @@
pcpodef 'a lift = "UNIV :: 'a discr u set"
by simp
+instance lift :: (finite) finite_po
+by (rule typedef_finite_po [OF type_definition_lift])
+
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
definition
--- a/src/HOLCF/Pcpodef.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy Fri Jan 04 00:01:02 2008 +0100
@@ -30,6 +30,41 @@
done
+subsection {* Proving a subtype is finite *}
+
+context type_definition
+begin
+
+lemma Abs_image:
+ shows "Abs ` A = UNIV"
+proof
+ show "Abs ` A <= UNIV" by simp
+ show "UNIV <= Abs ` A"
+ proof
+ fix x
+ have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
+ thus "x : Abs ` A" using Rep by (rule image_eqI)
+ qed
+qed
+
+lemma finite_UNIV: "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
+proof -
+ assume "finite A"
+ hence "finite (Abs ` A)" by (rule finite_imageI)
+ thus "finite (UNIV :: 'b set)" by (simp only: Abs_image)
+qed
+
+end
+
+theorem typedef_finite_po:
+ fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po"
+ assumes type: "type_definition Rep Abs A"
+ shows "OFCLASS('b, finite_po_class)"
+ apply (intro_classes)
+ apply (rule type_definition.finite_UNIV [OF type])
+ apply (rule finite)
+done
+
subsection {* Proving a subtype is chain-finite *}
lemma monofun_Rep:
--- a/src/HOLCF/Sprod.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Sprod.thy Fri Jan 04 00:01:02 2008 +0100
@@ -19,6 +19,12 @@
"{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
by simp
+instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+by (rule typedef_finite_po [OF type_definition_Sprod])
+
+instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+by (rule typedef_chfin [OF type_definition_Sprod less_Sprod_def])
+
syntax (xsymbols)
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
syntax (HTML output)
@@ -174,7 +180,6 @@
apply (simp add: less_sprod)
done
-
subsection {* Properties of @{term ssplit} *}
lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
@@ -186,4 +191,13 @@
lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"
by (cases z, simp_all)
+subsection {* Strict product preserves flatness *}
+
+instance "**" :: (flat, flat) flat
+apply (intro_classes, clarify)
+apply (rule_tac p=x in sprodE, simp)
+apply (rule_tac p=y in sprodE, simp)
+apply (simp add: flat_less_iff spair_less)
+done
+
end
--- a/src/HOLCF/Ssum.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Ssum.thy Fri Jan 04 00:01:02 2008 +0100
@@ -21,6 +21,12 @@
(cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
by simp
+instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+by (rule typedef_finite_po [OF type_definition_Ssum])
+
+instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+by (rule typedef_chfin [OF type_definition_Ssum less_Ssum_def])
+
syntax (xsymbols)
"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
syntax (HTML output)
@@ -186,4 +192,18 @@
lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
by (cases z, simp_all)
+subsection {* Strict sum preserves flatness *}
+
+lemma flat_less_iff:
+ fixes x y :: "'a::flat"
+ shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
+by (safe dest!: ax_flat [rule_format])
+
+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_less_iff)
+apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
+done
+
end
--- a/src/HOLCF/Up.thy Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Up.thy Fri Jan 04 00:01:02 2008 +0100
@@ -68,6 +68,13 @@
by (auto split: u.split_asm intro: trans_less)
qed
+lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
+by (auto, case_tac x, auto)
+
+instance u :: (finite_po) finite_po
+by (intro_classes, simp add: u_UNIV)
+
+
subsection {* Lifted cpo is a cpo *}
lemma is_lub_Iup:
@@ -310,12 +317,27 @@
lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
by (cases x, simp_all)
+text {* lifting preserves chain-finiteness *}
+
lemma up_chain_cases:
"chain Y \<Longrightarrow>
(\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
(\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
+instance u :: (chfin) chfin
+apply (intro_classes, clarify)
+apply (drule up_chain_cases, safe)
+apply (drule chfin [rule_format])
+apply (erule exE, rename_tac n)
+apply (rule_tac x="n + j" in exI)
+apply (simp only: max_in_chain_def)
+apply (clarify, rename_tac k)
+apply (subgoal_tac "\<exists>m. k = m + j", clarsimp)
+apply (rule_tac x="k - j" in exI, simp)
+apply (simp add: max_in_chain_def)
+done
+
lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
apply (unfold compact_def)
apply (rule admI)