replaced separate lemmas seq{1,2,3} with seq_simps
authorhuffman
Thu, 23 Dec 2010 11:52:26 -0800
changeset 41400 1a7557cc686a
parent 41399 ad093e4638e2
child 41401 e3ec82999306
replaced separate lemmas seq{1,2,3} with seq_simps
src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Thu Dec 23 11:51:59 2010 -0800
+++ b/src/HOL/HOLCF/Cfun.thy	Thu Dec 23 11:52:26 2010 -0800
@@ -483,14 +483,11 @@
 lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
 unfolding seq_def by simp
 
-lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
-by (simp add: seq_conv_if)
-
-lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
-by (simp add: seq_conv_if)
-
-lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
-by (simp add: seq_conv_if)
+lemma seq_simps [simp]:
+  "seq\<cdot>\<bottom> = \<bottom>"
+  "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
+  "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
+by (simp_all add: seq_conv_if)
 
 definition
   strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where