--- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon May 30 11:44:41 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon May 30 14:15:44 2016 +0200
@@ -109,9 +109,7 @@
(@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
@@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
@{syntax "fixes"} @{syntax "for_fixes"} \<newline>
- (@'where' clauses)? (@'monos' @{syntax thms})?
- ;
- clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
+ (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
;
@@{command print_inductives} ('!'?)
;
@@ -266,15 +264,12 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations
- ;
- (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?
- @{syntax "fixes"} \<newline> @'where' equations
+ @@{command (HOL) primrec} @{syntax "fixes"} @'where' @{syntax multi_specs}
;
-
- equations: (@{syntax thmdecl}? @{syntax prop} + '|')
+ (@@{command (HOL) fun} | @@{command (HOL) function}) function_opts? \<newline>
+ @{syntax "fixes"} @'where' @{syntax multi_specs}
;
- functionopts: '(' (('sequential' | 'domintros') + ',') ')'
+ function_opts: '(' (('sequential' | 'domintros') + ',') ')'
;
@@{command (HOL) termination} @{syntax term}?
;
@@ -568,8 +563,8 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) partial_function} '(' @{syntax name} ')' @{syntax "fixes"} \<newline>
- @'where' @{syntax thmdecl}? @{syntax prop}
+ @@{command (HOL) partial_function} '(' @{syntax name} ')' \<newline>
+ @{syntax "fixes"} @'where' @{syntax multi_specs}
\<close>}
\<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon May 30 11:44:41 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Mon May 30 14:15:44 2016 +0200
@@ -450,6 +450,29 @@
\<close>
+subsection \<open>Structured specifications\<close>
+
+text \<open>
+ Structured specifications use propositions with explicit notation for the
+ ``eigen-context'' to describe rule structure: \<open>\<And>x. A x \<Longrightarrow> \<dots> \<Longrightarrow> B x\<close> is
+ expressed as \<^theory_text>\<open>B x if A x and \<dots> for x\<close>. It is also possible to use dummy
+ terms ``\<open>_\<close>'' (underscore) to refer to locally fixed variables anonymously.
+
+ Multiple specifications are delimited by ``\<open>|\<close>'' to emphasize separate
+ cases: each with its own scope of inferred types for free variables.
+
+
+ @{rail \<open>
+ @{syntax_def multi_specs}: (@{syntax structured_spec} + '|')
+ ;
+ @{syntax_def structured_spec}:
+ @{syntax thmdecl}? @{syntax prop} @{syntax spec_prems} @{syntax for_fixes}
+ ;
+ @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))?
+ \<close>}
+\<close>
+
+
section \<open>Diagnostic commands\<close>
text \<open>
--- a/src/Doc/Isar_Ref/Spec.thy Mon May 30 11:44:41 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Mon May 30 14:15:44 2016 +0200
@@ -293,9 +293,8 @@
;
decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
;
- definition: @{syntax thmdecl}? @{syntax prop} prems @{syntax for_fixes}
- ;
- prems: (@'if' ((@{syntax prop}+) + @'and'))?
+ definition: @{syntax thmdecl}? @{syntax prop}
+ @{syntax spec_prems} @{syntax for_fixes}
;
abbreviation: @{syntax prop} @{syntax for_fixes}
\<close>}
@@ -345,9 +344,7 @@
@@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
;
axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
- prems @{syntax for_fixes}
- ;
- prems: (@'if' ((@{syntax prop}+) + @'and'))?
+ @{syntax spec_prems} @{syntax for_fixes}
\<close>}
\<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
--- a/src/HOL/HOLCF/Tools/fixrec.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon May 30 14:15:44 2016 +0200
@@ -334,7 +334,7 @@
val (skips, raw_spec) = ListPair.unzip raw_spec'
val (fixes : ((binding * typ) * mixfix) list,
spec : (Attrib.binding * term) list) =
- fst (prep_spec raw_fixes (map (rpair []) raw_spec) lthy)
+ fst (prep_spec raw_fixes (map (fn s => (s, [], [])) raw_spec) lthy)
val names = map (Binding.name_of o fst o fst) fixes
fun check_head name =
member (op =) names name orelse
--- a/src/HOL/Nominal/nominal_atoms.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon May 30 14:15:44 2016 +0200
@@ -192,7 +192,7 @@
thy' |>
BNF_LFP_Compat.primrec_global
[(Binding.name swap_name, SOME swapT, NoSyn)]
- [((Attrib.empty_binding, def1), [])] ||>
+ [((Attrib.empty_binding, def1), [], [])] ||>
Sign.parent_path ||>>
Global_Theory.add_defs_unchecked true
[((Binding.name name, def2), [])] |>> (snd o fst)
@@ -226,7 +226,7 @@
thy' |>
BNF_LFP_Compat.primrec_global
[(Binding.name prm_name, SOME prmT, NoSyn)]
- (map (fn def => ((Attrib.empty_binding, def), [])) [def1, def2]) ||>
+ (map (fn def => ((Attrib.empty_binding, def), [], [])) [def1, def2]) ||>
Sign.parent_path
end) ak_names_types thy3;
--- a/src/HOL/Nominal/nominal_datatype.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon May 30 14:15:44 2016 +0200
@@ -255,7 +255,7 @@
(Free (nth perm_names_types' i) $
Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
list_comb (c, args),
- list_comb (c, map perm_arg (dts ~~ args))))), [])
+ list_comb (c, map perm_arg (dts ~~ args))))), [], [])
end) constrs
end) descr;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon May 30 14:15:44 2016 +0200
@@ -265,7 +265,7 @@
val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
|> Local_Theory.open_target |> snd
|> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
- |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [])) eqs)
+ |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [], [])) eqs)
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon May 30 14:15:44 2016 +0200
@@ -1829,7 +1829,7 @@
val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
- [(((Binding.concealed Binding.empty, []), parsed_eq), [])]
+ [(((Binding.concealed Binding.empty, []), parsed_eq), [], [])]
Function_Common.default_config pat_completeness_auto lthy;
in
((defname, (pelim, pinduct, psimp)), lthy)
@@ -1982,7 +1982,7 @@
val (plugins, friend, transfer) = get_options lthy opts;
val ([((b, fun_T), mx)], [(_, eq)]) =
- fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [])] lthy);
+ fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [], [])] lthy);
val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
error ("Type of " ^ Binding.print b ^ " contains top sort");
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon May 30 14:15:44 2016 +0200
@@ -1588,7 +1588,7 @@
val (raw_specs, of_specs_opt) =
split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
val (fixes, specs) =
- fst (Specification.read_multi_specs raw_fixes (map (rpair []) raw_specs) lthy);
+ fst (Specification.read_multi_specs raw_fixes (map (fn spec => (spec, [], [])) raw_specs) lthy);
in
primcorec_ursive auto opts fixes specs of_specs_opt lthy
end;
--- a/src/HOL/Tools/Function/partial_function.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Mon May 30 14:15:44 2016 +0200
@@ -226,7 +226,7 @@
"Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
- val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [])] lthy;
+ val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [], [])] lthy;
val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
val ((f_binding, fT), mixfix) = the_single fixes;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon May 30 14:15:44 2016 +0200
@@ -365,7 +365,7 @@
Function.add_function
(map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
(names ~~ Ts))
- (map (fn t => (((Binding.concealed Binding.empty, []), t), [])) eqs_t)
+ (map (fn t => (((Binding.concealed Binding.empty, []), t), [], [])) eqs_t)
Function_Common.default_config pat_completeness_auto
#> snd
#> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
--- a/src/Pure/Isar/parse_spec.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Mon May 30 14:15:44 2016 +0200
@@ -60,7 +60,7 @@
val multi_specs =
Parse.enum1 "|"
- (opt_thm_name ":" -- Parse.prop -- if_assumes --|
+ ((opt_thm_name ":" -- Parse.prop -- if_assumes -- Parse.for_fixes >> Scan.triple1) --|
Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
--- a/src/Pure/Isar/specification.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/Pure/Isar/specification.ML Mon May 30 14:15:44 2016 +0200
@@ -17,8 +17,10 @@
(binding * string option * mixfix) list -> string list -> string -> Proof.context ->
((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
Proof.context
- type multi_specs = ((Attrib.binding * term) * term list) list
- type multi_specs_cmd = ((Attrib.binding * string) * string list) list
+ type multi_specs =
+ ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list
+ type multi_specs_cmd =
+ ((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list
val check_multi_specs: (binding * typ option * mixfix) list -> multi_specs -> Proof.context ->
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
val read_multi_specs: (binding * string option * mixfix) list -> multi_specs_cmd -> Proof.context ->
@@ -106,8 +108,8 @@
map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
in ((vars, xs), ctxt'') end;
-fun close_form ctxt prems concl =
- let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) []);
+fun close_form ctxt ys prems concl =
+ let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys));
in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
fun dummy_frees ctxt xs tss =
@@ -155,11 +157,13 @@
val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
val propss0 =
- map (fn ((_, raw_concl), raw_prems) => raw_concl :: raw_prems) raw_specss
- |> burrow (grouped 10 Par_List.map_independent (parse_prop vars_ctxt));
+ raw_specss |> map (fn ((_, raw_concl), raw_prems, raw_params) =>
+ let val (ys, ctxt') = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes
+ in (ys, map (pair ctxt') (raw_concl :: raw_prems)) end);
val props =
- dummy_frees vars_ctxt xs propss0
- |> map (fn concl :: prems => close_form vars_ctxt prems concl);
+ burrow (grouped 10 Par_List.map_independent (uncurry parse_prop)) (map #2 propss0)
+ |> dummy_frees vars_ctxt xs
+ |> map2 (fn (ys, _) => fn concl :: prems => close_form vars_ctxt ys prems concl) propss0;
val specs = Syntax.check_props vars_ctxt props;
val specs_ctxt = vars_ctxt |> fold Variable.declare_term specs;
@@ -175,8 +179,10 @@
val check_spec_open = prep_spec_open Proof_Context.cert_var (K I);
val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop;
-type multi_specs = ((Attrib.binding * term) * term list) list;
-type multi_specs_cmd = ((Attrib.binding * string) * string list) list;
+type multi_specs =
+ ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list;
+type multi_specs_cmd =
+ ((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list;
fun check_multi_specs xs specs =
prep_specs Proof_Context.cert_var (K I) (K I) xs specs;