[isabelle-dev] NEWS: structured Isar goal statements
makarius at sketis.net
Mon Jun 15 00:01:04 CEST 2015
* Local goals ('have', 'show', 'hence', 'thus') allow structured
statements like fixes/assumes/shows in theorem specifications, but the
notation is postfix with keywords 'if' and 'for'. For example:
have result: "C x y"
if "A x" and "B y"
for x :: 'a and y :: 'a
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
This refers e.g. to Isabelle/051b200f7578. The idea to provide a form of
fixes/assumes/shows within Isar proofs has been in the pipeline since
approx. 2006. It has many useful applications, also for internal use;
e.g. 'obtain' is now easier to implement as derived element.
Some examples are in ~~/src/HOL/Isar_Examples/Structured_Statements.thy
More information about the isabelle-dev