Re: [isabelle] strong and weak premises

On Fri, 5 Feb 2016, Buday Gergely wrote:

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


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.


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