# HG changeset patch
# User avigad
# Date 1247620774 14400
# Node ID a4213e1b4cc782b794d966c31ff4efa2de0fd064
# Parent  df28ead1cf19146afe851e8be1230495018adca7# Parent  b09916780820da8310590fa5b98fddf7b2e78448
commit merge

diff -r df28ead1cf19 -r a4213e1b4cc7 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Jul 14 20:58:53 2009 -0400
+++ b/CONTRIBUTORS	Tue Jul 14 21:19:34 2009 -0400
@@ -7,6 +7,12 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* July 2009: Florian Haftmann, TUM
+  New quickcheck implementation using new code generator
+
+* July 2009: Florian Haftmann, TUM
+  HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation
+
 * June 2009: Andreas Lochbihler, Uni Karlsruhe
   HOL/Library/Fin_Fun: almost everywhere constant functions
 
diff -r df28ead1cf19 -r a4213e1b4cc7 NEWS
--- a/NEWS	Tue Jul 14 20:58:53 2009 -0400
+++ b/NEWS	Tue Jul 14 21:19:34 2009 -0400
@@ -18,6 +18,16 @@
 
 *** HOL ***
 
+* Code generator attributes follow the usual underscore convention:
+    code_unfold     replaces    code unfold
+    code_post       replaces    code post
+    etc.
+  INCOMPATIBILITY.
+
+* New quickcheck implementation using new code generator.
+
+* New type class boolean_algebra.
+
 * Class semiring_div requires superclass no_zero_divisors and proof of
 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
diff -r df28ead1cf19 -r a4213e1b4cc7 doc-src/Codegen/Thy/ML.thy
--- a/doc-src/Codegen/Thy/ML.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/Codegen/Thy/ML.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -78,8 +78,7 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML Code.read_const: "theory -> string -> string"} \\
-  @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\
+  @{index_ML Code.read_const: "theory -> string -> string"}
   \end{mldecls}
 
   \begin{description}
@@ -87,11 +86,6 @@
   \item @{ML Code.read_const}~@{text thy}~@{text s}
      reads a constant as a concrete term expression @{text s}.
 
-  \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm}
-     rewrites a code equation @{text thm} with a simpset @{text ss};
-     only arguments and right hand side are rewritten,
-     not the head of the code equation.
-
   \end{description}
 
 *}
diff -r df28ead1cf19 -r a4213e1b4cc7 doc-src/Codegen/Thy/Program.thy
--- a/doc-src/Codegen/Thy/Program.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/Codegen/Thy/Program.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -153,14 +153,14 @@
   out: \emph{preprocessing}.  In essence, the preprocessor
   consists of two components: a \emph{simpset} and \emph{function transformers}.
 
-  The \emph{simpset} allows to employ the full generality of the Isabelle
-  simplifier.  Due to the interpretation of theorems
-  as code equations, rewrites are applied to the right
-  hand side and the arguments of the left hand side of an
-  equation, but never to the constant heading the left hand side.
-  An important special case are \emph{inline theorems} which may be
-  declared and undeclared using the
-  \emph{code inline} or \emph{code inline del} attribute respectively.
+  The \emph{simpset} allows to employ the full generality of the
+  Isabelle simplifier.  Due to the interpretation of theorems as code
+  equations, rewrites are applied to the right hand side and the
+  arguments of the left hand side of an equation, but never to the
+  constant heading the left hand side.  An important special case are
+  \emph{unfold theorems} which may be declared and undeclared using
+  the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
+  attribute respectively.
 
   Some common applications:
 *}
@@ -173,21 +173,21 @@
      \item replacing non-executable constructs by executable ones:
 *}     
 
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
   "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
 
 text {*
      \item eliminating superfluous constants:
 *}
 
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
   "1 = Suc 0" by simp
 
 text {*
      \item replacing executable but inconvenient constructs:
 *}
 
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
   "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
 
 text_raw {*
@@ -210,10 +210,10 @@
   on code equations.
 
   \begin{warn}
-    The attribute \emph{code unfold}
-    associated with the @{text "SML code generator"} also applies to
-    the @{text "generic code generator"}:
-    \emph{code unfold} implies \emph{code inline}.
+
+    Attribute @{attribute code_unfold} also applies to the
+    preprocessor of the ancient @{text "SML code generator"}; in case
+    this is not what you intend, use @{attribute code_inline} instead.
   \end{warn}
 *}
 
diff -r df28ead1cf19 -r a4213e1b4cc7 doc-src/Codegen/Thy/document/ML.tex
--- a/doc-src/Codegen/Thy/document/ML.tex	Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/Codegen/Thy/document/ML.tex	Tue Jul 14 21:19:34 2009 -0400
@@ -124,8 +124,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
-  \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
+  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
   \end{mldecls}
 
   \begin{description}
@@ -133,11 +132,6 @@
   \item \verb|Code.read_const|~\isa{thy}~\isa{s}
      reads a constant as a concrete term expression \isa{s}.
 
-  \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
-     rewrites a code equation \isa{thm} with a simpset \isa{ss};
-     only arguments and right hand side are rewritten,
-     not the head of the code equation.
-
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r df28ead1cf19 -r a4213e1b4cc7 doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/Codegen/Thy/document/Program.tex	Tue Jul 14 21:19:34 2009 -0400
@@ -395,14 +395,14 @@
   out: \emph{preprocessing}.  In essence, the preprocessor
   consists of two components: a \emph{simpset} and \emph{function transformers}.
 
-  The \emph{simpset} allows to employ the full generality of the Isabelle
-  simplifier.  Due to the interpretation of theorems
-  as code equations, rewrites are applied to the right
-  hand side and the arguments of the left hand side of an
-  equation, but never to the constant heading the left hand side.
-  An important special case are \emph{inline theorems} which may be
-  declared and undeclared using the
-  \emph{code inline} or \emph{code inline del} attribute respectively.
+  The \emph{simpset} allows to employ the full generality of the
+  Isabelle simplifier.  Due to the interpretation of theorems as code
+  equations, rewrites are applied to the right hand side and the
+  arguments of the left hand side of an equation, but never to the
+  constant heading the left hand side.  An important special case are
+  \emph{unfold theorems} which may be declared and undeclared using
+  the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
+  attribute respectively.
 
   Some common applications:%
 \end{isamarkuptext}%
@@ -421,7 +421,7 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
 \endisatagquote
@@ -442,7 +442,7 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp%
 \endisatagquote
@@ -463,7 +463,7 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
 \endisatagquote
@@ -491,10 +491,10 @@
   on code equations.
 
   \begin{warn}
-    The attribute \emph{code unfold}
-    associated with the \isa{SML\ code\ generator} also applies to
-    the \isa{generic\ code\ generator}:
-    \emph{code unfold} implies \emph{code inline}.
+
+    Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
+    preprocessor of the ancient \isa{SML\ code\ generator}; in case
+    this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
   \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r df28ead1cf19 -r a4213e1b4cc7 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -1190,7 +1190,13 @@
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
-    'code' ( 'inline' ) ? ( 'del' ) ?
+    'code' ( 'del' ) ?
+    ;
+
+    'code_unfold' ( 'del' ) ?
+    ;
+
+    'code_post' ( 'del' ) ?
     ;
   \end{rail}
 
@@ -1280,11 +1286,15 @@
   generation.  Usually packages introducing code equations provide
   a reasonable default setup for selection.
 
-  \item @{attribute (HOL) code}~@{text inline} declares (or with
+  \item @{attribute (HOL) code_inline} declares (or with
   option ``@{text "del"}'' removes) inlining theorems which are
   applied as rewrite rules to any code equation during
   preprocessing.
 
+  \item @{attribute (HOL) code_post} declares (or with
+  option ``@{text "del"}'' removes) theorems which are
+  applied as rewrite rules to any result of an evaluation.
+
   \item @{command (HOL) "print_codesetup"} gives an overview on
   selected code equations and code generator datatypes.
 
diff -r df28ead1cf19 -r a4213e1b4cc7 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jul 14 20:58:53 2009 -0400
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jul 14 21:19:34 2009 -0400
@@ -1201,7 +1201,13 @@
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
-    'code' ( 'inline' ) ? ( 'del' ) ?
+    'code' ( 'del' ) ?
+    ;
+
+    'code_unfold' ( 'del' ) ?
+    ;
+
+    'code_post' ( 'del' ) ?
     ;
   \end{rail}
 
@@ -1288,11 +1294,15 @@
   generation.  Usually packages introducing code equations provide
   a reasonable default setup for selection.
 
-  \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
+  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
   option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
   applied as rewrite rules to any code equation during
   preprocessing.
 
+  \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
+  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
+  applied as rewrite rules to any result of an evaluation.
+
   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
   selected code equations and code generator datatypes.
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Code_Eval.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -32,7 +32,7 @@
   \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
   "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
 
-lemma valapp_code [code, code inline]:
+lemma valapp_code [code, code_inline]:
   "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
   by (simp only: valapp_def fst_conv snd_conv)
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Code_Numeral.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -176,16 +176,16 @@
 
 end
 
-lemma zero_code_numeral_code [code inline, code]:
+lemma zero_code_numeral_code [code_inline, code]:
   "(0\<Colon>code_numeral) = Numeral0"
   by (simp add: number_of_code_numeral_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
+lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
   using zero_code_numeral_code ..
 
-lemma one_code_numeral_code [code inline, code]:
+lemma one_code_numeral_code [code_inline, code]:
   "(1\<Colon>code_numeral) = Numeral1"
   by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
+lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
   using one_code_numeral_code ..
 
 lemma plus_code_numeral_code [code nbe]:
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Divides.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -131,7 +131,7 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
 proof
   assume "b mod a = 0"
   with mod_div_equality [of b a] have "b div a * a = b" by simp
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Fact.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -261,7 +261,7 @@
 by (cases m) auto
 
 
-subsection {* fact and of_nat *}
+subsection {* @{term fact} and @{term of_nat} *}
 
 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
 by auto
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Finite_Set.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -218,6 +218,12 @@
  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
 by (induct rule:finite_induct) simp_all
 
+lemma finite_Inter[intro]: "EX A:M. finite(A) \<Longrightarrow> finite(Inter M)"
+by (blast intro: Inter_lower finite_subset)
+
+lemma finite_INT[intro]: "EX x:I. finite(A x) \<Longrightarrow> finite(INT x:I. A x)"
+by (blast intro: INT_lower finite_subset)
+
 lemma finite_empty_induct:
   assumes "finite A"
     and "P A"
@@ -784,6 +790,62 @@
 
 end
 
+context ab_semigroup_idem_mult
+begin
+
+lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
+apply unfold_locales
+ apply (simp add: mult_ac)
+apply (simp add: mult_idem mult_assoc[symmetric])
+done
+
+end
+
+context lower_semilattice
+begin
+
+lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+proof qed (rule inf_assoc inf_commute inf_idem)+
+
+lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
+by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
+
+lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
+by (induct pred:finite) auto
+
+lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
+proof(induct arbitrary: a pred:finite)
+  case empty thus ?case by simp
+next
+  case (insert x A)
+  show ?case
+  proof cases
+    assume "A = {}" thus ?thesis using insert by simp
+  next
+    assume "A \<noteq> {}" thus ?thesis using insert by auto
+  qed
+qed
+
+end
+
+context upper_semilattice
+begin
+
+lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
+
+lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
+by(rule lower_semilattice.fold_inf_insert)(rule dual_semilattice)
+
+lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
+by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice)
+
+lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
+by(rule lower_semilattice.fold_inf_le_inf)(rule dual_semilattice)
+
+end
+
+
 subsubsection{* The derived combinator @{text fold_image} *}
 
 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
@@ -801,7 +863,7 @@
 proof -
   interpret I: fun_left_comm "%x y. (g x) * y"
     by unfold_locales (simp add: mult_ac)
-  show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
+  show ?thesis using assms by(simp add:fold_image_def)
 qed
 
 (*
@@ -829,10 +891,7 @@
 lemma fold_image_reindex:
 assumes fin: "finite A"
 shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
-using fin apply induct
- apply simp
-apply simp
-done
+using fin by induct auto
 
 (*
 text{*
@@ -2351,14 +2410,15 @@
 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
 by(fastsimp simp:surj_def dest!: endo_inj_surj)
 
-corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
+corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
 proof
   assume "finite(UNIV::nat set)"
   with finite_UNIV_inj_surj[of Suc]
   show False by simp (blast dest: Suc_neq_Zero surjD)
 qed
 
-lemma infinite_UNIV_char_0:
+(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
+lemma infinite_UNIV_char_0[noatp]:
   "\<not> finite (UNIV::'a::semiring_char_0 set)"
 proof
   assume "finite (UNIV::'a set)"
@@ -2499,13 +2559,6 @@
 context ab_semigroup_idem_mult
 begin
 
-lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
-apply unfold_locales
- apply (simp add: mult_ac)
-apply (simp add: mult_idem mult_assoc[symmetric])
-done
-
-
 lemma fold1_insert_idem [simp]:
   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
   shows "fold1 times (insert x A) = x * fold1 times A"
@@ -2667,10 +2720,6 @@
 context lower_semilattice
 begin
 
-lemma ab_semigroup_idem_mult_inf:
-  "ab_semigroup_idem_mult inf"
-  proof qed (rule inf_assoc inf_commute inf_idem)+
-
 lemma below_fold1_iff:
   assumes "finite A" "A \<noteq> {}"
   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
@@ -2716,11 +2765,6 @@
 
 end
 
-lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
-  "ab_semigroup_idem_mult sup"
-  by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
-    (rule dual_lattice)
-
 context lattice
 begin
 
@@ -2741,7 +2785,7 @@
 apply(erule exE)
 apply(rule order_trans)
 apply(erule (1) fold1_belowI)
-apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
+apply(erule (1) lower_semilattice.fold1_belowI [OF dual_semilattice])
 done
 
 lemma sup_Inf_absorb [simp]:
@@ -2753,7 +2797,7 @@
 lemma inf_Sup_absorb [simp]:
   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
 by (simp add: Sup_fin_def inf_absorb1
-  lower_semilattice.fold1_belowI [OF dual_lattice])
+  lower_semilattice.fold1_belowI [OF dual_semilattice])
 
 end
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/GCD.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -37,7 +37,7 @@
 
 subsection {* gcd *}
 
-class gcd = one +
+class gcd = zero + one + dvd +
 
 fixes
   gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
@@ -540,15 +540,15 @@
 
 (* to do: add the three variations of these, and for ints? *)
 
-lemma finite_divisors_nat:
-  assumes "(m::nat)~= 0" shows "finite{d. d dvd m}"
+lemma finite_divisors_nat[simp]:
+  assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
 proof-
   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
   from finite_subset[OF _ this] show ?thesis using assms
     by(bestsimp intro!:dvd_imp_le)
 qed
 
-lemma finite_divisors_int:
+lemma finite_divisors_int[simp]:
   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
 proof-
   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
@@ -557,10 +557,25 @@
     by(bestsimp intro!:dvd_imp_le_int)
 qed
 
+lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
+apply(rule antisym)
+ apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
+apply simp
+done
+
+lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
+apply(rule antisym)
+ apply(rule Max_le_iff[THEN iffD2])
+   apply simp
+  apply fastsimp
+ apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
+apply simp
+done
+
 lemma gcd_is_Max_divisors_nat:
   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
 apply(rule Max_eqI[THEN sym])
-  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
+  apply (metis finite_Collect_conjI finite_divisors_nat)
  apply simp
  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
 apply simp
@@ -569,7 +584,7 @@
 lemma gcd_is_Max_divisors_int:
   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
 apply(rule Max_eqI[THEN sym])
-  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
+  apply (metis finite_Collect_conjI finite_divisors_int)
  apply simp
  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
 apply simp
@@ -1442,31 +1457,61 @@
 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
 
+lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
+by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
+
+lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
+by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
+
+lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
+by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
+
+lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
+by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
 
 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
-apply(rule lcm_unique_nat[THEN iffD1])
-apply (metis dvd.order_trans lcm_unique_nat)
-done
+by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
 
 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
-apply(rule lcm_unique_int[THEN iffD1])
-apply (metis dvd_trans lcm_unique_int)
-done
+by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
 
-lemmas lcm_left_commute_nat =
-  mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
-
-lemmas lcm_left_commute_int =
-  mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
+lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
+lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
 
 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
 
+lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
+proof qed (auto simp add: gcd_ac_nat)
+
+lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
+proof qed (auto simp add: gcd_ac_int)
+
+lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
+proof qed (auto simp add: lcm_ac_nat)
+
+lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
+proof qed (auto simp add: lcm_ac_int)
+
+
+(* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
+
+lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
+by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
+
+lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
+by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
+
+lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
+by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
+
+lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
+by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
+
 
 subsection {* Primes *}
 
-(* Is there a better way to handle these, rather than making them
-   elim rules? *)
+(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
 
 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
   by (unfold prime_nat_def, auto)
@@ -1490,7 +1535,7 @@
   by (unfold prime_nat_def, auto)
 
 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
-  by (unfold prime_int_def prime_nat_def, auto)
+  by (unfold prime_int_def prime_nat_def) auto
 
 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
   by (unfold prime_int_def prime_nat_def, auto)
@@ -1504,8 +1549,6 @@
 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
   by (unfold prime_int_def prime_nat_def, auto)
 
-thm prime_nat_def;
-thm prime_nat_def [transferred];
 
 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
     m = 1 \<or> m = p))"
@@ -1566,35 +1609,13 @@
 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   unfolding prime_nat_def dvd_def apply auto
-  apply (subgoal_tac "k > 1")
-  apply force
-  apply (subgoal_tac "k ~= 0")
-  apply force
-  apply (rule notI)
-  apply force
-done
+  by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
 
-(* there's a lot of messing around with signs of products here --
-   could this be made more automatic? *)
 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   unfolding prime_int_altdef dvd_def
   apply auto
-  apply (rule_tac x = m in exI)
-  apply (rule_tac x = k in exI)
-  apply (auto simp add: mult_compare_simps)
-  apply (subgoal_tac "k > 0")
-  apply arith
-  apply (case_tac "k <= 0")
-  apply (subgoal_tac "m * k <= 0")
-  apply force
-  apply (subst zero_compare_simps(8))
-  apply auto
-  apply (subgoal_tac "m * k <= 0")
-  apply force
-  apply (subst zero_compare_simps(8))
-  apply auto
-done
+  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
 
 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
     n > 0 --> (p dvd x^n --> p dvd x)"
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/HOL.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -1787,7 +1787,7 @@
   assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
 begin
 
-lemma eq [code unfold, code inline del]: "eq = (op =)"
+lemma eq [code_unfold, code_inline del]: "eq = (op =)"
   by (rule ext eq_equals)+
 
 lemma eq_refl: "eq x x \<longleftrightarrow> True"
@@ -1796,7 +1796,7 @@
 lemma equals_eq: "(op =) \<equiv> eq"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
 
-declare equals_eq [symmetric, code post]
+declare equals_eq [symmetric, code_post]
 
 end
 
@@ -1847,7 +1847,7 @@
 
 lemmas [code] = Let_def if_True if_False
 
-lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
+lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
 
 instantiation itself :: (type) eq
 begin
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -283,7 +283,7 @@
 where
   [code del]: "raise_exc e = raise []"
 
-lemma raise_raise_exc [code, code inline]:
+lemma raise_raise_exc [code, code_inline]:
   "raise s = raise_exc (Fail (STR s))"
   unfolding Fail_def raise_exc_def raise_def ..
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Int.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -650,11 +650,11 @@
 
 text {* Removal of leading zeroes *}
 
-lemma Bit0_Pls [simp, code post]:
+lemma Bit0_Pls [simp, code_post]:
   "Bit0 Pls = Pls"
   unfolding numeral_simps by simp
 
-lemma Bit1_Min [simp, code post]:
+lemma Bit1_Min [simp, code_post]:
   "Bit1 Min = Min"
   unfolding numeral_simps by simp
 
@@ -2126,11 +2126,11 @@
 
 hide (open) const nat_aux
 
-lemma zero_is_num_zero [code, code inline, symmetric, code post]:
+lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
   "(0\<Colon>int) = Numeral0" 
   by simp
 
-lemma one_is_num_one [code, code inline, symmetric, code post]:
+lemma one_is_num_one [code, code_inline, symmetric, code_post]:
   "(1\<Colon>int) = Numeral1" 
   by simp
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/IntDiv.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -36,7 +36,7 @@
 
 text{*algorithm for the general case @{term "b\<noteq>0"}*}
 definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
-  [code inline]: "negateSnd = apsnd uminus"
+  [code_inline]: "negateSnd = apsnd uminus"
 
 definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
     --{*The full division algorithm considers all possible signs for a, b
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Lattices.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -29,7 +29,7 @@
 
 text {* Dual lattice *}
 
-lemma dual_lattice:
+lemma dual_semilattice:
   "lower_semilattice (op \<ge>) (op >) sup"
 by (rule lower_semilattice.intro, rule dual_order)
   (unfold_locales, simp_all add: sup_least)
@@ -180,6 +180,11 @@
 context lattice
 begin
 
+lemma dual_lattice:
+  "lattice (op \<ge>) (op >) sup inf"
+  by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order)
+    (unfold_locales, auto)
+
 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
   by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
 
@@ -252,12 +257,148 @@
  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
 by(simp add:ACI inf_sup_distrib1)
 
+lemma dual_distrib_lattice:
+  "distrib_lattice (op \<ge>) (op >) sup inf"
+  by (rule distrib_lattice.intro, rule dual_lattice)
+    (unfold_locales, fact inf_sup_distrib1)
+
 lemmas distrib =
   sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
 
 end
 
 
+subsection {* Boolean algebras *}
+
+class boolean_algebra = distrib_lattice + top + bot + minus + uminus +
+  assumes inf_compl_bot: "x \<sqinter> - x = bot"
+    and sup_compl_top: "x \<squnion> - x = top"
+  assumes diff_eq: "x - y = x \<sqinter> - y"
+begin
+
+lemma dual_boolean_algebra:
+  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) top bot"
+  by (rule boolean_algebra.intro, rule dual_distrib_lattice)
+    (unfold_locales,
+      auto simp add: inf_compl_bot sup_compl_top diff_eq less_le_not_le)
+
+lemma compl_inf_bot:
+  "- x \<sqinter> x = bot"
+  by (simp add: inf_commute inf_compl_bot)
+
+lemma compl_sup_top:
+  "- x \<squnion> x = top"
+  by (simp add: sup_commute sup_compl_top)
+
+lemma inf_bot_left [simp]:
+  "bot \<sqinter> x = bot"
+  by (rule inf_absorb1) simp
+
+lemma inf_bot_right [simp]:
+  "x \<sqinter> bot = bot"
+  by (rule inf_absorb2) simp
+
+lemma sup_top_left [simp]:
+  "top \<squnion> x = top"
+  by (rule sup_absorb1) simp
+
+lemma sup_top_right [simp]:
+  "x \<squnion> top = top"
+  by (rule sup_absorb2) simp
+
+lemma inf_top_left [simp]:
+  "top \<sqinter> x = x"
+  by (rule inf_absorb2) simp
+
+lemma inf_top_right [simp]:
+  "x \<sqinter> top = x"
+  by (rule inf_absorb1) simp
+
+lemma sup_bot_left [simp]:
+  "bot \<squnion> x = x"
+  by (rule sup_absorb2) simp
+
+lemma sup_bot_right [simp]:
+  "x \<squnion> bot = x"
+  by (rule sup_absorb1) simp
+
+lemma compl_unique:
+  assumes "x \<sqinter> y = bot"
+    and "x \<squnion> y = top"
+  shows "- x = y"
+proof -
+  have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
+    using inf_compl_bot assms(1) by simp
+  then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
+    by (simp add: inf_commute)
+  then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
+    by (simp add: inf_sup_distrib1)
+  then have "- x \<sqinter> top = y \<sqinter> top"
+    using sup_compl_top assms(2) by simp
+  then show "- x = y" by (simp add: inf_top_right)
+qed
+
+lemma double_compl [simp]:
+  "- (- x) = x"
+  using compl_inf_bot compl_sup_top by (rule compl_unique)
+
+lemma compl_eq_compl_iff [simp]:
+  "- x = - y \<longleftrightarrow> x = y"
+proof
+  assume "- x = - y"
+  then have "- x \<sqinter> y = bot"
+    and "- x \<squnion> y = top"
+    by (simp_all add: compl_inf_bot compl_sup_top)
+  then have "- (- x) = y" by (rule compl_unique)
+  then show "x = y" by simp
+next
+  assume "x = y"
+  then show "- x = - y" by simp
+qed
+
+lemma compl_bot_eq [simp]:
+  "- bot = top"
+proof -
+  from sup_compl_top have "bot \<squnion> - bot = top" .
+  then show ?thesis by simp
+qed
+
+lemma compl_top_eq [simp]:
+  "- top = bot"
+proof -
+  from inf_compl_bot have "top \<sqinter> - top = bot" .
+  then show ?thesis by simp
+qed
+
+lemma compl_inf [simp]:
+  "- (x \<sqinter> y) = - x \<squnion> - y"
+proof (rule compl_unique)
+  have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)"
+    by (rule inf_sup_distrib1)
+  also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
+    by (simp only: inf_commute inf_assoc inf_left_commute)
+  finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = bot"
+    by (simp add: inf_compl_bot)
+next
+  have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
+    by (rule sup_inf_distrib2)
+  also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
+    by (simp only: sup_commute sup_assoc sup_left_commute)
+  finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = top"
+    by (simp add: sup_compl_top)
+qed
+
+lemma compl_sup [simp]:
+  "- (x \<squnion> y) = - x \<sqinter> - y"
+proof -
+  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
+    by (rule dual_boolean_algebra)
+  then show ?thesis by simp
+qed
+
+end
+
+
 subsection {* Uniqueness of inf and sup *}
 
 lemma (in lower_semilattice) inf_unique:
@@ -330,17 +471,24 @@
 
 subsection {* Bool as lattice *}
 
-instantiation bool :: distrib_lattice
+instantiation bool :: boolean_algebra
 begin
 
 definition
+  bool_Compl_def: "uminus = Not"
+
+definition
+  bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
+
+definition
   inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
 
 definition
   sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
 
-instance
-  by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
+instance proof
+qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def
+  bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto)
 
 end
 
@@ -369,7 +517,33 @@
 end
 
 instance "fun" :: (type, distrib_lattice) distrib_lattice
-  by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
+proof
+qed (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
+
+instantiation "fun" :: (type, uminus) uminus
+begin
+
+definition
+  fun_Compl_def: "- A = (\<lambda>x. - A x)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, minus) minus
+begin
+
+definition
+  fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
+
+instance ..
+
+end
+
+instance "fun" :: (type, boolean_algebra) boolean_algebra
+proof
+qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def
+  inf_compl_bot sup_compl_top diff_eq)
 
 
 text {* redundant bindings *}
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -24,11 +24,11 @@
 
 lemmas [code del] = char.recs char.cases char.size
 
-lemma [code, code inline]:
+lemma [code, code_inline]:
   "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
   by (cases c) (auto simp add: nibble_pair_of_nat_char)
 
-lemma [code, code inline]:
+lemma [code, code_inline]:
   "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
   by (cases c) (auto simp add: nibble_pair_of_nat_char)
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Countable.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -58,7 +58,7 @@
 subclass (in finite) countable
 proof
   have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
-  with finite_conv_nat_seg_image [of UNIV]
+  with finite_conv_nat_seg_image [of "UNIV::'a set"]
   obtain n and f :: "nat \<Rightarrow> 'a" 
     where "UNIV = f ` {i. i < n}" by auto
   then have "surj f" unfolding surj_def by auto
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -26,15 +26,15 @@
 
 code_datatype number_nat_inst.number_of_nat
 
-lemma zero_nat_code [code, code inline]:
+lemma zero_nat_code [code, code_inline]:
   "0 = (Numeral0 :: nat)"
   by simp
-lemmas [code post] = zero_nat_code [symmetric]
+lemmas [code_post] = zero_nat_code [symmetric]
 
-lemma one_nat_code [code, code inline]:
+lemma one_nat_code [code, code_inline]:
   "1 = (Numeral1 :: nat)"
   by simp
-lemmas [code post] = one_nat_code [symmetric]
+lemmas [code_post] = one_nat_code [symmetric]
 
 lemma Suc_code [code]:
   "Suc n = n + 1"
@@ -89,7 +89,7 @@
   expression:
 *}
 
