* 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
<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
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
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
