replaced separate lemmas seq{1,2,3} with seq_simps
authorhuffman
Thu Dec 23 11:52:26 2010 -0800 (2010-12-23)
changeset 414001a7557cc686a
parent 41399 ad093e4638e2
child 41401 e3ec82999306
replaced separate lemmas seq{1,2,3} with seq_simps
src/HOL/HOLCF/Cfun.thy
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Thu Dec 23 11:51:59 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Thu Dec 23 11:52:26 2010 -0800
     1.3 @@ -483,14 +483,11 @@
     1.4  lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
     1.5  unfolding seq_def by simp
     1.6  
     1.7 -lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
     1.8 -by (simp add: seq_conv_if)
     1.9 -
    1.10 -lemma seq2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
    1.11 -by (simp add: seq_conv_if)
    1.12 -
    1.13 -lemma seq3 [simp]: "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
    1.14 -by (simp add: seq_conv_if)
    1.15 +lemma seq_simps [simp]:
    1.16 +  "seq\<cdot>\<bottom> = \<bottom>"
    1.17 +  "seq\<cdot>x\<cdot>\<bottom> = \<bottom>"
    1.18 +  "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x = ID"
    1.19 +by (simp_all add: seq_conv_if)
    1.20  
    1.21  definition
    1.22    strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where