add csplit3, ssplit3, fup3 as simp rules
authorhuffman
Thu Jun 23 22:07:30 2005 +0200 (2005-06-23)
changeset 16553aa36d41e4263
parent 16552 0774e9bcdb6c
child 16554 5841e7f9eef5
add csplit3, ssplit3, fup3 as simp rules
src/HOLCF/Cprod.thy
src/HOLCF/Sprod.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Jun 23 21:27:23 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Jun 23 22:07:30 2005 +0200
     1.3 @@ -301,7 +301,7 @@
     1.4  lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
     1.5  by (simp add: csplit_def)
     1.6  
     1.7 -lemma csplit3: "csplit\<cdot>cpair\<cdot>z = z"
     1.8 +lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
     1.9  by (simp add: csplit_def surjective_pairing_Cprod2)
    1.10  
    1.11  lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
     2.1 --- a/src/HOLCF/Sprod.thy	Thu Jun 23 21:27:23 2005 +0200
     2.2 +++ b/src/HOLCF/Sprod.thy	Thu Jun 23 22:07:30 2005 +0200
     2.3 @@ -200,7 +200,7 @@
     2.4  lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:)= f\<cdot>x\<cdot>y"
     2.5  by (simp add: ssplit_def)
     2.6  
     2.7 -lemma ssplit3: "ssplit\<cdot>spair\<cdot>z = z"
     2.8 +lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"
     2.9  by (rule_tac p=z in sprodE, simp_all)
    2.10  
    2.11  end
     3.1 --- a/src/HOLCF/Up.thy	Thu Jun 23 21:27:23 2005 +0200
     3.2 +++ b/src/HOLCF/Up.thy	Thu Jun 23 22:07:30 2005 +0200
     3.3 @@ -309,7 +309,7 @@
     3.4  lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
     3.5  by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 )
     3.6  
     3.7 -lemma fup3: "fup\<cdot>up\<cdot>x = x"
     3.8 +lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
     3.9  by (rule_tac p=x in upE1, simp_all)
    3.10  
    3.11  end