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

[Peter Lammich]

Hi.

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.


--
  Peter