merged
authorwenzelm
Mon May 30 20:58:54 2016 +0200 (2016-05-30)
changeset 63184dd6cd88cebd9
parent 63175 d191892b1c23
parent 63183 4d04e14d7ab8
child 63185 08369e33c185
merged
NEWS
src/Tools/Code/code_runtime.ML
     1.1 --- a/NEWS	Sun May 29 14:43:18 2016 +0200
     1.2 +++ b/NEWS	Mon May 30 20:58:54 2016 +0200
     1.3 @@ -66,9 +66,13 @@
     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 +* Command 'axiomatization' has become more restrictive to correspond
    1.11 +better to internal axioms as singleton facts with mandatory name. Minor
    1.12 +INCOMPATIBILITY.
    1.13 +
    1.14 +* Many specification elements support structured statements with 'if' /
    1.15 +'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
    1.16 +'definition', 'inductive', 'function'.
    1.17  
    1.18  * Toplevel theorem statements support eigen-context notation with 'if' /
    1.19  'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
     2.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun May 29 14:43:18 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon May 30 20:58:54 2016 +0200
     2.3 @@ -109,9 +109,7 @@
     2.4      (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
     2.5        @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
     2.6        @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
     2.7 -      (@'where' clauses)? (@'monos' @{syntax thms})?
     2.8 -    ;
     2.9 -    clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
    2.10 +      (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
    2.11      ;
    2.12      @@{command print_inductives} ('!'?)
    2.13      ;
    2.14 @@ -266,15 +264,11 @@
    2.15    \end{matharray}
    2.16  
    2.17    @{rail \<open>
    2.18 -    @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations
    2.19 -    ;
    2.20 -    (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?
    2.21 -      @{syntax "fixes"} \<newline> @'where' equations
    2.22 +    @@{command (HOL) primrec} @{syntax specification}
    2.23      ;
    2.24 -
    2.25 -    equations: (@{syntax thmdecl}? @{syntax prop} + '|')
    2.26 +    (@@{command (HOL) fun} | @@{command (HOL) function}) opts? @{syntax specification}
    2.27      ;
    2.28 -    functionopts: '(' (('sequential' | 'domintros') + ',') ')'
    2.29 +    opts: '(' (('sequential' | 'domintros') + ',') ')'
    2.30      ;
    2.31      @@{command (HOL) termination} @{syntax term}?
    2.32      ;
    2.33 @@ -568,8 +562,8 @@
    2.34    \end{matharray}
    2.35  
    2.36    @{rail \<open>
    2.37 -    @@{command (HOL) partial_function} '(' @{syntax name} ')' @{syntax "fixes"} \<newline>
    2.38 -      @'where' @{syntax thmdecl}? @{syntax prop}
    2.39 +    @@{command (HOL) partial_function} '(' @{syntax name} ')'
    2.40 +      @{syntax specification}
    2.41    \<close>}
    2.42  
    2.43    \<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines
     3.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun May 29 14:43:18 2016 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon May 30 20:58:54 2016 +0200
     3.3 @@ -450,6 +450,31 @@
     3.4  \<close>
     3.5  
     3.6  
     3.7 +subsection \<open>Structured specifications\<close>
     3.8 +
     3.9 +text \<open>
    3.10 +  Structured specifications use propositions with explicit notation for the
    3.11 +  ``eigen-context'' to describe rule structure: \<open>\<And>x. A x \<Longrightarrow> \<dots> \<Longrightarrow> B x\<close> is
    3.12 +  expressed as \<^theory_text>\<open>B x if A x and \<dots> for x\<close>. It is also possible to use dummy
    3.13 +  terms ``\<open>_\<close>'' (underscore) to refer to locally fixed variables anonymously.
    3.14 +
    3.15 +  Multiple specifications are delimited by ``\<open>|\<close>'' to emphasize separate
    3.16 +  cases: each with its own scope of inferred types for free variables.
    3.17 +
    3.18 +
    3.19 +  @{rail \<open>
    3.20 +    @{syntax_def multi_specs}: (@{syntax structured_spec} + '|')
    3.21 +    ;
    3.22 +    @{syntax_def structured_spec}:
    3.23 +      @{syntax thmdecl}? @{syntax prop} @{syntax spec_prems} @{syntax for_fixes}
    3.24 +    ;
    3.25 +    @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))?
    3.26 +    ;
    3.27 +    @{syntax_def specification}: @{syntax "fixes"} @'where' @{syntax multi_specs}
    3.28 +  \<close>}
    3.29 +\<close>
    3.30 +
    3.31 +
    3.32  section \<open>Diagnostic commands\<close>
    3.33  
    3.34  text \<open>
     4.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sun May 29 14:43:18 2016 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon May 30 20:58:54 2016 +0200
     4.3 @@ -285,14 +285,18 @@
     4.4    ``abbreviation''.
     4.5  
     4.6    @{rail \<open>
     4.7 -    @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
     4.8 +    @@{command definition} decl? definition
     4.9      ;
    4.10 -    @@{command abbreviation} @{syntax mode}? \<newline>
    4.11 -      (decl @'where')? @{syntax prop}
    4.12 -    ;
    4.13 -    decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
    4.14 +    @@{command abbreviation} @{syntax mode}? decl? abbreviation
    4.15      ;
    4.16      @@{command print_abbrevs} ('!'?)
    4.17 +    ;
    4.18 +    decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
    4.19 +    ;
    4.20 +    definition: @{syntax thmdecl}? @{syntax prop}
    4.21 +      @{syntax spec_prems} @{syntax for_fixes}
    4.22 +    ;
    4.23 +    abbreviation: @{syntax prop} @{syntax for_fixes}
    4.24    \<close>}
    4.25  
    4.26    \<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according
    4.27 @@ -337,9 +341,10 @@
    4.28    \end{matharray}
    4.29  
    4.30    @{rail \<open>
    4.31 -    @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
    4.32 +    @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
    4.33      ;
    4.34 -    specs: (@{syntax thmdecl}? @{syntax props} + @'and')
    4.35 +    axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
    4.36 +      @{syntax spec_prems} @{syntax for_fixes}
    4.37    \<close>}
    4.38  
    4.39    \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
     5.1 --- a/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sun May 29 14:43:18 2016 +0200
     5.2 +++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy	Mon May 30 20:58:54 2016 +0200
     5.3 @@ -133,7 +133,7 @@
     5.4  *}
     5.5  
     5.6  axiomatization f :: "nat \<Rightarrow> nat"
     5.7 -  where f_ax: "f(f(n)) < f(Suc(n))"
     5.8 +  where f_ax: "f(f(n)) < f(Suc(n))" for n :: nat
     5.9  
    5.10  text{*
    5.11  \begin{warn}
     6.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Sun May 29 14:43:18 2016 +0200
     6.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon May 30 20:58:54 2016 +0200
     6.3 @@ -175,7 +175,7 @@
     6.4        Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))
     6.5      val ((_, (_, below_ldef)), lthy) = thy
     6.6        |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
     6.7 -      |> Specification.definition NONE []
     6.8 +      |> Specification.definition NONE [] []
     6.9            ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)
    6.10      val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
    6.11      val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
     7.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun May 29 14:43:18 2016 +0200
     7.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Mon May 30 20:58:54 2016 +0200
     7.3 @@ -138,17 +138,17 @@
     7.4      val lthy = thy
     7.5        |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
     7.6      val ((_, (_, emb_ldef)), lthy) =
     7.7 -        Specification.definition NONE [] (emb_bind, emb_eqn) lthy
     7.8 +        Specification.definition NONE [] [] (emb_bind, emb_eqn) lthy
     7.9      val ((_, (_, prj_ldef)), lthy) =
    7.10 -        Specification.definition NONE [] (prj_bind, prj_eqn) lthy
    7.11 +        Specification.definition NONE [] [] (prj_bind, prj_eqn) lthy
    7.12      val ((_, (_, defl_ldef)), lthy) =
    7.13 -        Specification.definition NONE [] (defl_bind, defl_eqn) lthy
    7.14 +        Specification.definition NONE [] [] (defl_bind, defl_eqn) lthy
    7.15      val ((_, (_, liftemb_ldef)), lthy) =
    7.16 -        Specification.definition NONE [] (liftemb_bind, liftemb_eqn) lthy
    7.17 +        Specification.definition NONE [] [] (liftemb_bind, liftemb_eqn) lthy
    7.18      val ((_, (_, liftprj_ldef)), lthy) =
    7.19 -        Specification.definition NONE [] (liftprj_bind, liftprj_eqn) lthy
    7.20 +        Specification.definition NONE [] [] (liftprj_bind, liftprj_eqn) lthy
    7.21      val ((_, (_, liftdefl_ldef)), lthy) =
    7.22 -        Specification.definition NONE [] (liftdefl_bind, liftdefl_eqn) lthy
    7.23 +        Specification.definition NONE [] [] (liftdefl_bind, liftdefl_eqn) lthy
    7.24      val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
    7.25      val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef
    7.26      val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef
     8.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun May 29 14:43:18 2016 +0200
     8.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon May 30 20:58:54 2016 +0200
     8.3 @@ -334,7 +334,7 @@
     8.4      val (skips, raw_spec) = ListPair.unzip raw_spec'
     8.5      val (fixes : ((binding * typ) * mixfix) list,
     8.6           spec : (Attrib.binding * term) list) =
     8.7 -          fst (prep_spec raw_fixes (map (rpair []) raw_spec) lthy)
     8.8 +          fst (prep_spec raw_fixes (map (fn s => (s, [], [])) raw_spec) lthy)
     8.9      val names = map (Binding.name_of o fst o fst) fixes
    8.10      fun check_head name =
    8.11          member (op =) names name orelse
     9.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Sun May 29 14:43:18 2016 +0200
     9.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Mon May 30 20:58:54 2016 +0200
     9.3 @@ -15,12 +15,29 @@
     9.4    append_name :: mname
     9.5  
     9.6  axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam
     9.7 -where distinct_fields: "val_name \<noteq> next_name"
     9.8 -  and distinct_vars:
     9.9 -  "l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam"
    9.10 -  "l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam"
    9.11 -  "l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam"
    9.12 -  "l3_nam \<noteq> l4_nam"
    9.13 +where distinct_fields: "val_nam \<noteq> next_nam"
    9.14 +  and distinct_vars1: "l_nam \<noteq> l1_nam"
    9.15 +  and distinct_vars2: "l_nam \<noteq> l2_nam"
    9.16 +  and distinct_vars3: "l_nam \<noteq> l3_nam"
    9.17 +  and distinct_vars4: "l_nam \<noteq> l4_nam"
    9.18 +  and distinct_vars5: "l1_nam \<noteq> l2_nam"
    9.19 +  and distinct_vars6: "l1_nam \<noteq> l3_nam"
    9.20 +  and distinct_vars7: "l1_nam \<noteq> l4_nam"
    9.21 +  and distinct_vars8: "l2_nam \<noteq> l3_nam"
    9.22 +  and distinct_vars9: "l2_nam \<noteq> l4_nam"
    9.23 +  and distinct_vars10: "l3_nam \<noteq> l4_nam"
    9.24 +
    9.25 +lemmas distinct_vars =
    9.26 +  distinct_vars1
    9.27 +  distinct_vars2
    9.28 +  distinct_vars3
    9.29 +  distinct_vars4
    9.30 +  distinct_vars5
    9.31 +  distinct_vars6
    9.32 +  distinct_vars7
    9.33 +  distinct_vars8
    9.34 +  distinct_vars9
    9.35 +  distinct_vars10
    9.36  
    9.37  definition list_name :: cname where
    9.38    "list_name = Cname list_nam"
    10.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sun May 29 14:43:18 2016 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 30 20:58:54 2016 +0200
    10.3 @@ -192,7 +192,7 @@
    10.4          thy' |>
    10.5          BNF_LFP_Compat.primrec_global
    10.6            [(Binding.name swap_name, SOME swapT, NoSyn)]
    10.7 -          [((Attrib.empty_binding, def1), [])] ||>
    10.8 +          [((Attrib.empty_binding, def1), [], [])] ||>
    10.9          Sign.parent_path ||>>
   10.10          Global_Theory.add_defs_unchecked true
   10.11            [((Binding.name name, def2), [])] |>> (snd o fst)
   10.12 @@ -226,7 +226,7 @@
   10.13          thy' |>
   10.14          BNF_LFP_Compat.primrec_global
   10.15            [(Binding.name prm_name, SOME prmT, NoSyn)]
   10.16 -          (map (fn def => ((Attrib.empty_binding, def), [])) [def1, def2]) ||>
   10.17 +          (map (fn def => ((Attrib.empty_binding, def), [], [])) [def1, def2]) ||>
   10.18          Sign.parent_path
   10.19        end) ak_names_types thy3;
   10.20      
    11.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun May 29 14:43:18 2016 +0200
    11.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon May 30 20:58:54 2016 +0200
    11.3 @@ -255,7 +255,7 @@
    11.4              (Free (nth perm_names_types' i) $
    11.5                 Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
    11.6                 list_comb (c, args),
    11.7 -             list_comb (c, map perm_arg (dts ~~ args))))), [])
    11.8 +             list_comb (c, map perm_arg (dts ~~ args))))), [], [])
    11.9          end) constrs
   11.10        end) descr;
   11.11  
    12.1 --- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sun May 29 14:43:18 2016 +0200
    12.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon May 30 20:58:54 2016 +0200
    12.3 @@ -109,9 +109,17 @@
    12.4  
    12.5  axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
    12.6      => 'b list => 'a Quickcheck_Exhaustive.three_valued"
    12.7 -where find_first'_code [code]:
    12.8 -  "find_first' f [] = Quickcheck_Exhaustive.No_value"
    12.9 -  "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
   12.10 +where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
   12.11 +  and find_first'_Cons: "find_first' f (x # xs) =
   12.12 +    (case f (Quickcheck_Exhaustive.Known x) of
   12.13 +      Quickcheck_Exhaustive.No_value => find_first' f xs
   12.14 +    | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x
   12.15 +    | Quickcheck_Exhaustive.Unknown_value =>
   12.16 +        (case find_first' f xs of Quickcheck_Exhaustive.Value x =>
   12.17 +          Quickcheck_Exhaustive.Value x
   12.18 +        | _ => Quickcheck_Exhaustive.Unknown_value))"
   12.19 +
   12.20 +lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons
   12.21  
   12.22  axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
   12.23  where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
    13.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sun May 29 14:43:18 2016 +0200
    13.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon May 30 20:58:54 2016 +0200
    13.3 @@ -1020,7 +1020,7 @@
    13.4              "\ndoes not match type " ^ ty' ^ " in definition");
    13.5          val id' = mk_rulename id;
    13.6          val ((t', (_, th)), lthy') = Named_Target.theory_init thy
    13.7 -          |> Specification.definition NONE []
    13.8 +          |> Specification.definition NONE [] []
    13.9              ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
   13.10          val phi =
   13.11            Proof_Context.export_morphism lthy'
    14.1 --- a/src/HOL/Tools/BNF/bnf_axiomatization.ML	Sun May 29 14:43:18 2016 +0200
    14.2 +++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML	Mon May 30 20:58:54 2016 +0200
    14.3 @@ -81,8 +81,10 @@
    14.4      val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    14.5      val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
    14.6  
    14.7 -    val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
    14.8 -      (Specification.axiomatization [] [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
    14.9 +    val (((_, raw_thms)), lthy) = Local_Theory.background_theory_result
   14.10 +      (Specification.axiomatization [] [] []
   14.11 +        (map_index (fn (i, ax) =>
   14.12 +          ((mk_b ("axiom" ^ string_of_int (i + 1)) Binding.empty, []), ax)) (flat all_goalss))) lthy;
   14.13  
   14.14      fun mk_wit_thms set_maps =
   14.15        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
    15.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Sun May 29 14:43:18 2016 +0200
    15.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon May 30 20:58:54 2016 +0200
    15.3 @@ -265,7 +265,7 @@
    15.4      val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
    15.5        |> Local_Theory.open_target |> snd
    15.6        |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
    15.7 -      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [])) eqs)
    15.8 +      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [], [])) eqs)
    15.9        ||> `Local_Theory.close_target;
   15.10  
   15.11      val phi = Proof_Context.export_morphism lthy_old lthy;
    16.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sun May 29 14:43:18 2016 +0200
    16.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon May 30 20:58:54 2016 +0200
    16.3 @@ -1829,7 +1829,7 @@
    16.4  
    16.5      val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
    16.6        Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
    16.7 -        [(((Binding.concealed Binding.empty, []), parsed_eq), [])]
    16.8 +        [(((Binding.concealed Binding.empty, []), parsed_eq), [], [])]
    16.9          Function_Common.default_config pat_completeness_auto lthy;
   16.10    in
   16.11      ((defname, (pelim, pinduct, psimp)), lthy)
   16.12 @@ -1982,7 +1982,7 @@
   16.13  
   16.14      val (plugins, friend, transfer) = get_options lthy opts;
   16.15      val ([((b, fun_T), mx)], [(_, eq)]) =
   16.16 -      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [])] lthy);
   16.17 +      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [], [])] lthy);
   16.18  
   16.19      val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
   16.20        error ("Type of " ^ Binding.print b ^ " contains top sort");
    17.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun May 29 14:43:18 2016 +0200
    17.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon May 30 20:58:54 2016 +0200
    17.3 @@ -1588,7 +1588,7 @@
    17.4      val (raw_specs, of_specs_opt) =
    17.5        split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
    17.6      val (fixes, specs) =
    17.7 -      fst (Specification.read_multi_specs raw_fixes (map (rpair []) raw_specs) lthy);
    17.8 +      fst (Specification.read_multi_specs raw_fixes (map (fn spec => (spec, [], [])) raw_specs) lthy);
    17.9    in
   17.10      primcorec_ursive auto opts fixes specs of_specs_opt lthy
   17.11    end;
    18.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun May 29 14:43:18 2016 +0200
    18.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon May 30 20:58:54 2016 +0200
    18.3 @@ -687,8 +687,7 @@
    18.4  val _ = Outer_Syntax.local_theory @{command_keyword primrec}
    18.5    "define primitive recursive functions"
    18.6    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
    18.7 -      --| @{keyword ")"}) []) --
    18.8 -    (Parse.fixes -- Parse_Spec.where_multi_specs)
    18.9 +      --| @{keyword ")"}) []) -- Parse_Spec.specification
   18.10      >> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
   18.11  
   18.12  end;
    19.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 29 14:43:18 2016 +0200
    19.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 30 20:58:54 2016 +0200
    19.3 @@ -623,11 +623,11 @@
    19.4                  else if Binding.eq_name (b, equal_binding) then
    19.5                    pair (Term.lambda u exist_xs_u_eq_ctr, refl)
    19.6                  else
    19.7 -                  Specification.definition (SOME (b, NONE, NoSyn)) []
    19.8 +                  Specification.definition (SOME (b, NONE, NoSyn)) [] []
    19.9                      ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd)
   19.10                ks exist_xs_u_eq_ctrs disc_bindings
   19.11              ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
   19.12 -              Specification.definition (SOME (b, NONE, NoSyn)) []
   19.13 +              Specification.definition (SOME (b, NONE, NoSyn)) [] []
   19.14                  ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos
   19.15              ||> `Local_Theory.close_target;
   19.16  
    20.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sun May 29 14:43:18 2016 +0200
    20.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon May 30 20:58:54 2016 +0200
    20.3 @@ -93,7 +93,7 @@
    20.4            mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
    20.5            |> Syntax.check_term lthy;
    20.6          val ((_, (_, raw_def)), lthy') =
    20.7 -          Specification.definition NONE [] (Attrib.empty_binding, spec) lthy;
    20.8 +          Specification.definition NONE [] [] (Attrib.empty_binding, spec) lthy;
    20.9          val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
   20.10          val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
   20.11        in
    21.1 --- a/src/HOL/Tools/Function/fun.ML	Sun May 29 14:43:18 2016 +0200
    21.2 +++ b/src/HOL/Tools/Function/fun.ML	Mon May 30 20:58:54 2016 +0200
    21.3 @@ -174,6 +174,6 @@
    21.4    Outer_Syntax.local_theory' @{command_keyword fun}
    21.5      "define general recursive functions (short version)"
    21.6      (function_parser fun_config
    21.7 -      >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
    21.8 +      >> (fn (config, (fixes, specs)) => add_fun_cmd fixes specs config))
    21.9  
   21.10  end
    22.1 --- a/src/HOL/Tools/Function/function.ML	Sun May 29 14:43:18 2016 +0200
    22.2 +++ b/src/HOL/Tools/Function/function.ML	Mon May 30 20:58:54 2016 +0200
    22.3 @@ -274,7 +274,7 @@
    22.4    Outer_Syntax.local_theory_to_proof' @{command_keyword function}
    22.5      "define general recursive functions"
    22.6      (function_parser default_config
    22.7 -      >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
    22.8 +      >> (fn (config, (fixes, specs)) => function_cmd fixes specs config))
    22.9  
   22.10  val _ =
   22.11    Outer_Syntax.local_theory_to_proof @{command_keyword termination}
    23.1 --- a/src/HOL/Tools/Function/function_common.ML	Sun May 29 14:43:18 2016 +0200
    23.2 +++ b/src/HOL/Tools/Function/function_common.ML	Mon May 30 20:58:54 2016 +0200
    23.3 @@ -99,8 +99,7 @@
    23.4    val import_last_function : Proof.context -> info option
    23.5    val default_config : function_config
    23.6    val function_parser : function_config ->
    23.7 -    ((function_config * (binding * string option * mixfix) list) *
    23.8 -      Specification.multi_specs_cmd) parser
    23.9 +    (function_config * ((binding * string option * mixfix) list * Specification.multi_specs_cmd)) parser
   23.10  end
   23.11  
   23.12  structure Function_Common : FUNCTION_COMMON =
   23.13 @@ -374,7 +373,7 @@
   23.14       >> (fn opts => fold apply_opt opts default)
   23.15  in
   23.16    fun function_parser default_cfg =
   23.17 -      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_multi_specs
   23.18 +      config_parser default_cfg -- Parse_Spec.specification
   23.19  end
   23.20  
   23.21  
    24.1 --- a/src/HOL/Tools/Function/partial_function.ML	Sun May 29 14:43:18 2016 +0200
    24.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 30 20:58:54 2016 +0200
    24.3 @@ -226,7 +226,7 @@
    24.4          "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
    24.5      val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
    24.6  
    24.7 -    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [])] lthy;
    24.8 +    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [], [])] lthy;
    24.9      val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
   24.10  
   24.11      val ((f_binding, fT), mixfix) = the_single fixes;
    25.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 29 14:43:18 2016 +0200
    25.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon May 30 20:58:54 2016 +0200
    25.3 @@ -89,7 +89,7 @@
    25.4      val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
    25.5      val definition_term = Logic.mk_equals (lhs, rhs)
    25.6      fun note_def lthy =
    25.7 -      Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) []
    25.8 +      Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
    25.9          ((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
   25.10      fun raw_def lthy =
   25.11        let
    26.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun May 29 14:43:18 2016 +0200
    26.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 20:58:54 2016 +0200
    26.3 @@ -56,7 +56,7 @@
    26.4      thy
    26.5      |> Class.instantiation ([tyco], vs, @{sort partial_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/Quickcheck/quickcheck_common.ML	Sun May 29 14:43:18 2016 +0200
    27.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon May 30 20:58:54 2016 +0200
    27.3 @@ -365,7 +365,7 @@
    27.4        Function.add_function
    27.5          (map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
    27.6            (names ~~ Ts))
    27.7 -        (map (fn t => (((Binding.concealed Binding.empty, []), t), [])) eqs_t)
    27.8 +        (map (fn t => (((Binding.concealed Binding.empty, []), t), [], [])) eqs_t)
    27.9          Function_Common.default_config pat_completeness_auto
   27.10        #> snd
   27.11        #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
    28.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun May 29 14:43:18 2016 +0200
    28.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon May 30 20:58:54 2016 +0200
    28.3 @@ -266,7 +266,7 @@
    28.4      |> random_aux_specification prfx random_auxN auxs_eqs
    28.5      |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
    28.6      |-> (fn random_defs' => fold_map (fn random_def =>
    28.7 -          Specification.definition NONE []
    28.8 +          Specification.definition NONE [] []
    28.9              ((Binding.concealed Binding.empty, []), random_def)) random_defs')
   28.10      |> snd
   28.11      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
    29.1 --- a/src/HOL/Tools/code_evaluation.ML	Sun May 29 14:43:18 2016 +0200
    29.2 +++ b/src/HOL/Tools/code_evaluation.ML	Mon May 30 20:58:54 2016 +0200
    29.3 @@ -43,7 +43,7 @@
    29.4      thy
    29.5      |> Class.instantiation ([tyco], vs, @{sort term_of})
    29.6      |> `(fn lthy => Syntax.check_term lthy eq)
    29.7 -    |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
    29.8 +    |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
    29.9      |> snd
   29.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   29.11    end;
    30.1 --- a/src/HOL/Tools/inductive.ML	Sun May 29 14:43:18 2016 +0200
    30.2 +++ b/src/HOL/Tools/inductive.ML	Mon May 30 20:58:54 2016 +0200
    30.3 @@ -610,7 +610,7 @@
    30.4  
    30.5  fun ind_cases_rules ctxt raw_props raw_fixes =
    30.6    let
    30.7 -    val (props, ctxt' ) = Specification.read_props raw_props raw_fixes ctxt;
    30.8 +    val (props, ctxt') = Specification.read_props raw_props raw_fixes ctxt;
    30.9      val rules = Proof_Context.export ctxt' ctxt (map (mk_cases ctxt') props);
   30.10    in rules end;
   30.11  
    31.1 --- a/src/HOL/Tools/record.ML	Sun May 29 14:43:18 2016 +0200
    31.2 +++ b/src/HOL/Tools/record.ML	Mon May 30 20:58:54 2016 +0200
    31.3 @@ -1734,7 +1734,7 @@
    31.4      thy
    31.5      |> Class.instantiation ([tyco], vs, sort)
    31.6      |> `(fn lthy => Syntax.check_term lthy eq)
    31.7 -    |-> (fn eq => Specification.definition NONE [] ((Binding.concealed Binding.empty, []), eq))
    31.8 +    |-> (fn eq => Specification.definition NONE [] [] ((Binding.concealed Binding.empty, []), eq))
    31.9      |> snd
   31.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   31.11    end;
   31.12 @@ -1781,7 +1781,7 @@
   31.13        |> fold Code.add_default_eqn simps
   31.14        |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
   31.15        |> `(fn lthy => Syntax.check_term lthy eq)
   31.16 -      |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
   31.17 +      |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
   31.18        |-> (fn (_, (_, eq_def)) =>
   31.19           Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
   31.20        |-> (fn eq_def => fn thy =>
    32.1 --- a/src/HOL/Typerep.thy	Sun May 29 14:43:18 2016 +0200
    32.2 +++ b/src/HOL/Typerep.thy	Mon May 30 20:58:54 2016 +0200
    32.3 @@ -58,7 +58,7 @@
    32.4      thy
    32.5      |> Class.instantiation ([tyco], vs, @{sort typerep})
    32.6      |> `(fn lthy => Syntax.check_term lthy eq)
    32.7 -    |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
    32.8 +    |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
    32.9      |> snd
   32.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   32.11    end;
    33.1 --- a/src/Pure/Isar/parse_spec.ML	Sun May 29 14:43:18 2016 +0200
    33.2 +++ b/src/Pure/Isar/parse_spec.ML	Mon May 30 20:58:54 2016 +0200
    33.3 @@ -12,10 +12,10 @@
    33.4    val simple_spec: (Attrib.binding * string) parser
    33.5    val simple_specs: (Attrib.binding * string list) parser
    33.6    val if_assumes: string list parser
    33.7 -  val spec: (string list * (Attrib.binding * string)) parser
    33.8    val multi_specs: Specification.multi_specs_cmd parser
    33.9    val where_multi_specs: Specification.multi_specs_cmd parser
   33.10 -  val specification: (string list * (Attrib.binding * string list) list) parser
   33.11 +  val specification:
   33.12 +    ((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser
   33.13    val constdecl: (binding * string option * mixfix) parser
   33.14    val includes: (xstring * Position.T) list parser
   33.15    val locale_fixes: (binding * string option * mixfix) list parser
   33.16 @@ -60,17 +60,14 @@
   33.17    Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat))
   33.18      [];
   33.19  
   33.20 -val spec = (opt_thm_name ":" -- Parse.prop) -- if_assumes >> swap;
   33.21 -
   33.22  val multi_specs =
   33.23    Parse.enum1 "|"
   33.24 -    (opt_thm_name ":" -- Parse.prop -- if_assumes --|
   33.25 +    ((opt_thm_name ":" -- Parse.prop -- if_assumes -- Parse.for_fixes >> Scan.triple1) --|
   33.26        Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
   33.27  
   33.28  val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
   33.29  
   33.30 -val specification =
   33.31 -  Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.prop) -- if_assumes >> swap;
   33.32 +val specification = Parse.fixes -- where_multi_specs;
   33.33  
   33.34  
   33.35  (* basic constant specifications *)
    34.1 --- a/src/Pure/Isar/specification.ML	Sun May 29 14:43:18 2016 +0200
    34.2 +++ b/src/Pure/Isar/specification.ML	Mon May 30 20:58:54 2016 +0200
    34.3 @@ -9,43 +9,42 @@
    34.4  sig
    34.5    val read_props: string list -> (binding * string option * mixfix) list -> Proof.context ->
    34.6      term list * Proof.context
    34.7 -  val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
    34.8 -    term * Proof.context
    34.9 -  val check_spec: (binding * typ option * mixfix) list ->
   34.10 -    term list -> Attrib.binding * term -> Proof.context ->
   34.11 -    ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
   34.12 -      * Proof.context
   34.13 -  val read_spec: (binding * string option * mixfix) list ->
   34.14 -    string list -> Attrib.binding * string -> Proof.context ->
   34.15 -    ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
   34.16 -      * Proof.context
   34.17 -  type multi_specs = ((Attrib.binding * term) * term list) list
   34.18 -  type multi_specs_cmd = ((Attrib.binding * string) * string list) list
   34.19 +  val check_spec_open: (binding * typ option * mixfix) list ->
   34.20 +    (binding * typ option * mixfix) list -> term list -> term -> Proof.context ->
   34.21 +    ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
   34.22 +    Proof.context
   34.23 +  val read_spec_open: (binding * string option * mixfix) list ->
   34.24 +    (binding * string option * mixfix) list -> string list -> string -> Proof.context ->
   34.25 +    ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
   34.26 +    Proof.context
   34.27 +  type multi_specs =
   34.28 +    ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list
   34.29 +  type multi_specs_cmd =
   34.30 +    ((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list
   34.31    val check_multi_specs: (binding * typ option * mixfix) list -> multi_specs -> Proof.context ->
   34.32      (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   34.33    val read_multi_specs: (binding * string option * mixfix) list -> multi_specs_cmd -> Proof.context ->
   34.34      (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   34.35 -  val check_specification: (binding * typ option * mixfix) list -> term list ->
   34.36 -    (Attrib.binding * term list) list -> Proof.context ->
   34.37 -    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   34.38 -  val read_specification: (binding * string option * mixfix) list -> string list ->
   34.39 -    (Attrib.binding * string list) list -> Proof.context ->
   34.40 -    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   34.41 -  val axiomatization: (binding * typ option * mixfix) list -> term list ->
   34.42 -    (Attrib.binding * term list) list -> theory -> (term list * thm list list) * theory
   34.43 -  val axiomatization_cmd: (binding * string option * mixfix) list -> string list ->
   34.44 -    (Attrib.binding * string list) list -> theory -> (term list * thm list list) * theory
   34.45 +  val axiomatization: (binding * typ option * mixfix) list ->
   34.46 +    (binding * typ option * mixfix) list -> term list ->
   34.47 +    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
   34.48 +  val axiomatization_cmd: (binding * string option * mixfix) list ->
   34.49 +    (binding * string option * mixfix) list -> string list ->
   34.50 +    (Attrib.binding * string) list -> theory -> (term list * thm list) * theory
   34.51    val axiom: Attrib.binding * term -> theory -> thm * theory
   34.52 -  val definition: (binding * typ option * mixfix) option -> term list ->
   34.53 -    Attrib.binding * term -> local_theory -> (term * (string * thm)) * local_theory
   34.54 -  val definition': (binding * typ option * mixfix) option -> term list ->
   34.55 -    Attrib.binding * term -> bool -> local_theory -> (term * (string * thm)) * local_theory
   34.56 -  val definition_cmd: (binding * string option * mixfix) option -> string list ->
   34.57 -    Attrib.binding * string -> bool -> local_theory -> (term * (string * thm)) * local_theory
   34.58 -  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option -> term ->
   34.59 -    bool -> local_theory -> local_theory
   34.60 -  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> string ->
   34.61 -    bool -> local_theory -> local_theory
   34.62 +  val definition: (binding * typ option * mixfix) option ->
   34.63 +    (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
   34.64 +    local_theory -> (term * (string * thm)) * local_theory
   34.65 +  val definition': (binding * typ option * mixfix) option ->
   34.66 +    (binding * typ option * mixfix) list ->  term list -> Attrib.binding * term ->
   34.67 +    bool -> local_theory -> (term * (string * thm)) * local_theory
   34.68 +  val definition_cmd: (binding * string option * mixfix) option ->
   34.69 +    (binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
   34.70 +    bool -> local_theory -> (term * (string * thm)) * local_theory
   34.71 +  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option ->
   34.72 +    (binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory
   34.73 +  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
   34.74 +    (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory
   34.75    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   34.76    val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
   34.77      local_theory -> local_theory
   34.78 @@ -91,26 +90,35 @@
   34.79      val ctxt3 = ctxt2 |> fold Variable.declare_term props3;
   34.80    in (props3, ctxt3) end;
   34.81  
   34.82 -fun read_prop raw_prop raw_fixes ctxt =
   34.83 -  let val ([prop], ctxt') = read_props [raw_prop] raw_fixes ctxt
   34.84 -  in (prop, ctxt') end;
   34.85 -
   34.86  
   34.87  (* prepare specification *)
   34.88  
   34.89  local
   34.90  
   34.91 -fun close_forms ctxt auto_close i prems concls =
   34.92 -  if not auto_close andalso null prems then concls
   34.93 -  else
   34.94 -    let
   34.95 -      val xs =
   34.96 -        if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) [])
   34.97 -        else [];
   34.98 -      val types =
   34.99 -        map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
  34.100 -      val uniform_typing = AList.lookup (op =) (xs ~~ types);
  34.101 -    in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
  34.102 +fun prep_decls prep_var raw_vars ctxt =
  34.103 +  let
  34.104 +    val (vars, ctxt') = fold_map prep_var raw_vars ctxt;
  34.105 +    val (xs, ctxt'') = ctxt'
  34.106 +      |> Context_Position.set_visible false
  34.107 +      |> Proof_Context.add_fixes vars
  34.108 +      ||> Context_Position.restore_visible ctxt';
  34.109 +    val _ =
  34.110 +      Context_Position.reports ctxt''
  34.111 +        (map (Binding.pos_of o #1) vars ~~
  34.112 +          map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
  34.113 +  in ((vars, xs), ctxt'') end;
  34.114 +
  34.115 +fun close_form ctxt ys prems concl =
  34.116 +  let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys));
  34.117 +  in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
  34.118 +
  34.119 +fun dummy_frees ctxt xs tss =
  34.120 +  let
  34.121 +    val names =
  34.122 +      Variable.names_of ((fold o fold) Variable.declare_term tss ctxt)
  34.123 +      |> fold Name.declare xs;
  34.124 +    val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names;
  34.125 +  in tss' end;
  34.126  
  34.127  fun get_positions ctxt x =
  34.128    let
  34.129 @@ -125,99 +133,92 @@
  34.130        | get _ _ = [];
  34.131    in get [] end;
  34.132  
  34.133 -fun prepare prep_var parse_prop prep_att auto_close raw_vars raw_specss ctxt =
  34.134 +fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt =
  34.135    let
  34.136 -    val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
  34.137 -    val (xs, params_ctxt) = vars_ctxt
  34.138 -      |> Context_Position.set_visible false
  34.139 -      |> Proof_Context.add_fixes vars
  34.140 -      ||> Context_Position.restore_visible vars_ctxt;
  34.141 -    val _ =
  34.142 -      Context_Position.reports params_ctxt
  34.143 -        (map (Binding.pos_of o #1) vars ~~
  34.144 -          map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
  34.145 +    val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
  34.146 +    val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes;
  34.147 +
  34.148 +    val props =
  34.149 +      map (parse_prop params_ctxt) (raw_concl :: raw_prems)
  34.150 +      |> singleton (dummy_frees params_ctxt (xs @ ys));
  34.151 +
  34.152 +    val concl :: prems = Syntax.check_props params_ctxt props;
  34.153 +    val spec = Logic.list_implies (prems, concl);
  34.154 +    val spec_ctxt = Variable.declare_term spec params_ctxt;
  34.155  
  34.156 -    val Asss0 =
  34.157 -      map (fn (raw_concls, raw_prems) => raw_prems :: map snd raw_concls) raw_specss
  34.158 -      |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
  34.159 -    val names =
  34.160 -      Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss0)
  34.161 -      |> fold Name.declare xs;
  34.162 +    fun get_pos x =
  34.163 +      (case maps (get_positions spec_ctxt x) props of
  34.164 +        [] => Position.none
  34.165 +      | pos :: _ => pos);
  34.166 +  in ((vars, xs, get_pos, spec), spec_ctxt) end;
  34.167 +
  34.168 +fun prep_specs prep_var parse_prop prep_att raw_vars raw_specss ctxt =
  34.169 +  let
  34.170 +    val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
  34.171  
  34.172 -    val (Asss1, _) = (fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss0 names;
  34.173 -    val idx = (fold o fold o fold) Term.maxidx_term Asss1 ~1 + 1;
  34.174 +    val propss0 =
  34.175 +      raw_specss |> map (fn ((_, raw_concl), raw_prems, raw_params) =>
  34.176 +        let val (ys, ctxt') = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes
  34.177 +        in (ys, map (pair ctxt') (raw_concl :: raw_prems)) end);
  34.178 +    val props =
  34.179 +      burrow (grouped 10 Par_List.map_independent (uncurry parse_prop)) (map #2 propss0)
  34.180 +      |> dummy_frees vars_ctxt xs
  34.181 +      |> map2 (fn (ys, _) => fn concl :: prems => close_form vars_ctxt ys prems concl) propss0;
  34.182  
  34.183 -    val (Asss2, _) =
  34.184 -      fold_map (fn prems :: conclss => fn i =>
  34.185 -        (burrow (close_forms params_ctxt auto_close i prems) conclss, i + 1)) Asss1 idx;
  34.186 -
  34.187 -    val specs = burrow (Syntax.check_props params_ctxt) (flat Asss2);
  34.188 -    val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
  34.189 +    val specs = Syntax.check_props vars_ctxt props;
  34.190 +    val specs_ctxt = vars_ctxt |> fold Variable.declare_term specs;
  34.191  
  34.192      val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
  34.193      val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
  34.194      val name_atts: Attrib.binding list =
  34.195 -      map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (maps #1 raw_specss);
  34.196 -
  34.197 -    fun get_pos x =
  34.198 -      (case (maps o maps o maps) (get_positions specs_ctxt x) Asss2 of
  34.199 -        [] => Position.none
  34.200 -      | pos :: _ => pos);
  34.201 -  in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
  34.202 -
  34.203 -
  34.204 -fun single_spec ((a, B), As) = ([(a, [B])], As);
  34.205 -fun the_spec (a, [prop]) = (a, prop);
  34.206 -
  34.207 -fun prep_specs prep_var parse_prop prep_att auto_close vars specs =
  34.208 -  prepare prep_var parse_prop prep_att auto_close
  34.209 -    vars (map single_spec specs) #>> (apfst o apsnd) (map the_spec);
  34.210 +      map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (map #1 raw_specss);
  34.211 +  in ((params, name_atts ~~ specs), specs_ctxt) end;
  34.212  
  34.213  in
  34.214  
  34.215 -fun check_spec xs As B =
  34.216 -  prep_specs Proof_Context.cert_var (K I) (K I) false xs [(B, As)] #>
  34.217 -  (apfst o apfst o apsnd) the_single;
  34.218 +val check_spec_open = prep_spec_open Proof_Context.cert_var (K I);
  34.219 +val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop;
  34.220  
  34.221 -fun read_spec xs As B =
  34.222 -  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src false xs [(B, As)] #>
  34.223 -  (apfst o apfst o apsnd) the_single;
  34.224 -
  34.225 -type multi_specs = ((Attrib.binding * term) * term list) list;
  34.226 -type multi_specs_cmd = ((Attrib.binding * string) * string list) list;
  34.227 +type multi_specs =
  34.228 +  ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list;
  34.229 +type multi_specs_cmd =
  34.230 +  ((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list;
  34.231  
  34.232  fun check_multi_specs xs specs =
  34.233 -  prep_specs Proof_Context.cert_var (K I) (K I) true xs specs #>> #1;
  34.234 +  prep_specs Proof_Context.cert_var (K I) (K I) xs specs;
  34.235  
  34.236  fun read_multi_specs xs specs =
  34.237 -  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs specs #>> #1;
  34.238 -
  34.239 -fun check_specification xs As Bs =
  34.240 -  prepare Proof_Context.cert_var (K I) (K I) true xs [(Bs, As)] #>> #1;
  34.241 -
  34.242 -fun read_specification xs As Bs =
  34.243 -  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs [(Bs, As)] #>> #1;
  34.244 +  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src xs specs;
  34.245  
  34.246  end;
  34.247  
  34.248  
  34.249  (* axiomatization -- within global theory *)
  34.250  
  34.251 -fun gen_axioms prep raw_decls raw_prems raw_concls thy =
  34.252 +fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy =
  34.253    let
  34.254 -    val ((decls, specs), _) = prep raw_decls raw_prems raw_concls (Proof_Context.init_global thy);
  34.255 -    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) decls;
  34.256 +    (*specification*)
  34.257 +    val ((vars, [prems, concls], _, _), vars_ctxt) =
  34.258 +      Proof_Context.init_global thy
  34.259 +      |> prep_stmt (raw_decls @ raw_fixes) ((map o map) (rpair []) [raw_prems, map snd raw_concls]);
  34.260 +    val (decls, fixes) = chop (length raw_decls) vars;
  34.261 +
  34.262 +    val frees =
  34.263 +      rev ((fold o fold) (Variable.add_frees vars_ctxt) [prems, concls] [])
  34.264 +      |> map (fn (x, T) => (x, Free (x, T)));
  34.265 +    val close = Logic.close_prop (map #2 fixes @ frees) prems;
  34.266 +    val specs =
  34.267 +      map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls;
  34.268  
  34.269      (*consts*)
  34.270 -    val (consts, consts_thy) = thy |> fold_map Theory.specify_const decls;
  34.271 -    val subst = Term.subst_atomic (map Free xs ~~ consts);
  34.272 +    val (consts, consts_thy) = thy
  34.273 +      |> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls;
  34.274 +    val subst = Term.subst_atomic (map (#2 o #2) decls ~~ consts);
  34.275  
  34.276      (*axioms*)
  34.277 -    val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
  34.278 -        fold_map Thm.add_axiom_global
  34.279 -          (map (apfst (fn a => Binding.map_name (K a) b))
  34.280 -            (Global_Theory.name_multi (Binding.name_of b) (map subst props)))
  34.281 -        #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
  34.282 +    val (axioms, axioms_thy) =
  34.283 +      (specs, consts_thy) |-> fold_map (fn ((b, atts), prop) =>
  34.284 +        Thm.add_axiom_global (b, subst prop) #>> (fn (_, th) => ((b, atts), [([th], [])])));
  34.285  
  34.286      (*facts*)
  34.287      val (facts, facts_lthy) = axioms_thy
  34.288 @@ -225,33 +226,33 @@
  34.289        |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
  34.290        |> Local_Theory.notes axioms;
  34.291  
  34.292 -  in ((consts, map #2 facts), Local_Theory.exit_global facts_lthy) end;
  34.293 +  in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;
  34.294  
  34.295 -val axiomatization = gen_axioms check_specification;
  34.296 -val axiomatization_cmd = gen_axioms read_specification;
  34.297 +val axiomatization = gen_axioms Proof_Context.cert_stmt (K I);
  34.298 +val axiomatization_cmd = gen_axioms Proof_Context.read_stmt Attrib.check_src;
  34.299  
  34.300 -fun axiom (b, ax) = axiomatization [] [] [(b, [ax])] #>> (hd o hd o snd);
  34.301 +fun axiom (b, ax) = axiomatization [] [] [] [(b, ax)] #>> (hd o snd);
  34.302  
  34.303  
  34.304  (* definition *)
  34.305  
  34.306 -fun gen_def prep raw_var raw_prems raw_spec int lthy =
  34.307 +fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy =
  34.308    let
  34.309 -    val ((vars, ((raw_name, atts), prop)), get_pos) =
  34.310 -      fst (prep (the_list raw_var) raw_prems raw_spec lthy);
  34.311 -    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} prop;
  34.312 +    val atts = map (prep_att lthy) raw_atts;
  34.313 +
  34.314 +    val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
  34.315 +      |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
  34.316 +    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} spec;
  34.317      val _ = Name.reject_internal (x, []);
  34.318      val (b, mx) =
  34.319 -      (case vars of
  34.320 -        [] => (Binding.make (x, get_pos x), NoSyn)
  34.321 -      | [((b, _), mx)] =>
  34.322 -          let
  34.323 -            val y = Variable.check_name b;
  34.324 -            val _ = x = y orelse
  34.325 -              error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
  34.326 -                Position.here (Binding.pos_of b));
  34.327 -          in (b, mx) end);
  34.328 -    val name = Thm.def_binding_optional b raw_name;
  34.329 +      (case (vars, xs) of
  34.330 +        ([], []) => (Binding.make (x, get_pos x), NoSyn)
  34.331 +      | ([(b, _, mx)], [y]) =>
  34.332 +          if x = y then (b, mx)
  34.333 +          else
  34.334 +            error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
  34.335 +              Position.here (Binding.pos_of b)));
  34.336 +    val name = Thm.def_binding_optional b a;
  34.337      val ((lhs, (_, raw_th)), lthy2) = lthy
  34.338        |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
  34.339  
  34.340 @@ -268,32 +269,29 @@
  34.341          (member (op =) (Term.add_frees lhs' [])) [(x, T)];
  34.342    in ((lhs, (def_name, th')), lthy4) end;
  34.343  
  34.344 -val definition' = gen_def check_spec;
  34.345 -fun definition xs As B = definition' xs As B false;
  34.346 -val definition_cmd = gen_def read_spec;
  34.347 +val definition' = gen_def check_spec_open (K I);
  34.348 +fun definition xs ys As B = definition' xs ys As B false;
  34.349 +val definition_cmd = gen_def read_spec_open Attrib.check_src;
  34.350  
  34.351  
  34.352  (* abbreviation *)
  34.353  
  34.354 -fun gen_abbrev prep mode raw_var raw_prop int lthy =
  34.355 +fun gen_abbrev prep_spec mode raw_var raw_params raw_spec int lthy =
  34.356    let
  34.357 -    val lthy1 = lthy
  34.358 -      |> Proof_Context.set_syntax_mode mode;
  34.359 -    val (((vars, (_, prop)), get_pos), _) =
  34.360 -      prep (the_list raw_var) [] (Attrib.empty_binding, raw_prop)
  34.361 -        (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
  34.362 -    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
  34.363 +    val lthy1 = lthy |> Proof_Context.set_syntax_mode mode;
  34.364 +    val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
  34.365 +      |> Proof_Context.set_mode Proof_Context.mode_abbrev
  34.366 +      |> prep_spec (the_list raw_var) raw_params [] raw_spec;
  34.367 +    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 spec));
  34.368      val _ = Name.reject_internal (x, []);
  34.369      val (b, mx) =
  34.370 -      (case vars of
  34.371 -        [] => (Binding.make (x, get_pos x), NoSyn)
  34.372 -      | [((b, _), mx)] =>
  34.373 -          let
  34.374 -            val y = Variable.check_name b;
  34.375 -            val _ = x = y orelse
  34.376 -              error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
  34.377 -                Position.here (Binding.pos_of b));
  34.378 -          in (b, mx) end);
  34.379 +      (case (vars, xs) of
  34.380 +        ([], []) => (Binding.make (x, get_pos x), NoSyn)
  34.381 +      | ([(b, _, mx)], [y]) =>
  34.382 +          if x = y then (b, mx)
  34.383 +          else
  34.384 +            error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
  34.385 +              Position.here (Binding.pos_of b)));
  34.386      val lthy2 = lthy1
  34.387        |> Local_Theory.abbrev mode ((b, mx), rhs) |> snd
  34.388        |> Proof_Context.restore_syntax_mode lthy;
  34.389 @@ -301,8 +299,8 @@
  34.390      val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
  34.391    in lthy2 end;
  34.392  
  34.393 -val abbreviation = gen_abbrev check_spec;
  34.394 -val abbreviation_cmd = gen_abbrev read_spec;
  34.395 +val abbreviation = gen_abbrev check_spec_open;
  34.396 +val abbreviation_cmd = gen_abbrev read_spec_open;
  34.397  
  34.398  
  34.399  (* notation *)
    35.1 --- a/src/Pure/Pure.thy	Sun May 29 14:43:18 2016 +0200
    35.2 +++ b/src/Pure/Pure.thy	Mon May 30 20:58:54 2016 +0200
    35.3 @@ -343,19 +343,24 @@
    35.4  
    35.5  val _ =
    35.6    Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
    35.7 -    (Scan.option Parse_Spec.constdecl -- Parse_Spec.spec
    35.8 -      >> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c));
    35.9 +    (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
   35.10 +      Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
   35.11 +        #2 oo Specification.definition_cmd decl params prems spec));
   35.12  
   35.13  val _ =
   35.14    Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   35.15 -    (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   35.16 -      >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
   35.17 +    (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
   35.18 +      >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
   35.19 +
   35.20 +val axiomatization =
   35.21 +  Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --
   35.22 +  Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
   35.23  
   35.24  val _ =
   35.25    Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
   35.26      (Scan.optional Parse.fixes [] --
   35.27 -      Scan.optional (Parse.where_ |-- Parse.!!! Parse_Spec.specification) ([], [])
   35.28 -      >> (fn (a, (b, c)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c)));
   35.29 +      Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
   35.30 +      >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
   35.31  
   35.32  in end\<close>
   35.33  
    36.1 --- a/src/Tools/Code/code_runtime.ML	Sun May 29 14:43:18 2016 +0200
    36.2 +++ b/src/Tools/Code/code_runtime.ML	Mon May 30 20:58:54 2016 +0200
    36.3 @@ -549,7 +549,7 @@
    36.4  fun add_definiendum (ml_name, (b, T)) thy =
    36.5    thy
    36.6    |> Code_Target.add_reserved target ml_name
    36.7 -  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] []
    36.8 +  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] []
    36.9    |-> (fn ([Const (const, _)], _) =>
   36.10      Code_Target.set_printings (Constant (const,
   36.11        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))