1.1 --- a/src/HOLCF/Cfun.thy	Sat Nov 27 18:51:15 2010 +0100
     1.2 +++ b/src/HOLCF/Cfun.thy	Sat Nov 27 12:26:18 2010 -0800
     1.3 @@ -484,28 +484,28 @@
     1.4  default_sort pcpo
     1.5  
     1.6  definition
     1.7 -  strict :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
     1.8 -  "strict = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
     1.9 +  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
    1.10 +  "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
    1.11  
    1.12 -lemma cont_strict: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
    1.13 +lemma cont_seq: "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 strict_conv_if: "strict\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
    1.18 -unfolding strict_def by (simp add: cont_strict)
    1.19 +lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
    1.20 +unfolding seq_def by (simp add: cont_seq)
    1.21  
    1.22 -lemma strict1 [simp]: "strict\<cdot>\<bottom> = \<bottom>"
    1.23 -by (simp add: strict_conv_if)
    1.24 +lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
    1.25 +by (simp add: seq_conv_if)
    1.26  
    1.27 -lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
    1.28 -by (simp add: strict_conv_if)
    1.29 +lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
    1.30 +by (simp add: seq_conv_if)
    1.31  
    1.32 -lemma strict3 [simp]: "strict\<cdot>x\<cdot>\<bottom> = \<bottom>"
    1.33 -by (simp add: strict_conv_if)
    1.34 +lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
    1.35 +by (simp add: seq_conv_if)
    1.36  
    1.37  definition
    1.38    strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
    1.39 -  "strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))"
    1.40 +  "strictify = (\<Lambda> f x. seq\<cdot>x\<cdot>(f\<cdot>x))"
    1.41  
    1.42  lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.43  unfolding strictify_def by simp

     2.1 --- a/src/HOLCF/Fixrec.thy	Sat Nov 27 18:51:15 2010 +0100
     2.2 +++ b/src/HOLCF/Fixrec.thy	Sat Nov 27 12:26:18 2010 -0800
     2.3 @@ -107,7 +107,7 @@
     2.4  definition
     2.5    match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
     2.6  where
     2.7 -  "match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)"
     2.8 +  "match_UU = (\<Lambda> x k. seq\<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	Sat Nov 27 18:51:15 2010 +0100
     3.2 +++ b/src/HOLCF/One.thy	Sat Nov 27 12:26:18 2010 -0800
     3.3 @@ -54,7 +54,7 @@
     3.4  
     3.5  definition
     3.6    one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
     3.7 -  "one_case = (\<Lambda> a x. strict\<cdot>x\<cdot>a)"
     3.8 +  "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)"
     3.9  
    3.10  translations
    3.11    "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"

     4.1 --- a/src/HOLCF/Sprod.thy	Sat Nov 27 18:51:15 2010 +0100
     4.2 +++ b/src/HOLCF/Sprod.thy	Sat Nov 27 12:26:18 2010 -0800
     4.3 @@ -37,11 +37,11 @@
     4.4  
     4.5  definition
     4.6    spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
     4.7 -  "spair = (\<Lambda> a b. Abs_sprod (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b))"
     4.8 +  "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))"
     4.9  
    4.10  definition
    4.11    ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
    4.12 -  "ssplit = (\<Lambda> f p. strict\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
    4.13 +  "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
    4.14  
    4.15  syntax
    4.16    "_stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
    4.17 @@ -54,10 +54,10 @@
    4.18  
    4.19  subsection {* Case analysis *}
    4.20  
    4.21 -lemma spair_sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> sprod"
    4.22 -by (simp add: sprod_def strict_conv_if)
    4.23 +lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod"
    4.24 +by (simp add: sprod_def seq_conv_if)
    4.25  
    4.26 -lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
    4.27 +lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)"
    4.28  by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)
    4.29  
    4.30  lemmas Rep_sprod_simps =
    4.31 @@ -82,16 +82,16 @@
    4.32  by (simp add: Rep_sprod_simps)
    4.33  
    4.34  lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
    4.35 -by (simp add: Rep_sprod_simps strict_conv_if)
    4.36 +by (simp add: Rep_sprod_simps seq_conv_if)
    4.37  
    4.38  lemma spair_below_iff:
    4.39    "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
    4.40 -by (simp add: Rep_sprod_simps strict_conv_if)
    4.41 +by (simp add: Rep_sprod_simps seq_conv_if)
    4.42  
    4.43  lemma spair_eq_iff:
    4.44    "((:a, b:) = (:c, d:)) =
    4.45      (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"
    4.46 -by (simp add: Rep_sprod_simps strict_conv_if)
    4.47 +by (simp add: Rep_sprod_simps seq_conv_if)
    4.48  
    4.49  lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
    4.50  by simp
    4.51 @@ -177,7 +177,7 @@
    4.52  by (rule compactI, simp add: ssnd_below_iff)
    4.53  
    4.54  lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
    4.55 -by (rule compact_sprod, simp add: Rep_sprod_spair strict_conv_if)
    4.56 +by (rule compact_sprod, simp add: Rep_sprod_spair seq_conv_if)
    4.57  
    4.58  lemma compact_spair_iff:
    4.59    "compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))"

     5.1 --- a/src/HOLCF/Ssum.thy	Sat Nov 27 18:51:15 2010 +0100
     5.2 +++ b/src/HOLCF/Ssum.thy	Sat Nov 27 12:26:18 2010 -0800
     5.3 @@ -32,22 +32,22 @@
     5.4  
     5.5  definition
     5.6    sinl :: "'a \<rightarrow> ('a ++ 'b)" where
     5.7 -  "sinl = (\<Lambda> a. Abs_ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>))"
     5.8 +  "sinl = (\<Lambda> a. Abs_ssum (seq\<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 (strict\<cdot>b\<cdot>FF, \<bottom>, b))"
    5.13 +  "sinr = (\<Lambda> b. Abs_ssum (seq\<cdot>b\<cdot>FF, \<bottom>, b))"
    5.14  
    5.15 -lemma sinl_ssum: "(strict\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
    5.16 -by (simp add: ssum_def strict_conv_if)
    5.17 +lemma sinl_ssum: "(seq\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
    5.18 +by (simp add: ssum_def seq_conv_if)
    5.19  
    5.20 -lemma sinr_ssum: "(strict\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
    5.21 -by (simp add: ssum_def strict_conv_if)
    5.22 +lemma sinr_ssum: "(seq\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
    5.23 +by (simp add: ssum_def seq_conv_if)
    5.24  
    5.25 -lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
    5.26 +lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (seq\<cdot>a\<cdot>TT, a, \<bottom>)"
    5.27  by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)
    5.28  
    5.29 -lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
    5.30 +lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (seq\<cdot>b\<cdot>FF, \<bottom>, b)"
    5.31  by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)
    5.32  
    5.33  lemmas Rep_ssum_simps =
    5.34 @@ -60,16 +60,16 @@
    5.35  text {* Ordering *}
    5.36  
    5.37  lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
    5.38 -by (simp add: Rep_ssum_simps strict_conv_if)
    5.39 +by (simp add: Rep_ssum_simps seq_conv_if)
    5.40  
    5.41  lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
    5.42 -by (simp add: Rep_ssum_simps strict_conv_if)
    5.43 +by (simp add: Rep_ssum_simps seq_conv_if)
    5.44  
    5.45  lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
    5.46 -by (simp add: Rep_ssum_simps strict_conv_if)
    5.47 +by (simp add: Rep_ssum_simps seq_conv_if)
    5.48  
    5.49  lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
    5.50 -by (simp add: Rep_ssum_simps strict_conv_if)
    5.51 +by (simp add: Rep_ssum_simps seq_conv_if)
    5.52  
    5.53  text {* Equality *}
    5.54