support 'assumes' in specifications, e.g. 'definition', 'inductive';
authorwenzelm
Thu Apr 28 09:43:11 2016 +0200 (2016-04-28)
changeset 630642f18172214c8
parent 63063 c9605a284fba
child 63065 3cb7b06d0a9f
support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/BNF/bnf_axiomatization.ML
src/HOL/Tools/BNF/bnf_gfp_grec.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/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/fun_cases.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Old_Datatype/old_primrec.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/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/record.ML
src/HOL/Typerep.thy
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/specification.ML
src/Pure/Pure.thy
src/Pure/ROOT.ML
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed Apr 27 10:03:35 2016 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Apr 28 09:43:11 2016 +0200
     1.3 @@ -175,8 +175,8 @@
     1.4        Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))
     1.5      val ((_, (_, below_ldef)), lthy) = thy
     1.6        |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
     1.7 -      |> Specification.definition (NONE,
     1.8 -          ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn))
     1.9 +      |> Specification.definition NONE []
    1.10 +          ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)
    1.11      val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
    1.12      val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
    1.13      val thy = lthy
     2.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Wed Apr 27 10:03:35 2016 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Thu Apr 28 09:43:11 2016 +0200
     2.3 @@ -138,17 +138,17 @@
     2.4      val lthy = thy
     2.5        |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
     2.6      val ((_, (_, emb_ldef)), lthy) =
     2.7 -        Specification.definition (NONE, (emb_bind, emb_eqn)) lthy
     2.8 +        Specification.definition NONE [] (emb_bind, emb_eqn) lthy
     2.9      val ((_, (_, prj_ldef)), lthy) =
    2.10 -        Specification.definition (NONE, (prj_bind, prj_eqn)) lthy
    2.11 +        Specification.definition NONE [] (prj_bind, prj_eqn) lthy
    2.12      val ((_, (_, defl_ldef)), lthy) =
    2.13 -        Specification.definition (NONE, (defl_bind, defl_eqn)) lthy
    2.14 +        Specification.definition NONE [] (defl_bind, defl_eqn) lthy
    2.15      val ((_, (_, liftemb_ldef)), lthy) =
    2.16 -        Specification.definition (NONE, (liftemb_bind, liftemb_eqn)) lthy
    2.17 +        Specification.definition NONE [] (liftemb_bind, liftemb_eqn) lthy
    2.18      val ((_, (_, liftprj_ldef)), lthy) =
    2.19 -        Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy
    2.20 +        Specification.definition NONE [] (liftprj_bind, liftprj_eqn) lthy
    2.21      val ((_, (_, liftdefl_ldef)), lthy) =
    2.22 -        Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) lthy
    2.23 +        Specification.definition NONE [] (liftdefl_bind, liftdefl_eqn) lthy
    2.24      val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
    2.25      val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef
    2.26      val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef
     3.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Wed Apr 27 10:03:35 2016 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Apr 28 09:43:11 2016 +0200
     3.3 @@ -334,7 +334,7 @@
     3.4      val (skips, raw_spec) = ListPair.unzip raw_spec'
     3.5      val (fixes : ((binding * typ) * mixfix) list,
     3.6           spec : (Attrib.binding * term) list) =
     3.7 -          fst (prep_spec raw_fixes raw_spec lthy)
     3.8 +          fst (prep_spec raw_fixes (map (rpair []) raw_spec) lthy)
     3.9      val names = map (Binding.name_of o fst o fst) fixes
    3.10      fun check_head name =
    3.11          member (op =) names name orelse
    3.12 @@ -377,8 +377,8 @@
    3.13  
    3.14  in
    3.15  
    3.16 -val add_fixrec = gen_fixrec Specification.check_spec
    3.17 -val add_fixrec_cmd = gen_fixrec Specification.read_spec
    3.18 +val add_fixrec = gen_fixrec Specification.check_multi_specs
    3.19 +val add_fixrec_cmd = gen_fixrec Specification.read_multi_specs
    3.20  
    3.21  end (* local *)
    3.22  
    3.23 @@ -394,13 +394,13 @@
    3.24  val spec' : (bool * (Attrib.binding * string)) parser =
    3.25    opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)))
    3.26  
    3.27 -val alt_specs' : (bool * (Attrib.binding * string)) list parser =
    3.28 +val multi_specs' : (bool * (Attrib.binding * string)) list parser =
    3.29    let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
    3.30    in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
    3.31  
    3.32  val _ =
    3.33    Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
    3.34 -    (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
    3.35 +    (Parse.fixes -- (Parse.where_ |-- Parse.!!! multi_specs')
    3.36        >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
    3.37  
    3.38  end
     4.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 27 10:03:35 2016 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Apr 28 09:43:11 2016 +0200
     4.3 @@ -192,7 +192,7 @@
     4.4          thy' |>
     4.5          BNF_LFP_Compat.primrec_global
     4.6            [(Binding.name swap_name, SOME swapT, NoSyn)]
     4.7 -          [(Attrib.empty_binding, def1)] ||>
     4.8 +          [((Attrib.empty_binding, def1), [])] ||>
     4.9          Sign.parent_path ||>>
    4.10          Global_Theory.add_defs_unchecked true
    4.11            [((Binding.name name, def2), [])] |>> (snd o fst)
    4.12 @@ -226,7 +226,7 @@
    4.13          thy' |>
    4.14          BNF_LFP_Compat.primrec_global
    4.15            [(Binding.name prm_name, SOME prmT, NoSyn)]
    4.16 -          [(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] ||>
    4.17 +          (map (fn def => ((Attrib.empty_binding, def), [])) [def1, def2]) ||>
    4.18          Sign.parent_path
    4.19        end) ak_names_types thy3;
    4.20      
     5.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 27 10:03:35 2016 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 28 09:43:11 2016 +0200
     5.3 @@ -251,11 +251,11 @@
     5.4                else Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x
     5.5              end;
     5.6          in
     5.7 -          (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
     5.8 +          ((Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
     5.9              (Free (nth perm_names_types' i) $
    5.10                 Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
    5.11                 list_comb (c, args),
    5.12 -             list_comb (c, map perm_arg (dts ~~ args)))))
    5.13 +             list_comb (c, map perm_arg (dts ~~ args))))), [])
    5.14          end) constrs
    5.15        end) descr;
    5.16  
     6.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Apr 27 10:03:35 2016 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Apr 28 09:43:11 2016 +0200
     6.3 @@ -11,11 +11,11 @@
     6.4    val primrec: term list option -> term option ->
     6.5      (binding * typ option * mixfix) list ->
     6.6      (binding * typ option * mixfix) list ->
     6.7 -    (Attrib.binding * term) list -> local_theory -> Proof.state
     6.8 +    Specification.multi_specs -> local_theory -> Proof.state
     6.9    val primrec_cmd: string list option -> string option ->
    6.10      (binding * string option * mixfix) list ->
    6.11      (binding * string option * mixfix) list ->
    6.12 -    (Attrib.binding * string) list -> local_theory -> Proof.state
    6.13 +    Specification.multi_specs_cmd -> local_theory -> Proof.state
    6.14  end;
    6.15  
    6.16  structure NominalPrimrec : NOMINAL_PRIMREC =
    6.17 @@ -380,8 +380,8 @@
    6.18  
    6.19  in
    6.20  
    6.21 -val primrec = gen_primrec Specification.check_spec (K I);
    6.22 -val primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
    6.23 +val primrec = gen_primrec Specification.check_multi_specs (K I);
    6.24 +val primrec_cmd = gen_primrec Specification.read_multi_specs Syntax.read_term;
    6.25  
    6.26  end;
    6.27  
    6.28 @@ -403,7 +403,7 @@
    6.29  val _ =
    6.30    Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
    6.31      "define primitive recursive functions on nominal datatypes"
    6.32 -    (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
    6.33 +    (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_multi_specs
    6.34        >> (fn ((((invs, fctxt), fixes), params), specs) =>
    6.35          primrec_cmd invs fctxt fixes params specs));
    6.36  
     7.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Apr 27 10:03:35 2016 +0200
     7.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Apr 28 09:43:11 2016 +0200
     7.3 @@ -1020,8 +1020,8 @@
     7.4              "\ndoes not match type " ^ ty' ^ " in definition");
     7.5          val id' = mk_rulename id;
     7.6          val ((t', (_, th)), lthy') = Named_Target.theory_init thy
     7.7 -          |> Specification.definition
     7.8 -            (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t))));
     7.9 +          |> Specification.definition NONE []
    7.10 +            ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
    7.11          val phi =
    7.12            Proof_Context.export_morphism lthy'
    7.13              (Proof_Context.init_global (Proof_Context.theory_of lthy'));
     8.1 --- a/src/HOL/Tools/BNF/bnf_axiomatization.ML	Wed Apr 27 10:03:35 2016 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML	Thu Apr 28 09:43:11 2016 +0200
     8.3 @@ -82,7 +82,7 @@
     8.4      val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
     8.5  
     8.6      val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
     8.7 -      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
     8.8 +      (Specification.axiomatization [] [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
     8.9  
    8.10      fun mk_wit_thms set_maps =
    8.11        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed Apr 27 10:03:35 2016 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Thu Apr 28 09:43:11 2016 +0200
     9.3 @@ -265,7 +265,7 @@
     9.4      val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
     9.5        |> Local_Theory.open_target |> snd
     9.6        |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
     9.7 -      |> primrec [(b, NONE, NoSyn)] (map (pair Attrib.empty_binding) eqs)
     9.8 +      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [])) eqs)
     9.9        ||> `Local_Theory.close_target;
    9.10  
    9.11      val phi = Proof_Context.export_morphism lthy_old lthy;
    10.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Apr 27 10:03:35 2016 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Thu Apr 28 09:43:11 2016 +0200
    10.3 @@ -1829,7 +1829,7 @@
    10.4  
    10.5      val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
    10.6        Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
    10.7 -        [(apfst Binding.concealed Attrib.empty_binding, parsed_eq)]
    10.8 +        [(((Binding.concealed Binding.empty, []), parsed_eq), [])]
    10.9          Function_Common.default_config pat_completeness_auto lthy;
   10.10    in
   10.11      ((defname, (pelim, pinduct, psimp)), lthy)
   10.12 @@ -1982,7 +1982,7 @@
   10.13  
   10.14      val (plugins, friend, transfer) = get_options lthy opts;
   10.15      val ([((b, fun_T), mx)], [(_, eq)]) =
   10.16 -      fst (Specification.read_spec raw_fixes [(Attrib.empty_binding, raw_eq)] lthy);
   10.17 +      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [])] lthy);
   10.18  
   10.19      val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
   10.20        error ("Type of " ^ Binding.print b ^ " contains top sort");
    11.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Apr 27 10:03:35 2016 +0200
    11.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Apr 28 09:43:11 2016 +0200
    11.3 @@ -1587,7 +1587,8 @@
    11.4  
    11.5      val (raw_specs, of_specs_opt) =
    11.6        split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
    11.7 -    val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
    11.8 +    val (fixes, specs) =
    11.9 +      fst (Specification.read_multi_specs raw_fixes (map (rpair []) raw_specs) lthy);
   11.10    in
   11.11      primcorec_ursive auto opts fixes specs of_specs_opt lthy
   11.12    end;
    12.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Apr 27 10:03:35 2016 +0200
    12.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Apr 28 09:43:11 2016 +0200
    12.3 @@ -26,12 +26,12 @@
    12.4    val datatype_compat_global: string list -> theory -> theory
    12.5    val datatype_compat_cmd: string list -> local_theory -> local_theory
    12.6    val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory
    12.7 -  val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
    12.8 +  val primrec: (binding * typ option * mixfix) list -> Specification.multi_specs ->
    12.9      local_theory -> (term list * thm list) * local_theory
   12.10    val primrec_global: (binding * typ option * mixfix) list ->
   12.11 -    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
   12.12 +    Specification.multi_specs -> theory -> (term list * thm list) * theory
   12.13    val primrec_overloaded: (string * (string * typ) * bool) list ->
   12.14 -    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory ->
   12.15 +    (binding * typ option * mixfix) list -> Specification.multi_specs -> theory ->
   12.16      (term list * thm list) * theory
   12.17    val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
   12.18      local_theory -> (string list * (term list * thm list)) * local_theory
    13.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Apr 27 10:03:35 2016 +0200
    13.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Apr 28 09:43:11 2016 +0200
    13.3 @@ -62,16 +62,16 @@
    13.4    val lfp_rec_sugar_interpretation: string ->
    13.5      (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
    13.6  
    13.7 -  val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
    13.8 +  val primrec: (binding * typ option * mixfix) list -> Specification.multi_specs ->
    13.9      local_theory -> (term list * thm list * thm list list) * local_theory
   13.10    val primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
   13.11 -    (Attrib.binding * string) list -> local_theory ->
   13.12 +    Specification.multi_specs_cmd -> local_theory ->
   13.13      (term list * thm list * thm list list) * local_theory
   13.14    val primrec_global: (binding * typ option * mixfix) list ->
   13.15 -    (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory
   13.16 +    Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
   13.17    val primrec_overloaded: (string * (string * typ) * bool) list ->
   13.18      (binding * typ option * mixfix) list ->
   13.19 -    (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory
   13.20 +    Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
   13.21    val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory ->
   13.22      ((string list * (binding -> binding) list) *
   13.23      (term list * thm list * (int list list * thm list list))) * local_theory
   13.24 @@ -666,8 +666,8 @@
   13.25      old_primrec raw_fixes raw_specs lthy
   13.26      |>> (fn (ts, thms) => (ts, [], [thms]));
   13.27  
   13.28 -val primrec = gen_primrec Old_Primrec.primrec Specification.check_spec [];
   13.29 -val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_spec;
   13.30 +val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs [];
   13.31 +val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs;
   13.32  
   13.33  fun primrec_global fixes specs =
   13.34    Named_Target.theory_init
   13.35 @@ -688,7 +688,7 @@
   13.36    "define primitive recursive functions"
   13.37    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
   13.38        --| @{keyword ")"}) []) --
   13.39 -    (Parse.fixes -- Parse_Spec.where_alt_specs)
   13.40 +    (Parse.fixes -- Parse_Spec.where_multi_specs)
   13.41      >> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
   13.42  
   13.43  end;
    14.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Apr 27 10:03:35 2016 +0200
    14.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 28 09:43:11 2016 +0200
    14.3 @@ -623,12 +623,12 @@
    14.4                  else if Binding.eq_name (b, equal_binding) then
    14.5                    pair (Term.lambda u exist_xs_u_eq_ctr, refl)
    14.6                  else
    14.7 -                  Specification.definition (SOME (b, NONE, NoSyn),
    14.8 -                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
    14.9 +                  Specification.definition (SOME (b, NONE, NoSyn)) []
   14.10 +                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd)
   14.11                ks exist_xs_u_eq_ctrs disc_bindings
   14.12              ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
   14.13 -              Specification.definition (SOME (b, NONE, NoSyn),
   14.14 -                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
   14.15 +              Specification.definition (SOME (b, NONE, NoSyn)) []
   14.16 +                ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos
   14.17              ||> `Local_Theory.close_target;
   14.18  
   14.19            val phi = Proof_Context.export_morphism lthy lthy';
    15.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Wed Apr 27 10:03:35 2016 +0200
    15.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Thu Apr 28 09:43:11 2016 +0200
    15.3 @@ -93,7 +93,7 @@
    15.4            mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
    15.5            |> Syntax.check_term lthy;
    15.6          val ((_, (_, raw_def)), lthy') =
    15.7 -          Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
    15.8 +          Specification.definition NONE [] (Attrib.empty_binding, spec) lthy;
    15.9          val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
   15.10          val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
   15.11        in
    16.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Apr 27 10:03:35 2016 +0200
    16.2 +++ b/src/HOL/Tools/Function/fun.ML	Thu Apr 28 09:43:11 2016 +0200
    16.3 @@ -9,10 +9,10 @@
    16.4  sig
    16.5    val fun_config : Function_Common.function_config
    16.6    val add_fun : (binding * typ option * mixfix) list ->
    16.7 -    (Attrib.binding * term) list -> Function_Common.function_config ->
    16.8 +    Specification.multi_specs -> Function_Common.function_config ->
    16.9      local_theory -> Proof.context
   16.10    val add_fun_cmd : (binding * string option * mixfix) list ->
   16.11 -    (Attrib.binding * string) list -> Function_Common.function_config ->
   16.12 +    Specification.multi_specs_cmd -> Function_Common.function_config ->
   16.13      bool -> local_theory -> Proof.context
   16.14  end
   16.15  
    17.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Wed Apr 27 10:03:35 2016 +0200
    17.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Thu Apr 28 09:43:11 2016 +0200
    17.3 @@ -56,7 +56,7 @@
    17.4  val _ =
    17.5    Outer_Syntax.local_theory @{command_keyword fun_cases}
    17.6      "create simplified instances of elimination rules for function equations"
    17.7 -    (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
    17.8 +    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo fun_cases_cmd));
    17.9  
   17.10  end;
   17.11  
    18.1 --- a/src/HOL/Tools/Function/function.ML	Wed Apr 27 10:03:35 2016 +0200
    18.2 +++ b/src/HOL/Tools/Function/function.ML	Thu Apr 28 09:43:11 2016 +0200
    18.3 @@ -9,19 +9,19 @@
    18.4    include FUNCTION_DATA
    18.5  
    18.6    val add_function: (binding * typ option * mixfix) list ->
    18.7 -    (Attrib.binding * term) list -> Function_Common.function_config ->
    18.8 +    Specification.multi_specs -> Function_Common.function_config ->
    18.9      (Proof.context -> tactic) -> local_theory -> info * local_theory
   18.10  
   18.11    val add_function_cmd: (binding * string option * mixfix) list ->
   18.12 -    (Attrib.binding * string) list -> Function_Common.function_config ->
   18.13 +    Specification.multi_specs_cmd -> Function_Common.function_config ->
   18.14      (Proof.context -> tactic) -> bool -> local_theory -> info * local_theory
   18.15  
   18.16    val function: (binding * typ option * mixfix) list ->
   18.17 -    (Attrib.binding * term) list -> Function_Common.function_config ->
   18.18 +    Specification.multi_specs -> Function_Common.function_config ->
   18.19      local_theory -> Proof.state
   18.20  
   18.21    val function_cmd: (binding * string option * mixfix) list ->
   18.22 -    (Attrib.binding * string) list -> Function_Common.function_config ->
   18.23 +    Specification.multi_specs_cmd -> Function_Common.function_config ->
   18.24      bool -> local_theory -> Proof.state
   18.25  
   18.26    val prove_termination: term option -> tactic -> local_theory ->
   18.27 @@ -149,8 +149,8 @@
   18.28      |> afterqed [[pattern_thm]]
   18.29    end
   18.30  
   18.31 -val add_function = gen_add_function false Specification.check_spec
   18.32 -fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec a b c d
   18.33 +val add_function = gen_add_function false Specification.check_multi_specs
   18.34 +fun add_function_cmd a b c d int = gen_add_function int Specification.read_multi_specs a b c d
   18.35  
   18.36  fun gen_function do_print prep fixspec eqns config lthy =
   18.37    let
   18.38 @@ -162,8 +162,8 @@
   18.39      |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
   18.40    end
   18.41  
   18.42 -val function = gen_function false Specification.check_spec
   18.43 -fun function_cmd a b c int = gen_function int Specification.read_spec a b c
   18.44 +val function = gen_function false Specification.check_multi_specs
   18.45 +fun function_cmd a b c int = gen_function int Specification.read_multi_specs a b c
   18.46  
   18.47  fun prepare_termination_proof prep_term raw_term_opt lthy =
   18.48    let
    19.1 --- a/src/HOL/Tools/Function/function_common.ML	Wed Apr 27 10:03:35 2016 +0200
    19.2 +++ b/src/HOL/Tools/Function/function_common.ML	Thu Apr 28 09:43:11 2016 +0200
    19.3 @@ -100,7 +100,7 @@
    19.4    val default_config : function_config
    19.5    val function_parser : function_config ->
    19.6      ((function_config * (binding * string option * mixfix) list) *
    19.7 -      (Attrib.binding * string) list) parser
    19.8 +      Specification.multi_specs_cmd) parser
    19.9  end
   19.10  
   19.11  structure Function_Common : FUNCTION_COMMON =
   19.12 @@ -374,7 +374,7 @@
   19.13       >> (fn opts => fold apply_opt opts default)
   19.14  in
   19.15    fun function_parser default_cfg =
   19.16 -      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
   19.17 +      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_multi_specs
   19.18  end
   19.19  
   19.20  
    20.1 --- a/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 10:03:35 2016 +0200
    20.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Thu Apr 28 09:43:11 2016 +0200
    20.3 @@ -226,7 +226,7 @@
    20.4          "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
    20.5      val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
    20.6  
    20.7 -    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
    20.8 +    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [])] lthy;
    20.9      val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
   20.10  
   20.11      val ((f_binding, fT), mixfix) = the_single fixes;
   20.12 @@ -306,14 +306,14 @@
   20.13      |> note_qualified ("fixp_induct", [specialized_fixp_induct])
   20.14    end;
   20.15  
   20.16 -val add_partial_function = gen_add_partial_function Specification.check_spec;
   20.17 -val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
   20.18 +val add_partial_function = gen_add_partial_function Specification.check_multi_specs;
   20.19 +val add_partial_function_cmd = gen_add_partial_function Specification.read_multi_specs;
   20.20  
   20.21  val mode = @{keyword "("} |-- Parse.name --| @{keyword ")"};
   20.22  
   20.23  val _ =
   20.24    Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
   20.25 -    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
   20.26 +    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.simple_spec)))
   20.27        >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
   20.28  
   20.29  end;
    21.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 27 10:03:35 2016 +0200
    21.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 28 09:43:11 2016 +0200
    21.3 @@ -89,8 +89,8 @@
    21.4      val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
    21.5      val definition_term = Logic.mk_equals (lhs, rhs)
    21.6      fun note_def lthy =
    21.7 -      Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), 
    21.8 -        ((Binding.empty, []), definition_term)) lthy |>> (snd #> snd);
    21.9 +      Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) []
   21.10 +        ((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
   21.11      fun raw_def lthy =
   21.12        let
   21.13          val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term;
    22.1 --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Wed Apr 27 10:03:35 2016 +0200
    22.2 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Thu Apr 28 09:43:11 2016 +0200
    22.3 @@ -9,14 +9,14 @@
    22.4  signature OLD_PRIMREC =
    22.5  sig
    22.6    val primrec: (binding * typ option * mixfix) list ->
    22.7 -    (Attrib.binding * term) list -> local_theory -> (term list * thm list) * local_theory
    22.8 +    Specification.multi_specs -> local_theory -> (term list * thm list) * local_theory
    22.9    val primrec_cmd: (binding * string option * mixfix) list ->
   22.10 -    (Attrib.binding * string) list -> local_theory -> (term list * thm list) * local_theory
   22.11 +    Specification.multi_specs_cmd -> local_theory -> (term list * thm list) * local_theory
   22.12    val primrec_global: (binding * typ option * mixfix) list ->
   22.13 -    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
   22.14 +    Specification.multi_specs -> theory -> (term list * thm list) * theory
   22.15    val primrec_overloaded: (string * (string * typ) * bool) list ->
   22.16      (binding * typ option * mixfix) list ->
   22.17 -    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
   22.18 +    Specification.multi_specs -> theory -> (term list * thm list) * theory
   22.19    val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
   22.20      local_theory -> (string * (term list * thm list)) * local_theory
   22.21  end;
   22.22 @@ -290,8 +290,8 @@
   22.23  
   22.24  in
   22.25  
   22.26 -val primrec = gen_primrec Specification.check_spec;
   22.27 -val primrec_cmd = gen_primrec Specification.read_spec;
   22.28 +val primrec = gen_primrec Specification.check_multi_specs;
   22.29 +val primrec_cmd = gen_primrec Specification.read_multi_specs;
   22.30  
   22.31  end;
   22.32  
    23.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 27 10:03:35 2016 +0200
    23.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Apr 28 09:43:11 2016 +0200
    23.3 @@ -56,7 +56,7 @@
    23.4      thy
    23.5      |> Class.instantiation ([tyco], vs, @{sort partial_term_of})
    23.6      |> `(fn lthy => Syntax.check_term lthy eq)
    23.7 -    |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    23.8 +    |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
    23.9      |> snd
   23.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   23.11    end
    24.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Apr 27 10:03:35 2016 +0200
    24.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Apr 28 09:43:11 2016 +0200
    24.3 @@ -365,7 +365,7 @@
    24.4        Function.add_function
    24.5          (map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
    24.6            (names ~~ Ts))
    24.7 -        (map (pair (apfst Binding.concealed Attrib.empty_binding)) eqs_t)
    24.8 +        (map (fn t => (((Binding.concealed Binding.empty, []), t), [])) eqs_t)
    24.9          Function_Common.default_config pat_completeness_auto
   24.10        #> snd
   24.11        #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
    25.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Apr 27 10:03:35 2016 +0200
    25.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Apr 28 09:43:11 2016 +0200
    25.3 @@ -266,8 +266,8 @@
    25.4      |> random_aux_specification prfx random_auxN auxs_eqs
    25.5      |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
    25.6      |-> (fn random_defs' => fold_map (fn random_def =>
    25.7 -          Specification.definition (NONE, (apfst Binding.concealed
    25.8 -            Attrib.empty_binding, random_def))) random_defs')
    25.9 +          Specification.definition NONE []
   25.10 +            ((Binding.concealed Binding.empty, []), random_def)) random_defs')
   25.11      |> snd
   25.12      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   25.13    end;
    26.1 --- a/src/HOL/Tools/code_evaluation.ML	Wed Apr 27 10:03:35 2016 +0200
    26.2 +++ b/src/HOL/Tools/code_evaluation.ML	Thu Apr 28 09:43:11 2016 +0200
    26.3 @@ -43,7 +43,7 @@
    26.4      thy
    26.5      |> Class.instantiation ([tyco], vs, @{sort term_of})
    26.6      |> `(fn lthy => Syntax.check_term lthy eq)
    26.7 -    |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    26.8 +    |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
    26.9      |> snd
   26.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   26.11    end;
    27.1 --- a/src/HOL/Tools/inductive.ML	Wed Apr 27 10:03:35 2016 +0200
    27.2 +++ b/src/HOL/Tools/inductive.ML	Thu Apr 28 09:43:11 2016 +0200
    27.3 @@ -54,7 +54,7 @@
    27.4    val add_inductive: bool -> bool ->
    27.5      (binding * string option * mixfix) list ->
    27.6      (binding * string option * mixfix) list ->
    27.7 -    (Attrib.binding * string) list ->
    27.8 +    Specification.multi_specs_cmd ->
    27.9      (Facts.ref * Token.src list) list ->
   27.10      local_theory -> inductive_result * local_theory
   27.11    val add_inductive_global: inductive_flags ->
   27.12 @@ -88,7 +88,7 @@
   27.13    val gen_add_inductive: add_ind_def -> bool -> bool ->
   27.14      (binding * string option * mixfix) list ->
   27.15      (binding * string option * mixfix) list ->
   27.16 -    (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
   27.17 +    Specification.multi_specs_cmd -> (Facts.ref * Token.src list) list ->
   27.18      local_theory -> inductive_result * local_theory
   27.19    val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
   27.20  end;
   27.21 @@ -1084,7 +1084,7 @@
   27.22    let
   27.23      val ((vars, intrs), _) = lthy
   27.24        |> Proof_Context.set_mode Proof_Context.mode_abbrev
   27.25 -      |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
   27.26 +      |> Specification.read_multi_specs (cnames_syn @ pnames_syn) intro_srcs;
   27.27      val (cs, ps) = chop (length cnames_syn) vars;
   27.28      val monos = Attrib.eval_thms lthy raw_monos;
   27.29      val flags =
   27.30 @@ -1170,7 +1170,7 @@
   27.31  
   27.32  fun gen_ind_decl mk_def coind =
   27.33    Parse.fixes -- Parse.for_fixes --
   27.34 -  Scan.optional Parse_Spec.where_alt_specs [] --
   27.35 +  Scan.optional Parse_Spec.where_multi_specs [] --
   27.36    Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) []
   27.37    >> (fn (((preds, params), specs), monos) =>
   27.38        (snd o gen_add_inductive mk_def true coind preds params specs monos));
   27.39 @@ -1188,12 +1188,12 @@
   27.40  val _ =
   27.41    Outer_Syntax.local_theory @{command_keyword inductive_cases}
   27.42      "create simplified instances of elimination rules"
   27.43 -    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
   27.44 +    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo inductive_cases));
   27.45  
   27.46  val _ =
   27.47    Outer_Syntax.local_theory @{command_keyword inductive_simps}
   27.48      "create simplification rules for inductive predicates"
   27.49 -    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
   27.50 +    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo inductive_simps));
   27.51  
   27.52  val _ =
   27.53    Outer_Syntax.command @{command_keyword print_inductives}
    28.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Apr 27 10:03:35 2016 +0200
    28.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Apr 28 09:43:11 2016 +0200
    28.3 @@ -20,7 +20,7 @@
    28.4    val add_inductive: bool -> bool ->
    28.5      (binding * string option * mixfix) list ->
    28.6      (binding * string option * mixfix) list ->
    28.7 -    (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
    28.8 +    Specification.multi_specs_cmd -> (Facts.ref * Token.src list) list ->
    28.9      local_theory -> Inductive.inductive_result * local_theory
   28.10    val mono_add: attribute
   28.11    val mono_del: attribute
    29.1 --- a/src/HOL/Tools/record.ML	Wed Apr 27 10:03:35 2016 +0200
    29.2 +++ b/src/HOL/Tools/record.ML	Thu Apr 28 09:43:11 2016 +0200
    29.3 @@ -1734,7 +1734,7 @@
    29.4      thy
    29.5      |> Class.instantiation ([tyco], vs, sort)
    29.6      |> `(fn lthy => Syntax.check_term lthy eq)
    29.7 -    |-> (fn eq => Specification.definition (NONE, (apfst Binding.concealed Attrib.empty_binding, eq)))
    29.8 +    |-> (fn eq => Specification.definition NONE [] ((Binding.concealed Binding.empty, []), eq))
    29.9      |> snd
   29.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   29.11    end;
   29.12 @@ -1781,8 +1781,7 @@
   29.13        |> fold Code.add_default_eqn simps
   29.14        |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
   29.15        |> `(fn lthy => Syntax.check_term lthy eq)
   29.16 -      |-> (fn eq => Specification.definition
   29.17 -            (NONE, (Attrib.empty_binding, eq)))
   29.18 +      |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
   29.19        |-> (fn (_, (_, eq_def)) =>
   29.20           Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
   29.21        |-> (fn eq_def => fn thy =>
    30.1 --- a/src/HOL/Typerep.thy	Wed Apr 27 10:03:35 2016 +0200
    30.2 +++ b/src/HOL/Typerep.thy	Thu Apr 28 09:43:11 2016 +0200
    30.3 @@ -58,7 +58,7 @@
    30.4      thy
    30.5      |> Class.instantiation ([tyco], vs, @{sort typerep})
    30.6      |> `(fn lthy => Syntax.check_term lthy eq)
    30.7 -    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    30.8 +    |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
    30.9      |> snd
   30.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   30.11    end;
    31.1 --- a/src/Pure/Isar/parse_spec.ML	Wed Apr 27 10:03:35 2016 +0200
    31.2 +++ b/src/Pure/Isar/parse_spec.ML	Thu Apr 28 09:43:11 2016 +0200
    31.3 @@ -8,13 +8,15 @@
    31.4  sig
    31.5    val thm_name: string -> Attrib.binding parser
    31.6    val opt_thm_name: string -> Attrib.binding parser
    31.7 -  val spec: (Attrib.binding * string) parser
    31.8 -  val specs: (Attrib.binding * string list) parser
    31.9 -  val alt_specs: (Attrib.binding * string) list parser
   31.10 -  val where_alt_specs: (Attrib.binding * string) list parser
   31.11    val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser
   31.12 +  val simple_spec: (Attrib.binding * string) parser
   31.13 +  val simple_specs: (Attrib.binding * string list) parser
   31.14 +  val if_assumes: string list parser
   31.15 +  val spec: (string list * (Attrib.binding * string)) parser
   31.16 +  val multi_specs: Specification.multi_specs_cmd parser
   31.17 +  val where_multi_specs: Specification.multi_specs_cmd parser
   31.18 +  val specification: (string list * (Attrib.binding * string list) list) parser
   31.19    val constdecl: (binding * string option * mixfix) parser
   31.20 -  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
   31.21    val includes: (xstring * Position.T) list parser
   31.22    val locale_fixes: (binding * string option * mixfix) list parser
   31.23    val locale_insts: (string option list * (Attrib.binding * string) list) parser
   31.24 @@ -37,7 +39,7 @@
   31.25  structure Parse_Spec: PARSE_SPEC =
   31.26  struct
   31.27  
   31.28 -(* theorem specifications *)
   31.29 +(* simple specifications *)
   31.30  
   31.31  fun thm_name s = Parse.binding -- Parse.opt_attribs --| Parse.$$$ s;
   31.32  
   31.33 @@ -46,18 +48,31 @@
   31.34      ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s)
   31.35      Attrib.empty_binding;
   31.36  
   31.37 -val spec = opt_thm_name ":" -- Parse.prop;
   31.38 -val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
   31.39 -
   31.40 -val alt_specs =
   31.41 -  Parse.enum1 "|"
   31.42 -    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
   31.43 -
   31.44 -val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
   31.45 +val simple_spec = opt_thm_name ":" -- Parse.prop;
   31.46 +val simple_specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
   31.47  
   31.48  val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.thms1);
   31.49  
   31.50  
   31.51 +(* structured specifications *)
   31.52 +
   31.53 +val if_assumes =
   31.54 +  Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat))
   31.55 +    [];
   31.56 +
   31.57 +val spec = (opt_thm_name ":" -- Parse.prop) -- if_assumes >> swap;
   31.58 +
   31.59 +val multi_specs =
   31.60 +  Parse.enum1 "|"
   31.61 +    (opt_thm_name ":" -- Parse.prop -- if_assumes --|
   31.62 +      Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
   31.63 +
   31.64 +val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
   31.65 +
   31.66 +val specification =
   31.67 +  Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.prop) -- if_assumes >> swap;
   31.68 +
   31.69 +
   31.70  (* basic constant specifications *)
   31.71  
   31.72  val constdecl =
   31.73 @@ -67,8 +82,6 @@
   31.74        Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
   31.75    >> Scan.triple2;
   31.76  
   31.77 -val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
   31.78 -
   31.79  
   31.80  (* locale and context elements *)
   31.81  
    32.1 --- a/src/Pure/Isar/specification.ML	Wed Apr 27 10:03:35 2016 +0200
    32.2 +++ b/src/Pure/Isar/specification.ML	Thu Apr 28 09:43:11 2016 +0200
    32.3 @@ -11,45 +11,40 @@
    32.4      term list * Proof.context
    32.5    val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
    32.6      term * Proof.context
    32.7 -  val check_free_spec:
    32.8 -    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
    32.9 -    ((((binding * typ) * mixfix) list * (Attrib.binding * term) list) * (string -> Position.T))
   32.10 +  val check_spec: (binding * typ option * mixfix) list ->
   32.11 +    term list -> Attrib.binding * term -> Proof.context ->
   32.12 +    ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
   32.13        * Proof.context
   32.14 -  val read_free_spec:
   32.15 -    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
   32.16 -    ((((binding * typ) * mixfix) list * (Attrib.binding * term) list) * (string -> Position.T))
   32.17 +  val read_spec: (binding * string option * mixfix) list ->
   32.18 +    string list -> Attrib.binding * string -> Proof.context ->
   32.19 +    ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
   32.20        * Proof.context
   32.21 -  val check_spec:
   32.22 -    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
   32.23 +  type multi_specs = ((Attrib.binding * term) * term list) list
   32.24 +  type multi_specs_cmd = ((Attrib.binding * string) * string list) list
   32.25 +  val check_multi_specs: (binding * typ option * mixfix) list -> multi_specs -> Proof.context ->
   32.26      (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   32.27 -  val read_spec:
   32.28 -    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
   32.29 +  val read_multi_specs: (binding * string option * mixfix) list -> multi_specs_cmd -> Proof.context ->
   32.30      (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   32.31 -  val check_specification: (binding * typ option * mixfix) list ->
   32.32 +  val check_specification: (binding * typ option * mixfix) list -> term list ->
   32.33      (Attrib.binding * term list) list -> Proof.context ->
   32.34      (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   32.35 -  val read_specification: (binding * string option * mixfix) list ->
   32.36 +  val read_specification: (binding * string option * mixfix) list -> string list ->
   32.37      (Attrib.binding * string list) list -> Proof.context ->
   32.38      (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   32.39 -  val axiomatization: (binding * typ option * mixfix) list ->
   32.40 -    (Attrib.binding * term list) list -> theory ->
   32.41 -    (term list * thm list list) * theory
   32.42 -  val axiomatization_cmd: (binding * string option * mixfix) list ->
   32.43 -    (Attrib.binding * string list) list -> theory ->
   32.44 -    (term list * thm list list) * theory
   32.45 +  val axiomatization: (binding * typ option * mixfix) list -> term list ->
   32.46 +    (Attrib.binding * term list) list -> theory -> (term list * thm list list) * theory
   32.47 +  val axiomatization_cmd: (binding * string option * mixfix) list -> string list ->
   32.48 +    (Attrib.binding * string list) list -> theory -> (term list * thm list list) * theory
   32.49    val axiom: Attrib.binding * term -> theory -> thm * theory
   32.50 -  val definition:
   32.51 -    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
   32.52 -    local_theory -> (term * (string * thm)) * local_theory
   32.53 -  val definition':
   32.54 -    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
   32.55 -    bool -> local_theory -> (term * (string * thm)) * local_theory
   32.56 -  val definition_cmd:
   32.57 -    (binding * string option * mixfix) option * (Attrib.binding * string) ->
   32.58 -    bool -> local_theory -> (term * (string * thm)) * local_theory
   32.59 -  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
   32.60 +  val definition: (binding * typ option * mixfix) option -> term list ->
   32.61 +    Attrib.binding * term -> local_theory -> (term * (string * thm)) * local_theory
   32.62 +  val definition': (binding * typ option * mixfix) option -> term list ->
   32.63 +    Attrib.binding * term -> bool -> local_theory -> (term * (string * thm)) * local_theory
   32.64 +  val definition_cmd: (binding * string option * mixfix) option -> string list ->
   32.65 +    Attrib.binding * string -> bool -> local_theory -> (term * (string * thm)) * local_theory
   32.66 +  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option -> term ->
   32.67      bool -> local_theory -> local_theory
   32.68 -  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
   32.69 +  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> string ->
   32.70      bool -> local_theory -> local_theory
   32.71    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   32.72    val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
   32.73 @@ -141,7 +136,7 @@
   32.74            map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
   32.75  
   32.76      val Asss0 =
   32.77 -      (map o map) snd raw_specss
   32.78 +      map (fn (raw_concls, raw_prems) => raw_prems :: map snd raw_concls) raw_specss
   32.79        |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
   32.80      val names =
   32.81        Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss0)
   32.82 @@ -151,8 +146,8 @@
   32.83      val idx = (fold o fold o fold) Term.maxidx_term Asss1 ~1 + 1;
   32.84  
   32.85      val (Asss2, _) =
   32.86 -      fold_map (fn Ass => fn i => (burrow (close_forms params_ctxt auto_close i []) Ass, i + 1))
   32.87 -        Asss1 idx;
   32.88 +      fold_map (fn prems :: conclss => fn i =>
   32.89 +        (burrow (close_forms params_ctxt auto_close i prems) conclss, i + 1)) Asss1 idx;
   32.90  
   32.91      val specs = burrow (Syntax.check_props params_ctxt) (flat Asss2);
   32.92      val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
   32.93 @@ -160,7 +155,7 @@
   32.94      val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
   32.95      val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
   32.96      val name_atts: Attrib.binding list =
   32.97 -      map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
   32.98 +      map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (maps #1 raw_specss);
   32.99  
  32.100      fun get_pos x =
  32.101        (case (maps o maps o maps) (get_positions specs_ctxt x) Asss2 of
  32.102 @@ -169,45 +164,50 @@
  32.103    in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
  32.104  
  32.105  
  32.106 -fun single_spec (a, prop) = [(a, [prop])];
  32.107 +fun single_spec ((a, B), As) = ([(a, [B])], As);
  32.108  fun the_spec (a, [prop]) = (a, prop);
  32.109  
  32.110 -fun prep_spec prep_var parse_prop prep_att auto_close vars specs =
  32.111 +fun prep_specs prep_var parse_prop prep_att auto_close vars specs =
  32.112    prepare prep_var parse_prop prep_att auto_close
  32.113      vars (map single_spec specs) #>> (apfst o apsnd) (map the_spec);
  32.114  
  32.115  in
  32.116  
  32.117 -fun check_free_spec vars specs =
  32.118 -  prep_spec Proof_Context.cert_var (K I) (K I) false vars specs;
  32.119 +fun check_spec xs As B =
  32.120 +  prep_specs Proof_Context.cert_var (K I) (K I) false xs [(B, As)] #>
  32.121 +  (apfst o apfst o apsnd) the_single;
  32.122  
  32.123 -fun read_free_spec vars specs =
  32.124 -  prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src false vars specs;
  32.125 +fun read_spec xs As B =
  32.126 +  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src false xs [(B, As)] #>
  32.127 +  (apfst o apfst o apsnd) the_single;
  32.128  
  32.129 -fun check_spec vars specs =
  32.130 -  prep_spec Proof_Context.cert_var (K I) (K I) true vars specs #> apfst fst;
  32.131 +type multi_specs = ((Attrib.binding * term) * term list) list;
  32.132 +type multi_specs_cmd = ((Attrib.binding * string) * string list) list;
  32.133  
  32.134 -fun read_spec vars specs =
  32.135 -  prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars specs #> apfst fst;
  32.136 +fun check_multi_specs xs specs =
  32.137 +  prep_specs Proof_Context.cert_var (K I) (K I) true xs specs #>> #1;
  32.138 +
  32.139 +fun read_multi_specs xs specs =
  32.140 +  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs specs #>> #1;
  32.141  
  32.142 -fun check_specification vars specs =
  32.143 -  prepare Proof_Context.cert_var (K I) (K I) true vars [specs] #> apfst fst
  32.144 +fun check_specification xs As Bs =
  32.145 +  prepare Proof_Context.cert_var (K I) (K I) true xs [(Bs, As)] #>> #1;
  32.146  
  32.147 -fun read_specification vars specs =
  32.148 -  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars [specs] #> apfst fst;
  32.149 +fun read_specification xs As Bs =
  32.150 +  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs [(Bs, As)] #>> #1;
  32.151  
  32.152  end;
  32.153  
  32.154  
  32.155  (* axiomatization -- within global theory *)
  32.156  
  32.157 -fun gen_axioms prep raw_vars raw_specs thy =
  32.158 +fun gen_axioms prep raw_decls raw_prems raw_concls thy =
  32.159    let
  32.160 -    val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
  32.161 -    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars;
  32.162 +    val ((decls, specs), _) = prep raw_decls raw_prems raw_concls (Proof_Context.init_global thy);
  32.163 +    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) decls;
  32.164  
  32.165      (*consts*)
  32.166 -    val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
  32.167 +    val (consts, consts_thy) = thy |> fold_map Theory.specify_const decls;
  32.168      val subst = Term.subst_atomic (map Free xs ~~ consts);
  32.169  
  32.170      (*axioms*)
  32.171 @@ -228,15 +228,15 @@
  32.172  val axiomatization = gen_axioms check_specification;
  32.173  val axiomatization_cmd = gen_axioms read_specification;
  32.174  
  32.175 -fun axiom (b, ax) = axiomatization [] [(b, [ax])] #>> (hd o hd o snd);
  32.176 +fun axiom (b, ax) = axiomatization [] [] [(b, [ax])] #>> (hd o hd o snd);
  32.177  
  32.178  
  32.179  (* definition *)
  32.180  
  32.181 -fun gen_def prep (raw_var, raw_spec) int lthy =
  32.182 +fun gen_def prep raw_var raw_prems raw_spec int lthy =
  32.183    let
  32.184 -    val ((vars, [((raw_name, atts), prop)]), get_pos) =
  32.185 -      fst (prep (the_list raw_var) [raw_spec] lthy);
  32.186 +    val ((vars, ((raw_name, atts), prop)), get_pos) =
  32.187 +      fst (prep (the_list raw_var) raw_prems raw_spec lthy);
  32.188      val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} prop;
  32.189      val _ = Name.reject_internal (x, []);
  32.190      val (b, mx) =
  32.191 @@ -266,19 +266,19 @@
  32.192          (member (op =) (Term.add_frees lhs' [])) [(x, T)];
  32.193    in ((lhs, (def_name, th')), lthy4) end;
  32.194  
  32.195 -val definition' = gen_def check_free_spec;
  32.196 -fun definition spec = definition' spec false;
  32.197 -val definition_cmd = gen_def read_free_spec;
  32.198 +val definition' = gen_def check_spec;
  32.199 +fun definition xs As B = definition' xs As B false;
  32.200 +val definition_cmd = gen_def read_spec;
  32.201  
  32.202  
  32.203  (* abbreviation *)
  32.204  
  32.205 -fun gen_abbrev prep mode (raw_var, raw_prop) int lthy =
  32.206 +fun gen_abbrev prep mode raw_var raw_prop int lthy =
  32.207    let
  32.208      val lthy1 = lthy
  32.209        |> Proof_Context.set_syntax_mode mode;
  32.210 -    val (((vars, [(_, prop)]), get_pos), _) =
  32.211 -      prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
  32.212 +    val (((vars, (_, prop)), get_pos), _) =
  32.213 +      prep (the_list raw_var) [] (Attrib.empty_binding, raw_prop)
  32.214          (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
  32.215      val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
  32.216      val _ = Name.reject_internal (x, []);
  32.217 @@ -299,8 +299,8 @@
  32.218      val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
  32.219    in lthy2 end;
  32.220  
  32.221 -val abbreviation = gen_abbrev check_free_spec;
  32.222 -val abbreviation_cmd = gen_abbrev read_free_spec;
  32.223 +val abbreviation = gen_abbrev check_spec;
  32.224 +val abbreviation_cmd = gen_abbrev read_spec;
  32.225  
  32.226  
  32.227  (* notation *)
    33.1 --- a/src/Pure/Pure.thy	Wed Apr 27 10:03:35 2016 +0200
    33.2 +++ b/src/Pure/Pure.thy	Thu Apr 28 09:43:11 2016 +0200
    33.3 @@ -343,18 +343,19 @@
    33.4  
    33.5  val _ =
    33.6    Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
    33.7 -    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
    33.8 +    (Scan.option Parse_Spec.constdecl -- Parse_Spec.spec
    33.9 +      >> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c));
   33.10  
   33.11  val _ =
   33.12    Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   33.13      (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   33.14 -      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   33.15 +      >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
   33.16  
   33.17  val _ =
   33.18    Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
   33.19      (Scan.optional Parse.fixes [] --
   33.20 -      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
   33.21 -      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
   33.22 +      Scan.optional (Parse.where_ |-- Parse.!!! Parse_Spec.specification) ([], [])
   33.23 +      >> (fn (a, (b, c)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c)));
   33.24  
   33.25  in end\<close>
   33.26  
    34.1 --- a/src/Pure/ROOT.ML	Wed Apr 27 10:03:35 2016 +0200
    34.2 +++ b/src/Pure/ROOT.ML	Thu Apr 28 09:43:11 2016 +0200
    34.3 @@ -251,9 +251,9 @@
    34.4  ML_file "Isar/code.ML";
    34.5  
    34.6  (*specifications*)
    34.7 -ML_file "Isar/parse_spec.ML";
    34.8  ML_file "Isar/spec_rules.ML";
    34.9  ML_file "Isar/specification.ML";
   34.10 +ML_file "Isar/parse_spec.ML";
   34.11  ML_file "Isar/typedecl.ML";
   34.12  
   34.13  (*toplevel transactions*)
    35.1 --- a/src/Tools/Code/code_runtime.ML	Wed Apr 27 10:03:35 2016 +0200
    35.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Apr 28 09:43:11 2016 +0200
    35.3 @@ -548,7 +548,7 @@
    35.4  fun add_definiendum (ml_name, (b, T)) thy =
    35.5    thy
    35.6    |> Code_Target.add_reserved target ml_name
    35.7 -  |> Specification.axiomatization [(b, SOME T, NoSyn)] []
    35.8 +  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] []
    35.9    |-> (fn ([Const (const, _)], _) =>
   35.10      Code_Target.set_printings (Constant (const,
   35.11        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))