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.

Tobias





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