-lemma [code, code unfold]:
+lemma [code, code_unfold]:
   "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
   by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
 
@@ -302,7 +302,7 @@
   Natural numerals.
 *}
 
-lemma [code inline, symmetric, code post]:
+lemma [code_inline, symmetric, code_post]:
   "nat (number_of i) = number_nat_inst.number_of_nat i"
   -- {* this interacts as desired with @{thm nat_number_of_def} *}
   by (simp add: number_nat_inst.number_of_nat)
@@ -335,9 +335,9 @@
   "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   unfolding nat_number_of_def number_of_is_id neg_def by simp
 
-lemma of_nat_int [code unfold]:
+lemma of_nat_int [code_unfold]:
   "of_nat = int" by (simp add: int_def)
-declare of_nat_int [symmetric, code post]
+declare of_nat_int [symmetric, code_post]
 
 code_const int
   (SML "_")
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Executable_Set.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -15,7 +15,7 @@
 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "subset = op \<le>"
 
-declare subset_def [symmetric, code unfold]
+declare subset_def [symmetric, code_unfold]
 
 lemma [code]:
   "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
@@ -25,7 +25,7 @@
   [code del]: "eq_set = op ="
 
 (* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code unfold]
+declare set_eq_subset[code_unfold]
 *)
 
 lemma [code]:
