Re: [isabelle] Monotonic operators and calculational reasoning

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

You did exactly the right thing.

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

As did Isabelle. The principle here is that the monotonicity assumptions that
arise in your calculational proof are carried around, accumulate, and get
discharged at the end. Thus you cannot simply say

  finally have "1+1 < (5::nat)" .

but need to do something like

  finally have  "1+1 < (5::nat)"  by (blast intro:add_less_mono1)

There may be slightly slicker proof patters.


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