src/HOLCF/UpperPD.thy
changeset 26041 c2e15e65165f
parent 25925 3dc4acca4388
child 26407 562a1d615336
     1.1 --- a/src/HOLCF/UpperPD.thy	Mon Feb 04 17:00:01 2008 +0100
     1.2 +++ b/src/HOLCF/UpperPD.thy	Wed Feb 06 08:34:32 2008 +0100
     1.3 @@ -403,10 +403,10 @@
     1.4      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     1.5      (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     1.6  
     1.7 -lemma ACI_upper_bind: "ACIf (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     1.8 +lemma ACI_upper_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     1.9  apply unfold_locales
    1.10 +apply (simp add: upper_plus_assoc)
    1.11  apply (simp add: upper_plus_commute)
    1.12 -apply (simp add: upper_plus_assoc)
    1.13  apply (simp add: upper_plus_absorb eta_cfun)
    1.14  done
    1.15  
    1.16 @@ -417,8 +417,8 @@
    1.17      (\<Lambda> f. upper_plus\<cdot>(upper_bind_basis t\<cdot>f)\<cdot>(upper_bind_basis u\<cdot>f))"
    1.18  unfolding upper_bind_basis_def
    1.19  apply -
    1.20 -apply (rule ACIf.fold_pd_PDUnit [OF ACI_upper_bind])
    1.21 -apply (rule ACIf.fold_pd_PDPlus [OF ACI_upper_bind])
    1.22 +apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_upper_bind])
    1.23 +apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_upper_bind])
    1.24  done
    1.25  
    1.26  lemma upper_bind_basis_mono: