--- a/src/HOLCF/Bifinite.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Bifinite.thy Sun Oct 24 15:11:24 2010 -0700
@@ -5,7 +5,7 @@
header {* Bifinite domains *}
theory Bifinite
-imports Algebraic Cprod Sprod Ssum Up Lift One Tr
+imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable
begin
subsection {* Class of bifinite domains *}
--- a/src/HOLCF/Cfun.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Cfun.thy Sun Oct 24 15:11:24 2010 -0700
@@ -95,12 +95,6 @@
lemma UU_CFun: "\<bottom> \<in> CFun"
by (simp add: CFun_def inst_fun_pcpo)
-instance cfun :: (finite_po, finite_po) finite_po
-by (rule typedef_finite_po [OF type_definition_CFun])
-
-instance cfun :: (finite_po, chfin) chfin
-by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
-
instance cfun :: (cpo, discrete_cpo) discrete_cpo
by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
@@ -550,7 +544,10 @@
lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
by (simp add: strict_conv_if)
- definition
+lemma strict3 [simp]: "strict\<cdot>x\<cdot>\<bottom> = \<bottom>"
+by (simp add: strict_conv_if)
+
+definition
strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
"strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))"
--- a/src/HOLCF/Discrete.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Discrete.thy Sun Oct 24 15:11:24 2010 -0700
@@ -44,22 +44,6 @@
"!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
by (fast elim: discr_chain0)
-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
-apply (rule_tac x=0 in exI)
-apply (unfold max_in_chain_def)
-apply (clarify, erule discr_chain0 [symmetric])
-done
-
subsection {* \emph{undiscr} *}
definition
--- a/src/HOLCF/FOCUS/Fstream.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Sun Oct 24 15:11:24 2010 -0700
@@ -42,11 +42,7 @@
lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
-apply (rule flat_eq [THEN iffD1, symmetric])
-apply (rule Def_not_UU)
-apply (drule antisym_less_inverse)
-apply (erule (1) conjunct2 [THEN trans_less])
-done
+by simp
section "fscons"
--- a/src/HOLCF/Fun_Cpo.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Fun_Cpo.thy Sun Oct 24 15:11:24 2010 -0700
@@ -110,26 +110,6 @@
from Yij Yik show "Y j = Y k" by auto
qed
-instance "fun" :: (finite, chfin) chfin
-proof
- 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)
- 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
-
-instance "fun" :: (finite, finite_po) finite_po ..
-
instance "fun" :: (type, discrete_cpo) discrete_cpo
proof
fix f g :: "'a \<Rightarrow> 'b"
--- a/src/HOLCF/Library/Sum_Cpo.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Library/Sum_Cpo.thy Sun Oct 24 15:11:24 2010 -0700
@@ -213,8 +213,6 @@
apply (case_tac "\<Squnion>i. Y i", simp_all)
done
-instance sum :: (finite_po, finite_po) finite_po ..
-
instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
by intro_classes (simp add: below_sum_def split: sum.split)
--- a/src/HOLCF/Lift.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Lift.thy Sun Oct 24 15:11:24 2010 -0700
@@ -5,17 +5,14 @@
header {* Lifting types of class type to flat pcpo's *}
theory Lift
-imports Discrete Up Countable
+imports Discrete Up
begin
default_sort type
-pcpodef 'a lift = "UNIV :: 'a discr u set"
+pcpodef (open) 'a lift = "UNIV :: 'a discr u set"
by simp_all
-instance lift :: (finite) finite_po
-by (rule typedef_finite_po [OF type_definition_lift])
-
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
definition
@@ -33,7 +30,7 @@
done
rep_datatype "\<bottom>\<Colon>'a lift" Def
- by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
+ by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
lemmas lift_distinct1 = lift.distinct(1)
lemmas lift_distinct2 = lift.distinct(2)
@@ -65,7 +62,7 @@
by simp
lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
-by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
+by (simp add: below_lift_def Def_def Abs_lift_inverse)
lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
by (induct y, simp, simp add: Def_below_Def)
@@ -80,6 +77,18 @@
by (induct x) auto
qed
+subsection {* Continuity of @{const lift_case} *}
+
+lemma lift_case_eq: "lift_case \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
+apply (induct x, unfold lift.cases)
+apply (simp add: Rep_lift_strict)
+apply (simp add: Def_def Abs_lift_inverse)
+done
+
+lemma cont2cont_lift_case [simp]:
+ "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
+unfolding lift_case_eq by (simp add: cont_Rep_lift [THEN cont_compose])
+
subsection {* Further operations *}
definition
@@ -90,59 +99,14 @@
flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
"flift2 f = (FLIFT x. Def (f x))"
-subsection {* Continuity Proofs for flift1, flift2 *}
-
-text {* Need the instance of @{text flat}. *}
-
-lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)"
-apply (induct x)
-apply simp
-apply simp
-apply (rule cont_id [THEN cont2cont_fun])
-done
-
-lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
-apply (rule flatdom_strict2cont)
-apply simp
-done
-
-lemma cont_flift1: "cont flift1"
-unfolding flift1_def
-apply (rule cont2cont_LAM)
-apply (rule cont_lift_case2)
-apply (rule cont_lift_case1)
-done
-
-lemma FLIFT_mono:
- "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
-apply (rule monofunE [where f=flift1])
-apply (rule cont2mono [OF cont_flift1])
-apply (simp add: fun_below_iff)
-done
-
-lemma cont2cont_flift1 [simp, cont2cont]:
- "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
-apply (rule cont_flift1 [THEN cont_compose])
-apply simp
-done
-
-lemma cont2cont_lift_case [simp]:
- "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
-apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
-apply (simp add: flift1_def cont_lift_case2)
-apply simp
-done
-
-text {* rewrites for @{term flift1}, @{term flift2} *}
-
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
-by (simp add: flift1_def cont_lift_case2)
+by (simp add: flift1_def)
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
by (simp add: flift2_def)
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
-by (simp add: flift1_def cont_lift_case2)
+by (simp add: flift1_def)
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
by (simp add: flift2_def)
@@ -153,4 +117,12 @@
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (cases x, simp_all)
+lemma FLIFT_mono:
+ "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
+by (rule cfun_belowI, case_tac x, simp_all)
+
+lemma cont2cont_flift1 [simp, cont2cont]:
+ "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
+by (simp add: flift1_def cont2cont_LAM)
+
end
--- a/src/HOLCF/Pcpo.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Pcpo.thy Sun Oct 24 15:11:24 2010 -0700
@@ -262,18 +262,6 @@
end
-class finite_po = finite + po
-begin
-
-subclass chfin
-apply default
-apply (drule finite_range_imp_finch)
-apply (rule finite)
-apply (simp add: finite_chain_def)
-done
-
-end
-
class flat = pcpo +
assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
begin
@@ -299,7 +287,7 @@
end
-text {* Discrete cpos *}
+subsection {* Discrete cpos *}
class discrete_cpo = below +
assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
@@ -320,14 +308,14 @@
thus "S i = S 0" by (rule sym)
qed
-subclass cpo
+subclass chfin
proof
fix S :: "nat \<Rightarrow> 'a"
assume S: "chain S"
- hence "\<exists>x. S = (\<lambda>i. x)"
- by (rule discrete_chain_const)
- thus "\<exists>x. range S <<| x"
- by (fast intro: lub_const)
+ hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const)
+ hence "max_in_chain 0 S"
+ unfolding max_in_chain_def by auto
+ thus "\<exists>i. max_in_chain i S" ..
qed
end
--- a/src/HOLCF/Pcpodef.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Pcpodef.thy Sun Oct 24 15:11:24 2010 -0700
@@ -46,15 +46,6 @@
by (simp only: type_definition.Abs_image [OF type])
qed
-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 typedef_finite_UNIV [OF type])
- apply (rule finite)
-done
-
subsection {* Proving a subtype is chain-finite *}
lemma ch2ch_Rep:
--- a/src/HOLCF/Product_Cpo.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Product_Cpo.thy Sun Oct 24 15:11:24 2010 -0700
@@ -12,19 +12,16 @@
subsection {* Unit type is a pcpo *}
-instantiation unit :: below
+instantiation unit :: discrete_cpo
begin
definition
below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
-instance ..
-end
+instance proof
+qed simp
-instance unit :: discrete_cpo
-by intro_classes simp
-
-instance unit :: finite_po ..
+end
instance unit :: pcpo
by intro_classes simp
@@ -157,8 +154,6 @@
thus "\<exists>x. range S <<| x" ..
qed
-instance prod :: (finite_po, finite_po) finite_po ..
-
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
proof
fix x y :: "'a \<times> 'b"
--- a/src/HOLCF/Sprod.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Sprod.thy Sun Oct 24 15:11:24 2010 -0700
@@ -12,37 +12,31 @@
subsection {* Definition of strict product type *}
-pcpodef (Sprod) ('a, 'b) sprod (infixr "**" 20) =
+pcpodef ('a, 'b) sprod (infixr "**" 20) =
"{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
by simp_all
-instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
-by (rule typedef_finite_po [OF type_definition_Sprod])
-
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
+by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])
type_notation (xsymbols)
sprod ("(_ \<otimes>/ _)" [21,20] 20)
type_notation (HTML output)
sprod ("(_ \<otimes>/ _)" [21,20] 20)
-lemma spair_lemma: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> Sprod"
-by (simp add: Sprod_def strict_conv_if)
-
subsection {* Definitions of constants *}
definition
sfst :: "('a ** 'b) \<rightarrow> 'a" where
- "sfst = (\<Lambda> p. fst (Rep_Sprod p))"
+ "sfst = (\<Lambda> p. fst (Rep_sprod p))"
definition
ssnd :: "('a ** 'b) \<rightarrow> 'b" where
- "ssnd = (\<Lambda> p. snd (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 (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b))"
+ "spair = (\<Lambda> a b. Abs_sprod (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b))"
definition
ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
@@ -59,28 +53,20 @@
subsection {* Case analysis *}
-lemma Rep_Sprod_spair:
- "Rep_Sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
-unfolding spair_def
-by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
-
-lemmas Rep_Sprod_simps =
- Rep_Sprod_inject [symmetric] below_Sprod_def
- Rep_Sprod_strict Rep_Sprod_spair
+lemma spair_sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> sprod"
+by (simp add: sprod_def strict_conv_if)
-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 Pair_fst_snd_eq)
-apply (simp add: Sprod_def)
-apply (erule disjE, simp)
-apply (simp add: strict_conv_if)
-apply fast
-done
+lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
+by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)
+
+lemmas Rep_sprod_simps =
+ Rep_sprod_inject [symmetric] below_sprod_def
+ Pair_fst_snd_eq below_prod_def
+ Rep_sprod_strict Rep_sprod_spair
lemma sprodE [case_names bottom spair, cases type: sprod]:
- "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-using Exh_Sprod [of p] by auto
+ obtains "p = \<bottom>" | x y where "p = (:x, y:)" and "x \<noteq> \<bottom>" and "y \<noteq> \<bottom>"
+using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps)
lemma sprod_induct [case_names bottom spair, induct type: sprod]:
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
@@ -89,22 +75,22 @@
subsection {* Properties of \emph{spair} *}
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps)
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps)
lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps strict_conv_if)
lemma spair_below_iff:
"((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps strict_conv_if)
lemma spair_eq_iff:
"((:a, b:) = (:c, d:)) =
(a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_sprod_simps strict_conv_if)
lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
by simp
@@ -118,6 +104,10 @@
lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
by simp
+lemma spair_below:
+ "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
+by (simp add: spair_below_iff)
+
lemma spair_eq:
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)"
by (simp add: spair_eq_iff)
@@ -135,16 +125,16 @@
subsection {* Properties of \emph{sfst} and \emph{ssnd} *}
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
-by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict)
+by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict)
lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
-by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_strict)
+by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict)
lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
-by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair)
+by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair)
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
-by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
+by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)
lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
by (cases p, simp_all)
@@ -158,24 +148,15 @@
lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
by simp
-lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
+lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
by (cases p, simp_all)
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 (simp only: below_prod_def)
-done
+by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod)
lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
by (auto simp add: po_eq_conv below_sprod)
-lemma spair_below:
- "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
-apply (cases "a = \<bottom>", simp)
-apply (cases "b = \<bottom>", simp)
-apply (simp add: below_sprod)
-done
-
lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
apply (simp add: below_sprod)
@@ -195,7 +176,7 @@
by (rule compactI, simp add: ssnd_below_iff)
lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
-by (rule compact_Sprod, simp add: Rep_Sprod_spair strict_conv_if)
+by (rule compact_sprod, simp add: Rep_sprod_spair strict_conv_if)
lemma compact_spair_iff:
"compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))"
--- a/src/HOLCF/Ssum.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Ssum.thy Sun Oct 24 15:11:24 2010 -0700
@@ -12,17 +12,14 @@
subsection {* Definition of strict sum type *}
-pcpodef (Ssum) ('a, 'b) ssum (infixr "++" 10) =
- "{p :: tr \<times> ('a \<times> 'b).
- (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
- (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
+pcpodef ('a, 'b) ssum (infixr "++" 10) =
+ "{p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
+ (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
+ (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>) }"
by simp_all
-instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
-by (rule typedef_finite_po [OF type_definition_Ssum])
-
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
+by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])
type_notation (xsymbols)
ssum ("(_ \<oplus>/ _)" [21, 20] 20)
@@ -34,45 +31,44 @@
definition
sinl :: "'a \<rightarrow> ('a ++ 'b)" where
- "sinl = (\<Lambda> a. Abs_Ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>))"
+ "sinl = (\<Lambda> a. Abs_ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>))"
definition
sinr :: "'b \<rightarrow> ('a ++ 'b)" where
- "sinr = (\<Lambda> b. Abs_Ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b))"
+ "sinr = (\<Lambda> b. Abs_ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b))"
-lemma sinl_Ssum: "(strict\<cdot>a\<cdot>TT, a, \<bottom>) \<in> Ssum"
-by (simp add: Ssum_def strict_conv_if)
+lemma sinl_ssum: "(strict\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
+by (simp add: ssum_def strict_conv_if)
-lemma sinr_Ssum: "(strict\<cdot>b\<cdot>FF, \<bottom>, b) \<in> Ssum"
-by (simp add: Ssum_def strict_conv_if)
+lemma sinr_ssum: "(strict\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
+by (simp add: ssum_def strict_conv_if)
-lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
-by (unfold sinl_def, simp add: cont_Abs_Ssum sinl_Ssum)
-
-lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
-by (unfold sinr_def, simp add: cont_Abs_Ssum sinr_Ssum)
+lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
+by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)
-lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
-by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum)
+lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
+by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)
-lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
-by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
+lemmas Rep_ssum_simps =
+ Rep_ssum_inject [symmetric] below_ssum_def
+ Pair_fst_snd_eq below_prod_def
+ Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
subsection {* Properties of \emph{sinl} and \emph{sinr} *}
text {* Ordering *}
lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl strict_conv_if)
+by (simp add: Rep_ssum_simps strict_conv_if)
lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: below_Ssum_def Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_ssum_simps strict_conv_if)
lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_ssum_simps strict_conv_if)
lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_ssum_simps strict_conv_if)
text {* Equality *}
@@ -97,30 +93,30 @@
text {* Strictness *}
lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinl_Abs_Ssum Abs_Ssum_strict)
+by (simp add: Rep_ssum_simps)
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinr_Abs_Ssum Abs_Ssum_strict)
+by (simp add: Rep_ssum_simps)
lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
-by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
+using sinl_eq [of "x" "\<bottom>"] by simp
lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
-by (cut_tac sinr_eq [of "x" "\<bottom>"], simp)
+using sinr_eq [of "x" "\<bottom>"] by simp
-lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
+lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
by simp
-lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
+lemma sinr_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
by simp
text {* Compactness *}
lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinl strict_conv_if)
+by (rule compact_ssum, simp add: Rep_ssum_sinl)
lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinr strict_conv_if)
+by (rule compact_ssum, simp add: Rep_ssum_sinr)
lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
unfolding compact_def
@@ -138,24 +134,11 @@
subsection {* Case analysis *}
-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 (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 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)
-apply (simp add: sinr_Abs_Ssum Ssum_def)
-done
-
lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:
- "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
- \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
- \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-using Exh_Ssum [of p] by auto
+ obtains "p = \<bottom>"
+ | x where "p = sinl\<cdot>x" and "x \<noteq> \<bottom>"
+ | y where "p = sinr\<cdot>y" and "y \<noteq> \<bottom>"
+using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps)
lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
"\<lbrakk>P \<bottom>;
@@ -177,7 +160,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) (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,17 +170,17 @@
"\<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) (Rep_Ssum s)"
-unfolding sscase_def by (simp add: cont_Rep_Ssum [THEN cont_compose])
+ "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)
+unfolding beta_sscase by (simp add: Rep_ssum_strict)
lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>x"
-unfolding beta_sscase by (simp add: Rep_Ssum_sinl)
+unfolding beta_sscase by (simp add: Rep_ssum_sinl)
lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<cdot>y"
-unfolding beta_sscase by (simp add: Rep_Ssum_sinr)
+unfolding beta_sscase by (simp add: Rep_ssum_sinr)
lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
by (cases z, simp_all)
--- a/src/HOLCF/Tools/Domain/domain.ML Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain.ML Sun Oct 24 15:11:24 2010 -0700
@@ -8,25 +8,21 @@
signature DOMAIN =
sig
val add_domain_cmd:
- binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
val add_domain:
- binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
val add_new_domain_cmd:
- binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
val add_new_domain:
- binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
@@ -50,7 +46,6 @@
(prep_typ : theory -> (string * sort) list -> 'a -> typ)
(add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
(arg_sort : bool -> sort)
- (comp_dbind : binding)
(raw_specs : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
(thy : theory) =
@@ -172,7 +167,7 @@
(dbinds ~~ rhss ~~ iso_infos);
val (take_rews, thy) =
- Domain_Induction.comp_theorems comp_dbind
+ Domain_Induction.comp_theorems
dbinds take_info constr_infos thy;
in
thy
@@ -240,27 +235,21 @@
(Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
val domains_decl =
- Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
- Parse.and_list1 domain_decl;
+ Parse.and_list1 domain_decl;
fun mk_domain
(definitional : bool)
- (opt_name : binding option,
- doms : ((((string * string option) list * binding) * mixfix) *
+ (doms : ((((string * string option) list * binding) * mixfix) *
((binding * (bool * binding option * string) list) * mixfix) list) list ) =
let
- val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
val specs : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list =
map (fn (((vs, t), mx), cons) =>
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
- val comp_dbind =
- case opt_name of NONE => Binding.name (space_implode "_" names)
- | SOME s => s;
in
- if definitional
- then add_new_domain_cmd comp_dbind specs
- else add_domain_cmd comp_dbind specs
+ if definitional
+ then add_new_domain_cmd specs
+ else add_domain_cmd specs
end;
val _ =
--- a/src/HOLCF/Tools/Domain/domain_induction.ML Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML Sun Oct 24 15:11:24 2010 -0700
@@ -8,7 +8,7 @@
signature DOMAIN_INDUCTION =
sig
val comp_theorems :
- binding -> binding list ->
+ binding list ->
Domain_Take_Proofs.take_induct_info ->
Domain_Constructors.constr_info list ->
theory -> thm list * theory
@@ -367,13 +367,14 @@
(******************************************************************************)
fun comp_theorems
- (comp_dbind : binding)
(dbinds : binding list)
(take_info : Domain_Take_Proofs.take_induct_info)
(constr_infos : Domain_Constructors.constr_info list)
(thy : theory) =
let
-val comp_dname = Binding.name_of comp_dbind;
+
+val comp_dname = space_implode "_" (map Binding.name_of dbinds);
+val comp_dbind = Binding.name comp_dname;
(* Test for emptiness *)
(* FIXME: reimplement emptiness test
--- a/src/HOLCF/Tools/fixrec.ML Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Sun Oct 24 15:11:24 2010 -0700
@@ -393,10 +393,16 @@
(******************************** Parsers ********************************)
(*************************************************************************)
+val opt_thm_name' : (bool * Attrib.binding) parser =
+ Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding)
+ || Parse_Spec.opt_thm_name ":" >> pair false;
+
+val spec' : (bool * (Attrib.binding * string)) parser =
+ opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)));
+
val alt_specs' : (bool * (Attrib.binding * string)) list parser =
- Parse.enum1 "|"
- (Parse.opt_keyword "unchecked" -- Parse_Spec.spec --|
- Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
+ let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(");
+ in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end;
val _ =
Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
--- a/src/HOLCF/Up.thy Sun Oct 24 21:25:13 2010 +0200
+++ b/src/HOLCF/Up.thy Sun Oct 24 15:11:24 2010 -0700
@@ -62,108 +62,67 @@
by (auto split: u.split_asm intro: below_trans)
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:
"range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
-apply (rule is_lubI)
-apply (rule ub_rangeI)
-apply (subst Iup_below)
-apply (erule is_ub_lub)
-apply (case_tac u)
-apply (drule ub_rangeD)
-apply simp
-apply simp
-apply (erule is_lub_lub)
-apply (rule ub_rangeI)
-apply (drule_tac i=i in ub_rangeD)
-apply simp
-done
-
-text {* Now some lemmas about chains of @{typ "'a u"} elements *}
-
-lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"
-by (case_tac z, simp_all)
-
-lemma up_lemma2:
- "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
-apply (erule contrapos_nn)
-apply (drule_tac i="j" and j="i + j" in chain_mono)
-apply (rule le_add2)
-apply (case_tac "Y j")
-apply assumption
-apply simp
-done
-
-lemma up_lemma3:
- "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
-by (rule up_lemma1 [OF up_lemma2])
-
-lemma up_lemma4:
- "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
-apply (rule chainI)
-apply (rule Iup_below [THEN iffD1])
-apply (subst up_lemma3, assumption+)+
-apply (simp add: chainE)
-done
-
-lemma up_lemma5:
- "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow>
- (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
-by (rule ext, rule up_lemma3 [symmetric])
-
-lemma up_lemma6:
- "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
- \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
-apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
-apply assumption
-apply (subst up_lemma5, assumption+)
-apply (rule is_lub_Iup)
-apply (rule cpo_lubI)
-apply (erule (1) up_lemma4)
-done
+unfolding is_lub_def is_ub_def ball_simps
+by (auto simp add: below_up_def split: u.split)
lemma up_chain_lemma:
- "chain Y \<Longrightarrow>
- (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = Iup (\<Squnion>i. A i) \<and>
- (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
-apply (rule disjCI)
-apply (simp add: fun_eq_iff)
-apply (erule exE, rename_tac j)
-apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
-apply (simp add: up_lemma4)
-apply (simp add: up_lemma6 [THEN thelubI])
-apply (rule_tac x=j in exI)
-apply (simp add: up_lemma3)
-done
-
-lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
-apply (frule up_chain_lemma, safe)
-apply (rule_tac x="Iup (\<Squnion>i. A i)" in exI)
-apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
-apply (simp add: is_lub_Iup cpo_lubI)
-apply (rule exI, rule lub_const)
-done
+ assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom"
+ | A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
+proof (cases "\<exists>k. Y k \<noteq> Ibottom")
+ case True
+ then obtain k where k: "Y k \<noteq> Ibottom" ..
+ def A \<equiv> "\<lambda>i. THE a. Iup a = Y (i + k)"
+ have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)"
+ proof
+ fix i :: nat
+ from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono)
+ with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto)
+ thus "Iup (A i) = Y (i + k)"
+ by (cases "Y (i + k)", simp_all add: A_def)
+ qed
+ from Y have chain_A: "chain A"
+ unfolding chain_def Iup_below [symmetric]
+ by (simp add: Iup_A)
+ hence "range A <<| (\<Squnion>i. A i)"
+ by (rule cpo_lubI)
+ hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)"
+ by (rule is_lub_Iup)
+ hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)"
+ by (simp only: Iup_A)
+ hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)"
+ by (simp only: is_lub_range_shift [OF Y])
+ with Iup_A chain_A show ?thesis ..
+next
+ case False
+ then have "\<forall>i. Y i = Ibottom" by simp
+ then show ?thesis ..
+qed
instance u :: (cpo) cpo
-by intro_classes (rule cpo_up)
+proof
+ fix S :: "nat \<Rightarrow> 'a u"
+ assume S: "chain S"
+ thus "\<exists>x. range (\<lambda>i. S i) <<| x"
+ proof (rule up_chain_lemma)
+ assume "\<forall>i. S i = Ibottom"
+ hence "range (\<lambda>i. S i) <<| Ibottom"
+ by (simp add: lub_const)
+ thus ?thesis ..
+ next
+ fix A :: "nat \<Rightarrow> 'a"
+ assume "range S <<| Iup (\<Squnion>i. A i)"
+ thus ?thesis ..
+ qed
+qed
subsection {* Lifted cpo is pointed *}
-lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
-apply (rule_tac x = "Ibottom" in exI)
-apply (rule minimal_up [THEN allI])
-done
-
instance u :: (cpo) pcpo
-by intro_classes (rule least_up)
+by intro_classes fast
text {* for compatibility with old HOLCF-Version *}
lemma inst_up_pcpo: "\<bottom> = Ibottom"
@@ -192,13 +151,22 @@
done
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
-apply (rule contI)
-apply (frule up_chain_lemma, safe)
-apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
-apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
-apply (simp add: cont_cfun_arg)
-apply (simp add: lub_const)
-done
+proof (rule contI2)
+ fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))"
+ from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))"
+ proof (rule up_chain_lemma)
+ fix A and k
+ assume A: "\<forall>i. Iup (A i) = Y (i + k)"
+ assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
+ hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
+ by (simp add: thelubI contlub_cfun_arg)
+ also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
+ by (simp add: A)
+ also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
+ using Y' by (rule lub_range_shift)
+ finally show ?thesis by simp
+ qed simp
+qed (rule monofun_Ifup2)
subsection {* Continuous versions of constants *}
@@ -251,18 +219,20 @@
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)
+ assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
+ | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
+apply (rule up_chain_lemma [OF Y])
+apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI)
+done
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
apply (rule compactI2)
-apply (drule up_chain_cases, safe)
+apply (erule up_chain_cases)
+apply simp
apply (drule (1) compactD2, simp)
-apply (erule exE, rule_tac x="i + j" in exI)
-apply simp
-apply simp
+apply (erule exE)
+apply (drule_tac f="up" and x="x" in monofun_cfun_arg)
+apply (simp, erule exI)
done
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"