# HG changeset patch
# User huffman
# Date 1290889578 28800
# Node ID a3e505b236e76399d9da8e068e5a3308441d2655
# Parent  d73659e8ccdd4ff1f193b0668d2b2b62d15ef9d1
rename function 'strict' to 'seq', which is its name in Haskell

diff -r d73659e8ccdd -r a3e505b236e7 src/HOLCF/Cfun.thy
--- 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
diff -r d73659e8ccdd -r a3e505b236e7 src/HOLCF/Fixrec.thy
--- 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"
diff -r d73659e8ccdd -r a3e505b236e7 src/HOLCF/One.thy
--- 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"
diff -r d73659e8ccdd -r a3e505b236e7 src/HOLCF/Sprod.thy
--- 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))"
diff -r d73659e8ccdd -r a3e505b236e7 src/HOLCF/Ssum.thy
--- 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 *}