clarified check_open_spec / read_open_spec;
authorwenzelm
Sun May 29 15:40:25 2016 +0200 (2016-05-29)
changeset 63180ddfd021884b4
parent 63179 231e261fd6bc
child 63181 ee1c9de4e03a
clarified check_open_spec / read_open_spec;
allow 'for' fixes in 'abbreviation', 'definition';
NEWS
src/Doc/Isar_Ref/Spec.thy
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/inductive.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
     1.1 --- a/NEWS	Sat May 28 23:55:41 2016 +0200
     1.2 +++ b/NEWS	Sun May 29 15:40:25 2016 +0200
     1.3 @@ -66,14 +66,14 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 -* Many specification elements support structured statements with 'if'
     1.8 -eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
     1.9 -'function'.
    1.10 -
    1.11  * Command 'axiomatization' has become more restrictive to correspond
    1.12  better to internal axioms as singleton facts with mandatory name. Minor
    1.13  INCOMPATIBILITY.
    1.14  
    1.15 +* Many specification elements support structured statements with 'if' /
    1.16 +'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
    1.17 +'definition', 'inductive', 'function'.
    1.18 +
    1.19  * Toplevel theorem statements support eigen-context notation with 'if' /
    1.20  'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
    1.21  traditional long statement form (in prefix). Local premises are called
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat May 28 23:55:41 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sun May 29 15:40:25 2016 +0200
     2.3 @@ -285,14 +285,19 @@
     2.4    ``abbreviation''.
     2.5  
     2.6    @{rail \<open>
     2.7 -    @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
     2.8 +    @@{command definition} decl? definition
     2.9      ;
    2.10 -    @@{command abbreviation} @{syntax mode}? \<newline>
    2.11 -      (decl @'where')? @{syntax prop}
    2.12 -    ;
    2.13 -    decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
    2.14 +    @@{command abbreviation} @{syntax mode}? decl? abbreviation
    2.15      ;
    2.16      @@{command print_abbrevs} ('!'?)
    2.17 +    ;
    2.18 +    decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
    2.19 +    ;
    2.20 +    definition: @{syntax thmdecl}? @{syntax prop} prems @{syntax for_fixes}
    2.21 +    ;
    2.22 +    prems: (@'if' ((@{syntax prop}+) + @'and'))?
    2.23 +    ;
    2.24 +    abbreviation: @{syntax prop} @{syntax for_fixes}
    2.25    \<close>}
    2.26  
    2.27    \<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according
     3.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Sat May 28 23:55:41 2016 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sun May 29 15:40:25 2016 +0200
     3.3 @@ -175,7 +175,7 @@
     3.4        Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))
     3.5      val ((_, (_, below_ldef)), lthy) = thy
     3.6        |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
     3.7 -      |> Specification.definition NONE []
     3.8 +      |> Specification.definition NONE [] []
     3.9            ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)
    3.10      val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
    3.11      val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
     4.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Sat May 28 23:55:41 2016 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun May 29 15:40:25 2016 +0200
     4.3 @@ -138,17 +138,17 @@
     4.4      val lthy = thy
     4.5        |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
     4.6      val ((_, (_, emb_ldef)), lthy) =
     4.7 -        Specification.definition NONE [] (emb_bind, emb_eqn) lthy
     4.8 +        Specification.definition NONE [] [] (emb_bind, emb_eqn) lthy
     4.9      val ((_, (_, prj_ldef)), lthy) =
    4.10 -        Specification.definition NONE [] (prj_bind, prj_eqn) lthy
    4.11 +        Specification.definition NONE [] [] (prj_bind, prj_eqn) lthy
    4.12      val ((_, (_, defl_ldef)), lthy) =
    4.13 -        Specification.definition NONE [] (defl_bind, defl_eqn) lthy
    4.14 +        Specification.definition NONE [] [] (defl_bind, defl_eqn) lthy
    4.15      val ((_, (_, liftemb_ldef)), lthy) =
    4.16 -        Specification.definition NONE [] (liftemb_bind, liftemb_eqn) lthy
    4.17 +        Specification.definition NONE [] [] (liftemb_bind, liftemb_eqn) lthy
    4.18      val ((_, (_, liftprj_ldef)), lthy) =
    4.19 -        Specification.definition NONE [] (liftprj_bind, liftprj_eqn) lthy
    4.20 +        Specification.definition NONE [] [] (liftprj_bind, liftprj_eqn) lthy
    4.21      val ((_, (_, liftdefl_ldef)), lthy) =
    4.22 -        Specification.definition NONE [] (liftdefl_bind, liftdefl_eqn) lthy
    4.23 +        Specification.definition NONE [] [] (liftdefl_bind, liftdefl_eqn) lthy
    4.24      val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
    4.25      val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef
    4.26      val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef
     5.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat May 28 23:55:41 2016 +0200
     5.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sun May 29 15:40:25 2016 +0200
     5.3 @@ -1020,7 +1020,7 @@
     5.4              "\ndoes not match type " ^ ty' ^ " in definition");
     5.5          val id' = mk_rulename id;
     5.6          val ((t', (_, th)), lthy') = Named_Target.theory_init thy
     5.7 -          |> Specification.definition NONE []
     5.8 +          |> Specification.definition NONE [] []
     5.9              ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
    5.10          val phi =
    5.11            Proof_Context.export_morphism lthy'
     6.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat May 28 23:55:41 2016 +0200
     6.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 29 15:40:25 2016 +0200
     6.3 @@ -623,11 +623,11 @@
     6.4                  else if Binding.eq_name (b, equal_binding) then
     6.5                    pair (Term.lambda u exist_xs_u_eq_ctr, refl)
     6.6                  else
     6.7 -                  Specification.definition (SOME (b, NONE, NoSyn)) []
     6.8 +                  Specification.definition (SOME (b, NONE, NoSyn)) [] []
     6.9                      ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd)
    6.10                ks exist_xs_u_eq_ctrs disc_bindings
    6.11              ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
    6.12 -              Specification.definition (SOME (b, NONE, NoSyn)) []
    6.13 +              Specification.definition (SOME (b, NONE, NoSyn)) [] []
    6.14                  ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos
    6.15              ||> `Local_Theory.close_target;
    6.16  
     7.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sat May 28 23:55:41 2016 +0200
     7.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sun May 29 15:40:25 2016 +0200
     7.3 @@ -93,7 +93,7 @@
     7.4            mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
     7.5            |> Syntax.check_term lthy;
     7.6          val ((_, (_, raw_def)), lthy') =
     7.7 -          Specification.definition NONE [] (Attrib.empty_binding, spec) lthy;
     7.8 +          Specification.definition NONE [] [] (Attrib.empty_binding, spec) lthy;
     7.9          val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
    7.10          val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
    7.11        in
     8.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sat May 28 23:55:41 2016 +0200
     8.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 29 15:40:25 2016 +0200
     8.3 @@ -89,7 +89,7 @@
     8.4      val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
     8.5      val definition_term = Logic.mk_equals (lhs, rhs)
     8.6      fun note_def lthy =
     8.7 -      Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) []
     8.8 +      Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
     8.9          ((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
    8.10      fun raw_def lthy =
    8.11        let
     9.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat May 28 23:55:41 2016 +0200
     9.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun May 29 15:40:25 2016 +0200
     9.3 @@ -56,7 +56,7 @@
     9.4      thy
     9.5      |> Class.instantiation ([tyco], vs, @{sort partial_term_of})
     9.6      |> `(fn lthy => Syntax.check_term lthy eq)
     9.7 -    |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
     9.8 +    |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
     9.9      |> snd
    9.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
    9.11    end
    10.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat May 28 23:55:41 2016 +0200
    10.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun May 29 15:40:25 2016 +0200
    10.3 @@ -266,7 +266,7 @@
    10.4      |> random_aux_specification prfx random_auxN auxs_eqs
    10.5      |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
    10.6      |-> (fn random_defs' => fold_map (fn random_def =>
    10.7 -          Specification.definition NONE []
    10.8 +          Specification.definition NONE [] []
    10.9              ((Binding.concealed Binding.empty, []), random_def)) random_defs')
   10.10      |> snd
   10.11      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
    11.1 --- a/src/HOL/Tools/code_evaluation.ML	Sat May 28 23:55:41 2016 +0200
    11.2 +++ b/src/HOL/Tools/code_evaluation.ML	Sun May 29 15:40:25 2016 +0200
    11.3 @@ -43,7 +43,7 @@
    11.4      thy
    11.5      |> Class.instantiation ([tyco], vs, @{sort term_of})
    11.6      |> `(fn lthy => Syntax.check_term lthy eq)
    11.7 -    |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
    11.8 +    |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
    11.9      |> snd
   11.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   11.11    end;
    12.1 --- a/src/HOL/Tools/inductive.ML	Sat May 28 23:55:41 2016 +0200
    12.2 +++ b/src/HOL/Tools/inductive.ML	Sun May 29 15:40:25 2016 +0200
    12.3 @@ -610,7 +610,7 @@
    12.4  
    12.5  fun ind_cases_rules ctxt raw_props raw_fixes =
    12.6    let
    12.7 -    val (props, ctxt' ) = Specification.read_props raw_props raw_fixes ctxt;
    12.8 +    val (props, ctxt') = Specification.read_props raw_props raw_fixes ctxt;
    12.9      val rules = Proof_Context.export ctxt' ctxt (map (mk_cases ctxt') props);
   12.10    in rules end;
   12.11  
    13.1 --- a/src/HOL/Tools/record.ML	Sat May 28 23:55:41 2016 +0200
    13.2 +++ b/src/HOL/Tools/record.ML	Sun May 29 15:40:25 2016 +0200
    13.3 @@ -1734,7 +1734,7 @@
    13.4      thy
    13.5      |> Class.instantiation ([tyco], vs, sort)
    13.6      |> `(fn lthy => Syntax.check_term lthy eq)
    13.7 -    |-> (fn eq => Specification.definition NONE [] ((Binding.concealed Binding.empty, []), eq))
    13.8 +    |-> (fn eq => Specification.definition NONE [] [] ((Binding.concealed Binding.empty, []), eq))
    13.9      |> snd
   13.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   13.11    end;
   13.12 @@ -1781,7 +1781,7 @@
   13.13        |> fold Code.add_default_eqn simps
   13.14        |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
   13.15        |> `(fn lthy => Syntax.check_term lthy eq)
   13.16 -      |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
   13.17 +      |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
   13.18        |-> (fn (_, (_, eq_def)) =>
   13.19           Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
   13.20        |-> (fn eq_def => fn thy =>
    14.1 --- a/src/HOL/Typerep.thy	Sat May 28 23:55:41 2016 +0200
    14.2 +++ b/src/HOL/Typerep.thy	Sun May 29 15:40:25 2016 +0200
    14.3 @@ -58,7 +58,7 @@
    14.4      thy
    14.5      |> Class.instantiation ([tyco], vs, @{sort typerep})
    14.6      |> `(fn lthy => Syntax.check_term lthy eq)
    14.7 -    |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
    14.8 +    |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
    14.9      |> snd
   14.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   14.11    end;
    15.1 --- a/src/Pure/Isar/parse_spec.ML	Sat May 28 23:55:41 2016 +0200
    15.2 +++ b/src/Pure/Isar/parse_spec.ML	Sun May 29 15:40:25 2016 +0200
    15.3 @@ -12,7 +12,6 @@
    15.4    val simple_spec: (Attrib.binding * string) parser
    15.5    val simple_specs: (Attrib.binding * string list) parser
    15.6    val if_assumes: string list parser
    15.7 -  val spec: (string list * (Attrib.binding * string)) parser
    15.8    val multi_specs: Specification.multi_specs_cmd parser
    15.9    val where_multi_specs: Specification.multi_specs_cmd parser
   15.10    val constdecl: (binding * string option * mixfix) parser
   15.11 @@ -59,8 +58,6 @@
   15.12    Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat))
   15.13      [];
   15.14  
   15.15 -val spec = (opt_thm_name ":" -- Parse.prop) -- if_assumes >> swap;
   15.16 -
   15.17  val multi_specs =
   15.18    Parse.enum1 "|"
   15.19      (opt_thm_name ":" -- Parse.prop -- if_assumes --|
    16.1 --- a/src/Pure/Isar/specification.ML	Sat May 28 23:55:41 2016 +0200
    16.2 +++ b/src/Pure/Isar/specification.ML	Sun May 29 15:40:25 2016 +0200
    16.3 @@ -11,14 +11,14 @@
    16.4      term list * Proof.context
    16.5    val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
    16.6      term * Proof.context
    16.7 -  val check_spec: (binding * typ option * mixfix) list ->
    16.8 -    term list -> Attrib.binding * term -> Proof.context ->
    16.9 -    ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
   16.10 -      * Proof.context
   16.11 -  val read_spec: (binding * string option * mixfix) list ->
   16.12 -    string list -> Attrib.binding * string -> Proof.context ->
   16.13 -    ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
   16.14 -      * Proof.context
   16.15 +  val check_spec_open: (binding * typ option * mixfix) list ->
   16.16 +    (binding * typ option * mixfix) list -> term list -> term -> Proof.context ->
   16.17 +    ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
   16.18 +    Proof.context
   16.19 +  val read_spec_open: (binding * string option * mixfix) list ->
   16.20 +    (binding * string option * mixfix) list -> string list -> string -> Proof.context ->
   16.21 +    ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
   16.22 +    Proof.context
   16.23    type multi_specs = ((Attrib.binding * term) * term list) list
   16.24    type multi_specs_cmd = ((Attrib.binding * string) * string list) list
   16.25    val check_multi_specs: (binding * typ option * mixfix) list -> multi_specs -> Proof.context ->
   16.26 @@ -32,16 +32,19 @@
   16.27      (binding * string option * mixfix) list -> string list ->
   16.28      (Attrib.binding * string) list -> theory -> (term list * thm list) * theory
   16.29    val axiom: Attrib.binding * term -> theory -> thm * theory
   16.30 -  val definition: (binding * typ option * mixfix) option -> term list ->
   16.31 -    Attrib.binding * term -> local_theory -> (term * (string * thm)) * local_theory
   16.32 -  val definition': (binding * typ option * mixfix) option -> term list ->
   16.33 -    Attrib.binding * term -> bool -> local_theory -> (term * (string * thm)) * local_theory
   16.34 -  val definition_cmd: (binding * string option * mixfix) option -> string list ->
   16.35 -    Attrib.binding * string -> bool -> local_theory -> (term * (string * thm)) * local_theory
   16.36 -  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option -> term ->
   16.37 -    bool -> local_theory -> local_theory
   16.38 -  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> string ->
   16.39 -    bool -> local_theory -> local_theory
   16.40 +  val definition: (binding * typ option * mixfix) option ->
   16.41 +    (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
   16.42 +    local_theory -> (term * (string * thm)) * local_theory
   16.43 +  val definition': (binding * typ option * mixfix) option ->
   16.44 +    (binding * typ option * mixfix) list ->  term list -> Attrib.binding * term ->
   16.45 +    bool -> local_theory -> (term * (string * thm)) * local_theory
   16.46 +  val definition_cmd: (binding * string option * mixfix) option ->
   16.47 +    (binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
   16.48 +    bool -> local_theory -> (term * (string * thm)) * local_theory
   16.49 +  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option ->
   16.50 +    (binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory
   16.51 +  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
   16.52 +    (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory
   16.53    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   16.54    val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
   16.55      local_theory -> local_theory
   16.56 @@ -96,14 +99,30 @@
   16.57  
   16.58  local
   16.59  
   16.60 -fun close_form ctxt auto_close prems concl =
   16.61 -  if not auto_close andalso null prems then concl
   16.62 -  else
   16.63 -    let
   16.64 -      val xs =
   16.65 -        if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) [])
   16.66 -        else [];
   16.67 -    in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
   16.68 +fun prep_decls prep_var raw_vars ctxt =
   16.69 +  let
   16.70 +    val (vars, ctxt') = fold_map prep_var raw_vars ctxt;
   16.71 +    val (xs, ctxt'') = ctxt'
   16.72 +      |> Context_Position.set_visible false
   16.73 +      |> Proof_Context.add_fixes vars
   16.74 +      ||> Context_Position.restore_visible ctxt';
   16.75 +    val _ =
   16.76 +      Context_Position.reports ctxt''
   16.77 +        (map (Binding.pos_of o #1) vars ~~
   16.78 +          map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
   16.79 +  in ((vars, xs), ctxt'') end;
   16.80 +
   16.81 +fun close_form ctxt prems concl =
   16.82 +  let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) []);
   16.83 +  in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
   16.84 +
   16.85 +fun dummy_frees ctxt xs tss =
   16.86 +  let
   16.87 +    val names =
   16.88 +      Variable.names_of ((fold o fold) Variable.declare_term tss ctxt)
   16.89 +      |> fold Name.declare xs;
   16.90 +    val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names;
   16.91 +  in tss' end;
   16.92  
   16.93  fun get_positions ctxt x =
   16.94    let
   16.95 @@ -118,60 +137,58 @@
   16.96        | get _ _ = [];
   16.97    in get [] end;
   16.98  
   16.99 -fun prep_specs prep_var parse_prop prep_att auto_close raw_vars raw_specss ctxt =
  16.100 +fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt =
  16.101    let
  16.102 -    val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
  16.103 -    val (xs, params_ctxt) = vars_ctxt
  16.104 -      |> Context_Position.set_visible false
  16.105 -      |> Proof_Context.add_fixes vars
  16.106 -      ||> Context_Position.restore_visible vars_ctxt;
  16.107 -    val _ =
  16.108 -      Context_Position.reports params_ctxt
  16.109 -        (map (Binding.pos_of o #1) vars ~~
  16.110 -          map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
  16.111 +    val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
  16.112 +    val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes;
  16.113 +
  16.114 +    val props =
  16.115 +      map (parse_prop params_ctxt) (raw_concl :: raw_prems)
  16.116 +      |> singleton (dummy_frees params_ctxt (xs @ ys));
  16.117 +
  16.118 +    val concl :: prems = Syntax.check_props params_ctxt props;
  16.119 +    val spec = Logic.list_implies (prems, concl);
  16.120 +    val spec_ctxt = Variable.declare_term spec params_ctxt;
  16.121 +
  16.122 +    fun get_pos x =
  16.123 +      (case maps (get_positions spec_ctxt x) props of
  16.124 +        [] => Position.none
  16.125 +      | pos :: _ => pos);
  16.126 +  in ((vars, xs, get_pos, spec), spec_ctxt) end;
  16.127 +
  16.128 +fun prep_specs prep_var parse_prop prep_att raw_vars raw_specss ctxt =
  16.129 +  let
  16.130 +    val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
  16.131  
  16.132      val propss0 =
  16.133        map (fn ((_, raw_concl), raw_prems) => raw_concl :: raw_prems) raw_specss
  16.134 -      |> burrow (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
  16.135 -    val names =
  16.136 -      Variable.names_of (params_ctxt |> (fold o fold) Variable.declare_term propss0)
  16.137 -      |> fold Name.declare xs;
  16.138 +      |> burrow (grouped 10 Par_List.map_independent (parse_prop vars_ctxt));
  16.139      val props =
  16.140 -      (fold_map o fold_map) Term.free_dummy_patterns propss0 names
  16.141 -      |> fst |> map (fn concl :: prems => close_form params_ctxt auto_close prems concl);
  16.142 +      dummy_frees vars_ctxt xs propss0
  16.143 +      |> map (fn concl :: prems => close_form vars_ctxt prems concl);
  16.144  
  16.145 -    val specs = Syntax.check_props params_ctxt props;
  16.146 -    val specs_ctxt = params_ctxt |> fold Variable.declare_term specs;
  16.147 +    val specs = Syntax.check_props vars_ctxt props;
  16.148 +    val specs_ctxt = vars_ctxt |> fold Variable.declare_term specs;
  16.149  
  16.150      val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
  16.151      val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
  16.152      val name_atts: Attrib.binding list =
  16.153        map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (map #1 raw_specss);
  16.154 -
  16.155 -    fun get_pos x =
  16.156 -      (case maps (get_positions specs_ctxt x) props of
  16.157 -        [] => Position.none
  16.158 -      | pos :: _ => pos);
  16.159 -  in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
  16.160 +  in ((params, name_atts ~~ specs), specs_ctxt) end;
  16.161  
  16.162  in
  16.163  
  16.164 -fun check_spec xs As B =
  16.165 -  prep_specs Proof_Context.cert_var (K I) (K I) false xs [(B, As)] #>
  16.166 -  (apfst o apfst o apsnd) the_single;
  16.167 -
  16.168 -fun read_spec xs As B =
  16.169 -  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src false xs [(B, As)] #>
  16.170 -  (apfst o apfst o apsnd) the_single;
  16.171 +val check_spec_open = prep_spec_open Proof_Context.cert_var (K I);
  16.172 +val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop;
  16.173  
  16.174  type multi_specs = ((Attrib.binding * term) * term list) list;
  16.175  type multi_specs_cmd = ((Attrib.binding * string) * string list) list;
  16.176  
  16.177  fun check_multi_specs xs specs =
  16.178 -  prep_specs Proof_Context.cert_var (K I) (K I) true xs specs #>> #1;
  16.179 +  prep_specs Proof_Context.cert_var (K I) (K I) xs specs;
  16.180  
  16.181  fun read_multi_specs xs specs =
  16.182 -  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs specs #>> #1;
  16.183 +  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src xs specs;
  16.184  
  16.185  end;
  16.186  
  16.187 @@ -219,23 +236,23 @@
  16.188  
  16.189  (* definition *)
  16.190  
  16.191 -fun gen_def prep raw_var raw_prems raw_spec int lthy =
  16.192 +fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy =
  16.193    let
  16.194 -    val ((vars, ((raw_name, atts), prop)), get_pos) =
  16.195 -      fst (prep (the_list raw_var) raw_prems raw_spec lthy);
  16.196 -    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} prop;
  16.197 +    val atts = map (prep_att lthy) raw_atts;
  16.198 +
  16.199 +    val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
  16.200 +      |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
  16.201 +    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} spec;
  16.202      val _ = Name.reject_internal (x, []);
  16.203      val (b, mx) =
  16.204 -      (case vars of
  16.205 -        [] => (Binding.make (x, get_pos x), NoSyn)
  16.206 -      | [((b, _), mx)] =>
  16.207 -          let
  16.208 -            val y = Variable.check_name b;
  16.209 -            val _ = x = y orelse
  16.210 -              error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
  16.211 -                Position.here (Binding.pos_of b));
  16.212 -          in (b, mx) end);
  16.213 -    val name = Thm.def_binding_optional b raw_name;
  16.214 +      (case (vars, xs) of
  16.215 +        ([], []) => (Binding.make (x, get_pos x), NoSyn)
  16.216 +      | ([(b, _, mx)], [y]) =>
  16.217 +          if x = y then (b, mx)
  16.218 +          else
  16.219 +            error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
  16.220 +              Position.here (Binding.pos_of b)));
  16.221 +    val name = Thm.def_binding_optional b a;
  16.222      val ((lhs, (_, raw_th)), lthy2) = lthy
  16.223        |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
  16.224  
  16.225 @@ -252,32 +269,29 @@
  16.226          (member (op =) (Term.add_frees lhs' [])) [(x, T)];
  16.227    in ((lhs, (def_name, th')), lthy4) end;
  16.228  
  16.229 -val definition' = gen_def check_spec;
  16.230 -fun definition xs As B = definition' xs As B false;
  16.231 -val definition_cmd = gen_def read_spec;
  16.232 +val definition' = gen_def check_spec_open (K I);
  16.233 +fun definition xs ys As B = definition' xs ys As B false;
  16.234 +val definition_cmd = gen_def read_spec_open Attrib.check_src;
  16.235  
  16.236  
  16.237  (* abbreviation *)
  16.238  
  16.239 -fun gen_abbrev prep mode raw_var raw_prop int lthy =
  16.240 +fun gen_abbrev prep_spec mode raw_var raw_params raw_spec int lthy =
  16.241    let
  16.242 -    val lthy1 = lthy
  16.243 -      |> Proof_Context.set_syntax_mode mode;
  16.244 -    val (((vars, (_, prop)), get_pos), _) =
  16.245 -      prep (the_list raw_var) [] (Attrib.empty_binding, raw_prop)
  16.246 -        (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
  16.247 -    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
  16.248 +    val lthy1 = lthy |> Proof_Context.set_syntax_mode mode;
  16.249 +    val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
  16.250 +      |> Proof_Context.set_mode Proof_Context.mode_abbrev
  16.251 +      |> prep_spec (the_list raw_var) raw_params [] raw_spec;
  16.252 +    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 spec));
  16.253      val _ = Name.reject_internal (x, []);
  16.254      val (b, mx) =
  16.255 -      (case vars of
  16.256 -        [] => (Binding.make (x, get_pos x), NoSyn)
  16.257 -      | [((b, _), mx)] =>
  16.258 -          let
  16.259 -            val y = Variable.check_name b;
  16.260 -            val _ = x = y orelse
  16.261 -              error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
  16.262 -                Position.here (Binding.pos_of b));
  16.263 -          in (b, mx) end);
  16.264 +      (case (vars, xs) of
  16.265 +        ([], []) => (Binding.make (x, get_pos x), NoSyn)
  16.266 +      | ([(b, _, mx)], [y]) =>
  16.267 +          if x = y then (b, mx)
  16.268 +          else
  16.269 +            error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
  16.270 +              Position.here (Binding.pos_of b)));
  16.271      val lthy2 = lthy1
  16.272        |> Local_Theory.abbrev mode ((b, mx), rhs) |> snd
  16.273        |> Proof_Context.restore_syntax_mode lthy;
  16.274 @@ -285,8 +299,8 @@
  16.275      val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
  16.276    in lthy2 end;
  16.277  
  16.278 -val abbreviation = gen_abbrev check_spec;
  16.279 -val abbreviation_cmd = gen_abbrev read_spec;
  16.280 +val abbreviation = gen_abbrev check_spec_open;
  16.281 +val abbreviation_cmd = gen_abbrev read_spec_open;
  16.282  
  16.283  
  16.284  (* notation *)
    17.1 --- a/src/Pure/Pure.thy	Sat May 28 23:55:41 2016 +0200
    17.2 +++ b/src/Pure/Pure.thy	Sun May 29 15:40:25 2016 +0200
    17.3 @@ -343,13 +343,14 @@
    17.4  
    17.5  val _ =
    17.6    Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
    17.7 -    (Scan.option Parse_Spec.constdecl -- Parse_Spec.spec
    17.8 -      >> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c));
    17.9 +    (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
   17.10 +      Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
   17.11 +        #2 oo Specification.definition_cmd decl params prems spec));
   17.12  
   17.13  val _ =
   17.14    Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   17.15 -    (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   17.16 -      >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
   17.17 +    (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
   17.18 +      >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
   17.19  
   17.20  val axiomatization =
   17.21    Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --