* 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
