[isabelle-dev] Split-lemmas for Option.bind

Peter Lammich lammich at in.tum.de
Tue Oct 21 12:18:39 CEST 2014


Is there any reason why the obvious split-lemmas for Option.bind are not
included in Option.thy?

  lemma bind_split: "P (bind m f) 
  ⟷ (m = None ⟶ P None) ∧ (∀v. m=Some v ⟶ P (f v))"
    by (cases m) auto

  lemma bind_split_asm: "P (bind m f) = (¬(
      m=None ∧ ¬P None 
    ∨ (∃x. m=Some x ∧ ¬P (f x))))"
    by (cases m) auto

They can be very handy for proofs in the option-monad.


More information about the isabelle-dev mailing list