# HG changeset patch # User wenzelm # Date 1464610544 -7200 # Node ID b065b4833092fec412841081217e58522f04e837 # Parent ee1c9de4e03ac45addd7eb765c907b14a2ed35d4 allow 'for' fixes for multi_specs; diff -r ee1c9de4e03a -r b065b4833092 src/Doc/Isar_Ref/HOL_Specific.thy --- 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"} \ - (@'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 \ - @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations - ; - (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts? - @{syntax "fixes"} \ @'where' equations + @@{command (HOL) primrec} @{syntax "fixes"} @'where' @{syntax multi_specs} ; - - equations: (@{syntax thmdecl}? @{syntax prop} + '|') + (@@{command (HOL) fun} | @@{command (HOL) function}) function_opts? \ + @{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 \ - @@{command (HOL) partial_function} '(' @{syntax name} ')' @{syntax "fixes"} \ - @'where' @{syntax thmdecl}? @{syntax prop} + @@{command (HOL) partial_function} '(' @{syntax name} ')' \ + @{syntax "fixes"} @'where' @{syntax multi_specs} \} \<^descr> @{command (HOL) "partial_function"}~\(mode)\ defines diff -r ee1c9de4e03a -r b065b4833092 src/Doc/Isar_Ref/Outer_Syntax.thy --- 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 @@ \ +subsection \Structured specifications\ + +text \ + Structured specifications use propositions with explicit notation for the + ``eigen-context'' to describe rule structure: \\x. A x \ \ \ B x\ is + expressed as \<^theory_text>\B x if A x and \ for x\. It is also possible to use dummy + terms ``\_\'' (underscore) to refer to locally fixed variables anonymously. + + Multiple specifications are delimited by ``\|\'' to emphasize separate + cases: each with its own scope of inferred types for free variables. + + + @{rail \ + @{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'))? + \} +\ + + section \Diagnostic commands\ text \ diff -r ee1c9de4e03a -r b065b4833092 src/Doc/Isar_Ref/Spec.thy --- 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} \} @@ -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} \} \<^descr> \<^theory_text>\axiomatization c\<^sub>1 \ c\<^sub>m where \\<^sub>1 \ \\<^sub>n\ introduces several constants diff -r ee1c9de4e03a -r b065b4833092 src/HOL/HOLCF/Tools/fixrec.ML --- 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 diff -r ee1c9de4e03a -r b065b4833092 src/HOL/Nominal/nominal_atoms.ML --- 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; diff -r ee1c9de4e03a -r b065b4833092 src/HOL/Nominal/nominal_datatype.ML --- 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; diff -r ee1c9de4e03a -r b065b4833092 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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; diff -r ee1c9de4e03a -r b065b4833092 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- 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"); diff -r ee1c9de4e03a -r b065b4833092 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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; diff -r ee1c9de4e03a -r b065b4833092 src/HOL/Tools/Function/partial_function.ML --- 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; diff -r ee1c9de4e03a -r b065b4833092 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- 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) diff -r ee1c9de4e03a -r b065b4833092 src/Pure/Isar/parse_spec.ML --- 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; diff -r ee1c9de4e03a -r b065b4833092 src/Pure/Isar/specification.ML --- 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;