src/HOLCF/Fixrec.thy
changeset 16779 ac1dc3d4746a
parent 16776 a3899ac14a1c
child 18094 404f298220af
equal deleted inserted replaced
16778:2162c0de4673 16779:ac1dc3d4746a
    71 
    71 
    72 lemma right_unit [simp]: "m >>= return = m"
    72 lemma right_unit [simp]: "m >>= return = m"
    73 by (rule_tac p=m in maybeE, simp_all)
    73 by (rule_tac p=m in maybeE, simp_all)
    74 
    74 
    75 lemma bind_assoc [simp]:
    75 lemma bind_assoc [simp]:
    76  "(do a <- m; b <- k\<cdot>a; h\<cdot>b) = (do b <- (do a <- m; k\<cdot>a); h\<cdot>b)"
    76  "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
    77 by (rule_tac p=m in maybeE, simp_all)
    77 by (rule_tac p=m in maybeE, simp_all)
    78 
    78 
    79 subsection {* Run operator *}
    79 subsection {* Run operator *}
    80 
    80 
    81 constdefs
    81 constdefs