Re: [isabelle] Properties on intervals



On Tue, 6 Feb 2007 04:31 pm, Antonio D'Ettole wrote:
> Specifically my goal is:
>
> [| ALL u. u <= 0 & ~ leaking (u + t); leaking t |] ==> False

> Does anybody know how to prove this?

It works:
------------------------------------------------------------
consts
 leaking :: "real  ==> bool"

theorem " [| ALL u. u <= 0 & ~ leaking(u + t); leaking t |]  ==> False"
proof -
  assume A1: "ALL (u::real). u <= 0 & ~ leaking(u + t)"
  assume A2: "leaking t"
  from A1 have "~leaking (0 + t)" by (blast)
  then have L: "~leaking t" by (simp add: real_add_zero_left)
  from A2 L show ?thesis by (blast)
qed
------------------------------------------------------------

Regards,
  Michael Nedzelsky






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.