[isabelle] Monotonic operators and calculational reasoning



How does Isar's calculational reasoner handle montonic operators?

For example, in the following

  have "(1::nat) < 3"
    by (auto)
  also have "(3::nat) + 1 < 5"
    by (auto)
  finally

the result is

calculation: (!!x y. x < y ==> x + 1 < y + 1) ==> 1 + 1 < 5

how do I treat this unwanted premise? Declaring add_less_mono1 as a
trans rule has no effect. You can't resolve the calculation with
add_less_mono1. I am puzzled.

------------------------------------------------------------------
Dr Brendan Mahony
Information Networks Division                   ph +61 8 8259 6046
Defence Science and Technology Organisation     fx +61 8 8259 5589
Edinburgh, South Australia      Brendan.Mahony at dsto.defence.gov.au

Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.







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