--- a/src/HOLCF/Cfun.thy Sat Nov 27 18:51:15 2010 +0100
+++ b/src/HOLCF/Cfun.thy Sat Nov 27 12:26:18 2010 -0800
@@ -484,28 +484,28 @@
default_sort pcpo
definition
- strict :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
- "strict = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
+ seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
+ "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
-lemma cont_strict: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
+lemma cont_seq: "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 strict_conv_if: "strict\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
-unfolding strict_def by (simp add: cont_strict)
+lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
+unfolding seq_def by (simp add: cont_seq)
-lemma strict1 [simp]: "strict\<cdot>\<bottom> = \<bottom>"
-by (simp add: strict_conv_if)
+lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
+by (simp add: seq_conv_if)
-lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
-by (simp add: strict_conv_if)
+lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
+by (simp add: seq_conv_if)
-lemma strict3 [simp]: "strict\<cdot>x\<cdot>\<bottom> = \<bottom>"
-by (simp add: strict_conv_if)
+lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
+by (simp add: seq_conv_if)
definition
strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
- "strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))"
+ "strictify = (\<Lambda> f x. seq\<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
--- a/src/HOLCF/Fixrec.thy Sat Nov 27 18:51:15 2010 +0100
+++ b/src/HOLCF/Fixrec.thy Sat Nov 27 12:26:18 2010 -0800
@@ -107,7 +107,7 @@
definition
match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
where
- "match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)"
+ "match_UU = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
definition
match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
--- a/src/HOLCF/One.thy Sat Nov 27 18:51:15 2010 +0100
+++ b/src/HOLCF/One.thy Sat Nov 27 12:26:18 2010 -0800
@@ -54,7 +54,7 @@
definition
one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
- "one_case = (\<Lambda> a x. strict\<cdot>x\<cdot>a)"
+ "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)"
translations
"case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
--- a/src/HOLCF/Sprod.thy Sat Nov 27 18:51:15 2010 +0100
+++ b/src/HOLCF/Sprod.thy Sat Nov 27 12:26:18 2010 -0800
@@ -37,11 +37,11 @@
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 (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))"
definition
ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
- "ssplit = (\<Lambda> f p. strict\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
+ "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
syntax
"_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
@@ -54,10 +54,10 @@
subsection {* Case analysis *}
-lemma spair_sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> sprod"
-by (simp add: sprod_def strict_conv_if)
+lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod"
+by (simp add: sprod_def seq_conv_if)
-lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
+lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)"
by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)
lemmas Rep_sprod_simps =
@@ -82,16 +82,16 @@
by (simp add: Rep_sprod_simps)
lemma spair_bottom_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 seq_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 seq_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 seq_conv_if)
lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
by simp
@@ -177,7 +177,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 seq_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 Sat Nov 27 18:51:15 2010 +0100
+++ b/src/HOLCF/Ssum.thy Sat Nov 27 12:26:18 2010 -0800
@@ -32,22 +32,22 @@
definition
sinl :: "'a \<rightarrow> ('a ++ 'b)" where
- "sinl = (\<Lambda> a. Abs_ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>))"
+ "sinl = (\<Lambda> a. Abs_ssum (seq\<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 (seq\<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: "(seq\<cdot>a\<cdot>TT, a, \<bottom>) \<in> ssum"
+by (simp add: ssum_def seq_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: "(seq\<cdot>b\<cdot>FF, \<bottom>, b) \<in> ssum"
+by (simp add: ssum_def seq_conv_if)
-lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
+lemma Rep_ssum_sinl: "Rep_ssum (sinl\<cdot>a) = (seq\<cdot>a\<cdot>TT, a, \<bottom>)"
by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)
-lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
+lemma Rep_ssum_sinr: "Rep_ssum (sinr\<cdot>b) = (seq\<cdot>b\<cdot>FF, \<bottom>, b)"
by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)
lemmas Rep_ssum_simps =
@@ -60,16 +60,16 @@
text {* Ordering *}
lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: Rep_ssum_simps strict_conv_if)
+by (simp add: Rep_ssum_simps seq_conv_if)
text {* Equality *}