@@ -40,7 +40,7 @@
 
 subsection {* Rewrites for primitive operations *}
 
-declare List_Set.project_def [symmetric, code unfold]
+declare List_Set.project_def [symmetric, code_unfold]
 
 
 subsection {* code generator setup *}
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Float.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -19,7 +19,7 @@
   "of_float (Float a b) = real a * pow2 b"
 
 defs (overloaded)
-  real_of_float_def [code unfold]: "real == of_float"
+  real_of_float_def [code_unfold]: "real == of_float"
 
 primrec mantissa :: "float \<Rightarrow> int" where
   "mantissa (Float a b) = a"
@@ -42,7 +42,7 @@
 instance ..
 end
 
-lemma number_of_float_Float [code inline, symmetric, code post]:
+lemma number_of_float_Float [code_inline, symmetric, code_post]:
   "number_of k = Float (number_of k) 0"
   by (simp add: number_of_float_def number_of_is_id)
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Fraction_Field.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -93,10 +93,10 @@
 begin
 
 definition
-  Zero_fract_def [code, code unfold]: "0 = Fract 0 1"
+  Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
 
 definition
-  One_fract_def [code, code unfold]: "1 = Fract 1 1"
+  One_fract_def [code, code_unfold]: "1 = Fract 1 1"
 
 definition
   add_fract_def [code del]:
@@ -196,14 +196,14 @@
 lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
   by (rule of_nat_fract [symmetric])
 
-lemma fract_collapse [code post]:
+lemma fract_collapse [code_post]:
   "Fract 0 k = 0"
   "Fract 1 1 = 1"
   "Fract k 0 = 0"
   by (cases "k = 0")
     (simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def)
 
-lemma fract_expand [code unfold]:
+lemma fract_expand [code_unfold]:
   "0 = Fract 0 1"
   "1 = Fract 1 1"
   by (simp_all add: fract_collapse)
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -40,10 +40,10 @@
   "0 = Fin 0"
 
 definition
-  [code inline]: "1 = Fin 1"
+  [code_inline]: "1 = Fin 1"
 
 definition
-  [code inline, code del]: "number_of k = Fin (number_of k)"
+  [code_inline, code del]: "number_of k = Fin (number_of k)"
 
 instance ..
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Library/Polynomial.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -1505,7 +1505,7 @@
 
 code_datatype "0::'a::zero poly" pCons
 
-declare pCons_0_0 [code post]
+declare pCons_0_0 [code_post]
 
 instantiation poly :: ("{zero,eq}") eq
 begin
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/List.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -2076,7 +2076,7 @@
 by(induct xs) simp_all
 
 text{* For efficient code generation: avoid intermediate list. *}
-lemma foldl_map[code unfold]:
+lemma foldl_map[code_unfold]:
   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
 by(induct xs arbitrary:a) simp_all
 
@@ -2198,7 +2198,7 @@
 
 text{* For efficient code generation ---
        @{const listsum} is not tail recursive but @{const foldl} is. *}
-lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
+lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
 by(simp add:listsum_foldr foldl_foldr1)
 
 lemma distinct_listsum_conv_Setsum:
@@ -3746,32 +3746,32 @@
   show ?case by (induct xs) (auto simp add: Cons aux)
 qed
 
-lemma mem_iff [code post]:
+lemma mem_iff [code_post]:
   "x mem xs \<longleftrightarrow> x \<in> set xs"
 by (induct xs) auto
 
-lemmas in_set_code [code unfold] = mem_iff [symmetric]
+lemmas in_set_code [code_unfold] = mem_iff [symmetric]
 
 lemma empty_null:
   "xs = [] \<longleftrightarrow> null xs"
 by (cases xs) simp_all
 
-lemma [code inline]:
+lemma [code_inline]:
   "eq_class.eq xs [] \<longleftrightarrow> null xs"
 by (simp add: eq empty_null)
 
-lemmas null_empty [code post] =
+lemmas null_empty [code_post] =
   empty_null [symmetric]
 
 lemma list_inter_conv:
   "set (list_inter xs ys) = set xs \<inter> set ys"
 by (induct xs) auto
 
-lemma list_all_iff [code post]:
+lemma list_all_iff [code_post]:
   "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
 by (induct xs) auto
 
-lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
+lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
 
 lemma list_all_append [simp]:
   "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
@@ -3785,11 +3785,11 @@
   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
   unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
 
-lemma list_ex_iff [code post]:
+lemma list_ex_iff [code_post]:
   "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
 by (induct xs) simp_all
 
-lemmas list_bex_code [code unfold] =
+lemmas list_bex_code [code_unfold] =
   list_ex_iff [symmetric]
 
 lemma list_ex_length:
