allow negative argument in "consumes" source format;
authorwenzelm
Tue Jan 08 16:23:07 2013 +0100 (2013-01-08)
changeset 507726973b3f41334
parent 50771 2852f997bfb5
child 50773 205d12333fdc
allow negative argument in "consumes" source format;
more documentation/NEWS;
NEWS
src/Doc/IsarRef/Proof.thy
src/Pure/Isar/attrib.ML
     1.1 --- a/NEWS	Tue Jan 08 16:01:07 2013 +0100
     1.2 +++ b/NEWS	Tue Jan 08 16:23:07 2013 +0100
     1.3 @@ -38,6 +38,13 @@
     1.4  specifications: nesting of "context fixes ... context assumes ..."
     1.5  and "class ... context ...".
     1.6  
     1.7 +* Attribute "consumes" allows a negative value as well, which is
     1.8 +interpreted relatively to the total number if premises of the rule in
     1.9 +the target context.  This form of declaration is stable when exported
    1.10 +from a nested 'context' with additional assumptions.  It is the
    1.11 +preferred form for definitional packages, notably cases/rules produced
    1.12 +in HOL/inductive and HOL/function.
    1.13 +
    1.14  * More informative error messages for Isar proof commands involving
    1.15  lazy enumerations (method applications etc.).
    1.16  
     2.1 --- a/src/Doc/IsarRef/Proof.thy	Tue Jan 08 16:01:07 2013 +0100
     2.2 +++ b/src/Doc/IsarRef/Proof.thy	Tue Jan 08 16:23:07 2013 +0100
     2.3 @@ -1197,7 +1197,7 @@
     2.4      ;
     2.5      @@{attribute params} ((@{syntax name} * ) + @'and')
     2.6      ;
     2.7 -    @@{attribute consumes} @{syntax nat}?
     2.8 +    @@{attribute consumes} @{syntax int}?
     2.9    "}
    2.10  
    2.11    \begin{description}
    2.12 @@ -1245,7 +1245,15 @@
    2.13    \secref{sec:hol-inductive}).  Rules without any @{attribute
    2.14    consumes} declaration given are treated as if @{attribute
    2.15    consumes}~@{text 0} had been specified.
    2.16 -  
    2.17 +
    2.18 +  A negative @{text n} is interpreted relatively to the total number
    2.19 +  if premises of the rule in the target context.  Thus its absolute
    2.20 +  value specifies the remaining number of premises, after subtracting
    2.21 +  the prefix of major premises as indicated above. This form of
    2.22 +  declaration has the technical advantage of being stable under more
    2.23 +  morphisms, notably those that export the result from a nested
    2.24 +  @{command_ref context} with additional assumptions.
    2.25 +
    2.26    Note that explicit @{attribute consumes} declarations are only
    2.27    rarely needed; this is already taken care of automatically by the
    2.28    higher-level @{attribute cases}, @{attribute induct}, and
     3.1 --- a/src/Pure/Isar/attrib.ML	Tue Jan 08 16:01:07 2013 +0100
     3.2 +++ b/src/Pure/Isar/attrib.ML	Tue Jan 08 16:23:07 2013 +0100
     3.3 @@ -391,7 +391,7 @@
     3.4      "rename bound variables in abstractions" #>
     3.5    setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
     3.6    setup (Binding.name "folded") folded "folded definitions" #>
     3.7 -  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
     3.8 +  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
     3.9      "number of consumed facts" #>
    3.10    setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
    3.11      "number of equality constraints" #>