Email Gateway (Aug 22 2022 at 12:49): Email Gateway (Aug 22 2022 at 12:49):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
in the Isar 2016 slides, strong and weak premises are shown:
strong premises: have B if A1 and A2
weak premises: have B when A1 and A2
but they are not explained in details.
What does
show A1 ==> A2 ... ==> B becomes free for re-interpretation
so these are strong premises
mean?
Email Gateway (Aug 22 2022 at 12:49):From: Makarius <makarius@sketis.net>
There is a bit more text in the isar-ref manual and the NEWS, notably:
The keyword 'when' may be used instead of 'if', to indicate 'presume'
instead of 'assume' above.
The meaning of 'show' with Pure rule statements has changed: premises
are treated in the sense of 'assume', instead of 'presume'.
Weak premises are relatively unexciting and rarely used in practice. The
change means that typical accidents by beginners with show "A ==> B" do
not lead to unexpected results and disrupt the process of learning Isar.
In the rare situations where the weak form is intended, the explicit
'when' context may be used.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC