allow 'for' fixes for multi_specs;
authorwenzelm
Mon May 30 14:15:44 2016 +0200 (2016-05-30)
changeset 63182b065b4833092
parent 63181 ee1c9de4e03a
child 63183 4d04e14d7ab8
allow 'for' fixes for multi_specs;
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Doc/Isar_Ref/Spec.thy
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.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/Function/partial_function.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon May 30 11:44:41 2016 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon May 30 14:15:44 2016 +0200
     1.3 @@ -109,9 +109,7 @@
     1.4      (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
     1.5        @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
     1.6        @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
     1.7 -      (@'where' clauses)? (@'monos' @{syntax thms})?
     1.8 -    ;
     1.9 -    clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
    1.10 +      (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
    1.11      ;
    1.12      @@{command print_inductives} ('!'?)
    1.13      ;
    1.14 @@ -266,15 +264,12 @@
    1.15    \end{matharray}
    1.16  
    1.17    @{rail \<open>
    1.18 -    @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations
    1.19 -    ;
    1.20 -    (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?
    1.21 -      @{syntax "fixes"} \<newline> @'where' equations
    1.22 +    @@{command (HOL) primrec} @{syntax "fixes"} @'where' @{syntax multi_specs}
    1.23      ;
    1.24 -
    1.25 -    equations: (@{syntax thmdecl}? @{syntax prop} + '|')
    1.26 +    (@@{command (HOL) fun} | @@{command (HOL) function}) function_opts? \<newline>
    1.27 +      @{syntax "fixes"} @'where' @{syntax multi_specs}
    1.28      ;
    1.29 -    functionopts: '(' (('sequential' | 'domintros') + ',') ')'
    1.30 +    function_opts: '(' (('sequential' | 'domintros') + ',') ')'
    1.31      ;
    1.32      @@{command (HOL) termination} @{syntax term}?
    1.33      ;
    1.34 @@ -568,8 +563,8 @@
    1.35    \end{matharray}
    1.36  
    1.37    @{rail \<open>
    1.38 -    @@{command (HOL) partial_function} '(' @{syntax name} ')' @{syntax "fixes"} \<newline>
    1.39 -      @'where' @{syntax thmdecl}? @{syntax prop}
    1.40 +    @@{command (HOL) partial_function} '(' @{syntax name} ')' \<newline>
    1.41 +      @{syntax "fixes"} @'where' @{syntax multi_specs}
    1.42    \<close>}
    1.43  
    1.44    \<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines
     2.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon May 30 11:44:41 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon May 30 14:15:44 2016 +0200
     2.3 @@ -450,6 +450,29 @@
     2.4  \<close>
     2.5  
     2.6  
     2.7 +subsection \<open>Structured specifications\<close>
     2.8 +
     2.9 +text \<open>
    2.10 +  Structured specifications use propositions with explicit notation for the
    2.11 +  ``eigen-context'' to describe rule structure: \<open>\<And>x. A x \<Longrightarrow> \<dots> \<Longrightarrow> B x\<close> is
    2.12 +  expressed as \<^theory_text>\<open>B x if A x and \<dots> for x\<close>. It is also possible to use dummy
    2.13 +  terms ``\<open>_\<close>'' (underscore) to refer to locally fixed variables anonymously.
    2.14 +
    2.15 +  Multiple specifications are delimited by ``\<open>|\<close>'' to emphasize separate
    2.16 +  cases: each with its own scope of inferred types for free variables.
    2.17 +
    2.18 +
    2.19 +  @{rail \<open>
    2.20 +    @{syntax_def multi_specs}: (@{syntax structured_spec} + '|')
    2.21 +    ;
    2.22 +    @{syntax_def structured_spec}:
    2.23 +      @{syntax thmdecl}? @{syntax prop} @{syntax spec_prems} @{syntax for_fixes}
    2.24 +    ;
    2.25 +    @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))?
    2.26 +  \<close>}
    2.27 +\<close>
    2.28 +
    2.29 +
    2.30  section \<open>Diagnostic commands\<close>
    2.31  
    2.32  text \<open>
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Mon May 30 11:44:41 2016 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon May 30 14:15:44 2016 +0200
     3.3 @@ -293,9 +293,8 @@
     3.4      ;
     3.5      decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
     3.6      ;
     3.7 -    definition: @{syntax thmdecl}? @{syntax prop} prems @{syntax for_fixes}
     3.8 -    ;
     3.9 -    prems: (@'if' ((@{syntax prop}+) + @'and'))?
    3.10 +    definition: @{syntax thmdecl}? @{syntax prop}
    3.11 +      @{syntax spec_prems} @{syntax for_fixes}
    3.12      ;
    3.13      abbreviation: @{syntax prop} @{syntax for_fixes}
    3.14    \<close>}
    3.15 @@ -345,9 +344,7 @@
    3.16      @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
    3.17      ;
    3.18      axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
    3.19 -      prems @{syntax for_fixes}
    3.20 -    ;
    3.21 -    prems: (@'if' ((@{syntax prop}+) + @'and'))?
    3.22 +      @{syntax spec_prems} @{syntax for_fixes}
    3.23    \<close>}
    3.24  
    3.25    \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
     4.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Mon May 30 11:44:41 2016 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon May 30 14:15:44 2016 +0200
     4.3 @@ -334,7 +334,7 @@
     4.4      val (skips, raw_spec) = ListPair.unzip raw_spec'
     4.5      val (fixes : ((binding * typ) * mixfix) list,
     4.6           spec : (Attrib.binding * term) list) =
     4.7 -          fst (prep_spec raw_fixes (map (rpair []) raw_spec) lthy)
     4.8 +          fst (prep_spec raw_fixes (map (fn s => (s, [], [])) raw_spec) lthy)
     4.9      val names = map (Binding.name_of o fst o fst) fixes
    4.10      fun check_head name =
    4.11          member (op =) names name orelse
     5.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon May 30 11:44:41 2016 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 30 14:15:44 2016 +0200
     5.3 @@ -192,7 +192,7 @@
     5.4          thy' |>
     5.5          BNF_LFP_Compat.primrec_global
     5.6            [(Binding.name swap_name, SOME swapT, NoSyn)]
     5.7 -          [((Attrib.empty_binding, def1), [])] ||>
     5.8 +          [((Attrib.empty_binding, def1), [], [])] ||>
     5.9          Sign.parent_path ||>>
    5.10          Global_Theory.add_defs_unchecked true
    5.11            [((Binding.name name, def2), [])] |>> (snd o fst)
    5.12 @@ -226,7 +226,7 @@
    5.13          thy' |>
    5.14          BNF_LFP_Compat.primrec_global
    5.15            [(Binding.name prm_name, SOME prmT, NoSyn)]
    5.16 -          (map (fn def => ((Attrib.empty_binding, def), [])) [def1, def2]) ||>
    5.17 +          (map (fn def => ((Attrib.empty_binding, def), [], [])) [def1, def2]) ||>
    5.18          Sign.parent_path
    5.19        end) ak_names_types thy3;
    5.20      
     6.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon May 30 11:44:41 2016 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon May 30 14:15:44 2016 +0200
     6.3 @@ -255,7 +255,7 @@
     6.4              (Free (nth perm_names_types' i) $
     6.5                 Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
     6.6                 list_comb (c, args),
     6.7 -             list_comb (c, map perm_arg (dts ~~ args))))), [])
     6.8 +             list_comb (c, map perm_arg (dts ~~ args))))), [], [])
     6.9          end) constrs
    6.10        end) descr;
    6.11  
     7.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon May 30 11:44:41 2016 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon May 30 14:15:44 2016 +0200
     7.3 @@ -265,7 +265,7 @@
     7.4      val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
     7.5        |> Local_Theory.open_target |> snd
     7.6        |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
     7.7 -      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [])) eqs)
     7.8 +      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [], [])) eqs)
     7.9        ||> `Local_Theory.close_target;
    7.10  
    7.11      val phi = Proof_Context.export_morphism lthy_old lthy;
     8.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon May 30 11:44:41 2016 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon May 30 14:15:44 2016 +0200
     8.3 @@ -1829,7 +1829,7 @@
     8.4  
     8.5      val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
     8.6        Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
     8.7 -        [(((Binding.concealed Binding.empty, []), parsed_eq), [])]
     8.8 +        [(((Binding.concealed Binding.empty, []), parsed_eq), [], [])]
     8.9          Function_Common.default_config pat_completeness_auto lthy;
    8.10    in
    8.11      ((defname, (pelim, pinduct, psimp)), lthy)
    8.12 @@ -1982,7 +1982,7 @@
    8.13  
    8.14      val (plugins, friend, transfer) = get_options lthy opts;
    8.15      val ([((b, fun_T), mx)], [(_, eq)]) =
    8.16 -      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [])] lthy);
    8.17 +      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [], [])] lthy);
    8.18  
    8.19      val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
    8.20        error ("Type of " ^ Binding.print b ^ " contains top sort");
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon May 30 11:44:41 2016 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon May 30 14:15:44 2016 +0200
     9.3 @@ -1588,7 +1588,7 @@
     9.4      val (raw_specs, of_specs_opt) =
     9.5        split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
     9.6      val (fixes, specs) =
     9.7 -      fst (Specification.read_multi_specs raw_fixes (map (rpair []) raw_specs) lthy);
     9.8 +      fst (Specification.read_multi_specs raw_fixes (map (fn spec => (spec, [], [])) raw_specs) lthy);
     9.9    in
    9.10      primcorec_ursive auto opts fixes specs of_specs_opt lthy
    9.11    end;
    10.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon May 30 11:44:41 2016 +0200
    10.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 30 14:15:44 2016 +0200
    10.3 @@ -226,7 +226,7 @@
    10.4          "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
    10.5      val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
    10.6  
    10.7 -    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [])] lthy;
    10.8 +    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [], [])] lthy;
    10.9      val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
   10.10  
   10.11      val ((f_binding, fT), mixfix) = the_single fixes;
    11.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon May 30 11:44:41 2016 +0200
    11.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon May 30 14:15:44 2016 +0200
    11.3 @@ -365,7 +365,7 @@
    11.4        Function.add_function
    11.5          (map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
    11.6            (names ~~ Ts))
    11.7 -        (map (fn t => (((Binding.concealed Binding.empty, []), t), [])) eqs_t)
    11.8 +        (map (fn t => (((Binding.concealed Binding.empty, []), t), [], [])) eqs_t)
    11.9          Function_Common.default_config pat_completeness_auto
   11.10        #> snd
   11.11        #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
    12.1 --- a/src/Pure/Isar/parse_spec.ML	Mon May 30 11:44:41 2016 +0200
    12.2 +++ b/src/Pure/Isar/parse_spec.ML	Mon May 30 14:15:44 2016 +0200
    12.3 @@ -60,7 +60,7 @@
    12.4  
    12.5  val multi_specs =
    12.6    Parse.enum1 "|"
    12.7 -    (opt_thm_name ":" -- Parse.prop -- if_assumes --|
    12.8 +    ((opt_thm_name ":" -- Parse.prop -- if_assumes -- Parse.for_fixes >> Scan.triple1) --|
    12.9        Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
   12.10  
   12.11  val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
    13.1 --- a/src/Pure/Isar/specification.ML	Mon May 30 11:44:41 2016 +0200
    13.2 +++ b/src/Pure/Isar/specification.ML	Mon May 30 14:15:44 2016 +0200
    13.3 @@ -17,8 +17,10 @@
    13.4      (binding * string option * mixfix) list -> string list -> string -> Proof.context ->
    13.5      ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
    13.6      Proof.context
    13.7 -  type multi_specs = ((Attrib.binding * term) * term list) list
    13.8 -  type multi_specs_cmd = ((Attrib.binding * string) * string list) list
    13.9 +  type multi_specs =
   13.10 +    ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list
   13.11 +  type multi_specs_cmd =
   13.12 +    ((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list
   13.13    val check_multi_specs: (binding * typ option * mixfix) list -> multi_specs -> Proof.context ->
   13.14      (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   13.15    val read_multi_specs: (binding * string option * mixfix) list -> multi_specs_cmd -> Proof.context ->
   13.16 @@ -106,8 +108,8 @@
   13.17            map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
   13.18    in ((vars, xs), ctxt'') end;
   13.19  
   13.20 -fun close_form ctxt prems concl =
   13.21 -  let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) []);
   13.22 +fun close_form ctxt ys prems concl =
   13.23 +  let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys));
   13.24    in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
   13.25  
   13.26  fun dummy_frees ctxt xs tss =
   13.27 @@ -155,11 +157,13 @@
   13.28      val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
   13.29  
   13.30      val propss0 =
   13.31 -      map (fn ((_, raw_concl), raw_prems) => raw_concl :: raw_prems) raw_specss
   13.32 -      |> burrow (grouped 10 Par_List.map_independent (parse_prop vars_ctxt));
   13.33 +      raw_specss |> map (fn ((_, raw_concl), raw_prems, raw_params) =>
   13.34 +        let val (ys, ctxt') = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes
   13.35 +        in (ys, map (pair ctxt') (raw_concl :: raw_prems)) end);
   13.36      val props =
   13.37 -      dummy_frees vars_ctxt xs propss0
   13.38 -      |> map (fn concl :: prems => close_form vars_ctxt prems concl);
   13.39 +      burrow (grouped 10 Par_List.map_independent (uncurry parse_prop)) (map #2 propss0)
   13.40 +      |> dummy_frees vars_ctxt xs
   13.41 +      |> map2 (fn (ys, _) => fn concl :: prems => close_form vars_ctxt ys prems concl) propss0;
   13.42  
   13.43      val specs = Syntax.check_props vars_ctxt props;
   13.44      val specs_ctxt = vars_ctxt |> fold Variable.declare_term specs;
   13.45 @@ -175,8 +179,10 @@
   13.46  val check_spec_open = prep_spec_open Proof_Context.cert_var (K I);
   13.47  val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop;
   13.48  
   13.49 -type multi_specs = ((Attrib.binding * term) * term list) list;
   13.50 -type multi_specs_cmd = ((Attrib.binding * string) * string list) list;
   13.51 +type multi_specs =
   13.52 +  ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list;
   13.53 +type multi_specs_cmd =
   13.54 +  ((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list;
   13.55  
   13.56  fun check_multi_specs xs specs =
   13.57    prep_specs Proof_Context.cert_var (K I) (K I) xs specs;