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"
    by (auto)
  also have "(3::nat) + 1 < 5"
    by (auto)

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 MHonArc.