merged
authorhaftmann
Tue Jul 14 10:56:43 2009 +0200 (2009-07-14)
changeset 32001fafefd0b341c
parent 31996 1d93369079c4
parent 32000 6f07563dc8a9
child 32002 1a35de4112bb
merged
     1.1 --- a/CONTRIBUTORS	Mon Jul 13 19:07:05 2009 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Jul 14 10:56:43 2009 +0200
     1.3 @@ -7,6 +7,12 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* July 2009: Florian Haftmann, TUM
     1.8 +  New quickcheck implementation using new code generator
     1.9 +
    1.10 +* July 2009: Florian Haftmann, TUM
    1.11 +  HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation
    1.12 +
    1.13  * June 2009: Andreas Lochbihler, Uni Karlsruhe
    1.14    HOL/Library/Fin_Fun: almost everywhere constant functions
    1.15  
     2.1 --- a/NEWS	Mon Jul 13 19:07:05 2009 +0200
     2.2 +++ b/NEWS	Tue Jul 14 10:56:43 2009 +0200
     2.3 @@ -18,6 +18,16 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Code generator attributes follow the usual underscore convention:
     2.8 +    code_unfold     replaces    code unfold
     2.9 +    code_post       replaces    code post
    2.10 +    etc.
    2.11 +  INCOMPATIBILITY.
    2.12 +
    2.13 +* New quickcheck implementation using new code generator.
    2.14 +
    2.15 +* New type class boolean_algebra.
    2.16 +
    2.17  * Class semiring_div requires superclass no_zero_divisors and proof of
    2.18  div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
    2.19  div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
     3.1 --- a/doc-src/Codegen/Thy/ML.thy	Mon Jul 13 19:07:05 2009 +0200
     3.2 +++ b/doc-src/Codegen/Thy/ML.thy	Tue Jul 14 10:56:43 2009 +0200
     3.3 @@ -78,8 +78,7 @@
     3.4  
     3.5  text %mlref {*
     3.6    \begin{mldecls}
     3.7 -  @{index_ML Code.read_const: "theory -> string -> string"} \\
     3.8 -  @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\
     3.9 +  @{index_ML Code.read_const: "theory -> string -> string"}
    3.10    \end{mldecls}
    3.11  
    3.12    \begin{description}
    3.13 @@ -87,11 +86,6 @@
    3.14    \item @{ML Code.read_const}~@{text thy}~@{text s}
    3.15       reads a constant as a concrete term expression @{text s}.
    3.16  
    3.17 -  \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm}
    3.18 -     rewrites a code equation @{text thm} with a simpset @{text ss};
    3.19 -     only arguments and right hand side are rewritten,
    3.20 -     not the head of the code equation.
    3.21 -
    3.22    \end{description}
    3.23  
    3.24  *}
     4.1 --- a/doc-src/Codegen/Thy/Program.thy	Mon Jul 13 19:07:05 2009 +0200
     4.2 +++ b/doc-src/Codegen/Thy/Program.thy	Tue Jul 14 10:56:43 2009 +0200
     4.3 @@ -153,14 +153,14 @@
     4.4    out: \emph{preprocessing}.  In essence, the preprocessor
     4.5    consists of two components: a \emph{simpset} and \emph{function transformers}.
     4.6  
     4.7 -  The \emph{simpset} allows to employ the full generality of the Isabelle
     4.8 -  simplifier.  Due to the interpretation of theorems
     4.9 -  as code equations, rewrites are applied to the right
    4.10 -  hand side and the arguments of the left hand side of an
    4.11 -  equation, but never to the constant heading the left hand side.
    4.12 -  An important special case are \emph{inline theorems} which may be
    4.13 -  declared and undeclared using the
    4.14 -  \emph{code inline} or \emph{code inline del} attribute respectively.
    4.15 +  The \emph{simpset} allows to employ the full generality of the
    4.16 +  Isabelle simplifier.  Due to the interpretation of theorems as code
    4.17 +  equations, rewrites are applied to the right hand side and the
    4.18 +  arguments of the left hand side of an equation, but never to the
    4.19 +  constant heading the left hand side.  An important special case are
    4.20 +  \emph{unfold theorems} which may be declared and undeclared using
    4.21 +  the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
    4.22 +  attribute respectively.
    4.23  
    4.24    Some common applications:
    4.25  *}
    4.26 @@ -173,21 +173,21 @@
    4.27       \item replacing non-executable constructs by executable ones:
    4.28  *}     
    4.29  
    4.30 -lemma %quote [code inline]:
    4.31 +lemma %quote [code_inline]:
    4.32    "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
    4.33  
    4.34  text {*
    4.35       \item eliminating superfluous constants:
    4.36  *}
    4.37  
    4.38 -lemma %quote [code inline]:
    4.39 +lemma %quote [code_inline]:
    4.40    "1 = Suc 0" by simp
    4.41  
    4.42  text {*
    4.43       \item replacing executable but inconvenient constructs:
    4.44  *}
    4.45  
    4.46 -lemma %quote [code inline]:
    4.47 +lemma %quote [code_inline]:
    4.48    "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
    4.49  
    4.50  text_raw {*
    4.51 @@ -210,10 +210,10 @@
    4.52    on code equations.
    4.53  
    4.54    \begin{warn}
    4.55 -    The attribute \emph{code unfold}
    4.56 -    associated with the @{text "SML code generator"} also applies to
    4.57 -    the @{text "generic code generator"}:
    4.58 -    \emph{code unfold} implies \emph{code inline}.
    4.59 +
    4.60 +    Attribute @{attribute code_unfold} also applies to the
    4.61 +    preprocessor of the ancient @{text "SML code generator"}; in case
    4.62 +    this is not what you intend, use @{attribute code_inline} instead.
    4.63    \end{warn}
    4.64  *}
    4.65  
     5.1 --- a/doc-src/Codegen/Thy/document/ML.tex	Mon Jul 13 19:07:05 2009 +0200
     5.2 +++ b/doc-src/Codegen/Thy/document/ML.tex	Tue Jul 14 10:56:43 2009 +0200
     5.3 @@ -124,8 +124,7 @@
     5.4  %
     5.5  \begin{isamarkuptext}%
     5.6  \begin{mldecls}
     5.7 -  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
     5.8 -  \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
     5.9 +  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
    5.10    \end{mldecls}
    5.11  
    5.12    \begin{description}
    5.13 @@ -133,11 +132,6 @@
    5.14    \item \verb|Code.read_const|~\isa{thy}~\isa{s}
    5.15       reads a constant as a concrete term expression \isa{s}.
    5.16  
    5.17 -  \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
    5.18 -     rewrites a code equation \isa{thm} with a simpset \isa{ss};
    5.19 -     only arguments and right hand side are rewritten,
    5.20 -     not the head of the code equation.
    5.21 -
    5.22    \end{description}%
    5.23  \end{isamarkuptext}%
    5.24  \isamarkuptrue%
     6.1 --- a/doc-src/Codegen/Thy/document/Program.tex	Mon Jul 13 19:07:05 2009 +0200
     6.2 +++ b/doc-src/Codegen/Thy/document/Program.tex	Tue Jul 14 10:56:43 2009 +0200
     6.3 @@ -395,14 +395,14 @@
     6.4    out: \emph{preprocessing}.  In essence, the preprocessor
     6.5    consists of two components: a \emph{simpset} and \emph{function transformers}.
     6.6  
     6.7 -  The \emph{simpset} allows to employ the full generality of the Isabelle
     6.8 -  simplifier.  Due to the interpretation of theorems
     6.9 -  as code equations, rewrites are applied to the right
    6.10 -  hand side and the arguments of the left hand side of an
    6.11 -  equation, but never to the constant heading the left hand side.
    6.12 -  An important special case are \emph{inline theorems} which may be
    6.13 -  declared and undeclared using the
    6.14 -  \emph{code inline} or \emph{code inline del} attribute respectively.
    6.15 +  The \emph{simpset} allows to employ the full generality of the
    6.16 +  Isabelle simplifier.  Due to the interpretation of theorems as code
    6.17 +  equations, rewrites are applied to the right hand side and the
    6.18 +  arguments of the left hand side of an equation, but never to the
    6.19 +  constant heading the left hand side.  An important special case are
    6.20 +  \emph{unfold theorems} which may be declared and undeclared using
    6.21 +  the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
    6.22 +  attribute respectively.
    6.23  
    6.24    Some common applications:%
    6.25  \end{isamarkuptext}%
    6.26 @@ -421,7 +421,7 @@
    6.27  %
    6.28  \isatagquote
    6.29  \isacommand{lemma}\isamarkupfalse%
    6.30 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
    6.31 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
    6.32  \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    6.33  \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
    6.34  \endisatagquote
    6.35 @@ -442,7 +442,7 @@
    6.36  %
    6.37  \isatagquote
    6.38  \isacommand{lemma}\isamarkupfalse%
    6.39 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
    6.40 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
    6.41  \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    6.42  \ simp%
    6.43  \endisatagquote
    6.44 @@ -463,7 +463,7 @@
    6.45  %
    6.46  \isatagquote
    6.47  \isacommand{lemma}\isamarkupfalse%
    6.48 -\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
    6.49 +\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
    6.50  \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    6.51  \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
    6.52  \endisatagquote
    6.53 @@ -491,10 +491,10 @@
    6.54    on code equations.
    6.55  
    6.56    \begin{warn}
    6.57 -    The attribute \emph{code unfold}
    6.58 -    associated with the \isa{SML\ code\ generator} also applies to
    6.59 -    the \isa{generic\ code\ generator}:
    6.60 -    \emph{code unfold} implies \emph{code inline}.
    6.61 +
    6.62 +    Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
    6.63 +    preprocessor of the ancient \isa{SML\ code\ generator}; in case
    6.64 +    this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
    6.65    \end{warn}%
    6.66  \end{isamarkuptext}%
    6.67  \isamarkuptrue%
     7.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jul 13 19:07:05 2009 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jul 14 10:56:43 2009 +0200
     7.3 @@ -1190,7 +1190,13 @@
     7.4      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     7.5      ;
     7.6  
     7.7 -    'code' ( 'inline' ) ? ( 'del' ) ?
     7.8 +    'code' ( 'del' ) ?
     7.9 +    ;
    7.10 +
    7.11 +    'code_unfold' ( 'del' ) ?
    7.12 +    ;
    7.13 +
    7.14 +    'code_post' ( 'del' ) ?
    7.15      ;
    7.16    \end{rail}
    7.17  
    7.18 @@ -1280,11 +1286,15 @@
    7.19    generation.  Usually packages introducing code equations provide
    7.20    a reasonable default setup for selection.
    7.21  
    7.22 -  \item @{attribute (HOL) code}~@{text inline} declares (or with
    7.23 +  \item @{attribute (HOL) code_inline} declares (or with
    7.24    option ``@{text "del"}'' removes) inlining theorems which are
    7.25    applied as rewrite rules to any code equation during
    7.26    preprocessing.
    7.27  
    7.28 +  \item @{attribute (HOL) code_post} declares (or with
    7.29 +  option ``@{text "del"}'' removes) theorems which are
    7.30 +  applied as rewrite rules to any result of an evaluation.
    7.31 +
    7.32    \item @{command (HOL) "print_codesetup"} gives an overview on
    7.33    selected code equations and code generator datatypes.
    7.34  
     8.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jul 13 19:07:05 2009 +0200
     8.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jul 14 10:56:43 2009 +0200
     8.3 @@ -1201,7 +1201,13 @@
     8.4      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     8.5      ;
     8.6  
     8.7 -    'code' ( 'inline' ) ? ( 'del' ) ?
     8.8 +    'code' ( 'del' ) ?
     8.9 +    ;
    8.10 +
    8.11 +    'code_unfold' ( 'del' ) ?
    8.12 +    ;
    8.13 +
    8.14 +    'code_post' ( 'del' ) ?
    8.15      ;
    8.16    \end{rail}
    8.17  
    8.18 @@ -1288,11 +1294,15 @@
    8.19    generation.  Usually packages introducing code equations provide
    8.20    a reasonable default setup for selection.
    8.21  
    8.22 -  \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
    8.23 +  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
    8.24    option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
    8.25    applied as rewrite rules to any code equation during
    8.26    preprocessing.
    8.27  
    8.28 +  \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
    8.29 +  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
    8.30 +  applied as rewrite rules to any result of an evaluation.
    8.31 +
    8.32    \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
    8.33    selected code equations and code generator datatypes.
    8.34  
     9.1 --- a/src/HOL/Code_Eval.thy	Mon Jul 13 19:07:05 2009 +0200
     9.2 +++ b/src/HOL/Code_Eval.thy	Tue Jul 14 10:56:43 2009 +0200
     9.3 @@ -32,7 +32,7 @@
     9.4    \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
     9.5    "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
     9.6  
     9.7 -lemma valapp_code [code, code inline]:
     9.8 +lemma valapp_code [code, code_inline]:
     9.9    "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    9.10    by (simp only: valapp_def fst_conv snd_conv)
    9.11  
    10.1 --- a/src/HOL/Code_Numeral.thy	Mon Jul 13 19:07:05 2009 +0200
    10.2 +++ b/src/HOL/Code_Numeral.thy	Tue Jul 14 10:56:43 2009 +0200
    10.3 @@ -176,16 +176,16 @@
    10.4  
    10.5  end
    10.6  
    10.7 -lemma zero_code_numeral_code [code inline, code]:
    10.8 +lemma zero_code_numeral_code [code_inline, code]:
    10.9    "(0\<Colon>code_numeral) = Numeral0"
   10.10    by (simp add: number_of_code_numeral_def Pls_def)
   10.11 -lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
   10.12 +lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
   10.13    using zero_code_numeral_code ..
   10.14  
   10.15 -lemma one_code_numeral_code [code inline, code]:
   10.16 +lemma one_code_numeral_code [code_inline, code]:
   10.17    "(1\<Colon>code_numeral) = Numeral1"
   10.18    by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
   10.19 -lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
   10.20 +lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
   10.21    using one_code_numeral_code ..
   10.22  
   10.23  lemma plus_code_numeral_code [code nbe]:
    11.1 --- a/src/HOL/Divides.thy	Mon Jul 13 19:07:05 2009 +0200
    11.2 +++ b/src/HOL/Divides.thy	Tue Jul 14 10:56:43 2009 +0200
    11.3 @@ -131,7 +131,7 @@
    11.4    note that ultimately show thesis by blast
    11.5  qed
    11.6  
    11.7 -lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
    11.8 +lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
    11.9  proof
   11.10    assume "b mod a = 0"
   11.11    with mod_div_equality [of b a] have "b div a * a = b" by simp
    12.1 --- a/src/HOL/HOL.thy	Mon Jul 13 19:07:05 2009 +0200
    12.2 +++ b/src/HOL/HOL.thy	Tue Jul 14 10:56:43 2009 +0200
    12.3 @@ -1787,7 +1787,7 @@
    12.4    assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
    12.5  begin
    12.6  
    12.7 -lemma eq [code unfold, code inline del]: "eq = (op =)"
    12.8 +lemma eq [code_unfold, code_inline del]: "eq = (op =)"
    12.9    by (rule ext eq_equals)+
   12.10  
   12.11  lemma eq_refl: "eq x x \<longleftrightarrow> True"
   12.12 @@ -1796,7 +1796,7 @@
   12.13  lemma equals_eq: "(op =) \<equiv> eq"
   12.14    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
   12.15  
   12.16 -declare equals_eq [symmetric, code post]
   12.17 +declare equals_eq [symmetric, code_post]
   12.18  
   12.19  end
   12.20  
   12.21 @@ -1847,7 +1847,7 @@
   12.22  
   12.23  lemmas [code] = Let_def if_True if_False
   12.24  
   12.25 -lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
   12.26 +lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
   12.27  
   12.28  instantiation itself :: (type) eq
   12.29  begin
    13.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 13 19:07:05 2009 +0200
    13.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 14 10:56:43 2009 +0200
    13.3 @@ -283,7 +283,7 @@
    13.4  where
    13.5    [code del]: "raise_exc e = raise []"
    13.6  
    13.7 -lemma raise_raise_exc [code, code inline]:
    13.8 +lemma raise_raise_exc [code, code_inline]:
    13.9    "raise s = raise_exc (Fail (STR s))"
   13.10    unfolding Fail_def raise_exc_def raise_def ..
   13.11  
    14.1 --- a/src/HOL/Int.thy	Mon Jul 13 19:07:05 2009 +0200
    14.2 +++ b/src/HOL/Int.thy	Tue Jul 14 10:56:43 2009 +0200
    14.3 @@ -650,11 +650,11 @@
    14.4  
    14.5  text {* Removal of leading zeroes *}
    14.6  
    14.7 -lemma Bit0_Pls [simp, code post]:
    14.8 +lemma Bit0_Pls [simp, code_post]:
    14.9    "Bit0 Pls = Pls"
   14.10    unfolding numeral_simps by simp
   14.11  
   14.12 -lemma Bit1_Min [simp, code post]:
   14.13 +lemma Bit1_Min [simp, code_post]:
   14.14    "Bit1 Min = Min"
   14.15    unfolding numeral_simps by simp
   14.16  
   14.17 @@ -2126,11 +2126,11 @@
   14.18  
   14.19  hide (open) const nat_aux
   14.20  
   14.21 -lemma zero_is_num_zero [code, code inline, symmetric, code post]:
   14.22 +lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
   14.23    "(0\<Colon>int) = Numeral0" 
   14.24    by simp
   14.25  
   14.26 -lemma one_is_num_one [code, code inline, symmetric, code post]:
   14.27 +lemma one_is_num_one [code, code_inline, symmetric, code_post]:
   14.28    "(1\<Colon>int) = Numeral1" 
   14.29    by simp
   14.30  
    15.1 --- a/src/HOL/IntDiv.thy	Mon Jul 13 19:07:05 2009 +0200
    15.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 14 10:56:43 2009 +0200
    15.3 @@ -36,7 +36,7 @@
    15.4  
    15.5  text{*algorithm for the general case @{term "b\<noteq>0"}*}
    15.6  definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
    15.7 -  [code inline]: "negateSnd = apsnd uminus"
    15.8 +  [code_inline]: "negateSnd = apsnd uminus"
    15.9  
   15.10  definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
   15.11      --{*The full division algorithm considers all possible signs for a, b
    16.1 --- a/src/HOL/Library/Code_Char_chr.thy	Mon Jul 13 19:07:05 2009 +0200
    16.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 10:56:43 2009 +0200
    16.3 @@ -24,11 +24,11 @@
    16.4  
    16.5  lemmas [code del] = char.recs char.cases char.size
    16.6  
    16.7 -lemma [code, code inline]:
    16.8 +lemma [code, code_inline]:
    16.9    "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
   16.10    by (cases c) (auto simp add: nibble_pair_of_nat_char)
   16.11  
   16.12 -lemma [code, code inline]:
   16.13 +lemma [code, code_inline]:
   16.14    "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
   16.15    by (cases c) (auto simp add: nibble_pair_of_nat_char)
   16.16  
    17.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 13 19:07:05 2009 +0200
    17.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 10:56:43 2009 +0200
    17.3 @@ -26,15 +26,15 @@
    17.4  
    17.5  code_datatype number_nat_inst.number_of_nat
    17.6  
    17.7 -lemma zero_nat_code [code, code inline]:
    17.8 +lemma zero_nat_code [code, code_inline]:
    17.9    "0 = (Numeral0 :: nat)"
   17.10    by simp
   17.11 -lemmas [code post] = zero_nat_code [symmetric]
   17.12 +lemmas [code_post] = zero_nat_code [symmetric]
   17.13  
   17.14 -lemma one_nat_code [code, code inline]:
   17.15 +lemma one_nat_code [code, code_inline]:
   17.16    "1 = (Numeral1 :: nat)"
   17.17    by simp
   17.18 -lemmas [code post] = one_nat_code [symmetric]
   17.19 +lemmas [code_post] = one_nat_code [symmetric]
   17.20  
   17.21  lemma Suc_code [code]:
   17.22    "Suc n = n + 1"
   17.23 @@ -89,7 +89,7 @@
   17.24    expression:
   17.25  *}
   17.26  
   17.27 -lemma [code, code unfold]:
   17.28 +lemma [code, code_unfold]:
   17.29    "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
   17.30    by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
   17.31  
   17.32 @@ -302,7 +302,7 @@
   17.33    Natural numerals.
   17.34  *}
   17.35  
   17.36 -lemma [code inline, symmetric, code post]:
   17.37 +lemma [code_inline, symmetric, code_post]:
   17.38    "nat (number_of i) = number_nat_inst.number_of_nat i"
   17.39    -- {* this interacts as desired with @{thm nat_number_of_def} *}
   17.40    by (simp add: number_nat_inst.number_of_nat)
   17.41 @@ -335,9 +335,9 @@
   17.42    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   17.43    unfolding nat_number_of_def number_of_is_id neg_def by simp
   17.44  
   17.45 -lemma of_nat_int [code unfold]:
   17.46 +lemma of_nat_int [code_unfold]:
   17.47    "of_nat = int" by (simp add: int_def)
   17.48 -declare of_nat_int [symmetric, code post]
   17.49 +declare of_nat_int [symmetric, code_post]
   17.50  
   17.51  code_const int
   17.52    (SML "_")
    18.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Jul 13 19:07:05 2009 +0200
    18.2 +++ b/src/HOL/Library/Executable_Set.thy	Tue Jul 14 10:56:43 2009 +0200
    18.3 @@ -15,7 +15,7 @@
    18.4  definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    18.5    "subset = op \<le>"
    18.6  
    18.7 -declare subset_def [symmetric, code unfold]
    18.8 +declare subset_def [symmetric, code_unfold]
    18.9  
   18.10  lemma [code]:
   18.11    "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   18.12 @@ -25,7 +25,7 @@
   18.13    [code del]: "eq_set = op ="
   18.14  
   18.15  (* FIXME allow for Stefan's code generator:
   18.16 -declare set_eq_subset[code unfold]
   18.17 +declare set_eq_subset[code_unfold]
   18.18  *)
   18.19  
   18.20  lemma [code]:
   18.21 @@ -40,7 +40,7 @@
   18.22  
   18.23  subsection {* Rewrites for primitive operations *}
   18.24  
   18.25 -declare List_Set.project_def [symmetric, code unfold]
   18.26 +declare List_Set.project_def [symmetric, code_unfold]
   18.27  
   18.28  
   18.29  subsection {* code generator setup *}
    19.1 --- a/src/HOL/Library/Float.thy	Mon Jul 13 19:07:05 2009 +0200
    19.2 +++ b/src/HOL/Library/Float.thy	Tue Jul 14 10:56:43 2009 +0200
    19.3 @@ -19,7 +19,7 @@
    19.4    "of_float (Float a b) = real a * pow2 b"
    19.5  
    19.6  defs (overloaded)
    19.7 -  real_of_float_def [code unfold]: "real == of_float"
    19.8 +  real_of_float_def [code_unfold]: "real == of_float"
    19.9  
   19.10  primrec mantissa :: "float \<Rightarrow> int" where
   19.11    "mantissa (Float a b) = a"
   19.12 @@ -42,7 +42,7 @@
   19.13  instance ..
   19.14  end
   19.15  
   19.16 -lemma number_of_float_Float [code inline, symmetric, code post]:
   19.17 +lemma number_of_float_Float [code_inline, symmetric, code_post]:
   19.18    "number_of k = Float (number_of k) 0"
   19.19    by (simp add: number_of_float_def number_of_is_id)
   19.20  
    20.1 --- a/src/HOL/Library/Fraction_Field.thy	Mon Jul 13 19:07:05 2009 +0200
    20.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Jul 14 10:56:43 2009 +0200
    20.3 @@ -93,10 +93,10 @@
    20.4  begin
    20.5  
    20.6  definition
    20.7 -  Zero_fract_def [code, code unfold]: "0 = Fract 0 1"
    20.8 +  Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
    20.9  
   20.10  definition
   20.11 -  One_fract_def [code, code unfold]: "1 = Fract 1 1"
   20.12 +  One_fract_def [code, code_unfold]: "1 = Fract 1 1"
   20.13  
   20.14  definition
   20.15    add_fract_def [code del]:
   20.16 @@ -196,14 +196,14 @@
   20.17  lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
   20.18    by (rule of_nat_fract [symmetric])
   20.19  
   20.20 -lemma fract_collapse [code post]:
   20.21 +lemma fract_collapse [code_post]:
   20.22    "Fract 0 k = 0"
   20.23    "Fract 1 1 = 1"
   20.24    "Fract k 0 = 0"
   20.25    by (cases "k = 0")
   20.26      (simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def)
   20.27  
   20.28 -lemma fract_expand [code unfold]:
   20.29 +lemma fract_expand [code_unfold]:
   20.30    "0 = Fract 0 1"
   20.31    "1 = Fract 1 1"
   20.32    by (simp_all add: fract_collapse)
    21.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Jul 13 19:07:05 2009 +0200
    21.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 10:56:43 2009 +0200
    21.3 @@ -40,10 +40,10 @@
    21.4    "0 = Fin 0"
    21.5  
    21.6  definition
    21.7 -  [code inline]: "1 = Fin 1"
    21.8 +  [code_inline]: "1 = Fin 1"
    21.9  
   21.10  definition
   21.11 -  [code inline, code del]: "number_of k = Fin (number_of k)"
   21.12 +  [code_inline, code del]: "number_of k = Fin (number_of k)"
   21.13  
   21.14  instance ..
   21.15  
    22.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jul 13 19:07:05 2009 +0200
    22.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Jul 14 10:56:43 2009 +0200
    22.3 @@ -1505,7 +1505,7 @@
    22.4  
    22.5  code_datatype "0::'a::zero poly" pCons
    22.6  
    22.7 -declare pCons_0_0 [code post]
    22.8 +declare pCons_0_0 [code_post]
    22.9  
   22.10  instantiation poly :: ("{zero,eq}") eq
   22.11  begin
    23.1 --- a/src/HOL/List.thy	Mon Jul 13 19:07:05 2009 +0200
    23.2 +++ b/src/HOL/List.thy	Tue Jul 14 10:56:43 2009 +0200
    23.3 @@ -2076,7 +2076,7 @@
    23.4  by(induct xs) simp_all
    23.5  
    23.6  text{* For efficient code generation: avoid intermediate list. *}
    23.7 -lemma foldl_map[code unfold]:
    23.8 +lemma foldl_map[code_unfold]:
    23.9    "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
   23.10  by(induct xs arbitrary:a) simp_all
   23.11  
   23.12 @@ -2198,7 +2198,7 @@
   23.13  
   23.14  text{* For efficient code generation ---
   23.15         @{const listsum} is not tail recursive but @{const foldl} is. *}
   23.16 -lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
   23.17 +lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
   23.18  by(simp add:listsum_foldr foldl_foldr1)
   23.19  
   23.20  lemma distinct_listsum_conv_Setsum:
   23.21 @@ -3746,32 +3746,32 @@
   23.22    show ?case by (induct xs) (auto simp add: Cons aux)
   23.23  qed
   23.24  
   23.25 -lemma mem_iff [code post]:
   23.26 +lemma mem_iff [code_post]:
   23.27    "x mem xs \<longleftrightarrow> x \<in> set xs"
   23.28  by (induct xs) auto
   23.29  
   23.30 -lemmas in_set_code [code unfold] = mem_iff [symmetric]
   23.31 +lemmas in_set_code [code_unfold] = mem_iff [symmetric]
   23.32  
   23.33  lemma empty_null:
   23.34    "xs = [] \<longleftrightarrow> null xs"
   23.35  by (cases xs) simp_all
   23.36  
   23.37 -lemma [code inline]:
   23.38 +lemma [code_inline]:
   23.39    "eq_class.eq xs [] \<longleftrightarrow> null xs"
   23.40  by (simp add: eq empty_null)
   23.41  
   23.42 -lemmas null_empty [code post] =
   23.43 +lemmas null_empty [code_post] =
   23.44    empty_null [symmetric]
   23.45  
   23.46  lemma list_inter_conv:
   23.47    "set (list_inter xs ys) = set xs \<inter> set ys"
   23.48  by (induct xs) auto
   23.49  
   23.50 -lemma list_all_iff [code post]:
   23.51 +lemma list_all_iff [code_post]:
   23.52    "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
   23.53  by (induct xs) auto
   23.54  
   23.55 -lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
   23.56 +lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
   23.57  
   23.58  lemma list_all_append [simp]:
   23.59    "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
   23.60 @@ -3785,11 +3785,11 @@
   23.61    "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
   23.62    unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
   23.63  
   23.64 -lemma list_ex_iff [code post]:
   23.65 +lemma list_ex_iff [code_post]:
   23.66    "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
   23.67  by (induct xs) simp_all
   23.68  
   23.69 -lemmas list_bex_code [code unfold] =
   23.70 +lemmas list_bex_code [code_unfold] =
   23.71    list_ex_iff [symmetric]
   23.72  
   23.73  lemma list_ex_length:
   23.74 @@ -3804,7 +3804,7 @@
   23.75    "map_filter f P xs = map f (filter P xs)"
   23.76  by (induct xs) auto
   23.77  
   23.78 -lemma length_remdups_length_unique [code inline]:
   23.79 +lemma length_remdups_length_unique [code_inline]:
   23.80    "length (remdups xs) = length_unique xs"
   23.81    by (induct xs) simp_all
   23.82  
   23.83 @@ -3813,43 +3813,43 @@
   23.84  
   23.85  text {* Code for bounded quantification and summation over nats. *}
   23.86  
   23.87 -lemma atMost_upto [code unfold]:
   23.88 +lemma atMost_upto [code_unfold]:
   23.89    "{..n} = set [0..<Suc n]"
   23.90  by auto
   23.91  
   23.92 -lemma atLeast_upt [code unfold]:
   23.93 +lemma atLeast_upt [code_unfold]:
   23.94    "{..<n} = set [0..<n]"
   23.95  by auto
   23.96  
   23.97 -lemma greaterThanLessThan_upt [code unfold]:
   23.98 +lemma greaterThanLessThan_upt [code_unfold]:
   23.99    "{n<..<m} = set [Suc n..<m]"
  23.100  by auto
  23.101  
  23.102 -lemma atLeastLessThan_upt [code unfold]:
  23.103 +lemma atLeastLessThan_upt [code_unfold]:
  23.104    "{n..<m} = set [n..<m]"
  23.105  by auto
  23.106  
  23.107 -lemma greaterThanAtMost_upt [code unfold]:
  23.108 +lemma greaterThanAtMost_upt [code_unfold]:
  23.109    "{n<..m} = set [Suc n..<Suc m]"
  23.110  by auto
  23.111  
  23.112 -lemma atLeastAtMost_upt [code unfold]:
  23.113 +lemma atLeastAtMost_upt [code_unfold]:
  23.114    "{n..m} = set [n..<Suc m]"
  23.115  by auto
  23.116  
  23.117 -lemma all_nat_less_eq [code unfold]:
  23.118 +lemma all_nat_less_eq [code_unfold]:
  23.119    "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
  23.120  by auto
  23.121  
  23.122 -lemma ex_nat_less_eq [code unfold]:
  23.123 +lemma ex_nat_less_eq [code_unfold]:
  23.124    "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
  23.125  by auto
  23.126  
  23.127 -lemma all_nat_less [code unfold]:
  23.128 +lemma all_nat_less [code_unfold]:
  23.129    "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
  23.130  by auto
  23.131  
  23.132 -lemma ex_nat_less [code unfold]:
  23.133 +lemma ex_nat_less [code_unfold]:
  23.134    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
  23.135  by auto
  23.136  
  23.137 @@ -3857,30 +3857,30 @@
  23.138    "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
  23.139  by (induct xs) simp_all
  23.140  
  23.141 -lemma setsum_set_upt_conv_listsum [code unfold]:
  23.142 +lemma setsum_set_upt_conv_listsum [code_unfold]:
  23.143    "setsum f (set [m..<n]) = listsum (map f [m..<n])"
  23.144  by (rule setsum_set_distinct_conv_listsum) simp
  23.145  
  23.146  
  23.147  text {* Code for summation over ints. *}
  23.148  
  23.149 -lemma greaterThanLessThan_upto [code unfold]:
  23.150 +lemma greaterThanLessThan_upto [code_unfold]:
  23.151    "{i<..<j::int} = set [i+1..j - 1]"
  23.152  by auto
  23.153  
  23.154 -lemma atLeastLessThan_upto [code unfold]:
  23.155 +lemma atLeastLessThan_upto [code_unfold]:
  23.156    "{i..<j::int} = set [i..j - 1]"
  23.157  by auto
  23.158  
  23.159 -lemma greaterThanAtMost_upto [code unfold]:
  23.160 +lemma greaterThanAtMost_upto [code_unfold]:
  23.161    "{i<..j::int} = set [i+1..j]"
  23.162  by auto
  23.163  
  23.164 -lemma atLeastAtMost_upto [code unfold]:
  23.165 +lemma atLeastAtMost_upto [code_unfold]:
  23.166    "{i..j::int} = set [i..j]"
  23.167  by auto
  23.168  
  23.169 -lemma setsum_set_upto_conv_listsum [code unfold]:
  23.170 +lemma setsum_set_upto_conv_listsum [code_unfold]:
  23.171    "setsum f (set [i..j::int]) = listsum (map f [i..j])"
  23.172  by (rule setsum_set_distinct_conv_listsum) simp
  23.173  
    24.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Jul 13 19:07:05 2009 +0200
    24.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Jul 14 10:56:43 2009 +0200
    24.3 @@ -467,7 +467,7 @@
    24.4  
    24.5  lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
    24.6  
    24.7 -lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
    24.8 +lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
    24.9  
   24.10  code_module BV
   24.11  contains
    25.1 --- a/src/HOL/Nat.thy	Mon Jul 13 19:07:05 2009 +0200
    25.2 +++ b/src/HOL/Nat.thy	Tue Jul 14 10:56:43 2009 +0200
    25.3 @@ -1200,9 +1200,9 @@
    25.4  text {* for code generation *}
    25.5  
    25.6  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    25.7 -  funpow_code_def [code post]: "funpow = compow"
    25.8 +  funpow_code_def [code_post]: "funpow = compow"
    25.9  
   25.10 -lemmas [code unfold] = funpow_code_def [symmetric]
   25.11 +lemmas [code_unfold] = funpow_code_def [symmetric]
   25.12  
   25.13  lemma [code]:
   25.14    "funpow 0 f = id"
   25.15 @@ -1265,7 +1265,7 @@
   25.16  
   25.17  end
   25.18  
   25.19 -declare of_nat_code [code, code unfold, code inline del]
   25.20 +declare of_nat_code [code, code_unfold, code_inline del]
   25.21  
   25.22  text{*Class for unital semirings with characteristic zero.
   25.23   Includes non-ordered rings like the complex numbers.*}
    26.1 --- a/src/HOL/Nat_Numeral.thy	Mon Jul 13 19:07:05 2009 +0200
    26.2 +++ b/src/HOL/Nat_Numeral.thy	Tue Jul 14 10:56:43 2009 +0200
    26.3 @@ -20,13 +20,13 @@
    26.4  begin
    26.5  
    26.6  definition
    26.7 -  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
    26.8 +  nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
    26.9  
   26.10  instance ..
   26.11  
   26.12  end
   26.13  
   26.14 -lemma [code post]:
   26.15 +lemma [code_post]:
   26.16    "nat (number_of v) = number_of v"
   26.17    unfolding nat_number_of_def ..
   26.18  
   26.19 @@ -316,13 +316,13 @@
   26.20  lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
   26.21  by (simp add: nat_number_of_def)
   26.22  
   26.23 -lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
   26.24 +lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
   26.25  by (simp add: nat_number_of_def)
   26.26  
   26.27  lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
   26.28  by (simp add: nat_1 nat_number_of_def)
   26.29  
   26.30 -lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
   26.31 +lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
   26.32  by (simp add: nat_numeral_1_eq_1)
   26.33  
   26.34  
    27.1 --- a/src/HOL/Option.thy	Mon Jul 13 19:07:05 2009 +0200
    27.2 +++ b/src/HOL/Option.thy	Tue Jul 14 10:56:43 2009 +0200
    27.3 @@ -94,7 +94,7 @@
    27.4  subsubsection {* Code generator setup *}
    27.5  
    27.6  definition is_none :: "'a option \<Rightarrow> bool" where
    27.7 -  [code post]: "is_none x \<longleftrightarrow> x = None"
    27.8 +  [code_post]: "is_none x \<longleftrightarrow> x = None"
    27.9  
   27.10  lemma is_none_code [code]:
   27.11    shows "is_none None \<longleftrightarrow> True"
   27.12 @@ -105,7 +105,7 @@
   27.13    "is_none x \<longleftrightarrow> x = None"
   27.14    by (simp add: is_none_def)
   27.15  
   27.16 -lemma [code inline]:
   27.17 +lemma [code_inline]:
   27.18    "eq_class.eq x None \<longleftrightarrow> is_none x"
   27.19    by (simp add: eq is_none_none)
   27.20  
    28.1 --- a/src/HOL/Orderings.thy	Mon Jul 13 19:07:05 2009 +0200
    28.2 +++ b/src/HOL/Orderings.thy	Tue Jul 14 10:56:43 2009 +0200
    28.3 @@ -268,13 +268,13 @@
    28.4  
    28.5  text {* Explicit dictionaries for code generation *}
    28.6  
    28.7 -lemma min_ord_min [code, code unfold, code inline del]:
    28.8 +lemma min_ord_min [code, code_unfold, code_inline del]:
    28.9    "min = ord.min (op \<le>)"
   28.10    by (rule ext)+ (simp add: min_def ord.min_def)
   28.11  
   28.12  declare ord.min_def [code]
   28.13  
   28.14 -lemma max_ord_max [code, code unfold, code inline del]:
   28.15 +lemma max_ord_max [code, code_unfold, code_inline del]:
   28.16    "max = ord.max (op \<le>)"
   28.17    by (rule ext)+ (simp add: max_def ord.max_def)
   28.18  
    29.1 --- a/src/HOL/Power.thy	Mon Jul 13 19:07:05 2009 +0200
    29.2 +++ b/src/HOL/Power.thy	Tue Jul 14 10:56:43 2009 +0200
    29.3 @@ -455,7 +455,7 @@
    29.4  
    29.5  subsection {* Code generator tweak *}
    29.6  
    29.7 -lemma power_power_power [code, code unfold, code inline del]:
    29.8 +lemma power_power_power [code, code_unfold, code_inline del]:
    29.9    "power = power.power (1::'a::{power}) (op *)"
   29.10    unfolding power_def power.power_def ..
   29.11  
    30.1 --- a/src/HOL/Rational.thy	Mon Jul 13 19:07:05 2009 +0200
    30.2 +++ b/src/HOL/Rational.thy	Tue Jul 14 10:56:43 2009 +0200
    30.3 @@ -93,10 +93,10 @@
    30.4  begin
    30.5  
    30.6  definition
    30.7 -  Zero_rat_def [code, code unfold]: "0 = Fract 0 1"
    30.8 +  Zero_rat_def [code, code_unfold]: "0 = Fract 0 1"
    30.9  
   30.10  definition
   30.11 -  One_rat_def [code, code unfold]: "1 = Fract 1 1"
   30.12 +  One_rat_def [code, code_unfold]: "1 = Fract 1 1"
   30.13  
   30.14  definition
   30.15    add_rat_def [code del]:
   30.16 @@ -211,7 +211,7 @@
   30.17  
   30.18  end
   30.19  
   30.20 -lemma rat_number_collapse [code post]:
   30.21 +lemma rat_number_collapse [code_post]:
   30.22    "Fract 0 k = 0"
   30.23    "Fract 1 1 = 1"
   30.24    "Fract (number_of k) 1 = number_of k"
   30.25 @@ -219,7 +219,7 @@
   30.26    by (cases "k = 0")
   30.27      (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
   30.28  
   30.29 -lemma rat_number_expand [code unfold]:
   30.30 +lemma rat_number_expand [code_unfold]:
   30.31    "0 = Fract 0 1"
   30.32    "1 = Fract 1 1"
   30.33    "number_of k = Fract (number_of k) 1"
   30.34 @@ -291,11 +291,11 @@
   30.35  lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
   30.36    by (simp add: Fract_of_int_eq [symmetric])
   30.37  
   30.38 -lemma Fract_number_of_quotient [code post]:
   30.39 +lemma Fract_number_of_quotient [code_post]:
   30.40    "Fract (number_of k) (number_of l) = number_of k / number_of l"
   30.41    unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
   30.42  
   30.43 -lemma Fract_1_number_of [code post]:
   30.44 +lemma Fract_1_number_of [code_post]:
   30.45    "Fract 1 (number_of k) = 1 / number_of k"
   30.46    unfolding Fract_of_int_quotient number_of_eq by simp
   30.47  
   30.48 @@ -1003,7 +1003,7 @@
   30.49  
   30.50  definition (in term_syntax)
   30.51    valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
   30.52 -  [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
   30.53 +  [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
   30.54  
   30.55  notation fcomp (infixl "o>" 60)
   30.56  notation scomp (infixl "o\<rightarrow>" 60)
    31.1 --- a/src/HOL/RealDef.thy	Mon Jul 13 19:07:05 2009 +0200
    31.2 +++ b/src/HOL/RealDef.thy	Tue Jul 14 10:56:43 2009 +0200
    31.3 @@ -559,8 +559,8 @@
    31.4    real :: "'a => real"
    31.5  
    31.6  defs (overloaded)
    31.7 -  real_of_nat_def [code unfold]: "real == real_of_nat"
    31.8 -  real_of_int_def [code unfold]: "real == real_of_int"
    31.9 +  real_of_nat_def [code_unfold]: "real == real_of_nat"
   31.10 +  real_of_int_def [code_unfold]: "real == real_of_int"
   31.11  
   31.12  lemma real_eq_of_nat: "real = of_nat"
   31.13    unfolding real_of_nat_def ..
   31.14 @@ -946,7 +946,7 @@
   31.15  
   31.16  end
   31.17  
   31.18 -lemma [code unfold, symmetric, code post]:
   31.19 +lemma [code_unfold, symmetric, code_post]:
   31.20    "number_of k = real_of_int (number_of k)"
   31.21    unfolding number_of_is_id real_number_of_def ..
   31.22  
   31.23 @@ -1061,29 +1061,29 @@
   31.24  
   31.25  code_datatype Ratreal
   31.26  
   31.27 -lemma Ratreal_number_collapse [code post]:
   31.28 +lemma Ratreal_number_collapse [code_post]:
   31.29    "Ratreal 0 = 0"
   31.30    "Ratreal 1 = 1"
   31.31    "Ratreal (number_of k) = number_of k"
   31.32  by simp_all
   31.33  
   31.34 -lemma zero_real_code [code, code unfold]:
   31.35 +lemma zero_real_code [code, code_unfold]:
   31.36    "0 = Ratreal 0"
   31.37  by simp
   31.38  
   31.39 -lemma one_real_code [code, code unfold]:
   31.40 +lemma one_real_code [code, code_unfold]:
   31.41    "1 = Ratreal 1"
   31.42  by simp
   31.43  
   31.44 -lemma number_of_real_code [code unfold]:
   31.45 +lemma number_of_real_code [code_unfold]:
   31.46    "number_of k = Ratreal (number_of k)"
   31.47  by simp
   31.48  
   31.49 -lemma Ratreal_number_of_quotient [code post]:
   31.50 +lemma Ratreal_number_of_quotient [code_post]:
   31.51    "Ratreal (number_of r) / Ratreal (number_of s) = number_of r / number_of s"
   31.52  by simp
   31.53  
   31.54 -lemma Ratreal_number_of_quotient2 [code post]:
   31.55 +lemma Ratreal_number_of_quotient2 [code_post]:
   31.56    "Ratreal (number_of r / number_of s) = number_of r / number_of s"
   31.57  unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
   31.58  
   31.59 @@ -1129,7 +1129,7 @@
   31.60  
   31.61  definition (in term_syntax)
   31.62    valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
   31.63 -  [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
   31.64 +  [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
   31.65  
   31.66  notation fcomp (infixl "o>" 60)
   31.67  notation scomp (infixl "o\<rightarrow>" 60)
    32.1 --- a/src/HOL/SetInterval.thy	Mon Jul 13 19:07:05 2009 +0200
    32.2 +++ b/src/HOL/SetInterval.thy	Tue Jul 14 10:56:43 2009 +0200
    32.3 @@ -284,8 +284,8 @@
    32.4  lemma atLeast0AtMost: "{0..n::nat} = {..n}"
    32.5  by(simp add:atMost_def atLeastAtMost_def)
    32.6  
    32.7 -declare atLeast0LessThan[symmetric, code unfold]
    32.8 -        atLeast0AtMost[symmetric, code unfold]
    32.9 +declare atLeast0LessThan[symmetric, code_unfold]
   32.10 +        atLeast0AtMost[symmetric, code_unfold]
   32.11  
   32.12  lemma atLeastLessThan0: "{m..<0::nat} = {}"
   32.13  by (simp add: atLeastLessThan_def)
    33.1 --- a/src/HOL/String.thy	Mon Jul 13 19:07:05 2009 +0200
    33.2 +++ b/src/HOL/String.thy	Tue Jul 14 10:56:43 2009 +0200
    33.3 @@ -58,11 +58,11 @@
    33.4  end
    33.5  *}
    33.6  
    33.7 -lemma char_case_nibble_pair [code, code inline]:
    33.8 +lemma char_case_nibble_pair [code, code_inline]:
    33.9    "char_case f = split f o nibble_pair_of_char"
   33.10    by (simp add: expand_fun_eq split: char.split)
   33.11  
   33.12 -lemma char_rec_nibble_pair [code, code inline]:
   33.13 +lemma char_rec_nibble_pair [code, code_inline]:
   33.14    "char_rec f = split f o nibble_pair_of_char"
   33.15    unfolding char_case_nibble_pair [symmetric]
   33.16    by (simp add: expand_fun_eq split: char.split)
    34.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Jul 13 19:07:05 2009 +0200
    34.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jul 14 10:56:43 2009 +0200
    34.3 @@ -697,7 +697,8 @@
    34.4  
    34.5  val setup =
    34.6    add_codegen "inductive" inductive_codegen #>
    34.7 -  Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
    34.8 -    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
    34.9 +  Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
   34.10 +    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
   34.11 +    "introduction rules for executable predicates";
   34.12  
   34.13  end;
    35.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Jul 13 19:07:05 2009 +0200
    35.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Jul 14 10:56:43 2009 +0200
    35.3 @@ -541,8 +541,9 @@
    35.4      "declare rules for converting between predicate and set notation" #>
    35.5    Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
    35.6    Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
    35.7 -  Code.add_attribute ("ind_set",
    35.8 -    Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
    35.9 +  Attrib.setup @{binding code_ind_set}
   35.10 +    (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
   35.11 +    "introduction rules for executable predicates" #>
   35.12    Codegen.add_preprocessor codegen_preproc #>
   35.13    Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
   35.14      "declaration of monotonicity rule for set operators" #>
    36.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon Jul 13 19:07:05 2009 +0200
    36.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jul 14 10:56:43 2009 +0200
    36.3 @@ -23,15 +23,13 @@
    36.4    fun merge _ = Symtab.merge (K true);
    36.5  );
    36.6  
    36.7 -fun add_thm NONE thm thy = Code.add_eqn thm thy
    36.8 -  | add_thm (SOME module_name) thm thy =
    36.9 -      let
   36.10 -        val (thm', _) = Code.mk_eqn thy (thm, true)
   36.11 -      in
   36.12 -        thy
   36.13 -        |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
   36.14 -        |> Code.add_eqn thm'
   36.15 -      end;
   36.16 +fun add_thm_target module_name thm thy =
   36.17 +  let
   36.18 +    val (thm', _) = Code.mk_eqn thy (thm, true)
   36.19 +  in
   36.20 +    thy
   36.21 +    |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
   36.22 +  end;
   36.23  
   36.24  fun expand_eta thy [] = []
   36.25    | expand_eta thy (thms as thm :: _) =
   36.26 @@ -163,15 +161,8 @@
   36.27          end)
   36.28    | _ => NONE);
   36.29  
   36.30 -val setup = let
   36.31 -  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
   36.32 -    (add_thm opt_module thm) I);
   36.33 -  val del = Thm.declaration_attribute (fn thm => Context.mapping
   36.34 -    (Code.del_eqn thm) I);
   36.35 -in
   36.36 +val setup = 
   36.37    add_codegen "recfun" recfun_codegen
   36.38 -  #> Code.add_attribute ("", Args.del |-- Scan.succeed del
   36.39 -     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
   36.40 -end;
   36.41 +  #> Code.set_code_target_attr add_thm_target;
   36.42  
   36.43  end;
    37.1 --- a/src/HOL/ex/Numeral.thy	Mon Jul 13 19:07:05 2009 +0200
    37.2 +++ b/src/HOL/ex/Numeral.thy	Tue Jul 14 10:56:43 2009 +0200
    37.3 @@ -751,14 +751,14 @@
    37.4  subsection {* Code generator setup for @{typ int} *}
    37.5  
    37.6  definition Pls :: "num \<Rightarrow> int" where
    37.7 -  [simp, code post]: "Pls n = of_num n"
    37.8 +  [simp, code_post]: "Pls n = of_num n"
    37.9  
   37.10  definition Mns :: "num \<Rightarrow> int" where
   37.11 -  [simp, code post]: "Mns n = - of_num n"
   37.12 +  [simp, code_post]: "Mns n = - of_num n"
   37.13  
   37.14  code_datatype "0::int" Pls Mns
   37.15  
   37.16 -lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
   37.17 +lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
   37.18  
   37.19  definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   37.20    [simp, code del]: "sub m n = (of_num m - of_num n)"
   37.21 @@ -874,10 +874,10 @@
   37.22    using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   37.23    by (simp_all add: of_num_less_iff)
   37.24  
   37.25 -lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp
   37.26 -lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp
   37.27 -declare zero_is_num_zero [code inline del]
   37.28 -declare one_is_num_one [code inline del]
   37.29 +lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
   37.30 +lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
   37.31 +declare zero_is_num_zero [code_inline del]
   37.32 +declare one_is_num_one [code_inline del]
   37.33  
   37.34  hide (open) const sub dup
   37.35  
    38.1 --- a/src/Pure/Isar/code.ML	Mon Jul 13 19:07:05 2009 +0200
    38.2 +++ b/src/Pure/Isar/code.ML	Tue Jul 14 10:56:43 2009 +0200
    38.3 @@ -62,7 +62,7 @@
    38.4    val print_codesetup: theory -> unit
    38.5  
    38.6    (*infrastructure*)
    38.7 -  val add_attribute: string * attribute parser -> theory -> theory
    38.8 +  val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
    38.9    val purge_data: theory -> theory
   38.10  end;
   38.11  
   38.12 @@ -235,31 +235,6 @@
   38.13    end;
   38.14  
   38.15  
   38.16 -(** code attributes **)
   38.17 -
   38.18 -structure Code_Attr = TheoryDataFun (
   38.19 -  type T = (string * attribute parser) list;
   38.20 -  val empty = [];
   38.21 -  val copy = I;
   38.22 -  val extend = I;
   38.23 -  fun merge _ = AList.merge (op = : string * string -> bool) (K true);
   38.24 -);
   38.25 -
   38.26 -fun add_attribute (attr as (name, _)) =
   38.27 -  let
   38.28 -    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
   38.29 -      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
   38.30 -  in Code_Attr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
   38.31 -    then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
   38.32 -  end;
   38.33 -
   38.34 -val _ = Context.>> (Context.map_theory
   38.35 -  (Attrib.setup (Binding.name "code")
   38.36 -    (Scan.peek (fn context =>
   38.37 -      List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context)))))
   38.38 -    "declare theorems for code generation"));
   38.39 -
   38.40 -
   38.41  (** data store **)
   38.42  
   38.43  (* code equations *)
   38.44 @@ -543,7 +518,7 @@
   38.45        in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
   38.46      fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
   38.47        let
   38.48 -        val _ = if tyco' <> tyco
   38.49 +        val _ = if (tyco' : string) <> tyco
   38.50            then error "Different type constructors in constructor set"
   38.51            else ();
   38.52          val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
   38.53 @@ -911,18 +886,32 @@
   38.54   of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   38.55    | NONE => thy;
   38.56  
   38.57 +structure Code_Attr = TheoryDataFun (
   38.58 +  type T = (string -> thm -> theory -> theory) option;
   38.59 +  val empty = NONE;
   38.60 +  val copy = I;
   38.61 +  val extend = I;
   38.62 +  fun merge _ (NONE, f2) = f2
   38.63 +    | merge _ (f1, _) = f1;
   38.64 +);
   38.65 +
   38.66 +fun set_code_target_attr f = Code_Attr.map (K (SOME f));
   38.67 +
   38.68  val _ = Context.>> (Context.map_theory
   38.69    (let
   38.70      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   38.71 -    fun add_simple_attribute (name, f) =
   38.72 -      add_attribute (name, Scan.succeed (mk_attribute f));
   38.73 -    fun add_del_attribute (name, (add, del)) =
   38.74 -      add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
   38.75 -        || Scan.succeed (mk_attribute add))
   38.76 +    val code_attribute_parser =
   38.77 +      Args.del |-- Scan.succeed (mk_attribute del_eqn)
   38.78 +      || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
   38.79 +      || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
   38.80 +           (fn prefix => mk_attribute (fn thm => fn thy => thy
   38.81 +             |> add_warning_eqn thm
   38.82 +             |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
   38.83 +      || Scan.succeed (mk_attribute add_warning_eqn);
   38.84    in
   38.85      Type_Interpretation.init
   38.86 -    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
   38.87 -    #> add_simple_attribute ("nbe", add_nbe_eqn)
   38.88 +    #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
   38.89 +        "declare theorems for code generation"
   38.90    end));
   38.91  
   38.92  
    39.1 --- a/src/Tools/Code/code_preproc.ML	Mon Jul 13 19:07:05 2009 +0200
    39.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jul 14 10:56:43 2009 +0200
    39.3 @@ -526,14 +526,16 @@
    39.4  val setup = 
    39.5    let
    39.6      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    39.7 -    fun add_del_attribute (name, (add, del)) =
    39.8 -      Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
    39.9 -        || Scan.succeed (mk_attribute add))
   39.10 +    fun add_del_attribute_parser (add, del) =
   39.11 +      Attrib.add_del (mk_attribute add) (mk_attribute del);
   39.12    in
   39.13 -    add_del_attribute ("inline", (add_inline, del_inline))
   39.14 -    #> add_del_attribute ("post", (add_post, del_post))
   39.15 -    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
   39.16 -       (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I)))
   39.17 +    Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
   39.18 +        "preprocessing equations for code generator"
   39.19 +    #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
   39.20 +        "postprocessing equations for code generator"
   39.21 +    #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
   39.22 +       (fn thm => Codegen.add_unfold thm #> add_inline thm)))
   39.23 +        "preprocessing equations for code generators"
   39.24    end;
   39.25  
   39.26  val _ =