# HG changeset patch
# User huffman
# Date 1287628802 25200
# Node ID ba2e41c8b725abcb54c9c02e160e9e9d25672315
# Parent  e0f372e18f3e1c9d9a6ae3faebad8336caf9f5b0
introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions

diff -r e0f372e18f3e -r ba2e41c8b725 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Oct 20 17:25:22 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Wed Oct 20 19:40:02 2010 -0700
@@ -534,32 +534,28 @@
 default_sort pcpo
 
 definition
-  strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
-  "strictify = (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+  strict :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
+  "strict = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
 
-text {* results about strictify *}
+lemma cont_strict: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
+unfolding cont_def is_lub_def is_ub_def ball_simps
+by (simp add: lub_eq_bottom_iff)
 
-lemma cont_strictify1: "cont (\<lambda>f. if x = \<bottom> then \<bottom> else f\<cdot>x)"
-by simp
+lemma strict_conv_if: "strict\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
+unfolding strict_def by (simp add: cont_strict)
 
-lemma monofun_strictify2: "monofun (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
-apply (rule monofunI)
-apply (auto simp add: monofun_cfun_arg)
-done
+lemma strict1 [simp]: "strict\<cdot>\<bottom> = \<bottom>"
+by (simp add: strict_conv_if)
 
-lemma cont_strictify2: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
-apply (rule contI2)
-apply (rule monofun_strictify2)
-apply (case_tac "(\<Squnion>i. Y i) = \<bottom>", simp)
-apply (simp add: contlub_cfun_arg del: if_image_distrib)
-apply (drule chain_UU_I_inverse2, clarify, rename_tac j)
-apply (rule lub_mono2, rule_tac x=j in exI, simp_all)
-apply (auto dest!: chain_mono_less)
-done
+lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
+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))"
 
 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
-  unfolding strictify_def
-  by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM)
+unfolding strictify_def by simp
 
 lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (simp add: strictify_conv_if)
diff -r e0f372e18f3e -r ba2e41c8b725 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Oct 20 17:25:22 2010 -0700
+++ b/src/HOLCF/Fixrec.thy	Wed Oct 20 19:40:02 2010 -0700
@@ -115,7 +115,7 @@
 definition
   match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
 where
-  "match_UU = strictify\<cdot>(\<Lambda> x k. fail)"
+  "match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)"
 
 definition
   match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
diff -r e0f372e18f3e -r ba2e41c8b725 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Wed Oct 20 17:25:22 2010 -0700
+++ b/src/HOLCF/One.thy	Wed Oct 20 19:40:02 2010 -0700
@@ -54,7 +54,7 @@
 
 definition
   one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
-  "one_when = (\<Lambda> a. strictify\<cdot>(\<Lambda> _. a))"
+  "one_when = (\<Lambda> a x. strict\<cdot>x\<cdot>a)"
 
 translations
   "case x of XCONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
diff -r e0f372e18f3e -r ba2e41c8b725 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Wed Oct 20 17:25:22 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Wed Oct 20 19:40:02 2010 -0700
@@ -27,9 +27,8 @@
 type_notation (HTML output)
   sprod  ("(_ \<otimes>/ _)" [21,20] 20)
 
-lemma spair_lemma:
-  "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
-by (simp add: Sprod_def strictify_conv_if)
+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 *}
 
@@ -43,12 +42,11 @@
 
 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))"
+  "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
-  "ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
+  "ssplit = (\<Lambda> f p. strict\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
 syntax
   "_stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
@@ -62,7 +60,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:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
 unfolding spair_def
 by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
 
@@ -76,7 +74,7 @@
 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)
+apply (simp add: strict_conv_if)
 apply fast
 done
 
@@ -91,22 +89,22 @@
 subsection {* Properties of \emph{spair} *}
 
 lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
-by (simp add: Rep_Sprod_simps strictify_conv_if)
+by (simp add: Rep_Sprod_simps strict_conv_if)
 
 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
-by (simp add: Rep_Sprod_simps strictify_conv_if)
+by (simp add: Rep_Sprod_simps strict_conv_if)
 
 lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
-by (simp add: Rep_Sprod_simps strictify_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 strictify_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 strictify_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
@@ -197,7 +195,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 strictify_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))"
diff -r e0f372e18f3e -r ba2e41c8b725 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Oct 20 17:25:22 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Wed Oct 20 19:40:02 2010 -0700
@@ -34,28 +34,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 (strict\<cdot>a\<cdot>TT, 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 (strict\<cdot>b\<cdot>FF, \<bottom>, b))"
 
-lemma sinl_Ssum: "(strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>) \<in> Ssum"
-by (simp add: Ssum_def strictify_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: "(strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b) \<in> Ssum"
-by (simp add: Ssum_def strictify_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 (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>)"
+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 (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"
+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) = (strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>)"
+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) = (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"
+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)
 
 subsection {* Properties of \emph{sinl} and \emph{sinr} *}
@@ -63,16 +63,16 @@
 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 strictify_conv_if)
+by (simp add: below_Ssum_def Rep_Ssum_sinl 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 strictify_conv_if)
+by (simp add: below_Ssum_def Rep_Ssum_sinr 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 strictify_conv_if)
+by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr 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 strictify_conv_if)
+by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
 
 text {* Equality *}
 
@@ -117,10 +117,10 @@
 text {* Compactness *}
 
 lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinl strictify_conv_if)
+by (rule compact_Ssum, simp add: Rep_Ssum_sinl strict_conv_if)
 
 lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinr strictify_conv_if)
+by (rule compact_Ssum, simp add: Rep_Ssum_sinr strict_conv_if)
 
 lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def