Re: [isabelle] Monotonic operators and calculational reasoning
have "(1::nat) < 3"
also have "(3::nat) + 1 < 5"
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