Email Gateway (Aug 17 2022 at 14:16): Email Gateway (Aug 17 2022 at 14:16):From: Brendan Mahony <Brendan.Mahony@dsto.defence.gov.au>
How does Isar's calculational reasoner handle montonic operators?
For example, in the following
have "(1::nat) < 3"
by (auto)
also have "(3::nat) + 1 < 5"
by (auto)
finally
the result is
calculation: (!!x y. x < y ==> x + 1 < y + 1) ==> 1 + 1 < 5
how do I treat this unwanted premise? Declaring add_less_mono1 as a
trans rule has no effect. You can't resolve the calculation with
add_less_mono1. I am puzzled.
Dr Brendan Mahony
Information Networks Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
Email Gateway (Aug 17 2022 at 14:43):From: nipkow@in.tum.de
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
Last updated: May 03 2024 at 04:19 UTC