@@ -3804,7 +3804,7 @@
   "map_filter f P xs = map f (filter P xs)"
 by (induct xs) auto
 
-lemma length_remdups_length_unique [code inline]:
+lemma length_remdups_length_unique [code_inline]:
   "length (remdups xs) = length_unique xs"
   by (induct xs) simp_all
 
@@ -3813,43 +3813,43 @@
 
 text {* Code for bounded quantification and summation over nats. *}
 
-lemma atMost_upto [code unfold]:
+lemma atMost_upto [code_unfold]:
   "{..n} = set [0..<Suc n]"
 by auto
 
-lemma atLeast_upt [code unfold]:
+lemma atLeast_upt [code_unfold]:
   "{..<n} = set [0..<n]"
 by auto
 
-lemma greaterThanLessThan_upt [code unfold]:
+lemma greaterThanLessThan_upt [code_unfold]:
   "{n<..<m} = set [Suc n..<m]"
 by auto
 
-lemma atLeastLessThan_upt [code unfold]:
+lemma atLeastLessThan_upt [code_unfold]:
   "{n..<m} = set [n..<m]"
 by auto
 
-lemma greaterThanAtMost_upt [code unfold]:
+lemma greaterThanAtMost_upt [code_unfold]:
   "{n<..m} = set [Suc n..<Suc m]"
 by auto
 
-lemma atLeastAtMost_upt [code unfold]:
+lemma atLeastAtMost_upt [code_unfold]:
   "{n..m} = set [n..<Suc m]"
 by auto
 
-lemma all_nat_less_eq [code unfold]:
+lemma all_nat_less_eq [code_unfold]:
   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
 by auto
 
-lemma ex_nat_less_eq [code unfold]:
+lemma ex_nat_less_eq [code_unfold]:
   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
 by auto
 
-lemma all_nat_less [code unfold]:
+lemma all_nat_less [code_unfold]:
   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
 by auto
 
-lemma ex_nat_less [code unfold]:
+lemma ex_nat_less [code_unfold]:
   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
 by auto
 
@@ -3857,30 +3857,30 @@
   "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
 by (induct xs) simp_all
 
-lemma setsum_set_upt_conv_listsum [code unfold]:
+lemma setsum_set_upt_conv_listsum [code_unfold]:
   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
 by (rule setsum_set_distinct_conv_listsum) simp
 
 
 text {* Code for summation over ints. *}
 
-lemma greaterThanLessThan_upto [code unfold]:
+lemma greaterThanLessThan_upto [code_unfold]:
   "{i<..<j::int} = set [i+1..j - 1]"
 by auto
 
-lemma atLeastLessThan_upto [code unfold]:
+lemma atLeastLessThan_upto [code_unfold]:
   "{i..<j::int} = set [i..j - 1]"
 by auto
 
-lemma greaterThanAtMost_upto [code unfold]:
+lemma greaterThanAtMost_upto [code_unfold]:
   "{i<..j::int} = set [i+1..j]"
 by auto
 
-lemma atLeastAtMost_upto [code unfold]:
+lemma atLeastAtMost_upto [code_unfold]:
   "{i..j::int} = set [i..j]"
 by auto
 
-lemma setsum_set_upto_conv_listsum [code unfold]:
+lemma setsum_set_upto_conv_listsum [code_unfold]:
   "setsum f (set [i..j::int]) = listsum (map f [i..j])"
 by (rule setsum_set_distinct_conv_listsum) simp
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -467,7 +467,7 @@
 
 lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
 
-lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
+lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
 
 code_module BV
 contains
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Nat.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -1200,9 +1200,9 @@
 text {* for code generation *}
 
 definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-  funpow_code_def [code post]: "funpow = compow"
+  funpow_code_def [code_post]: "funpow = compow"
 
-lemmas [code unfold] = funpow_code_def [symmetric]
+lemmas [code_unfold] = funpow_code_def [symmetric]
 
 lemma [code]:
   "funpow 0 f = id"
@@ -1265,7 +1265,7 @@
 
 end
 
