Re: [isabelle] Monotonic operators and calculational reasoning
On 3 Apr 2006, at 6:57, Brendan Mahony wrote:
How does Isar's calculational reasoner handle montonic operators?
The appropriate transitivity lemmas have the attribute [trans].
For example, in the following
have "(1::nat) < 3"
also have "(3::nat) + 1 < 5"
Terms in the chain have to agree. That is, you have to insert a "have
3 < 3 + 1".
This archive was generated by a fusion of
Pipermail (Mailman edition) and