more informative Spec_Rules.Equational, notably primrec argument types;
authorwenzelm
Tue Mar 26 22:13:36 2019 +0100 (7 months ago)
changeset 69992bd3c10813cc4
parent 69991 6b097aeb3650
child 69993 3fd083253a1c
more informative Spec_Rules.Equational, notably primrec argument types;
src/HOL/Library/old_recdef.ML
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_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Nunchaku/nunchaku_collect.ML
src/HOL/Tools/Old_Datatype/old_primrec.ML
src/HOL/Tools/record.ML
src/Pure/Isar/spec_rules.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/extraction.ML
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/HOL/Library/old_recdef.ML	Tue Mar 26 14:23:18 2019 +0100
     1.2 +++ b/src/HOL/Library/old_recdef.ML	Tue Mar 26 22:13:36 2019 +0100
     1.3 @@ -2842,7 +2842,7 @@
     1.4        |> Global_Theory.add_thmss
     1.5          (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
     1.6        ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
     1.7 -      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules)
     1.8 +      ||> Spec_Rules.add_global Spec_Rules.equational_recdef ([lhs], flat rules)
     1.9        ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules));
    1.10      val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
    1.11      val thy3 =
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 26 22:13:36 2019 +0100
     2.3 @@ -1414,10 +1414,10 @@
     2.4            |> massage_simple_notes fp_b_name;
     2.5  
     2.6          val (noted, lthy') = lthy
     2.7 -          |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
     2.8 +          |> Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) map_thms)
     2.9            |> fp = Least_FP
    2.10 -            ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_code_thms)
    2.11 -          |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms)
    2.12 +            ? Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) rel_code_thms)
    2.13 +          |> Spec_Rules.add Spec_Rules.equational (`(single o lhs_head_of o hd) set0_thms)
    2.14            |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms))
    2.15            |> Local_Theory.notes (anonymous_notes @ notes);
    2.16  
    2.17 @@ -2689,7 +2689,7 @@
    2.18            |> massage_multi_notes fp_b_names fpTs;
    2.19        in
    2.20          lthy
    2.21 -        |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
    2.22 +        |> Spec_Rules.add Spec_Rules.equational (recs, flat rec_thmss)
    2.23          |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
    2.24          |> Local_Theory.notes (common_notes @ notes)
    2.25          (* for "datatype_realizer.ML": *)
    2.26 @@ -2869,7 +2869,7 @@
    2.27            |> massage_multi_notes fp_b_names fpTs;
    2.28        in
    2.29          lthy
    2.30 -        |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
    2.31 +        |> fold (curry (Spec_Rules.add Spec_Rules.equational) corecs)
    2.32            [flat corec_sel_thmss, flat corec_thmss]
    2.33          |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms)
    2.34          |> Local_Theory.notes (common_notes @ notes)
     3.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 26 22:13:36 2019 +0100
     3.3 @@ -2154,10 +2154,10 @@
     3.4        in
     3.5          lthy
     3.6  (* TODO:
     3.7 -        |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], flat sel_thmss)
     3.8 -        |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], flat ctr_thmss)
     3.9 +        |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat sel_thmss)
    3.10 +        |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat ctr_thmss)
    3.11  *)
    3.12 -        |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], [code_thm])
    3.13 +        |> Spec_Rules.add Spec_Rules.equational ([fun_t0], [code_thm])
    3.14          |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
    3.15          |> Local_Theory.notes (anonymous_notes @ notes)
    3.16          |> snd
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 26 22:13:36 2019 +0100
     4.3 @@ -1532,9 +1532,9 @@
     4.4          val fun_ts0 = map fst def_infos;
     4.5        in
     4.6          lthy
     4.7 -        |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat sel_thmss)
     4.8 -        |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat ctr_thmss)
     4.9 -        |> Spec_Rules.add Spec_Rules.Equational (fun_ts0, flat code_thmss)
    4.10 +        |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat sel_thmss)
    4.11 +        |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat ctr_thmss)
    4.12 +        |> Spec_Rules.add Spec_Rules.equational (fun_ts0, flat code_thmss)
    4.13          |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
    4.14          |> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
    4.15          |> snd
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Mar 26 22:13:36 2019 +0100
     5.3 @@ -580,7 +580,7 @@
     5.4          ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs),
     5.5            [(thms, [])]));
     5.6    in
     5.7 -    (((fun_names, qualifys, defs),
     5.8 +    (((fun_names, qualifys, arg_Ts, defs),
     5.9        fn lthy => fn defs =>
    5.10          let
    5.11            val def_thms = map (snd o snd) defs;
    5.12 @@ -605,24 +605,29 @@
    5.13      val nonexhaustives = replicate actual_nn nonexhaustive;
    5.14      val transfers = replicate actual_nn transfer;
    5.15  
    5.16 -    val (((names, qualifys, defs), prove), lthy') =
    5.17 +    val (((names, qualifys, arg_Ts, defs), prove), lthy') =
    5.18        prepare_primrec plugins nonexhaustives transfers fixes ts lthy;
    5.19    in
    5.20      lthy'
    5.21      |> fold_map Local_Theory.define defs
    5.22      |> tap (uncurry (print_def_consts int))
    5.23      |-> (fn defs => fn lthy =>
    5.24 -      let val ((jss, simpss), lthy) = prove lthy defs in
    5.25 -        (((names, qualifys), (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy)
    5.26 -      end)
    5.27 +      let
    5.28 +        val ((jss, simpss), lthy) = prove lthy defs;
    5.29 +        val res =
    5.30 +          {prefix = (names, qualifys),
    5.31 +           types = map (#1 o dest_Type) arg_Ts,
    5.32 +           result = (map fst defs, map (snd o snd) defs, (jss, simpss))};
    5.33 +      in (res, lthy) end)
    5.34    end;
    5.35  
    5.36  fun primrec_simple int fixes ts lthy =
    5.37    primrec_simple0 int Plugin_Name.default_filter false false fixes ts lthy
    5.38 +    |>> (fn {prefix, result, ...} => (prefix, result))
    5.39    handle OLD_PRIMREC () =>
    5.40      Old_Primrec.primrec_simple int fixes ts lthy
    5.41 -    |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single
    5.42 -    |>> apfst (map_split (rpair I));
    5.43 +    |>> (fn {prefix, result = (ts, thms), ...} =>
    5.44 +          (map_split (rpair I) [prefix], (ts, [], ([], [thms]))))
    5.45  
    5.46  fun gen_primrec old_primrec prep_spec int opts raw_fixes raw_specs lthy =
    5.47    let
    5.48 @@ -648,8 +653,8 @@
    5.49    in
    5.50      lthy
    5.51      |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs)
    5.52 -    |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) =>
    5.53 -      Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
    5.54 +    |-> (fn {prefix = (names, qualifys), types, result = (ts, defs, (jss, simpss))} =>
    5.55 +      Spec_Rules.add (Spec_Rules.equational_primrec types) (ts, flat simpss)
    5.56        #> Local_Theory.notes (mk_notes jss names qualifys simpss)
    5.57        #-> (fn notes =>
    5.58          plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (maps snd notes))
    5.59 @@ -657,7 +662,7 @@
    5.60    end
    5.61    handle OLD_PRIMREC () =>
    5.62      old_primrec int raw_fixes raw_specs lthy
    5.63 -    |>> (fn (ts, thms) => (ts, [], [thms]));
    5.64 +    |>> (fn {result = (ts, thms), ...} => (ts, [], [thms]));
    5.65  
    5.66  val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs;
    5.67  val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs;
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 26 14:23:18 2019 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 26 22:13:36 2019 +0100
     6.3 @@ -373,8 +373,8 @@
     6.4  
     6.5        val (noted, lthy3) =
     6.6          lthy2
     6.7 -        |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
     6.8 -        |> Spec_Rules.add Spec_Rules.Equational (overloaded_size_consts, overloaded_size_simps)
     6.9 +        |> Spec_Rules.add Spec_Rules.equational (size_consts, size_simps)
    6.10 +        |> Spec_Rules.add Spec_Rules.equational (overloaded_size_consts, overloaded_size_simps)
    6.11          |> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
    6.12            (*Ideally, this would be issued only if the "code" plugin is enabled.*)
    6.13          |> Local_Theory.notes notes;
     7.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Mar 26 14:23:18 2019 +0100
     7.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Mar 26 22:13:36 2019 +0100
     7.3 @@ -1111,10 +1111,10 @@
     7.4              ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
     7.5  
     7.6          val (noted, lthy') = lthy
     7.7 -          |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
     7.8 -          |> fold (Spec_Rules.add Spec_Rules.Equational)
     7.9 +          |> Spec_Rules.add Spec_Rules.equational ([casex], case_thms)
    7.10 +          |> fold (Spec_Rules.add Spec_Rules.equational)
    7.11              (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
    7.12 -          |> fold (Spec_Rules.add Spec_Rules.Equational)
    7.13 +          |> fold (Spec_Rules.add Spec_Rules.equational)
    7.14              (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
    7.15            |> Local_Theory.declaration {syntax = false, pervasive = true}
    7.16              (fn phi => Case_Translation.register
     8.1 --- a/src/HOL/Tools/Function/function.ML	Tue Mar 26 14:23:18 2019 +0100
     8.2 +++ b/src/HOL/Tools/Function/function.ML	Tue Mar 26 22:13:36 2019 +0100
     8.3 @@ -210,7 +210,7 @@
     8.4               lthy
     8.5               |> Local_Theory.declaration {syntax = false, pervasive = false}
     8.6                 (fn phi => add_function_data (transform_function_data phi info'))
     8.7 -             |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
     8.8 +             |> Spec_Rules.add Spec_Rules.equational_recdef (fs, tsimps))
     8.9            end)
    8.10        end
    8.11    in
     9.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Mar 26 14:23:18 2019 +0100
     9.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Mar 26 22:13:36 2019 +0100
     9.3 @@ -302,7 +302,7 @@
     9.4      val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule])
     9.5    in
     9.6      lthy''
     9.7 -    |> Spec_Rules.add Spec_Rules.Equational ([f], [rec_rule'])
     9.8 +    |> Spec_Rules.add Spec_Rules.equational_recdef ([f], [rec_rule'])
     9.9      |> note_qualified ("simps", [rec_rule'])
    9.10      |> note_qualified ("mono", [mono_thm])
    9.11      |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm]))
    10.1 --- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Mar 26 14:23:18 2019 +0100
    10.2 +++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Tue Mar 26 22:13:36 2019 +0100
    10.3 @@ -506,7 +506,7 @@
    10.4            if card = Inf orelse card = Fin_or_Inf then
    10.5              spec_rules ()
    10.6            else
    10.7 -            [(Spec_Rules.Equational, ([Logic.varify_global \<^term>\<open>finite\<close>],
    10.8 +            [(Spec_Rules.equational, ([Logic.varify_global \<^term>\<open>finite\<close>],
    10.9                 [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]))]
   10.10          end
   10.11        else
    11.1 --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Tue Mar 26 14:23:18 2019 +0100
    11.2 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Tue Mar 26 22:13:36 2019 +0100
    11.3 @@ -9,16 +9,18 @@
    11.4  signature OLD_PRIMREC =
    11.5  sig
    11.6    val primrec: bool -> (binding * typ option * mixfix) list ->
    11.7 -    Specification.multi_specs -> local_theory -> (term list * thm list) * local_theory
    11.8 +    Specification.multi_specs -> local_theory ->
    11.9 +    {types: string list, result: term list * thm list} * local_theory
   11.10    val primrec_cmd: bool -> (binding * string option * mixfix) list ->
   11.11 -    Specification.multi_specs_cmd -> local_theory -> (term list * thm list) * local_theory
   11.12 +    Specification.multi_specs_cmd -> local_theory ->
   11.13 +    {types: string list, result: term list * thm list} * local_theory
   11.14    val primrec_global: bool -> (binding * typ option * mixfix) list ->
   11.15      Specification.multi_specs -> theory -> (term list * thm list) * theory
   11.16    val primrec_overloaded: bool -> (string * (string * typ) * bool) list ->
   11.17      (binding * typ option * mixfix) list ->
   11.18      Specification.multi_specs -> theory -> (term list * thm list) * theory
   11.19 -  val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list ->
   11.20 -    local_theory -> (string * (term list * thm list)) * local_theory
   11.21 +  val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list -> local_theory ->
   11.22 +    {prefix: string, types: string list, result: term list * thm list} * local_theory
   11.23  end;
   11.24  
   11.25  structure Old_Primrec : OLD_PRIMREC =
   11.26 @@ -195,13 +197,13 @@
   11.27  
   11.28  fun make_def ctxt fixes fs (fname, ls, rec_name) =
   11.29    let
   11.30 -    val SOME (var, varT) = get_first (fn ((b, T), mx) =>
   11.31 +    val SOME (var, varT) = get_first (fn ((b, T), mx: mixfix) =>
   11.32        if Binding.name_of b = fname then SOME ((b, mx), T) else NONE) fixes;
   11.33      val def_name = Thm.def_name (Long_Name.base_name fname);
   11.34      val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
   11.35        (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
   11.36      val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs);
   11.37 -  in (var, ((Binding.concealed (Binding.name def_name), []), rhs)) end;
   11.38 +  in (var, ((Binding.concealed (Binding.name def_name), []): Attrib.binding, rhs)) end;
   11.39  
   11.40  
   11.41  (* find datatypes which contain all datatypes in tnames' *)
   11.42 @@ -250,7 +252,7 @@
   11.43            (fn {context = ctxt', ...} =>
   11.44              EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac ctxt' [refl] 1])) eqs
   11.45        end;
   11.46 -  in ((prefix, (fs, defs)), prove) end
   11.47 +  in ((prefix, tnames, (fs, defs)), prove) end
   11.48    handle PrimrecError (msg, some_eqn) =>
   11.49      error ("Primrec definition error:\n" ^ msg ^
   11.50        (case some_eqn of
   11.51 @@ -262,12 +264,13 @@
   11.52  
   11.53  fun primrec_simple int fixes ts lthy =
   11.54    let
   11.55 -    val ((prefix, (_, defs)), prove) = distill lthy fixes ts;
   11.56 +    val ((prefix, tnames, (_, defs)), prove) = distill lthy fixes ts;
   11.57    in
   11.58      lthy
   11.59      |> fold_map Local_Theory.define defs
   11.60      |> tap (uncurry (BNF_FP_Rec_Sugar_Util.print_def_consts int))
   11.61 -    |-> (fn defs => `(fn lthy => (prefix, (map fst defs, prove lthy defs))))
   11.62 +    |-> (fn defs =>
   11.63 +      `(fn lthy => {prefix = prefix, types = tnames, result = (map fst defs, prove lthy defs)}))
   11.64    end;
   11.65  
   11.66  local
   11.67 @@ -282,13 +285,13 @@
   11.68    in
   11.69      lthy
   11.70      |> primrec_simple int fixes (map snd spec)
   11.71 -    |-> (fn (prefix, (ts, simps)) =>
   11.72 -      Spec_Rules.add Spec_Rules.Equational (ts, simps)
   11.73 +    |-> (fn {prefix, types, result = (ts, simps)} =>
   11.74 +      Spec_Rules.add (Spec_Rules.equational_primrec types) (ts, simps)
   11.75        #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
   11.76        #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
   11.77 -      #-> (fn (_, simps'') => 
   11.78 -        Code.declare_default_eqns (map (rpair true) simps'')
   11.79 -        #> pair (ts, simps''))))
   11.80 +        #-> (fn (_, simps'') => 
   11.81 +          Code.declare_default_eqns (map (rpair true) simps'')
   11.82 +          #> pair {types = types, result = (ts, simps'')})))
   11.83    end;
   11.84  
   11.85  in
   11.86 @@ -301,14 +304,14 @@
   11.87  fun primrec_global int fixes specs thy =
   11.88    let
   11.89      val lthy = Named_Target.theory_init thy;
   11.90 -    val ((ts, simps), lthy') = primrec int fixes specs lthy;
   11.91 +    val ({result = (ts, simps), ...}, lthy') = primrec int fixes specs lthy;
   11.92      val simps' = Proof_Context.export lthy' lthy simps;
   11.93    in ((ts, simps'), Local_Theory.exit_global lthy') end;
   11.94  
   11.95  fun primrec_overloaded int ops fixes specs thy =
   11.96    let
   11.97      val lthy = Overloading.overloading ops thy;
   11.98 -    val ((ts, simps), lthy') = primrec int fixes specs lthy;
   11.99 +    val ({result = (ts, simps), ...}, lthy') = primrec int fixes specs lthy;
  11.100      val simps' = Proof_Context.export lthy' lthy simps;
  11.101    in ((ts, simps'), Local_Theory.exit_global lthy') end;
  11.102  
    12.1 --- a/src/HOL/Tools/record.ML	Tue Mar 26 14:23:18 2019 +0100
    12.2 +++ b/src/HOL/Tools/record.ML	Tue Mar 26 22:13:36 2019 +0100
    12.3 @@ -1814,7 +1814,7 @@
    12.4  
    12.5  fun add_spec_rule rule =
    12.6    let val head = head_of (lhs_of_equation (Thm.prop_of rule)) in
    12.7 -    Spec_Rules.add_global Spec_Rules.Equational ([head], [rule])
    12.8 +    Spec_Rules.add_global Spec_Rules.equational ([head], [rule])
    12.9    end;
   12.10  
   12.11  (* definition *)
    13.1 --- a/src/Pure/Isar/spec_rules.ML	Tue Mar 26 14:23:18 2019 +0100
    13.2 +++ b/src/Pure/Isar/spec_rules.ML	Tue Mar 26 22:13:36 2019 +0100
    13.3 @@ -8,8 +8,13 @@
    13.4  
    13.5  signature SPEC_RULES =
    13.6  sig
    13.7 -  datatype rough_classification = Equational | Inductive | Co_Inductive | Unknown
    13.8 +  datatype recursion = Primrec of string list | Recdef | Unknown_Recursion
    13.9 +  val recursion_ord: recursion * recursion -> order
   13.10 +  datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown
   13.11    val rough_classification_ord: rough_classification * rough_classification -> order
   13.12 +  val equational_primrec: string list -> rough_classification
   13.13 +  val equational_recdef: rough_classification
   13.14 +  val equational: rough_classification
   13.15    val is_equational: rough_classification -> bool
   13.16    val is_inductive: rough_classification -> bool
   13.17    val is_co_inductive: rough_classification -> bool
   13.18 @@ -26,14 +31,28 @@
   13.19  structure Spec_Rules: SPEC_RULES =
   13.20  struct
   13.21  
   13.22 +(* recursion *)
   13.23 +
   13.24 +datatype recursion = Primrec of string list | Recdef | Unknown_Recursion;
   13.25 +
   13.26 +fun recursion_ord (Primrec Ts1, Primrec Ts2) = list_ord fast_string_ord (Ts1, Ts2)
   13.27 +  | recursion_ord rs =
   13.28 +      int_ord (apply2 (fn Primrec _ => 0 | Recdef => 1 | Unknown_Recursion => 2) rs);
   13.29 +
   13.30 +
   13.31  (* rough classification *)
   13.32  
   13.33 -datatype rough_classification = Equational | Inductive | Co_Inductive | Unknown;
   13.34 +datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown;
   13.35 +
   13.36 +fun rough_classification_ord (Equational r1, Equational r2) = recursion_ord (r1, r2)
   13.37 +  | rough_classification_ord cs =
   13.38 +      int_ord (apply2 (fn Equational _ => 0 | Inductive => 1 | Co_Inductive => 2 | Unknown => 3) cs);
   13.39  
   13.40 -val rough_classification_ord =
   13.41 -  int_ord o apply2 (fn Equational => 0 | Inductive => 1 | Co_Inductive => 2 | Unknown => 3);
   13.42 +val equational_primrec = Equational o Primrec;
   13.43 +val equational_recdef = Equational Recdef;
   13.44 +val equational = Equational Unknown_Recursion;
   13.45  
   13.46 -val is_equational = fn Equational => true | _ => false;
   13.47 +val is_equational = fn Equational _ => true | _ => false;
   13.48  val is_inductive = fn Inductive => true | _ => false;
   13.49  val is_co_inductive = fn Co_Inductive => true | _ => false;
   13.50  val is_unknown = fn Unknown => true | _ => false;
   13.51 @@ -48,8 +67,8 @@
   13.52    type T = spec Item_Net.T;
   13.53    val empty : T =
   13.54      Item_Net.init
   13.55 -      (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) =>
   13.56 -        rough_classification_ord (class1, class2) = EQUAL andalso
   13.57 +      (fn ((c1, (ts1, ths1)), (c2, (ts2, ths2))) =>
   13.58 +        is_equal (rough_classification_ord (c1, c2)) andalso
   13.59          eq_list (op aconv) (ts1, ts2) andalso
   13.60          eq_list Thm.eq_thm_prop (ths1, ths2))
   13.61        (#1 o #2);
    14.1 --- a/src/Pure/Isar/specification.ML	Tue Mar 26 14:23:18 2019 +0100
    14.2 +++ b/src/Pure/Isar/specification.ML	Tue Mar 26 22:13:36 2019 +0100
    14.3 @@ -263,7 +263,7 @@
    14.4        |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
    14.5  
    14.6      val th = prove lthy2 raw_th;
    14.7 -    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
    14.8 +    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.equational ([lhs], [th]);
    14.9  
   14.10      val ([(def_name, [th'])], lthy4) = lthy3
   14.11        |> Local_Theory.notes [((name, atts), [([th], [])])];
    15.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 26 14:23:18 2019 +0100
    15.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 26 22:13:36 2019 +0100
    15.3 @@ -801,7 +801,7 @@
    15.4             [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
    15.5               Logic.mk_equals (head, ft)), [])]
    15.6          |-> (fn [def_thm] =>
    15.7 -           Spec_Rules.add_global Spec_Rules.Equational ([head], [def_thm])
    15.8 +           Spec_Rules.add_global Spec_Rules.equational ([head], [def_thm])
    15.9             #> Code.declare_default_eqns_global [(def_thm, true)])
   15.10        end;
   15.11  
    16.1 --- a/src/Pure/Thy/export_theory.ML	Tue Mar 26 14:23:18 2019 +0100
    16.2 +++ b/src/Pure/Thy/export_theory.ML	Tue Mar 26 22:13:36 2019 +0100
    16.3 @@ -101,6 +101,14 @@
    16.4    (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
    16.5  
    16.6  
    16.7 +(* spec rules *)
    16.8 +
    16.9 +fun primrec_types ctxt const =
   16.10 +  Spec_Rules.retrieve ctxt (Const const)
   16.11 +  |> get_first (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME types | _ => NONE)
   16.12 +  |> the_default [];
   16.13 +
   16.14 +
   16.15  (* locales content *)
   16.16  
   16.17  fun locale_content thy loc =
   16.18 @@ -230,17 +238,21 @@
   16.19      (* consts *)
   16.20  
   16.21      val encode_const =
   16.22 -      let open XML.Encode Term_XML.Encode
   16.23 -      in pair encode_syntax (pair (list string) (pair typ (pair (option term) bool))) end;
   16.24 +      let open XML.Encode Term_XML.Encode in
   16.25 +        pair encode_syntax
   16.26 +          (pair (list string) (pair typ (pair (option term) (pair bool (list string)))))
   16.27 +      end;
   16.28  
   16.29      fun export_const c (T, abbrev) =
   16.30        let
   16.31          val syntax = get_syntax_const thy_ctxt c;
   16.32 -        val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
   16.33 +        val U = Logic.unvarifyT_global T;
   16.34 +        val U0 = Type.strip_sorts U;
   16.35 +        val primrec_types = primrec_types thy_ctxt (c, U);
   16.36          val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
   16.37 -        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
   16.38 -        val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type T');
   16.39 -      in encode_const (syntax, (args, (T', (abbrev', propositional)))) end;
   16.40 +        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, U0));
   16.41 +        val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
   16.42 +      in encode_const (syntax, (args, (U0, (abbrev', (propositional, primrec_types))))) end;
   16.43  
   16.44      val _ =
   16.45        export_entities "consts" (SOME oo export_const) Sign.const_space
    17.1 --- a/src/Pure/Thy/export_theory.scala	Tue Mar 26 14:23:18 2019 +0100
    17.2 +++ b/src/Pure/Thy/export_theory.scala	Tue Mar 26 22:13:36 2019 +0100
    17.3 @@ -252,7 +252,8 @@
    17.4      typargs: List[String],
    17.5      typ: Term.Typ,
    17.6      abbrev: Option[Term.Term],
    17.7 -    propositional: Boolean)
    17.8 +    propositional: Boolean,
    17.9 +    primrec_types: List[String])
   17.10    {
   17.11      def cache(cache: Term.Cache): Const =
   17.12        Const(entity.cache(cache),
   17.13 @@ -260,20 +261,23 @@
   17.14          typargs.map(cache.string(_)),
   17.15          cache.typ(typ),
   17.16          abbrev.map(cache.term(_)),
   17.17 -        propositional)
   17.18 +        propositional,
   17.19 +        primrec_types.map(cache.string(_)))
   17.20    }
   17.21  
   17.22    def read_consts(provider: Export.Provider): List[Const] =
   17.23      provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
   17.24        {
   17.25          val (entity, body) = decode_entity(Kind.CONST, tree)
   17.26 -        val (syntax, (args, (typ, (abbrev, propositional)))) =
   17.27 +        val (syntax, (args, (typ, (abbrev, (propositional, primrec_types))))) =
   17.28          {
   17.29            import XML.Decode._
   17.30 -          pair(decode_syntax, pair(list(string),
   17.31 -            pair(Term_XML.Decode.typ, pair(option(Term_XML.Decode.term), bool))))(body)
   17.32 +          pair(decode_syntax,
   17.33 +            pair(list(string),
   17.34 +              pair(Term_XML.Decode.typ,
   17.35 +                pair(option(Term_XML.Decode.term), pair(bool, list(string))))))(body)
   17.36          }
   17.37 -        Const(entity, syntax, args, typ, abbrev, propositional)
   17.38 +        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types)
   17.39        })
   17.40  
   17.41