-declare of_nat_code [code, code unfold, code inline del]
+declare of_nat_code [code, code_unfold, code_inline del]
 
 text{*Class for unital semirings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Nat_Numeral.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -20,13 +20,13 @@
 begin
 
 definition
-  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
+  nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
 
 instance ..
 
 end
 
-lemma [code post]:
+lemma [code_post]:
   "nat (number_of v) = number_of v"
   unfolding nat_number_of_def ..
 
@@ -316,13 +316,13 @@
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
 by (simp add: nat_number_of_def)
 
-lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
+lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
 by (simp add: nat_number_of_def)
 
 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
 by (simp add: nat_1 nat_number_of_def)
 
-lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
+lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
 by (simp add: nat_numeral_1_eq_1)
 
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Option.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -94,7 +94,7 @@
 subsubsection {* Code generator setup *}
 
 definition is_none :: "'a option \<Rightarrow> bool" where
-  [code post]: "is_none x \<longleftrightarrow> x = None"
+  [code_post]: "is_none x \<longleftrightarrow> x = None"
 
 lemma is_none_code [code]:
   shows "is_none None \<longleftrightarrow> True"
@@ -105,7 +105,7 @@
   "is_none x \<longleftrightarrow> x = None"
   by (simp add: is_none_def)
 
-lemma [code inline]:
+lemma [code_inline]:
   "eq_class.eq x None \<longleftrightarrow> is_none x"
   by (simp add: eq is_none_none)
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Orderings.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -268,13 +268,13 @@
 
 text {* Explicit dictionaries for code generation *}
 
-lemma min_ord_min [code, code unfold, code inline del]:
+lemma min_ord_min [code, code_unfold, code_inline del]:
   "min = ord.min (op \<le>)"
   by (rule ext)+ (simp add: min_def ord.min_def)
 
 declare ord.min_def [code]
 
-lemma max_ord_max [code, code unfold, code inline del]:
+lemma max_ord_max [code, code_unfold, code_inline del]:
   "max = ord.max (op \<le>)"
   by (rule ext)+ (simp add: max_def ord.max_def)
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Power.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -455,7 +455,7 @@
 
 subsection {* Code generator tweak *}
 
-lemma power_power_power [code, code unfold, code inline del]:
+lemma power_power_power [code, code_unfold, code_inline del]:
   "power = power.power (1::'a::{power}) (op *)"
   unfolding power_def power.power_def ..
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Rational.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -93,10 +93,10 @@
 begin
 
 definition
-  Zero_rat_def [code, code unfold]: "0 = Fract 0 1"
+  Zero_rat_def [code, code_unfold]: "0 = Fract 0 1"
 
 definition
-  One_rat_def [code, code unfold]: "1 = Fract 1 1"
+  One_rat_def [code, code_unfold]: "1 = Fract 1 1"
 
 definition
   add_rat_def [code del]:
@@ -211,7 +211,7 @@
 
 end
 
-lemma rat_number_collapse [code post]:
+lemma rat_number_collapse [code_post]:
   "Fract 0 k = 0"
   "Fract 1 1 = 1"
   "Fract (number_of k) 1 = number_of k"
@@ -219,7 +219,7 @@
   by (cases "k = 0")
     (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
 
-lemma rat_number_expand [code unfold]:
+lemma rat_number_expand [code_unfold]:
   "0 = Fract 0 1"
   "1 = Fract 1 1"
   "number_of k = Fract (number_of k) 1"
@@ -291,11 +291,11 @@
 lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
   by (simp add: Fract_of_int_eq [symmetric])
 
-lemma Fract_number_of_quotient [code post]:
+lemma Fract_number_of_quotient [code_post]:
   "Fract (number_of k) (number_of l) = number_of k / number_of l"
   unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
 
-lemma Fract_1_number_of [code post]:
+lemma Fract_1_number_of [code_post]:
   "Fract 1 (number_of k) = 1 / number_of k"
   unfolding Fract_of_int_quotient number_of_eq by simp
 
@@ -1003,7 +1003,7 @@
 
 definition (in term_syntax)
   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
-  [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+  [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/RealDef.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -559,8 +559,8 @@
   real :: "'a => real"
 
 defs (overloaded)
-  real_of_nat_def [code unfold]: "real == real_of_nat"
-  real_of_int_def [code unfold]: "real == real_of_int"
+  real_of_nat_def [code_unfold]: "real == real_of_nat"
+  real_of_int_def [code_unfold]: "real == real_of_int"
 
 lemma real_eq_of_nat: "real = of_nat"
   unfolding real_of_nat_def ..
@@ -946,7 +946,7 @@
 
 end
 
-lemma [code unfold, symmetric, code post]:
+lemma [code_unfold, symmetric, code_post]:
   "number_of k = real_of_int (number_of k)"
   unfolding number_of_is_id real_number_of_def ..
 
@@ -1061,29 +1061,29 @@
 
 code_datatype Ratreal
 
-lemma Ratreal_number_collapse [code post]:
+lemma Ratreal_number_collapse [code_post]:
   "Ratreal 0 = 0"
   "Ratreal 1 = 1"
   "Ratreal (number_of k) = number_of k"
 by simp_all
 
-lemma zero_real_code [code, code unfold]:
+lemma zero_real_code [code, code_unfold]:
   "0 = Ratreal 0"
 by simp
 
-lemma one_real_code [code, code unfold]:
+lemma one_real_code [code, code_unfold]:
   "1 = Ratreal 1"
 by simp
 
-lemma number_of_real_code [code unfold]:
+lemma number_of_real_code [code_unfold]:
   "number_of k = Ratreal (number_of k)"
 by simp
 
-lemma Ratreal_number_of_quotient [code post]:
+lemma Ratreal_number_of_quotient [code_post]:
   "Ratreal (number_of r) / Ratreal (number_of s) = number_of r / number_of s"
 by simp
 
-lemma Ratreal_number_of_quotient2 [code post]:
+lemma Ratreal_number_of_quotient2 [code_post]:
   "Ratreal (number_of r / number_of s) = number_of r / number_of s"
 unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
 
@@ -1129,7 +1129,7 @@
 
 definition (in term_syntax)
   valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+  [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Set.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -10,7 +10,6 @@
 
 text {* A set in HOL is simply a predicate. *}
 
-
 subsection {* Basic syntax *}
 
 global
@@ -363,46 +362,6 @@
   Bex_def:      "Bex A P        == EX x. x:A & P(x)"
   Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
 
-instantiation "fun" :: (type, minus) minus
-begin
-
-definition
-  fun_diff_def: "A - B = (%x. A x - B x)"
-
-instance ..
-
-end
-
-instantiation bool :: minus
-begin
-
-definition
-  bool_diff_def: "A - B = (A & ~ B)"
-
-instance ..
-
-end
-
-instantiation "fun" :: (type, uminus) uminus
-begin
-
-definition
-  fun_Compl_def: "- A = (%x. - A x)"
-
-instance ..
-
-end
-
-instantiation bool :: uminus
-begin
-
-definition
-  bool_Compl_def: "- A = (~ A)"
-
-instance ..
-
-end
-
 definition Pow :: "'a set => 'a set set" where
   Pow_def: "Pow A = {B. B \<le> A}"
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/SetInterval.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -284,8 +284,8 @@
 lemma atLeast0AtMost: "{0..n::nat} = {..n}"
 by(simp add:atMost_def atLeastAtMost_def)
 
-declare atLeast0LessThan[symmetric, code unfold]
-        atLeast0AtMost[symmetric, code unfold]
+declare atLeast0LessThan[symmetric, code_unfold]
+        atLeast0AtMost[symmetric, code_unfold]
 
 lemma atLeastLessThan0: "{m..<0::nat} = {}"
 by (simp add: atLeastLessThan_def)
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/String.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -58,11 +58,11 @@
 end
 *}
 
-lemma char_case_nibble_pair [code, code inline]:
+lemma char_case_nibble_pair [code, code_inline]:
   "char_case f = split f o nibble_pair_of_char"
   by (simp add: expand_fun_eq split: char.split)
 
-lemma char_rec_nibble_pair [code, code inline]:
+lemma char_rec_nibble_pair [code, code_inline]:
   "char_rec f = split f o nibble_pair_of_char"
   unfolding char_case_nibble_pair [symmetric]
   by (simp add: expand_fun_eq split: char.split)
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jul 14 21:19:34 2009 -0400
@@ -697,7 +697,8 @@
 
 val setup =
   add_codegen "inductive" inductive_codegen #>
-  Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
-    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
+  Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
+    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+    "introduction rules for executable predicates";
 
 end;
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Tools/inductive_set.ML	Tue Jul 14 21:19:34 2009 -0400
@@ -541,8 +541,9 @@
     "declare rules for converting between predicate and set notation" #>
   Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
   Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
-  Code.add_attribute ("ind_set",
-    Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
+  Attrib.setup @{binding code_ind_set}
+    (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
+    "introduction rules for executable predicates" #>
   Codegen.add_preprocessor codegen_preproc #>
   Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
     "declaration of monotonicity rule for set operators" #>
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jul 14 21:19:34 2009 -0400
@@ -23,15 +23,13 @@
   fun merge _ = Symtab.merge (K true);
 );
 
-fun add_thm NONE thm thy = Code.add_eqn thm thy
-  | add_thm (SOME module_name) thm thy =
-      let
-        val (thm', _) = Code.mk_eqn thy (thm, true)
-      in
-        thy
-        |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
-        |> Code.add_eqn thm'
-      end;
+fun add_thm_target module_name thm thy =
+  let
+    val (thm', _) = Code.mk_eqn thy (thm, true)
+  in
+    thy
+    |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
+  end;
 
 fun expand_eta thy [] = []
   | expand_eta thy (thms as thm :: _) =
@@ -163,15 +161,8 @@
         end)
   | _ => NONE);
 
-val setup = let
-  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
-    (add_thm opt_module thm) I);
-  val del = Thm.declaration_attribute (fn thm => Context.mapping
-    (Code.del_eqn thm) I);
-in
+val setup = 
   add_codegen "recfun" recfun_codegen
-  #> Code.add_attribute ("", Args.del |-- Scan.succeed del
-     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
-end;
+  #> Code.set_code_target_attr add_thm_target;
 
 end;
diff -r df28ead1cf19 -r a4213e1b4cc7 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/HOL/ex/Numeral.thy	Tue Jul 14 21:19:34 2009 -0400
@@ -751,14 +751,14 @@
 subsection {* Code generator setup for @{typ int} *}
 
 definition Pls :: "num \<Rightarrow> int" where
-  [simp, code post]: "Pls n = of_num n"
+  [simp, code_post]: "Pls n = of_num n"
 
 definition Mns :: "num \<Rightarrow> int" where
-  [simp, code post]: "Mns n = - of_num n"
+  [simp, code_post]: "Mns n = - of_num n"
 
 code_datatype "0::int" Pls Mns
 
-lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
+lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
 
 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   [simp, code del]: "sub m n = (of_num m - of_num n)"
@@ -874,10 +874,10 @@
   using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   by (simp_all add: of_num_less_iff)
 
-lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp
-lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp
-declare zero_is_num_zero [code inline del]
-declare one_is_num_one [code inline del]
+lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
+lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
+declare zero_is_num_zero [code_inline del]
+declare one_is_num_one [code_inline del]
 
 hide (open) const sub dup
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Pure/Isar/code.ML	Tue Jul 14 21:19:34 2009 -0400
@@ -62,7 +62,7 @@
   val print_codesetup: theory -> unit
 
   (*infrastructure*)
-  val add_attribute: string * attribute parser -> theory -> theory
+  val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
   val purge_data: theory -> theory
 end;
 
@@ -235,31 +235,6 @@
   end;
 
 
-(** code attributes **)
-
-structure Code_Attr = TheoryDataFun (
-  type T = (string * attribute parser) list;
-  val empty = [];
-  val copy = I;
-  val extend = I;
-  fun merge _ = AList.merge (op = : string * string -> bool) (K true);
-);
-
-fun add_attribute (attr as (name, _)) =
-  let
-    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
-      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
-  in Code_Attr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
-    then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
-  end;
-
-val _ = Context.>> (Context.map_theory
-  (Attrib.setup (Binding.name "code")
-    (Scan.peek (fn context =>
-      List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context)))))
-    "declare theorems for code generation"));
-
-
 (** data store **)
 
 (* code equations *)
@@ -543,7 +518,7 @@
       in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
     fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
       let
-        val _ = if tyco' <> tyco
+        val _ = if (tyco' : string) <> tyco
           then error "Different type constructors in constructor set"
           else ();
         val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
@@ -911,18 +886,32 @@
  of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   | NONE => thy;
 
+structure Code_Attr = TheoryDataFun (
+  type T = (string -> thm -> theory -> theory) option;
+  val empty = NONE;
+  val copy = I;
+  val extend = I;
+  fun merge _ (NONE, f2) = f2
+    | merge _ (f1, _) = f1;
+);
+
+fun set_code_target_attr f = Code_Attr.map (K (SOME f));
+
 val _ = Context.>> (Context.map_theory
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-    fun add_simple_attribute (name, f) =
-      add_attribute (name, Scan.succeed (mk_attribute f));
-    fun add_del_attribute (name, (add, del)) =
-      add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
-        || Scan.succeed (mk_attribute add))
+    val code_attribute_parser =
+      Args.del |-- Scan.succeed (mk_attribute del_eqn)
+      || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
+      || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
+           (fn prefix => mk_attribute (fn thm => fn thy => thy
+             |> add_warning_eqn thm
+             |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
+      || Scan.succeed (mk_attribute add_warning_eqn);
   in
     Type_Interpretation.init
-    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
-    #> add_simple_attribute ("nbe", add_nbe_eqn)
+    #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
+        "declare theorems for code generation"
   end));
 
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 14 21:19:34 2009 -0400
@@ -523,16 +523,17 @@
 
 (* patterns *)
 
-fun prepare_patternT ctxt =
-  let val Mode {pattern, schematic, ...} = get_mode ctxt in
-    if pattern orelse schematic then I
-    else Term.map_atyps
-      (fn T as TVar (xi, _) =>
-            if not (TypeInfer.is_param xi)
-            then error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
-            else T
-        | T => T)
-  end;
+fun prepare_patternT ctxt T =
+  let
+    val Mode {pattern, schematic, ...} = get_mode ctxt;
+    val _ =
+      pattern orelse schematic orelse
+        T |> Term.exists_subtype
+          (fn TVar (xi, _) =>
+            not (TypeInfer.is_param xi) andalso
+              error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
+          | _ => false)
+  in T end;
 
 
 local
diff -r df28ead1cf19 -r a4213e1b4cc7 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Pure/logic.ML	Tue Jul 14 21:19:34 2009 -0400
@@ -71,9 +71,7 @@
   val varify: term -> term
   val unvarify: term -> term
   val legacy_varifyT: typ -> typ
-  val legacy_unvarifyT: typ -> typ
   val legacy_varify: term -> term
-  val legacy_unvarify: term -> term
   val get_goal: term -> int -> term
   val goal_params: term -> int -> term * term list
   val prems_of_goal: term -> int -> term list
@@ -508,16 +506,11 @@
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
-val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
 
 val legacy_varify =
   Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
   Term.map_types legacy_varifyT;
 
-val legacy_unvarify =
-  Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
-  Term.map_types legacy_unvarifyT;
-
 
 (* goal states *)
 
diff -r df28ead1cf19 -r a4213e1b4cc7 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Pure/type_infer.ML	Tue Jul 14 21:19:34 2009 -0400
@@ -39,7 +39,8 @@
 fun is_param (x, _: int) = String.isPrefix "?" x;
 fun param i (x, S) = TVar (("?" ^ x, i), S);
 
-val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | T => T);
+val paramify_vars =
+  perhaps (Term_Subst.map_atypsT_option (fn TVar ((x, i), S) => SOME (param i (x, S)) | _ => NONE));
 
 val paramify_dummies =
   let
diff -r df28ead1cf19 -r a4213e1b4cc7 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Jul 14 20:58:53 2009 -0400
+++ b/src/Tools/Code/code_preproc.ML	Tue Jul 14 21:19:34 2009 -0400
@@ -526,14 +526,16 @@
 val setup = 
   let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-    fun add_del_attribute (name, (add, del)) =
-      Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
-        || Scan.succeed (mk_attribute add))
+    fun add_del_attribute_parser (add, del) =
+      Attrib.add_del (mk_attribute add) (mk_attribute del);
   in
-    add_del_attribute ("inline", (add_inline, del_inline))
-    #> add_del_attribute ("post", (add_post, del_post))
-    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
-       (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I)))
+    Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
+        "preprocessing equations for code generator"
+    #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
+        "postprocessing equations for code generator"
+    #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
+       (fn thm => Codegen.add_unfold thm #> add_inline thm)))
+        "preprocessing equations for code generators"
   end;
 
 val _ =