proper concept of code declaration wrt. atomicity and Isar declarations
authorhaftmann
Sun Jul 02 20:13:38 2017 +0200 (2017-07-02)
changeset 66251cd935b7cb3fb
parent 66250 56a87a5093be
child 66252 b73f94b366b7
proper concept of code declaration wrt. atomicity and Isar declarations
src/Doc/Codegen/Further.thy
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Codegenerator_Test/Generate.thy
src/HOL/HOL.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/old_recdef.ML
src/HOL/Predicate.thy
src/HOL/Product_Type.thy
src/HOL/String.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Old_Datatype/old_primrec.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Old_Datatype/old_size.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/record.ML
src/Pure/Isar/code.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/extraction.ML
src/Pure/Pure.thy
     1.1 --- a/src/Doc/Codegen/Further.thy	Mon Jul 03 14:25:07 2017 +0200
     1.2 +++ b/src/Doc/Codegen/Further.thy	Sun Jul 02 20:13:38 2017 +0200
     1.3 @@ -215,121 +215,4 @@
     1.4    short primer document.
     1.5  \<close>
     1.6  
     1.7 -
     1.8 -subsection \<open>ML system interfaces \label{sec:ml}\<close>
     1.9 -
    1.10 -text \<open>
    1.11 -  Since the code generator framework not only aims to provide a nice
    1.12 -  Isar interface but also to form a base for code-generation-based
    1.13 -  applications, here a short description of the most fundamental ML
    1.14 -  interfaces.
    1.15 -\<close>
    1.16 -
    1.17 -subsubsection \<open>Managing executable content\<close>
    1.18 -
    1.19 -text %mlref \<open>
    1.20 -  \begin{mldecls}
    1.21 -  @{index_ML Code.read_const: "theory -> string -> string"} \\
    1.22 -  @{index_ML Code.add_eqn: "Code.kind * bool -> thm -> theory -> theory"} \\
    1.23 -  @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
    1.24 -  @{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\
    1.25 -  @{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\
    1.26 -  @{index_ML Code_Preproc.add_functrans: "
    1.27 -    string * (Proof.context -> (thm * bool) list -> (thm * bool) list option)
    1.28 -      -> theory -> theory"} \\
    1.29 -  @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
    1.30 -  @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
    1.31 -  @{index_ML Code.get_type: "theory -> string
    1.32 -    -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\
    1.33 -  @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
    1.34 -  \end{mldecls}
    1.35 -
    1.36 -  \begin{description}
    1.37 -
    1.38 -  \item @{ML Code.read_const}~@{text thy}~@{text s}
    1.39 -     reads a constant as a concrete term expression @{text s}.
    1.40 -
    1.41 -  \item @{ML Code.add_eqn}~@{text "(kind, default)"}~@{text "thm"}~@{text "thy"} adds code equation
    1.42 -     @{text "thm"} to executable content.
    1.43 -
    1.44 -  \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes code equation
    1.45 -     @{text "thm"} from executable content, if present.
    1.46 -
    1.47 -  \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
    1.48 -     the preprocessor simpset.
    1.49 -
    1.50 -  \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    1.51 -     function transformer @{text f} (named @{text name}) to executable content;
    1.52 -     @{text f} is a transformer of the code equations belonging
    1.53 -     to a certain function definition, depending on the
    1.54 -     current theory context.  Returning @{text NONE} indicates that no
    1.55 -     transformation took place;  otherwise, the whole process will be iterated
    1.56 -     with the new code equations.
    1.57 -
    1.58 -  \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
    1.59 -     function transformer named @{text name} from executable content.
    1.60 -
    1.61 -  \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
    1.62 -     a datatype to executable content, with generation
    1.63 -     set @{text cs}.
    1.64 -
    1.65 -  \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
    1.66 -     returns type constructor corresponding to
    1.67 -     constructor @{text const}; returns @{text NONE}
    1.68 -     if @{text const} is no constructor.
    1.69 -
    1.70 -  \end{description}
    1.71 -\<close>
    1.72 -
    1.73 -
    1.74 -subsubsection \<open>Data depending on the theory's executable content\<close>
    1.75 -
    1.76 -text \<open>
    1.77 -  Implementing code generator applications on top of the framework set
    1.78 -  out so far usually not only involves using those primitive
    1.79 -  interfaces but also storing code-dependent data and various other
    1.80 -  things.
    1.81 -
    1.82 -  Due to incrementality of code generation, changes in the theory's
    1.83 -  executable content have to be propagated in a certain fashion.
    1.84 -  Additionally, such changes may occur not only during theory
    1.85 -  extension but also during theory merge, which is a little bit nasty
    1.86 -  from an implementation point of view.  The framework provides a
    1.87 -  solution to this technical challenge by providing a functorial data
    1.88 -  slot @{ML_functor Code_Data}; on instantiation of this functor, the
    1.89 -  following types and operations are required:
    1.90 -
    1.91 -  \medskip
    1.92 -  \begin{tabular}{l}
    1.93 -  @{text "type T"} \\
    1.94 -  @{text "val empty: T"} \\
    1.95 -  \end{tabular}
    1.96 -
    1.97 -  \begin{description}
    1.98 -
    1.99 -  \item @{text T} the type of data to store.
   1.100 -
   1.101 -  \item @{text empty} initial (empty) data.
   1.102 -
   1.103 -  \end{description}
   1.104 -
   1.105 -  \noindent An instance of @{ML_functor Code_Data} provides the
   1.106 -  following interface:
   1.107 -
   1.108 -  \medskip
   1.109 -  \begin{tabular}{l}
   1.110 -  @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
   1.111 -  @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
   1.112 -  \end{tabular}
   1.113 -
   1.114 -  \begin{description}
   1.115 -
   1.116 -  \item @{text change} update of current data (cached!) by giving a
   1.117 -    continuation.
   1.118 -
   1.119 -  \item @{text change_yield} update with side result.
   1.120 -
   1.121 -  \end{description}
   1.122 -\<close>
   1.123 -
   1.124  end
     2.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Mon Jul 03 14:25:07 2017 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Sun Jul 02 20:13:38 2017 +0200
     2.3 @@ -25,7 +25,7 @@
     2.4    val tycos = Sign.logical_types thy;
     2.5    val consts = map_filter (try (curry (Axclass.param_of_inst thy)
     2.6      @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
     2.7 -in fold Code.del_eqns consts thy end
     2.8 +in fold Code.declare_unimplemented_global consts thy end
     2.9  \<close>
    2.10  
    2.11  text \<open>Simple example for the predicate compiler.\<close>
     3.1 --- a/src/HOL/Codegenerator_Test/Generate.thy	Mon Jul 03 14:25:07 2017 +0200
     3.2 +++ b/src/HOL/Codegenerator_Test/Generate.thy	Sun Jul 02 20:13:38 2017 +0200
     3.3 @@ -18,4 +18,3 @@
     3.4  export_code _ checking SML OCaml? Haskell? Scala
     3.5  
     3.6  end
     3.7 -
     4.1 --- a/src/HOL/HOL.thy	Mon Jul 03 14:25:07 2017 +0200
     4.2 +++ b/src/HOL/HOL.thy	Sun Jul 02 20:13:38 2017 +0200
     4.3 @@ -1856,8 +1856,8 @@
     4.4    using assms by simp_all
     4.5  
     4.6  setup \<open>
     4.7 -  Code.add_case @{thm Let_case_cert} #>
     4.8 -  Code.add_undefined @{const_name undefined}
     4.9 +  Code.declare_case_global @{thm Let_case_cert} #>
    4.10 +  Code.declare_undefined_global @{const_name undefined}
    4.11  \<close>
    4.12  
    4.13  declare [[code abort: undefined]]
     5.1 --- a/src/HOL/Library/Mapping.thy	Mon Jul 03 14:25:07 2017 +0200
     5.2 +++ b/src/HOL/Library/Mapping.thy	Sun Jul 02 20:13:38 2017 +0200
     5.3 @@ -117,8 +117,9 @@
     5.4  
     5.5  definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)"
     5.6  
     5.7 -declare [[code drop: Mapping.lookup]]
     5.8 -setup \<open>Code.add_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\<close>  (* FIXME lifting *)
     5.9 +lemma [code abstract]:
    5.10 +  "lookup (Mapping f) = f"
    5.11 +  by (fact Mapping.lookup.abs_eq) (* FIXME lifting *)
    5.12  
    5.13  lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
    5.14    is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .
     6.1 --- a/src/HOL/Library/old_recdef.ML	Mon Jul 03 14:25:07 2017 +0200
     6.2 +++ b/src/HOL/Library/old_recdef.ML	Sun Jul 02 20:13:38 2017 +0200
     6.3 @@ -2834,7 +2834,7 @@
     6.4      val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     6.5      val simp_att =
     6.6        if null tcs then [Simplifier.simp_add,
     6.7 -        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute Code.Equation]
     6.8 +        Named_Theorems.add @{named_theorems nitpick_simp}]
     6.9        else [];
    6.10      val ((simps' :: rules', [induct']), thy2) =
    6.11        Proof_Context.theory_of ctxt1
    6.12 @@ -2842,7 +2842,8 @@
    6.13        |> Global_Theory.add_thmss
    6.14          (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    6.15        ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
    6.16 -      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
    6.17 +      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules)
    6.18 +      ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules));
    6.19      val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
    6.20      val thy3 =
    6.21        thy2
     7.1 --- a/src/HOL/Predicate.thy	Mon Jul 03 14:25:07 2017 +0200
     7.2 +++ b/src/HOL/Predicate.thy	Sun Jul 02 20:13:38 2017 +0200
     7.3 @@ -208,16 +208,14 @@
     7.4    by (auto simp add: is_empty_def)
     7.5  
     7.6  definition singleton :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
     7.7 -  "\<And>default. singleton default A = (if \<exists>!x. eval A x then THE x. eval A x else default ())"
     7.8 +  "singleton default A = (if \<exists>!x. eval A x then THE x. eval A x else default ())" for default
     7.9  
    7.10  lemma singleton_eqI:
    7.11 -  fixes default
    7.12 -  shows "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton default A = x"
    7.13 +  "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton default A = x" for default
    7.14    by (auto simp add: singleton_def)
    7.15  
    7.16  lemma eval_singletonI:
    7.17 -  fixes default
    7.18 -  shows "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton default A)"
    7.19 +  "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton default A)" for default
    7.20  proof -
    7.21    assume assm: "\<exists>!x. eval A x"
    7.22    then obtain x where x: "eval A x" ..
    7.23 @@ -226,8 +224,7 @@
    7.24  qed
    7.25  
    7.26  lemma single_singleton:
    7.27 -  fixes default
    7.28 -  shows "\<exists>!x. eval A x \<Longrightarrow> single (singleton default A) = A"
    7.29 +  "\<exists>!x. eval A x \<Longrightarrow> single (singleton default A) = A" for default
    7.30  proof -
    7.31    assume assm: "\<exists>!x. eval A x"
    7.32    then have "eval A (singleton default A)"
    7.33 @@ -242,23 +239,19 @@
    7.34  qed
    7.35  
    7.36  lemma singleton_undefinedI:
    7.37 -  fixes default
    7.38 -  shows "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton default A = default ()"
    7.39 +  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton default A = default ()" for default
    7.40    by (simp add: singleton_def)
    7.41  
    7.42  lemma singleton_bot:
    7.43 -  fixes default
    7.44 -  shows "singleton default \<bottom> = default ()"
    7.45 +  "singleton default \<bottom> = default ()" for default
    7.46    by (auto simp add: bot_pred_def intro: singleton_undefinedI)
    7.47  
    7.48  lemma singleton_single:
    7.49 -  fixes default
    7.50 -  shows "singleton default (single x) = x"
    7.51 +  "singleton default (single x) = x" for default
    7.52    by (auto simp add: intro: singleton_eqI singleI elim: singleE)
    7.53  
    7.54  lemma singleton_sup_single_single:
    7.55 -  fixes default
    7.56 -  shows "singleton default (single x \<squnion> single y) = (if x = y then x else default ())"
    7.57 +  "singleton default (single x \<squnion> single y) = (if x = y then x else default ())" for default
    7.58  proof (cases "x = y")
    7.59    case True then show ?thesis by (simp add: singleton_single)
    7.60  next
    7.61 @@ -274,12 +267,10 @@
    7.62  qed
    7.63  
    7.64  lemma singleton_sup_aux:
    7.65 -  fixes default
    7.66 -  shows
    7.67    "singleton default (A \<squnion> B) = (if A = \<bottom> then singleton default B
    7.68      else if B = \<bottom> then singleton default A
    7.69      else singleton default
    7.70 -      (single (singleton default A) \<squnion> single (singleton default B)))"
    7.71 +      (single (singleton default A) \<squnion> single (singleton default B)))" for default
    7.72  proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
    7.73    case True then show ?thesis by (simp add: single_singleton)
    7.74  next
    7.75 @@ -306,11 +297,9 @@
    7.76  qed
    7.77  
    7.78  lemma singleton_sup:
    7.79 -  fixes default
    7.80 -  shows
    7.81    "singleton default (A \<squnion> B) = (if A = \<bottom> then singleton default B
    7.82      else if B = \<bottom> then singleton default A
    7.83 -    else if singleton default A = singleton default B then singleton default A else default ())"
    7.84 +    else if singleton default A = singleton default B then singleton default A else default ())" for default
    7.85    using singleton_sup_aux [of default A B] by (simp only: singleton_sup_single_single)
    7.86  
    7.87  
    7.88 @@ -567,24 +556,21 @@
    7.89    by (simp add: null_is_empty Seq_def)
    7.90  
    7.91  primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
    7.92 -  [code del]: "\<And>default. the_only default Empty = default ()"
    7.93 -| "\<And>default. the_only default (Insert x P) =
    7.94 -    (if is_empty P then x else let y = singleton default P in if x = y then x else default ())"
    7.95 -| "\<And>default. the_only default (Join P xq) =
    7.96 +  "the_only default Empty = default ()" for default
    7.97 +| "the_only default (Insert x P) =
    7.98 +    (if is_empty P then x else let y = singleton default P in if x = y then x else default ())" for default
    7.99 +| "the_only default (Join P xq) =
   7.100      (if is_empty P then the_only default xq else if null xq then singleton default P
   7.101         else let x = singleton default P; y = the_only default xq in
   7.102 -       if x = y then x else default ())"
   7.103 +       if x = y then x else default ())" for default
   7.104  
   7.105  lemma the_only_singleton:
   7.106 -  fixes default
   7.107 -  shows "the_only default xq = singleton default (pred_of_seq xq)"
   7.108 +  "the_only default xq = singleton default (pred_of_seq xq)" for default
   7.109    by (induct xq)
   7.110      (auto simp add: singleton_bot singleton_single is_empty_def
   7.111      null_is_empty Let_def singleton_sup)
   7.112  
   7.113  lemma singleton_code [code]:
   7.114 -  fixes default
   7.115 -  shows
   7.116    "singleton default (Seq f) =
   7.117      (case f () of
   7.118        Empty \<Rightarrow> default ()
   7.119 @@ -594,7 +580,7 @@
   7.120      | Join P xq \<Rightarrow> if is_empty P then the_only default xq
   7.121          else if null xq then singleton default P
   7.122          else let x = singleton default P; y = the_only default xq in
   7.123 -          if x = y then x else default ())"
   7.124 +          if x = y then x else default ())" for default
   7.125    by (cases "f ()")
   7.126     (auto simp add: Seq_def the_only_singleton is_empty_def
   7.127        null_is_empty singleton_bot singleton_single singleton_sup Let_def)
     8.1 --- a/src/HOL/Product_Type.thy	Mon Jul 03 14:25:07 2017 +0200
     8.2 +++ b/src/HOL/Product_Type.thy	Sun Jul 02 20:13:38 2017 +0200
     8.3 @@ -49,7 +49,7 @@
     8.4    shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
     8.5    using assms by simp_all
     8.6  
     8.7 -setup \<open>Code.add_case @{thm If_case_cert}\<close>
     8.8 +setup \<open>Code.declare_case_global @{thm If_case_cert}\<close>
     8.9  
    8.10  code_printing
    8.11    constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
     9.1 --- a/src/HOL/String.thy	Mon Jul 03 14:25:07 2017 +0200
     9.2 +++ b/src/HOL/String.thy	Sun Jul 02 20:13:38 2017 +0200
     9.3 @@ -319,7 +319,7 @@
     9.4  definition implode :: "string \<Rightarrow> String.literal"
     9.5  where
     9.6    [code del]: "implode = STR"
     9.7 -  
     9.8 +
     9.9  instantiation literal :: size
    9.10  begin
    9.11  
    10.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
    10.3 @@ -1386,11 +1386,8 @@
    10.4              |> Proof_Context.export names_lthy lthy
    10.5            end;
    10.6  
    10.7 -        val code_attrs =
    10.8 -          if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
    10.9 -
   10.10          val anonymous_notes =
   10.11 -          [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
   10.12 +          [(rel_code_thms, nitpicksimp_attrs)]
   10.13            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   10.14  
   10.15          val notes =
   10.16 @@ -1402,7 +1399,7 @@
   10.17             (ctr_transferN, ctr_transfer_thms, K []),
   10.18             (disc_transferN, disc_transfer_thms, K []),
   10.19             (sel_transferN, sel_transfer_thms, K []),
   10.20 -           (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
   10.21 +           (mapN, map_thms, K (nitpicksimp_attrs @ simp_attrs)),
   10.22             (map_disc_iffN, map_disc_iff_thms, K simp_attrs),
   10.23             (map_selN, map_sel_thms, K []),
   10.24             (pred_injectN, pred_injects, K simp_attrs),
   10.25 @@ -1411,7 +1408,7 @@
   10.26             (rel_injectN, rel_inject_thms, K simp_attrs),
   10.27             (rel_introsN, rel_intro_thms, K []),
   10.28             (rel_selN, rel_sel_thms, K []),
   10.29 -           (setN, set_thms, K (code_attrs @ case_fp fp nitpicksimp_attrs [] @ simp_attrs)),
   10.30 +           (setN, set_thms, K (case_fp fp nitpicksimp_attrs [] @ simp_attrs)),
   10.31             (set_casesN, set_cases_thms, nth set_cases_attrss),
   10.32             (set_introsN, set_intros_thms, K []),
   10.33             (set_selN, set_sel_thms, K [])]
   10.34 @@ -1422,6 +1419,7 @@
   10.35            |> fp = Least_FP
   10.36              ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_code_thms)
   10.37            |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms)
   10.38 +          |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms))
   10.39            |> Local_Theory.notes (anonymous_notes @ notes);
   10.40  
   10.41          val subst = Morphism.thm (substitute_noted_thm noted);
   10.42 @@ -1848,11 +1846,9 @@
   10.43  
   10.44      val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
   10.45  
   10.46 -    val code_attrs =
   10.47 -      if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
   10.48    in
   10.49      ((induct_thms, induct_thm, mk_induct_attrs ctrss),
   10.50 -     (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
   10.51 +     (rec_thmss, nitpicksimp_attrs @ simp_attrs))
   10.52    end;
   10.53  
   10.54  fun mk_coinduct_attrs fpTs ctrss discss mss =
   10.55 @@ -2480,9 +2476,6 @@
   10.56      val fpTs = map (domain_type o fastype_of) dtors;
   10.57      val fpBTs = map B_ify_T fpTs;
   10.58  
   10.59 -    val code_attrs =
   10.60 -      if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
   10.61 -
   10.62      val real_unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fpTs);
   10.63  
   10.64      val ctr_Tsss = map (map (map real_unfreeze_fp)) ctrXs_Tsss;
   10.65 @@ -2698,6 +2691,7 @@
   10.66        in
   10.67          lthy
   10.68          |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
   10.69 +        |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
   10.70          |> Local_Theory.notes (common_notes @ notes)
   10.71          (* for "datatype_realizer.ML": *)
   10.72          |>> name_noted_thms
   10.73 @@ -2865,7 +2859,7 @@
   10.74              fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
   10.75             (coinduct_strongN, map single coinduct_strong_thms, K coinduct_attrs),
   10.76             (corecN, corec_thmss, K []),
   10.77 -           (corec_codeN, map single corec_code_thms, K (code_attrs @ nitpicksimp_attrs)),
   10.78 +           (corec_codeN, map single corec_code_thms, K (nitpicksimp_attrs)),
   10.79             (corec_discN, corec_disc_thmss, K []),
   10.80             (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
   10.81             (corec_selN, corec_sel_thmss, K corec_sel_attrs),
   10.82 @@ -2878,6 +2872,7 @@
   10.83          lthy
   10.84          |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
   10.85            [flat corec_sel_thmss, flat corec_thmss]
   10.86 +        |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms)
   10.87          |> Local_Theory.notes (common_notes @ notes)
   10.88          |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
   10.89            fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars
    11.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
    11.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
    11.3 @@ -2121,8 +2121,6 @@
    11.4            |> derive_and_update_coinduct_cong_intross [corec_info];
    11.5          val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
    11.6  
    11.7 -        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
    11.8 -
    11.9          val anonymous_notes = [];
   11.10  (* TODO:
   11.11            [(flat disc_iff_or_disc_thmss, simp_attrs)]
   11.12 @@ -2131,7 +2129,7 @@
   11.13  
   11.14          val notes =
   11.15            [(cong_introsN, maps snd cong_intros_pairs, []),
   11.16 -           (codeN, [code_thm], code_attrs @ nitpicksimp_attrs),
   11.17 +           (codeN, [code_thm], nitpicksimp_attrs),
   11.18             (coinductN, [coinduct], coinduct_attrs),
   11.19             (inner_inductN, inner_fp_inducts, []),
   11.20             (uniqueN, uniques, [])] @
   11.21 @@ -2160,6 +2158,7 @@
   11.22          |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], flat ctr_thmss)
   11.23  *)
   11.24          |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], [code_thm])
   11.25 +        |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
   11.26          |> Local_Theory.notes (anonymous_notes @ notes)
   11.27          |> snd
   11.28        end;
    12.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
    12.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
    12.3 @@ -1498,8 +1498,6 @@
    12.4          val common_name = mk_common_name fun_names;
    12.5          val common_qualify = fold_rev I qualifys;
    12.6  
    12.7 -        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
    12.8 -
    12.9          val anonymous_notes =
   12.10            [(flat disc_iff_or_disc_thmss, simp_attrs)]
   12.11            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   12.12 @@ -1516,7 +1514,7 @@
   12.13            [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs),
   12.14             (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms,
   12.15              coinduct_attrs),
   12.16 -           (codeN, code_thmss, code_attrs @ nitpicksimp_attrs),
   12.17 +           (codeN, code_thmss, nitpicksimp_attrs),
   12.18             (ctrN, ctr_thmss, []),
   12.19             (discN, disc_thmss, []),
   12.20             (disc_iffN, disc_iff_thmss, []),
   12.21 @@ -1537,6 +1535,7 @@
   12.22          |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat sel_thmss)
   12.23          |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat ctr_thmss)
   12.24          |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat code_thmss)
   12.25 +        |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
   12.26          |> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
   12.27          |> snd
   12.28          |> (fn lthy =>
    13.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jul 03 14:25:07 2017 +0200
    13.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sun Jul 02 20:13:38 2017 +0200
    13.3 @@ -460,16 +460,16 @@
    13.4    Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
    13.5    #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f);
    13.6  
    13.7 -val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib Code.Equation :: @{attributes [nitpick_simp, simp]};
    13.8 +val nitpicksimp_simp_attrs = @{attributes [nitpick_simp, simp]};
    13.9  
   13.10  fun datatype_compat fpT_names lthy =
   13.11    let
   13.12      val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
   13.13        mk_infos_of_mutually_recursive_new_datatypes [] eq_set fpT_names lthy;
   13.14  
   13.15 -    val all_notes =
   13.16 +    val (all_notes, rec_thmss) =
   13.17        (case lfp_sugar_thms of
   13.18 -        NONE => []
   13.19 +        NONE => ([], [])
   13.20        | SOME ((inducts, induct, induct_attrs), (rec_thmss, _)) =>
   13.21          let
   13.22            val common_name = compat_N ^ mk_common_name b_names;
   13.23 @@ -482,7 +482,7 @@
   13.24  
   13.25            val notes =
   13.26              [(inductN, map single inducts, induct_attrs),
   13.27 -             (recN, rec_thmss, code_nitpicksimp_simp_attrs)]
   13.28 +             (recN, rec_thmss, nitpicksimp_simp_attrs)]
   13.29              |> filter_out (null o #2)
   13.30              |> maps (fn (thmN, thmss, attrs) =>
   13.31                if forall null thmss then
   13.32 @@ -492,7 +492,7 @@
   13.33                      ((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])]))
   13.34                    compat_b_names thmss);
   13.35          in
   13.36 -          common_notes @ notes
   13.37 +          (common_notes @ notes, rec_thmss)
   13.38          end);
   13.39  
   13.40      val register_interpret =
   13.41 @@ -503,6 +503,7 @@
   13.42      |> Local_Theory.raw_theory register_interpret
   13.43      |> Local_Theory.notes all_notes
   13.44      |> snd
   13.45 +    |> Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
   13.46    end;
   13.47  
   13.48  val datatype_compat_global = Named_Target.theory_map o datatype_compat;
    14.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
    14.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
    14.3 @@ -623,8 +623,6 @@
    14.4      val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts;
    14.5      val transfer = exists (can (fn Transfer_Option => ())) opts;
    14.6  
    14.7 -    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
    14.8 -
    14.9      val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
   14.10  
   14.11      val mk_notes =
   14.12 @@ -633,7 +631,7 @@
   14.13            val (bs, attrss) = map_split (fst o nth specs) js;
   14.14            val notes =
   14.15              @{map 3} (fn b => fn attrs => fn thm =>
   14.16 -                ((Binding.qualify false prefix b, code_attrs @ nitpicksimp_simp_attrs @ attrs),
   14.17 +                ((Binding.qualify false prefix b, nitpicksimp_simp_attrs @ attrs),
   14.18                   [([thm], [])]))
   14.19                bs attrss thms;
   14.20          in
   14.21 @@ -645,7 +643,9 @@
   14.22      |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) =>
   14.23        Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
   14.24        #> Local_Theory.notes (mk_notes jss names qualifys simpss)
   14.25 -      #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
   14.26 +      #-> (fn notes =>
   14.27 +        plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (maps snd notes))
   14.28 +        #> pair (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
   14.29    end
   14.30    handle OLD_PRIMREC () =>
   14.31      old_primrec int raw_fixes raw_specs lthy
    15.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Jul 03 14:25:07 2017 +0200
    15.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sun Jul 02 20:13:38 2017 +0200
    15.3 @@ -355,9 +355,6 @@
    15.4              size_gen_o_map_thmss
    15.5            end;
    15.6  
    15.7 -      (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
    15.8 -      val code_attrs = Code.add_default_eqn_attrib Code.Equation;
    15.9 -
   15.10        val massage_multi_notes =
   15.11          maps (fn (thmN, thmss, attrs) =>
   15.12            map2 (fn T_name => fn thms =>
   15.13 @@ -367,7 +364,7 @@
   15.14          #> filter_out (null o fst o hd o snd);
   15.15  
   15.16        val notes =
   15.17 -        [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
   15.18 +        [(sizeN, size_thmss, nitpicksimp_attrs @ simp_attrs),
   15.19           (size_genN, size_gen_thmss, []),
   15.20           (size_gen_o_mapN, size_gen_o_map_thmss, []),
   15.21           (size_neqN, size_neq_thmss, [])]
   15.22 @@ -377,6 +374,8 @@
   15.23          lthy2
   15.24          |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
   15.25          |> Spec_Rules.add Spec_Rules.Equational (overloaded_size_consts, overloaded_size_simps)
   15.26 +        |> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
   15.27 +          (*Ideally, this would only be issued if the "code" plugin is enabled.*)
   15.28          |> Local_Theory.notes notes;
   15.29  
   15.30        val phi0 = substitute_noted_thm noted;
    16.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jul 03 14:25:07 2017 +0200
    16.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun Jul 02 20:13:38 2017 +0200
    16.3 @@ -1072,19 +1072,17 @@
    16.4          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    16.5          val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
    16.6  
    16.7 -        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
    16.8 -
    16.9          val nontriv_disc_eq_thmss =
   16.10            map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
   16.11              handle THM _ => th RS @{thm eq_True[THEN iffD2]})) nontriv_disc_thmss;
   16.12  
   16.13          val anonymous_notes =
   16.14            [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
   16.15 -           (flat nontriv_disc_eq_thmss, code_attrs @ nitpicksimp_attrs)]
   16.16 +           (flat nontriv_disc_eq_thmss, nitpicksimp_attrs)]
   16.17            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   16.18  
   16.19          val notes =
   16.20 -          [(caseN, case_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
   16.21 +          [(caseN, case_thms, nitpicksimp_attrs @ simp_attrs),
   16.22             (case_congN, [case_cong_thm], []),
   16.23             (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
   16.24             (case_distribN, [case_distrib_thm], []),
   16.25 @@ -1101,7 +1099,7 @@
   16.26             (expandN, expand_thms, []),
   16.27             (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
   16.28             (nchotomyN, [nchotomy_thm], []),
   16.29 -           (selN, all_sel_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
   16.30 +           (selN, all_sel_thms, nitpicksimp_attrs @ simp_attrs),
   16.31             (splitN, [split_thm], []),
   16.32             (split_asmN, [split_asm_thm], []),
   16.33             (split_selN, split_sel_thms, []),
   16.34 @@ -1121,15 +1119,14 @@
   16.35            |> Local_Theory.declaration {syntax = false, pervasive = true}
   16.36              (fn phi => Case_Translation.register
   16.37                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
   16.38 -          |> Local_Theory.background_theory
   16.39 -            (fold (fold Code.del_eqn_silent) [nontriv_disc_defs, sel_defs])
   16.40            |> plugins code_plugin ?
   16.41 -             Local_Theory.declaration {syntax = false, pervasive = false}
   16.42 +             (Code.declare_default_eqns (map (rpair true) (flat nontriv_disc_eq_thmss @ case_thms @ all_sel_thms))
   16.43 +             #> Local_Theory.declaration {syntax = false, pervasive = false}
   16.44                 (fn phi => Context.mapping
   16.45                    (add_ctr_code fcT_name (map (Morphism.typ phi) As)
   16.46                       (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
   16.47                       (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
   16.48 -                  I)
   16.49 +                  I))
   16.50            |> Local_Theory.notes (anonymous_notes @ notes)
   16.51            (* for "datatype_realizer.ML": *)
   16.52            |>> name_noted_thms fcT_name exhaustN;
    17.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Jul 03 14:25:07 2017 +0200
    17.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sun Jul 02 20:13:38 2017 +0200
    17.3 @@ -109,12 +109,13 @@
    17.4      Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
    17.5      #> add_def
    17.6      #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single
    17.7 -    #-> fold Code.del_eqn
    17.8 +    #> snd
    17.9      #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
   17.10      #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.theoremK
   17.11 -      [((qualify reflN, [Code.add_default_eqn_attribute Code.Nbe]), [([thm], [])]),
   17.12 -        ((qualify simpsN, [Code.add_default_eqn_attribute Code.Equation]), [(rev thms, [])])])
   17.13 -    #> snd
   17.14 +          [((qualify reflN, []), [([thm], [])]),
   17.15 +            ((qualify simpsN, []), [(rev thms, [])])])
   17.16 +    #-> (fn [(_, [thm]), (_, thms)] =>
   17.17 +          Code.declare_default_eqns_global ((thm, false) :: map (rpair true) thms))
   17.18    end;
   17.19  
   17.20  fun add_ctr_code fcT_name raw_As raw_ctrs inject_thms distinct_thms case_thms thy =
   17.21 @@ -126,9 +127,9 @@
   17.22    in
   17.23      if can (Code.constrset_of_consts thy) unover_ctrs then
   17.24        thy
   17.25 -      |> Code.add_datatype ctrs
   17.26 -      |> fold_rev (Code.add_eqn (Code.Equation, true)) case_thms
   17.27 -      |> Code.add_case (mk_case_certificate (Proof_Context.init_global thy) case_thms)
   17.28 +      |> Code.declare_datatype_global ctrs
   17.29 +      |> Code.declare_default_eqns_global (map (rpair true) (rev case_thms))
   17.30 +      |> Code.declare_case_global (mk_case_certificate (Proof_Context.init_global thy) case_thms)
   17.31        |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
   17.32          ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
   17.33      else
    18.1 --- a/src/HOL/Tools/Function/function.ML	Mon Jul 03 14:25:07 2017 +0200
    18.2 +++ b/src/HOL/Tools/Function/function.ML	Sun Jul 02 20:13:38 2017 +0200
    18.3 @@ -45,7 +45,7 @@
    18.4  open Function_Common
    18.5  
    18.6  val simp_attribs =
    18.7 -  @{attributes [simp, nitpick_simp]} @ [Code.add_default_eqn_attrib Code.Equation]
    18.8 +  @{attributes [simp, nitpick_simp]}
    18.9  
   18.10  val psimp_attribs =
   18.11    @{attributes [nitpick_psimp]}
   18.12 @@ -195,6 +195,7 @@
   18.13        in
   18.14          lthy
   18.15          |> add_simps I "simps" I simp_attribs tsimps
   18.16 +        ||> Code.declare_default_eqns (map (rpair true) tsimps)
   18.17          ||>> Local_Theory.note
   18.18            ((derived_name defname "induct", [Attrib.case_names case_names]), tinduct)
   18.19          ||>> fold_map (note_derived ("elims", [Attrib.consumes 1, Attrib.constraints 1]))
    19.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Jul 03 14:25:07 2017 +0200
    19.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun Jul 02 20:13:38 2017 +0200
    19.3 @@ -451,17 +451,17 @@
    19.4  
    19.5    in
    19.6      if is_valid_eq abs_eq_thm then
    19.7 -      (ABS_EQ, Code.add_eqn (Code.Equation, true) abs_eq_thm thy)
    19.8 +      (ABS_EQ, Code.declare_default_eqns_global [(abs_eq_thm, true)] thy)
    19.9      else
   19.10        let
   19.11          val (rty_body, qty_body) = get_body_types (rty, qty)
   19.12        in
   19.13          if rty_body = qty_body then
   19.14 -          (REP_EQ, Code.add_eqn (Code.Equation, true) (the opt_rep_eq_thm) thy)
   19.15 +          (REP_EQ, Code.declare_default_eqns_global [(the opt_rep_eq_thm, true)] thy)
   19.16          else
   19.17            if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm)
   19.18            then
   19.19 -            (REP_EQ, Code.add_eqn (Code.Abstract, true) (the opt_rep_eq_thm) thy)
   19.20 +            (REP_EQ, Code.declare_abstract_eqn_global (the opt_rep_eq_thm) thy)
   19.21            else
   19.22              (NONE_EQ, thy)
   19.23        end
    20.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Jul 03 14:25:07 2017 +0200
    20.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun Jul 02 20:13:38 2017 +0200
    20.3 @@ -177,25 +177,16 @@
    20.4        let
    20.5          val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy
    20.6        in  
    20.7 -         Local_Theory.background_theory (Code.add_datatype [dest_Const fixed_abs]) lthy'
    20.8 +         Local_Theory.background_theory
    20.9 +           (Code.declare_datatype_global [dest_Const fixed_abs]) lthy'
   20.10        end
   20.11      else
   20.12        lthy
   20.13    end
   20.14  
   20.15 -fun define_abs_type quot_thm lthy =
   20.16 -  if Lifting_Def.can_generate_code_cert quot_thm then
   20.17 -    let
   20.18 -      val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
   20.19 -      val add_abstype_attribute = 
   20.20 -          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype_default thm) I)
   20.21 -        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
   20.22 -    in
   20.23 -      lthy
   20.24 -        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
   20.25 -    end
   20.26 -  else
   20.27 -    lthy
   20.28 +fun define_abs_type quot_thm =
   20.29 +  Lifting_Def.can_generate_code_cert quot_thm ?
   20.30 +    Code.declare_abstype (quot_thm RS @{thm Quotient_abs_rep});
   20.31  
   20.32  local
   20.33    exception QUOT_ERROR of Pretty.T list
    21.1 --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Jul 03 14:25:07 2017 +0200
    21.2 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Jul 02 20:13:38 2017 +0200
    21.3 @@ -276,7 +276,7 @@
    21.4    let
    21.5      val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
    21.6      fun attr_bindings prefix = map (fn ((b, attrs), _) =>
    21.7 -      (Binding.qualify false prefix b, Code.add_default_eqn_attrib Code.Equation :: attrs)) spec;
    21.8 +      (Binding.qualify false prefix b, attrs)) spec;
    21.9      fun simp_attr_binding prefix =
   21.10        (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]});
   21.11    in
   21.12 @@ -286,7 +286,9 @@
   21.13        Spec_Rules.add Spec_Rules.Equational (ts, simps)
   21.14        #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
   21.15        #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
   21.16 -      #>> (fn (_, simps'') => (ts, simps''))))
   21.17 +      #-> (fn (_, simps'') => 
   21.18 +        Code.declare_default_eqns (map (rpair true) simps'')
   21.19 +        #> pair (ts, simps''))))
   21.20    end;
   21.21  
   21.22  in
    22.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Jul 03 14:25:07 2017 +0200
    22.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Jul 02 20:13:38 2017 +0200
    22.3 @@ -570,7 +570,6 @@
    22.4          ((prfx (Binding.name "splits"), []), [(maps (fn (x, y) => [x, y]) splits, [])]),
    22.5          ((Binding.empty, [Simplifier.simp_add]),
    22.6            [(flat case_rewrites @ flat distinct @ rec_rewrites, [])]),
    22.7 -        ((Binding.empty, [Code.add_default_eqn_attribute Code.Equation]), [(rec_rewrites, [])]),
    22.8          ((Binding.empty, [iff_add]), [(flat inject, [])]),
    22.9          ((Binding.empty, [Classical.safe_elim NONE]),
   22.10            [(map (fn th => th RS notE) (flat distinct), [])]),
   22.11 @@ -578,6 +577,7 @@
   22.12          ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
   22.13            named_rules @ unnamed_rules)
   22.14      |> snd
   22.15 +    |> Code.declare_default_eqns_global (map (rpair true) rec_rewrites)
   22.16      |> Old_Datatype_Data.register dt_infos
   22.17      |> Context.theory_map (fold2 Case_Translation.register case_combs constrss)
   22.18      |> Old_Datatype_Data.interpretation_data (config, dt_names)
    23.1 --- a/src/HOL/Tools/Old_Datatype/old_size.ML	Mon Jul 03 14:25:07 2017 +0200
    23.2 +++ b/src/HOL/Tools/Old_Datatype/old_size.ML	Sun Jul 02 20:13:38 2017 +0200
    23.3 @@ -195,14 +195,15 @@
    23.4          val ([(_, size_thms)], thy'') = thy'
    23.5            |> Global_Theory.note_thmss ""
    23.6              [((Binding.name "size",
    23.7 -                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
    23.8 -                 Code.add_default_eqn_attribute Code.Equation]),
    23.9 +                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}]),
   23.10                [(size_eqns, [])])];
   23.11  
   23.12        in
   23.13 -        fold2 (fn new_type_name => fn size_name =>
   23.14 +        thy''
   23.15 +        |> fold2 (fn new_type_name => fn size_name =>
   23.16              BNF_LFP_Size.register_size_global new_type_name size_name refl(*dummy*) size_thms [])
   23.17 -          new_type_names size_names thy''
   23.18 +          new_type_names size_names 
   23.19 +        |> Code.declare_default_eqns_global (map (rpair true) size_thms)
   23.20        end
   23.21    end;
   23.22  
    24.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jul 03 14:25:07 2017 +0200
    24.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Jul 02 20:13:38 2017 +0200
    24.3 @@ -1421,15 +1421,13 @@
    24.4      val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
    24.5        (maps_modes result_thms)
    24.6      val qname = #qname (dest_steps steps)
    24.7 -    val attrib = Thm.declaration_attribute (fn thm => Context.mapping
    24.8 -      (Code.add_eqn (Code.Equation, false) thm) I)
    24.9 -      (*FIXME default code equation!?*)
   24.10 -    val thy''' =
   24.11 -      cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ =>
   24.12 -      fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
   24.13 -      [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
   24.14 -        [attrib])] thy))
   24.15 -      result_thms' thy'')
   24.16 +    val thy''' = cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...."
   24.17 +      (fn _ =>
   24.18 +        thy''
   24.19 +        |> fold_map (fn (name, result_thms) => (Global_Theory.add_thmss
   24.20 +            [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [])]))
   24.21 +            result_thms'
   24.22 +        |-> (fn notes => Code.declare_default_eqns_global (map (rpair true) (flat (flat (notes))))))
   24.23    in
   24.24      thy'''
   24.25    end
    25.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 03 14:25:07 2017 +0200
    25.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Jul 02 20:13:38 2017 +0200
    25.3 @@ -110,8 +110,7 @@
    25.4      val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs
    25.5    in
    25.6      thy
    25.7 -    |> Code.del_eqns const
    25.8 -    |> fold (Code.add_eqn (Code.Equation, false)) eqs (*FIXME default code equation!?*)
    25.9 +    |> Code.declare_default_eqns_global (map (rpair true) eqs)
   25.10    end
   25.11  
   25.12  fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
    26.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jul 03 14:25:07 2017 +0200
    26.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Jul 02 20:13:38 2017 +0200
    26.3 @@ -382,11 +382,11 @@
    26.4          val eqs = map (fn eq => Goal.prove lthy argnames [] eq
    26.5            (fn {context = ctxt, ...} => ALLGOALS (Skip_Proof.cheat_tac ctxt))) eqs_t
    26.6        in
    26.7 -        fold (fn (name, eq) => Local_Theory.note
    26.8 -          ((Binding.qualify true prfx
    26.9 -              (Binding.qualify true name (Binding.name "simps")),
   26.10 -             [Code.add_default_eqn_attrib Code.Equation]), [eq]) #> snd)
   26.11 -          (names ~~ eqs) lthy
   26.12 +        lthy
   26.13 +        |> fold_map (fn (name, eq) => Local_Theory.note
   26.14 +             (((Binding.qualify true prfx o Binding.qualify true name) (Binding.name "simps"), []), [eq]))
   26.15 +               (names ~~ eqs) 
   26.16 +        |-> (fn notes => Code.declare_default_eqns (map (rpair true) (maps snd notes)))
   26.17        end)
   26.18  
   26.19  
    27.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 03 14:25:07 2017 +0200
    27.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Jul 02 20:13:38 2017 +0200
    27.3 @@ -179,8 +179,8 @@
    27.4      |> random_aux_primrec_multi (name ^ prfx) proto_eqs
    27.5      |-> prove_simps
    27.6      |-> (fn simps => Local_Theory.note
    27.7 -      ((b, Code.add_default_eqn_attrib Code.Equation:: @{attributes [simp, nitpick_simp]}), simps))
    27.8 -    |> snd
    27.9 +          ((b, @{attributes [simp, nitpick_simp]}), simps))
   27.10 +    |-> (fn (_, thms) => Code.declare_default_eqns (map (rpair true) thms))
   27.11    end
   27.12  
   27.13  
    28.1 --- a/src/HOL/Tools/code_evaluation.ML	Mon Jul 03 14:25:07 2017 +0200
    28.2 +++ b/src/HOL/Tools/code_evaluation.ML	Sun Jul 02 20:13:38 2017 +0200
    28.3 @@ -83,8 +83,7 @@
    28.4      val eqs = map (mk_term_of_eq thy ty) cs;
    28.5   in
    28.6      thy
    28.7 -    |> Code.del_eqns const
    28.8 -    |> fold (Code.add_eqn (Code.Equation, false)) eqs
    28.9 +    |> Code.declare_default_eqns_global (map (rpair true) eqs)
   28.10    end;
   28.11  
   28.12  fun ensure_term_of_code (tyco, (vs, cs)) =
   28.13 @@ -115,8 +114,7 @@
   28.14      val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
   28.15   in
   28.16      thy
   28.17 -    |> Code.del_eqns const
   28.18 -    |> Code.add_eqn (Code.Equation, false) eq
   28.19 +    |> Code.declare_default_eqns_global [(eq, true)]
   28.20    end;
   28.21  
   28.22  fun ensure_abs_term_of_code (tyco, (vs, ((abs, (_, ty)), (proj, _)))) =
    29.1 --- a/src/HOL/Tools/record.ML	Mon Jul 03 14:25:07 2017 +0200
    29.2 +++ b/src/HOL/Tools/record.ML	Sun Jul 02 20:13:38 2017 +0200
    29.3 @@ -1775,20 +1775,24 @@
    29.4        val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
    29.5        val ensure_exhaustive_record =
    29.6          ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
    29.7 +      fun add_code eq_def thy =
    29.8 +        let
    29.9 +          val ctxt = Proof_Context.init_global thy;
   29.10 +        in
   29.11 +          thy
   29.12 +          |> Code.declare_default_eqns_global
   29.13 +               [(mk_eq (Proof_Context.init_global thy) eq_def, true), (mk_eq_refl (Proof_Context.init_global thy), false)]
   29.14 +        end;
   29.15      in
   29.16        thy
   29.17 -      |> Code.add_datatype [ext]
   29.18 -      |> fold (Code.add_eqn (Code.Equation, true)) simps
   29.19 +      |> Code.declare_datatype_global [ext]
   29.20 +      |> Code.declare_default_eqns_global (map (rpair true) simps)
   29.21        |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
   29.22        |> `(fn lthy => Syntax.check_term lthy eq)
   29.23        |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
   29.24        |-> (fn (_, (_, eq_def)) =>
   29.25           Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
   29.26 -      |-> (fn eq_def => fn thy =>
   29.27 -            thy
   29.28 -            |> Code.del_eqn eq_def
   29.29 -            |> Code.add_eqn (Code.Equation, true) (mk_eq (Proof_Context.init_global thy) eq_def))
   29.30 -      |> (fn thy => Code.add_eqn (Code.Nbe, true) (mk_eq_refl (Proof_Context.init_global thy)) thy)
   29.31 +      |-> add_code
   29.32        |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
   29.33        |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
   29.34      end
   29.35 @@ -2045,8 +2049,7 @@
   29.36            ||>> (Global_Theory.add_defs false o
   29.37                  map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
   29.38            ||>> (Global_Theory.add_defs false o
   29.39 -                map (rpair [Code.add_default_eqn_attribute Code.Equation]
   29.40 -                o apfst (Binding.concealed o Binding.name)))
   29.41 +                map (Thm.no_attributes o apfst (Binding.concealed o Binding.name)))
   29.42              [make_spec, fields_spec, extend_spec, truncate_spec]);
   29.43      val defs_ctxt = Proof_Context.init_global defs_thy;
   29.44  
   29.45 @@ -2212,6 +2215,7 @@
   29.46            (_, splits' as [split_meta', split_object', split_ex']), (_, derived_defs'),
   29.47            (_, [surjective']), (_, [equality']), (_, [induct_scheme']), (_, [induct']),
   29.48            (_, [cases_scheme']), (_, [cases'])], thms_thy) = defs_thy
   29.49 +      |> Code.declare_default_eqns_global (map (rpair true) derived_defs)
   29.50        |> Global_Theory.note_thmss ""
   29.51         [((Binding.name "select_convs", []), [(sel_convs, [])]),
   29.52          ((Binding.name "update_convs", []), [(upd_convs, [])]),
    30.1 --- a/src/Pure/Isar/code.ML	Mon Jul 03 14:25:07 2017 +0200
    30.2 +++ b/src/Pure/Isar/code.ML	Sun Jul 02 20:13:38 2017 +0200
    30.3 @@ -30,29 +30,28 @@
    30.4    val pretty_cert: theory -> cert -> Pretty.T list
    30.5  
    30.6    (*executable code*)
    30.7 -  val add_datatype: (string * typ) list -> theory -> theory
    30.8 -  val add_datatype_cmd: string list -> theory -> theory
    30.9 +  val declare_datatype_global: (string * typ) list -> theory -> theory
   30.10 +  val declare_datatype_cmd: string list -> theory -> theory
   30.11    val datatype_interpretation:
   30.12      (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
   30.13        -> theory -> theory) -> theory -> theory
   30.14 -  val add_abstype: thm -> theory -> theory
   30.15 -  val add_abstype_default: thm -> theory -> theory
   30.16 +  val declare_abstype: thm -> local_theory -> local_theory
   30.17 +  val declare_abstype_global: thm -> theory -> theory
   30.18    val abstype_interpretation:
   30.19      (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
   30.20        -> theory -> theory) -> theory -> theory
   30.21 -  type kind
   30.22 -  val Equation: kind
   30.23 -  val Nbe: kind
   30.24 -  val Abstract: kind
   30.25 -  val add_eqn: kind * bool -> thm -> theory -> theory
   30.26 -  val add_default_eqn_attribute: kind -> attribute
   30.27 -  val add_default_eqn_attrib: kind -> Token.src
   30.28 -  val del_eqn_silent: thm -> theory -> theory
   30.29 -  val del_eqn: thm -> theory -> theory
   30.30 -  val del_eqns: string -> theory -> theory
   30.31 -  val del_exception: string -> theory -> theory
   30.32 -  val add_case: thm -> theory -> theory
   30.33 -  val add_undefined: string -> theory -> theory
   30.34 +  val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory
   30.35 +  val declare_default_eqns_global: (thm * bool) list -> theory -> theory
   30.36 +  val declare_eqns: (thm * bool) list -> local_theory -> local_theory
   30.37 +  val declare_eqns_global: (thm * bool) list -> theory -> theory
   30.38 +  val add_eqn_global: thm * bool -> theory -> theory
   30.39 +  val del_eqn_global: thm -> theory -> theory
   30.40 +  val declare_abstract_eqn: thm -> local_theory -> local_theory
   30.41 +  val declare_abstract_eqn_global: thm -> theory -> theory
   30.42 +  val declare_empty_global: string -> theory -> theory
   30.43 +  val declare_unimplemented_global: string -> theory -> theory
   30.44 +  val declare_case_global: thm -> theory -> theory
   30.45 +  val declare_undefined_global: string -> theory -> theory
   30.46    val get_type: theory -> string
   30.47      -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool
   30.48    val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
   30.49 @@ -169,21 +168,17 @@
   30.50  (* functions *)
   30.51  
   30.52  datatype fun_spec = Unimplemented
   30.53 -  | Eqns_Default of (thm * bool) list * (thm * bool) list lazy
   30.54 -      (* (cache for default equations, lazy computation of default equations)
   30.55 -         -- helps to restore natural order of default equations *)
   30.56 +  | Eqns_Default of (thm * bool) list
   30.57    | Eqns of (thm * bool) list
   30.58 -  | Proj of (term * string) * bool
   30.59 -  | Abstr of (thm * string) * bool;
   30.60 +  | Proj of term * string
   30.61 +  | Abstr of thm * string;
   30.62  
   30.63 -val default_fun_spec = Eqns_Default ([], Lazy.value []);
   30.64 +val default_fun_spec = Eqns_Default [];
   30.65  
   30.66  fun is_default (Eqns_Default _) = true
   30.67 -  | is_default (Proj (_, default)) = default
   30.68 -  | is_default (Abstr (_, default)) = default
   30.69    | is_default _ = false;
   30.70  
   30.71 -fun associated_abstype (Abstr ((_, tyco), _)) = SOME tyco
   30.72 +fun associated_abstype (Abstr (_, tyco)) = SOME tyco
   30.73    | associated_abstype _ = NONE;
   30.74  
   30.75  
   30.76 @@ -648,6 +643,33 @@
   30.77  fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
   30.78  
   30.79  
   30.80 +(* preparation and classification of code equations *)
   30.81 +
   30.82 +fun prep_eqn strictness thy =
   30.83 +  apfst (meta_rewrite thy)
   30.84 +  #> generic_assert_eqn strictness thy false
   30.85 +  #> Option.map (fn eqn => (const_eqn thy (fst eqn), eqn));
   30.86 +  
   30.87 +fun prep_eqns strictness thy =
   30.88 +  map_filter (prep_eqn strictness thy)
   30.89 +  #> AList.group (op =);
   30.90 +
   30.91 +fun prep_abs_eqn strictness thy =
   30.92 +  meta_rewrite thy
   30.93 +  #> generic_assert_abs_eqn strictness thy NONE
   30.94 +  #> Option.map (fn abs_eqn => (const_abs_eqn thy (fst abs_eqn), abs_eqn));
   30.95 +
   30.96 +fun prep_maybe_abs_eqn thy raw_thm =
   30.97 +  let
   30.98 +    val thm = meta_rewrite thy raw_thm;
   30.99 +    val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm;
  30.100 +  in case some_abs_thm of
  30.101 +      SOME (thm, tyco) => SOME (const_abs_eqn thy thm, ((thm, true), SOME tyco))
  30.102 +    | NONE => generic_assert_eqn Liberal thy false (thm, false)
  30.103 +        |> Option.map (fn (thm, _) => (const_eqn thy thm, ((thm, is_linear thm), NONE)))
  30.104 +  end;
  30.105 +
  30.106 +
  30.107  (* abstype certificates *)
  30.108  
  30.109  local
  30.110 @@ -947,12 +969,12 @@
  30.111  fun get_cert ctxt functrans c =
  30.112    case retrieve_raw (Proof_Context.theory_of ctxt) c of
  30.113      Unimplemented => nothing_cert ctxt c
  30.114 -  | Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
  30.115 +  | Eqns_Default eqns => eqns
  30.116        |> cert_of_eqns_preprocess ctxt functrans c
  30.117    | Eqns eqns => eqns
  30.118        |> cert_of_eqns_preprocess ctxt functrans c
  30.119 -  | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco
  30.120 -  | Abstr ((abs_thm, tyco), _) => abs_thm
  30.121 +  | Proj (_, tyco) => cert_of_proj ctxt c tyco
  30.122 +  | Abstr (abs_thm, tyco) => abs_thm
  30.123       |> preprocess Conv.arg_conv ctxt
  30.124       |> cert_of_abs ctxt tyco c;
  30.125  
  30.126 @@ -1027,13 +1049,13 @@
  30.127      fun pretty_equations const thms =
  30.128        (Pretty.block o Pretty.fbreaks)
  30.129          (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
  30.130 -    fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
  30.131 -          pretty_equations const (map fst (Lazy.force eqns_lazy))
  30.132 +    fun pretty_function (const, Eqns_Default eqns) =
  30.133 +          pretty_equations const (map fst eqns)
  30.134        | pretty_function (const, Eqns eqns) =
  30.135            pretty_equations const (map fst eqns)
  30.136 -      | pretty_function (const, Proj ((proj, _), _)) = Pretty.block
  30.137 +      | pretty_function (const, Proj (proj, _)) = Pretty.block
  30.138            [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
  30.139 -      | pretty_function (const, Abstr ((thm, _), _)) = pretty_equations const [thm];
  30.140 +      | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm];
  30.141      fun pretty_typ (tyco, vs) = Pretty.str
  30.142        (string_of_typ thy (Type (tyco, map TFree vs)));
  30.143      fun pretty_typspec (typ, (cos, abstract)) = if null cos
  30.144 @@ -1089,118 +1111,114 @@
  30.145  (* code equations *)
  30.146  
  30.147  (*
  30.148 -  external distinction:
  30.149 -    kind * default
  30.150 -  processual distinction:
  30.151 -    thm * proper  for concrete equations
  30.152 -    thm  for abstract equations
  30.153 -
  30.154    strictness wrt. shape of theorem propositions:
  30.155 -    * default attributes: silent
  30.156 -    * user attributes: warnings (after morphism application!)
  30.157 -    * Isabelle/ML functions: strict
  30.158 +    * default equations: silent
  30.159 +    * using declarations and attributes: warnings (after morphism application!)
  30.160 +    * using global declarations (... -> thy -> thy): strict
  30.161      * internal processing after storage: strict
  30.162  *)
  30.163  
  30.164 -fun gen_add_eqn default (raw_thm, proper) thy =
  30.165 -  let
  30.166 -    val thm = Thm.close_derivation raw_thm;
  30.167 -    val c = const_eqn thy thm;
  30.168 -    fun update_subsume verbose (thm, proper) eqns =
  30.169 -      let
  30.170 -        val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
  30.171 -          o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
  30.172 -        val args = args_of thm;
  30.173 -        val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
  30.174 -        fun matches_args args' =
  30.175 -          let
  30.176 -            val k = length args' - length args
  30.177 -          in if k >= 0
  30.178 -            then Pattern.matchess thy (args, (map incr_idx o drop k) args')
  30.179 -            else false
  30.180 -          end;
  30.181 -        fun drop (thm', proper') = if (proper orelse not proper')
  30.182 -          andalso matches_args (args_of thm') then
  30.183 -            (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
  30.184 -                Thm.string_of_thm_global thy thm') else (); true)
  30.185 -          else false;
  30.186 -      in (thm, proper) :: filter_out drop eqns end;
  30.187 -    fun natural_order eqns =
  30.188 -      (eqns, Lazy.lazy_name "code" (fn () => fold (update_subsume false) eqns []))
  30.189 -    fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
  30.190 -      | add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
  30.191 -          (*this restores the natural order and drops syntactic redundancies*)
  30.192 -      | add_eqn' true fun_spec = fun_spec
  30.193 -      | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
  30.194 -      | add_eqn' false _ = Eqns [(thm, proper)];
  30.195 -  in change_fun_spec c (add_eqn' default) thy end;
  30.196 +fun generic_code_declaration strictness lift_phi f x =
  30.197 +  Local_Theory.declaration
  30.198 +    {syntax = false, pervasive = false}
  30.199 +    (fn phi => Context.mapping (f strictness (lift_phi phi x)) I);
  30.200  
  30.201 -fun gen_add_abs_eqn default raw_thm thy =
  30.202 +fun silent_code_declaration lift_phi = generic_code_declaration Silent lift_phi;
  30.203 +fun code_declaration lift_phi = generic_code_declaration Liberal lift_phi;
  30.204 +
  30.205 +local
  30.206 +
  30.207 +fun subsumptive_add thy verbose (thm, proper) eqns =
  30.208    let
  30.209 -    val (abs_thm, tyco) = apfst Thm.close_derivation raw_thm;
  30.210 -    val c = const_abs_eqn thy abs_thm;
  30.211 -  in change_fun_spec c (K (Abstr ((abs_thm, tyco), default))) thy end;
  30.212 -
  30.213 -datatype kind = Equation | Nbe | Abstract;
  30.214 +    val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
  30.215 +      o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
  30.216 +    val args = args_of thm;
  30.217 +    val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
  30.218 +    fun matches_args args' =
  30.219 +      let
  30.220 +        val k = length args' - length args
  30.221 +      in if k >= 0
  30.222 +        then Pattern.matchess thy (args, (map incr_idx o drop k) args')
  30.223 +        else false
  30.224 +      end;
  30.225 +    fun drop (thm', proper') = if (proper orelse not proper')
  30.226 +      andalso matches_args (args_of thm') then
  30.227 +        (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
  30.228 +            Thm.string_of_thm_global thy thm') else (); true)
  30.229 +      else false;
  30.230 +  in (thm, proper) :: filter_out drop eqns end;
  30.231  
  30.232 -fun mk_eqn strictness thy = generic_assert_eqn strictness thy false o
  30.233 -  apfst (meta_rewrite thy);
  30.234 -
  30.235 -fun mk_abs_eqn strictness thy = generic_assert_abs_eqn strictness thy NONE o
  30.236 -  meta_rewrite thy;
  30.237 -
  30.238 -fun mk_maybe_abs_eqn thy raw_thm =
  30.239 +fun add_eqn_for (c, proto_eqn) thy =
  30.240    let
  30.241 -    val thm = meta_rewrite thy raw_thm;
  30.242 -    val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm;
  30.243 -  in case some_abs_thm
  30.244 -   of SOME (thm, tyco) => SOME ((thm, true), SOME tyco)
  30.245 -    | NONE => Option.map (fn (thm, _) => ((thm, is_linear thm), NONE))
  30.246 -        (generic_assert_eqn Liberal thy false (thm, false))
  30.247 -  end;
  30.248 +    val eqn = apfst Thm.close_derivation proto_eqn;
  30.249 +    fun add (Eqns eqns) = Eqns (subsumptive_add thy true eqn eqns)
  30.250 +      | add _ = Eqns [eqn];
  30.251 +  in change_fun_spec c add thy end;
  30.252 +
  30.253 +fun add_eqns_for default (c, proto_eqns) thy =
  30.254 +  let
  30.255 +    val eqns = []
  30.256 +      |> fold_rev (subsumptive_add thy (not default)) proto_eqns
  30.257 +      |> (map o apfst) Thm.close_derivation;
  30.258 +    fun add (Eqns_Default _) = Eqns_Default eqns
  30.259 +      | add data = data;
  30.260 +  in change_fun_spec c (if default then add else K (Eqns eqns)) thy end;
  30.261  
  30.262 -fun generic_add_eqn strictness (kind, default) thm thy =
  30.263 -  case kind of
  30.264 -    Equation => fold (gen_add_eqn default)
  30.265 -      (the_list (mk_eqn strictness thy (thm, true))) thy
  30.266 -  | Nbe => fold (gen_add_eqn default)
  30.267 -      (the_list (mk_eqn strictness thy (thm, false))) thy
  30.268 -  | Abstract => fold (gen_add_abs_eqn default)
  30.269 -      (the_list (mk_abs_eqn strictness thy thm)) thy;
  30.270 +fun add_abstract_for (c, proto_abs_eqn) =
  30.271 +  let
  30.272 +    val abs_eqn = apfst Thm.close_derivation proto_abs_eqn;
  30.273 +  in change_fun_spec c (K (Abstr abs_eqn)) end;
  30.274 +
  30.275 +in
  30.276  
  30.277 -val add_eqn = generic_add_eqn Strict;
  30.278 -
  30.279 -fun lift_attribute f = Thm.declaration_attribute
  30.280 -  (fn thm => Context.mapping (f thm) I);
  30.281 +fun generic_declare_eqns default strictness raw_eqns thy =
  30.282 +  fold (add_eqns_for default) (prep_eqns strictness thy raw_eqns) thy;
  30.283  
  30.284 -fun add_default_eqn_attribute kind =
  30.285 -  lift_attribute (generic_add_eqn Silent (kind, true));
  30.286 +fun generic_add_eqn strictness raw_eqn thy =
  30.287 +  fold add_eqn_for (the_list (prep_eqn strictness thy raw_eqn)) thy;
  30.288  
  30.289 -fun add_default_eqn_attrib kind =
  30.290 -  Attrib.internal (K (add_default_eqn_attribute kind));
  30.291 +fun generic_declare_abstract_eqn strictness raw_abs_eqn thy =
  30.292 +  fold add_abstract_for (the_list (prep_abs_eqn strictness thy raw_abs_eqn)) thy;
  30.293  
  30.294  fun add_maybe_abs_eqn_liberal thm thy =
  30.295 -  case mk_maybe_abs_eqn thy thm
  30.296 -   of SOME (eqn, NONE) => gen_add_eqn false eqn thy
  30.297 -    | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn false (thm, tyco) thy
  30.298 +  case prep_maybe_abs_eqn thy thm
  30.299 +   of SOME (c, (eqn, NONE)) => add_eqn_for (c, eqn) thy
  30.300 +    | SOME (c, ((thm, _), SOME tyco)) => add_abstract_for (c, (thm, tyco)) thy
  30.301      | NONE => thy;
  30.302  
  30.303 -fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true)
  30.304 - of SOME (thm, _) =>
  30.305 +end;
  30.306 +
  30.307 +val declare_default_eqns_global = generic_declare_eqns true Silent;
  30.308 +
  30.309 +val declare_default_eqns =
  30.310 +  silent_code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns true);
  30.311 +
  30.312 +val declare_eqns_global = generic_declare_eqns false Strict;
  30.313 +
  30.314 +val declare_eqns =
  30.315 +  code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns false);
  30.316 +
  30.317 +val add_eqn_global = generic_add_eqn Strict;
  30.318 +
  30.319 +fun del_eqn_global thm thy =
  30.320 +  case prep_eqn Liberal thy (thm, false) of
  30.321 +    SOME (c, (thm, _)) =>
  30.322        let
  30.323 -        fun del_eqn' (Eqns_Default _) = default_fun_spec
  30.324 -          | del_eqn' (Eqns eqns) =
  30.325 +        fun del (Eqns_Default _) = Eqns []
  30.326 +          | del (Eqns eqns) =
  30.327                Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
  30.328 -          | del_eqn' spec = spec
  30.329 -      in change_fun_spec (const_eqn thy thm) del_eqn' thy end
  30.330 +          | del spec = spec
  30.331 +      in change_fun_spec c del thy end
  30.332    | NONE => thy;
  30.333  
  30.334 -val del_eqn_silent = generic_del_eqn Silent;
  30.335 -val del_eqn = generic_del_eqn Liberal;
  30.336 +val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict;
  30.337  
  30.338 -fun del_eqns c = change_fun_spec c (K Unimplemented);
  30.339 +val declare_abstract_eqn =
  30.340 +  code_declaration Morphism.thm generic_declare_abstract_eqn;
  30.341  
  30.342 -fun del_exception c = change_fun_spec c (K (Eqns []));
  30.343 +fun declare_empty_global c = change_fun_spec c (K (Eqns []));
  30.344 +
  30.345 +fun declare_unimplemented_global c = change_fun_spec c (K Unimplemented);
  30.346  
  30.347  
  30.348  (* cases *)
  30.349 @@ -1223,7 +1241,7 @@
  30.350          THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm]))
  30.351    end;
  30.352  
  30.353 -fun add_case thm thy =
  30.354 +fun declare_case_global thm thy =
  30.355    let
  30.356      val (case_const, (k, cos)) = case_cert thm;
  30.357      val _ = case (filter_out (is_constr thy) o map_filter I) cos
  30.358 @@ -1246,7 +1264,7 @@
  30.359      |-> (fn cong => map_spec_purge (register_case cong #> register_type))
  30.360    end;
  30.361  
  30.362 -fun add_undefined c =
  30.363 +fun declare_undefined_global c =
  30.364    (map_spec_purge o map_cases) (Symtab.update (c, Undefined));
  30.365  
  30.366  
  30.367 @@ -1273,7 +1291,7 @@
  30.368            then insert (op =) c else I | _ => I) cases []) cases;
  30.369    in
  30.370      thy
  30.371 -    |> fold del_eqns (outdated_funs1 @ outdated_funs2)
  30.372 +    |> fold declare_unimplemented_global (outdated_funs1 @ outdated_funs2)
  30.373      |> map_spec_purge
  30.374          ((map_types o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
  30.375          #> map_cases drop_outdated_cases)
  30.376 @@ -1292,7 +1310,7 @@
  30.377        |> f (tyco, fst (get_type thy tyco))
  30.378        |> Sign.restore_naming thy));
  30.379  
  30.380 -fun add_datatype proto_constrs thy =
  30.381 +fun declare_datatype_global proto_constrs thy =
  30.382    let
  30.383      fun unoverload_const_typ (c, ty) =
  30.384        (Axclass.unoverload_const thy (c, ty), ty);
  30.385 @@ -1304,8 +1322,8 @@
  30.386      |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
  30.387    end;
  30.388  
  30.389 -fun add_datatype_cmd raw_constrs thy =
  30.390 -  add_datatype (map (read_bare_const thy) raw_constrs) thy;
  30.391 +fun declare_datatype_cmd raw_constrs thy =
  30.392 +  declare_datatype_global (map (read_bare_const thy) raw_constrs) thy;
  30.393  
  30.394  structure Abstype_Plugin = Plugin(type T = string);
  30.395  
  30.396 @@ -1316,35 +1334,48 @@
  30.397      (fn tyco =>
  30.398        Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
  30.399  
  30.400 -fun generic_add_abstype strictness default proto_thm thy =
  30.401 +fun generic_declare_abstype strictness proto_thm thy =
  30.402    case check_abstype_cert strictness thy proto_thm of
  30.403      SOME (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =>
  30.404        thy
  30.405        |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
  30.406        |> change_fun_spec rep
  30.407 -        (K (Proj ((Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco), default)))
  30.408 +        (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
  30.409        |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
  30.410    | NONE => thy;
  30.411  
  30.412 -val add_abstype = generic_add_abstype Strict false;
  30.413 -val add_abstype_default = generic_add_abstype Strict true;
  30.414 +val declare_abstype_global = generic_declare_abstype Strict;
  30.415 +
  30.416 +val declare_abstype =
  30.417 +  code_declaration Morphism.thm generic_declare_abstype;
  30.418  
  30.419  
  30.420  (* setup *)
  30.421  
  30.422 +fun code_attribute f = Thm.declaration_attribute
  30.423 +  (fn thm => Context.mapping (f thm) I);
  30.424 +
  30.425 +fun code_const_attribute f cs =
  30.426 +  code_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
  30.427 +
  30.428  val _ = Theory.setup
  30.429    (let
  30.430 -    fun lift_const_attribute f cs =
  30.431 -      lift_attribute (K (fold (fn c => fn thy => f (read_const thy c) thy) cs));
  30.432      val code_attribute_parser =
  30.433 -      Args.$$$ "equation" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Equation, false)))
  30.434 -      || Args.$$$ "nbe" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Nbe, false)))
  30.435 -      || Args.$$$ "abstract" |-- Scan.succeed (lift_attribute (generic_add_eqn Liberal (Abstract, false)))
  30.436 -      || Args.$$$ "abstype" |-- Scan.succeed (lift_attribute (generic_add_abstype Liberal false))
  30.437 -      || Args.del |-- Scan.succeed (lift_attribute del_eqn)
  30.438 -      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_eqns)
  30.439 -      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> lift_const_attribute del_exception)
  30.440 -      || Scan.succeed (lift_attribute add_maybe_abs_eqn_liberal);
  30.441 +      Args.$$$ "equation" |-- Scan.succeed (code_attribute
  30.442 +          (fn thm => generic_add_eqn Liberal (thm, true)))
  30.443 +      || Args.$$$ "nbe" |-- Scan.succeed (code_attribute
  30.444 +          (fn thm => generic_add_eqn Liberal (thm, false)))
  30.445 +      || Args.$$$ "abstract" |-- Scan.succeed (code_attribute
  30.446 +          (generic_declare_abstract_eqn Liberal))
  30.447 +      || Args.$$$ "abstype" |-- Scan.succeed (code_attribute
  30.448 +          (generic_declare_abstype Liberal))
  30.449 +      || Args.del |-- Scan.succeed (code_attribute del_eqn_global)
  30.450 +      || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term
  30.451 +          >> code_const_attribute declare_empty_global)
  30.452 +      || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term
  30.453 +          >> code_const_attribute declare_unimplemented_global)
  30.454 +      || Scan.succeed (code_attribute
  30.455 +          add_maybe_abs_eqn_liberal);
  30.456    in
  30.457      Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
  30.458          "declare theorems for code generation"
    31.1 --- a/src/Pure/Isar/specification.ML	Mon Jul 03 14:25:07 2017 +0200
    31.2 +++ b/src/Pure/Isar/specification.ML	Sun Jul 02 20:13:38 2017 +0200
    31.3 @@ -266,14 +266,17 @@
    31.4      val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
    31.5  
    31.6      val ([(def_name, [th'])], lthy4) = lthy3
    31.7 -      |> Local_Theory.notes [((name, Code.add_default_eqn_attrib Code.Equation :: atts), [([th], [])])];
    31.8 +      |> Local_Theory.notes [((name, atts), [([th], [])])];
    31.9  
   31.10 -    val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
   31.11 +    val lthy5 = lthy4
   31.12 +      |> Code.declare_default_eqns [(th', true)];
   31.13 +
   31.14 +    val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs;
   31.15  
   31.16      val _ =
   31.17 -      Proof_Display.print_consts int (Position.thread_data ()) lthy4
   31.18 +      Proof_Display.print_consts int (Position.thread_data ()) lthy5
   31.19          (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   31.20 -  in ((lhs, (def_name, th')), lthy4) end;
   31.21 +  in ((lhs, (def_name, th')), lthy5) end;
   31.22  
   31.23  val definition' = gen_def check_spec_open (K I);
   31.24  fun definition xs ys As B = definition' xs ys As B false;
    32.1 --- a/src/Pure/Proof/extraction.ML	Mon Jul 03 14:25:07 2017 +0200
    32.2 +++ b/src/Pure/Proof/extraction.ML	Sun Jul 02 20:13:38 2017 +0200
    32.3 @@ -802,7 +802,7 @@
    32.4               Logic.mk_equals (head, ft)), [])]
    32.5          |-> (fn [def_thm] =>
    32.6             Spec_Rules.add_global Spec_Rules.Equational ([head], [def_thm])
    32.7 -           #> Code.add_eqn (Code.Equation, true) def_thm)
    32.8 +           #> Code.declare_default_eqns_global [(def_thm, true)])
    32.9        end;
   32.10  
   32.11      fun add_corr (s, (vs, prf)) thy =
    33.1 --- a/src/Pure/Pure.thy	Mon Jul 03 14:25:07 2017 +0200
    33.2 +++ b/src/Pure/Pure.thy	Sun Jul 02 20:13:38 2017 +0200
    33.3 @@ -1307,7 +1307,7 @@
    33.4  val _ =
    33.5    Outer_Syntax.command @{command_keyword code_datatype}
    33.6      "define set of code datatype constructors"
    33.7 -    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
    33.8 +    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd));
    33.9  
   33.10  in end\<close>
   33.11