Re: [isabelle-dev] NEWS: structured Isar goal statements (update)

[Makarius]

On Wed, 24 Jun 2015, Makarius wrote:


The keyword 'when' may be used instead of 'if', to indicate 'presume'
instead of 'assume' above.


This refers to Isabelle/51a6997b1384.

The 'presume' element is rarely used, and the 'when' eigen-context is mainly 
an exercise in orthogonality of the language. There might be useful 
applications nonetheless, e.g. see the examples about suffices-to-show in 
~~/src/HOL/Isar_Examples/Structured_Statements.thy


Now that 'presume' semantics has a separate syntax, the normal == is free 
to be re-interpreted.  So here is another breaking NEWS entry for 
Isabelle/804dfdc82835:



* The meaning of 'show' with Pure rule statements has changed: premises
are treated in the sense of 'assume', instead of 'presume'. This means,
a goal like ⋀x. A x ⟹ B x ⟹ C x can be solved completely as follows:

  show ⋀x. A x ⟹ B x ⟹ C x

or:

  show C x if A x B x for x

Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:

  show C x when A x B x for x


This means the common beginner-mistake to use Pure rule statements for 
show no longer leads to bad surprises.  As a consequence, there might be 
more ugly proofs emerging than necessary, but better than no proof at all 
in the first attempt.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: structured Isar goal statements (update)

[Makarius]

* Local goals ('have', 'show', 'hence', 'thus') allow structured
statements like fixes/assumes/shows in theorem specifications, but the
notation is postfix with keywords 'if' (or 'when') and 'for'. For
example:

  have result: C x y
if A x and B y
for x :: 'a and y :: 'a
proof

The local assumptions are bound to the name that. The result is
exported from context of the statement as usual. The above roughly
corresponds to a raw proof block like this:

  {
fix x :: 'a and y :: 'a
assume that: A x B y
have C x y proof
  }
  note result = this

The keyword 'when' may be used instead of 'if', to indicate 'presume'
instead of 'assume' above.


This refers to Isabelle/51a6997b1384.

The 'presume' element is rarely used, and the 'when' eigen-context is 
mainly an exercise in orthogonality of the language. There might be useful 
applications nonetheless, e.g. see the examples about suffices-to-show 
in ~~/src/HOL/Isar_Examples/Structured_Statements.thy



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev