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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
