introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
authorhuffman
Wed Oct 20 19:40:02 2010 -0700 (2010-10-20)
changeset 40046ba2e41c8b725
parent 40045 e0f372e18f3e
child 40047 6547d0f079ed
introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
src/HOLCF/Cfun.thy
src/HOLCF/Fixrec.thy
src/HOLCF/One.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Wed Oct 20 17:25:22 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Wed Oct 20 19:40:02 2010 -0700
     1.3 @@ -534,32 +534,28 @@
     1.4  default_sort pcpo
     1.5  
     1.6  definition
     1.7 -  strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
     1.8 -  "strictify = (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
     1.9 +  strict :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
    1.10 +  "strict = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
    1.11  
    1.12 -text {* results about strictify *}
    1.13 +lemma cont_strict: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
    1.14 +unfolding cont_def is_lub_def is_ub_def ball_simps
    1.15 +by (simp add: lub_eq_bottom_iff)
    1.16  
    1.17 -lemma cont_strictify1: "cont (\<lambda>f. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.18 -by simp
    1.19 +lemma strict_conv_if: "strict\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
    1.20 +unfolding strict_def by (simp add: cont_strict)
    1.21  
    1.22 -lemma monofun_strictify2: "monofun (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.23 -apply (rule monofunI)
    1.24 -apply (auto simp add: monofun_cfun_arg)
    1.25 -done
    1.26 +lemma strict1 [simp]: "strict\<cdot>\<bottom> = \<bottom>"
    1.27 +by (simp add: strict_conv_if)
    1.28  
    1.29 -lemma cont_strictify2: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.30 -apply (rule contI2)
    1.31 -apply (rule monofun_strictify2)
    1.32 -apply (case_tac "(\<Squnion>i. Y i) = \<bottom>", simp)
    1.33 -apply (simp add: contlub_cfun_arg del: if_image_distrib)
    1.34 -apply (drule chain_UU_I_inverse2, clarify, rename_tac j)
    1.35 -apply (rule lub_mono2, rule_tac x=j in exI, simp_all)
    1.36 -apply (auto dest!: chain_mono_less)
    1.37 -done
    1.38 +lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
    1.39 +by (simp add: strict_conv_if)
    1.40 +
    1.41 + definition
    1.42 +  strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
    1.43 +  "strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))"
    1.44  
    1.45  lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.46 -  unfolding strictify_def
    1.47 -  by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM)
    1.48 +unfolding strictify_def by simp
    1.49  
    1.50  lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>"
    1.51  by (simp add: strictify_conv_if)
     2.1 --- a/src/HOLCF/Fixrec.thy	Wed Oct 20 17:25:22 2010 -0700
     2.2 +++ b/src/HOLCF/Fixrec.thy	Wed Oct 20 19:40:02 2010 -0700
     2.3 @@ -115,7 +115,7 @@
     2.4  definition
     2.5    match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
     2.6  where
     2.7 -  "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
     2.8 +  "match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)"
     2.9  
    2.10  definition
    2.11    match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
     3.1 --- a/src/HOLCF/One.thy	Wed Oct 20 17:25:22 2010 -0700
     3.2 +++ b/src/HOLCF/One.thy	Wed Oct 20 19:40:02 2010 -0700
     3.3 @@ -54,7 +54,7 @@
     3.4  
     3.5  definition
     3.6    one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
     3.7 -  "one_when = (\<Lambda> a. strictify\<cdot>(\<Lambda> _. a))"
     3.8 +  "one_when = (\<Lambda> a x. strict\<cdot>x\<cdot>a)"
     3.9  
    3.10  translations
    3.11    "case x of XCONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
     4.1 --- a/src/HOLCF/Sprod.thy	Wed Oct 20 17:25:22 2010 -0700
     4.2 +++ b/src/HOLCF/Sprod.thy	Wed Oct 20 19:40:02 2010 -0700
     4.3 @@ -27,9 +27,8 @@
     4.4  type_notation (HTML output)
     4.5    sprod  ("(_ \<otimes>/ _)" [21,20] 20)
     4.6  
     4.7 -lemma spair_lemma:
     4.8 -  "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
     4.9 -by (simp add: Sprod_def strictify_conv_if)
    4.10 +lemma spair_lemma: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> Sprod"
    4.11 +by (simp add: Sprod_def strict_conv_if)
    4.12  
    4.13  subsection {* Definitions of constants *}
    4.14  
    4.15 @@ -43,12 +42,11 @@
    4.16  
    4.17  definition
    4.18    spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
    4.19 -  "spair = (\<Lambda> a b. Abs_Sprod
    4.20 -             (strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a))"
    4.21 +  "spair = (\<Lambda> a b. Abs_Sprod (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b))"
    4.22  
    4.23  definition
    4.24    ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
    4.25 -  "ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
    4.26 +  "ssplit = (\<Lambda> f p. strict\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
    4.27  
    4.28  syntax
    4.29    "_stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
    4.30 @@ -62,7 +60,7 @@
    4.31  subsection {* Case analysis *}
    4.32  
    4.33  lemma Rep_Sprod_spair:
    4.34 -  "Rep_Sprod (:a, b:) = (strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a)"
    4.35 +  "Rep_Sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
    4.36  unfolding spair_def
    4.37  by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
    4.38  
    4.39 @@ -76,7 +74,7 @@
    4.40  apply (simp add: Rep_Sprod_simps Pair_fst_snd_eq)
    4.41  apply (simp add: Sprod_def)
    4.42  apply (erule disjE, simp)
    4.43 -apply (simp add: strictify_conv_if)
    4.44 +apply (simp add: strict_conv_if)
    4.45  apply fast
    4.46  done
    4.47  
    4.48 @@ -91,22 +89,22 @@
    4.49  subsection {* Properties of \emph{spair} *}
    4.50  
    4.51  lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
    4.52 -by (simp add: Rep_Sprod_simps strictify_conv_if)
    4.53 +by (simp add: Rep_Sprod_simps strict_conv_if)
    4.54  
    4.55  lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
    4.56 -by (simp add: Rep_Sprod_simps strictify_conv_if)
    4.57 +by (simp add: Rep_Sprod_simps strict_conv_if)
    4.58  
    4.59  lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
    4.60 -by (simp add: Rep_Sprod_simps strictify_conv_if)
    4.61 +by (simp add: Rep_Sprod_simps strict_conv_if)
    4.62  
    4.63  lemma spair_below_iff:
    4.64    "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
    4.65 -by (simp add: Rep_Sprod_simps strictify_conv_if)
    4.66 +by (simp add: Rep_Sprod_simps strict_conv_if)
    4.67  
    4.68  lemma spair_eq_iff:
    4.69    "((:a, b:) = (:c, d:)) =
    4.70      (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"
    4.71 -by (simp add: Rep_Sprod_simps strictify_conv_if)
    4.72 +by (simp add: Rep_Sprod_simps strict_conv_if)
    4.73  
    4.74  lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
    4.75  by simp
    4.76 @@ -197,7 +195,7 @@
    4.77  by (rule compactI, simp add: ssnd_below_iff)
    4.78  
    4.79  lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
    4.80 -by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
    4.81 +by (rule compact_Sprod, simp add: Rep_Sprod_spair strict_conv_if)
    4.82  
    4.83  lemma compact_spair_iff:
    4.84    "compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))"
     5.1 --- a/src/HOLCF/Ssum.thy	Wed Oct 20 17:25:22 2010 -0700
     5.2 +++ b/src/HOLCF/Ssum.thy	Wed Oct 20 19:40:02 2010 -0700
     5.3 @@ -34,28 +34,28 @@
     5.4  
     5.5  definition
     5.6    sinl :: "'a \<rightarrow> ('a ++ 'b)" where
     5.7 -  "sinl = (\<Lambda> a. Abs_Ssum (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>))"
     5.8 +  "sinl = (\<Lambda> a. Abs_Ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>))"
     5.9  
    5.10  definition
    5.11    sinr :: "'b \<rightarrow> ('a ++ 'b)" where
    5.12 -  "sinr = (\<Lambda> b. Abs_Ssum (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b))"
    5.13 +  "sinr = (\<Lambda> b. Abs_Ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b))"
    5.14  
    5.15 -lemma sinl_Ssum: "(strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>) \<in> Ssum"
    5.16 -by (simp add: Ssum_def strictify_conv_if)
    5.17 +lemma sinl_Ssum: "(strict\<cdot>a\<cdot>TT, a, \<bottom>) \<in> Ssum"
    5.18 +by (simp add: Ssum_def strict_conv_if)
    5.19  
    5.20 -lemma sinr_Ssum: "(strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b) \<in> Ssum"
    5.21 -by (simp add: Ssum_def strictify_conv_if)
    5.22 +lemma sinr_Ssum: "(strict\<cdot>b\<cdot>FF, \<bottom>, b) \<in> Ssum"
    5.23 +by (simp add: Ssum_def strict_conv_if)
    5.24  
    5.25 -lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>)"
    5.26 +lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
    5.27  by (unfold sinl_def, simp add: cont_Abs_Ssum sinl_Ssum)
    5.28  
    5.29 -lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"
    5.30 +lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
    5.31  by (unfold sinr_def, simp add: cont_Abs_Ssum sinr_Ssum)
    5.32  
    5.33 -lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>)"
    5.34 +lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
    5.35  by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum)
    5.36  
    5.37 -lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"
    5.38 +lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
    5.39  by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
    5.40  
    5.41  subsection {* Properties of \emph{sinl} and \emph{sinr} *}
    5.42 @@ -63,16 +63,16 @@
    5.43  text {* Ordering *}
    5.44  
    5.45  lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
    5.46 -by (simp add: below_Ssum_def Rep_Ssum_sinl strictify_conv_if)
    5.47 +by (simp add: below_Ssum_def Rep_Ssum_sinl strict_conv_if)
    5.48  
    5.49  lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
    5.50 -by (simp add: below_Ssum_def Rep_Ssum_sinr strictify_conv_if)
    5.51 +by (simp add: below_Ssum_def Rep_Ssum_sinr strict_conv_if)
    5.52  
    5.53  lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
    5.54 -by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
    5.55 +by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
    5.56  
    5.57  lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
    5.58 -by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
    5.59 +by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
    5.60  
    5.61  text {* Equality *}
    5.62  
    5.63 @@ -117,10 +117,10 @@
    5.64  text {* Compactness *}
    5.65  
    5.66  lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
    5.67 -by (rule compact_Ssum, simp add: Rep_Ssum_sinl strictify_conv_if)
    5.68 +by (rule compact_Ssum, simp add: Rep_Ssum_sinl strict_conv_if)
    5.69  
    5.70  lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
    5.71 -by (rule compact_Ssum, simp add: Rep_Ssum_sinr strictify_conv_if)
    5.72 +by (rule compact_Ssum, simp add: Rep_Ssum_sinr strict_conv_if)
    5.73  
    5.74  lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
    5.75  unfolding compact_def