[isabelle-dev] NEWS: structured Isar goal statements

Makarius 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
     <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


More information about the isabelle-dev mailing list