--- a/NEWS Sun May 29 14:43:18 2016 +0200
+++ b/NEWS Mon May 30 20:58:54 2016 +0200
@@ -66,9 +66,13 @@
*** Isar ***
-* Many specification elements support structured statements with 'if'
-eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
-'function'.
+* Command 'axiomatization' has become more restrictive to correspond
+better to internal axioms as singleton facts with mandatory name. Minor
+INCOMPATIBILITY.
+
+* Many specification elements support structured statements with 'if' /
+'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
+'definition', 'inductive', 'function'.
* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sun May 29 14:43:18 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon May 30 20:58:54 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,11 @@
\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 specification}
;
-
- equations: (@{syntax thmdecl}? @{syntax prop} + '|')
+ (@@{command (HOL) fun} | @@{command (HOL) function}) opts? @{syntax specification}
;
- functionopts: '(' (('sequential' | 'domintros') + ',') ')'
+ opts: '(' (('sequential' | 'domintros') + ',') ')'
;
@@{command (HOL) termination} @{syntax term}?
;
@@ -568,8 +562,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} ')'
+ @{syntax specification}
\<close>}
\<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sun May 29 14:43:18 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Mon May 30 20:58:54 2016 +0200
@@ -450,6 +450,31 @@
\<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'))?
+ ;
+ @{syntax_def specification}: @{syntax "fixes"} @'where' @{syntax multi_specs}
+ \<close>}
+\<close>
+
+
section \<open>Diagnostic commands\<close>
text \<open>
--- a/src/Doc/Isar_Ref/Spec.thy Sun May 29 14:43:18 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Mon May 30 20:58:54 2016 +0200
@@ -285,14 +285,18 @@
``abbreviation''.
@{rail \<open>
- @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
+ @@{command definition} decl? definition
;
- @@{command abbreviation} @{syntax mode}? \<newline>
- (decl @'where')? @{syntax prop}
- ;
- decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
+ @@{command abbreviation} @{syntax mode}? decl? abbreviation
;
@@{command print_abbrevs} ('!'?)
+ ;
+ decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
+ ;
+ definition: @{syntax thmdecl}? @{syntax prop}
+ @{syntax spec_prems} @{syntax for_fixes}
+ ;
+ abbreviation: @{syntax prop} @{syntax for_fixes}
\<close>}
\<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according
@@ -337,9 +341,10 @@
\end{matharray}
@{rail \<open>
- @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
+ @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
;
- specs: (@{syntax thmdecl}? @{syntax props} + @'and')
+ axiomatization: (@{syntax thmdecl} @{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/Doc/Tutorial/Misc/AdvancedInd.thy Sun May 29 14:43:18 2016 +0200
+++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy Mon May 30 20:58:54 2016 +0200
@@ -133,7 +133,7 @@
*}
axiomatization f :: "nat \<Rightarrow> nat"
- where f_ax: "f(f(n)) < f(Suc(n))"
+ where f_ax: "f(f(n)) < f(Suc(n))" for n :: nat
text{*
\begin{warn}
--- a/src/HOL/HOLCF/Tools/cpodef.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Mon May 30 20:58:54 2016 +0200
@@ -175,7 +175,7 @@
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))
val ((_, (_, below_ldef)), lthy) = thy
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
- |> Specification.definition NONE []
+ |> Specification.definition NONE [] []
((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
--- a/src/HOL/HOLCF/Tools/domaindef.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Mon May 30 20:58:54 2016 +0200
@@ -138,17 +138,17 @@
val lthy = thy
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
val ((_, (_, emb_ldef)), lthy) =
- Specification.definition NONE [] (emb_bind, emb_eqn) lthy
+ Specification.definition NONE [] [] (emb_bind, emb_eqn) lthy
val ((_, (_, prj_ldef)), lthy) =
- Specification.definition NONE [] (prj_bind, prj_eqn) lthy
+ Specification.definition NONE [] [] (prj_bind, prj_eqn) lthy
val ((_, (_, defl_ldef)), lthy) =
- Specification.definition NONE [] (defl_bind, defl_eqn) lthy
+ Specification.definition NONE [] [] (defl_bind, defl_eqn) lthy
val ((_, (_, liftemb_ldef)), lthy) =
- Specification.definition NONE [] (liftemb_bind, liftemb_eqn) lthy
+ Specification.definition NONE [] [] (liftemb_bind, liftemb_eqn) lthy
val ((_, (_, liftprj_ldef)), lthy) =
- Specification.definition NONE [] (liftprj_bind, liftprj_eqn) lthy
+ Specification.definition NONE [] [] (liftprj_bind, liftprj_eqn) lthy
val ((_, (_, liftdefl_ldef)), lthy) =
- Specification.definition NONE [] (liftdefl_bind, liftdefl_eqn) lthy
+ Specification.definition NONE [] [] (liftdefl_bind, liftdefl_eqn) lthy
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef
val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef
--- a/src/HOL/HOLCF/Tools/fixrec.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon May 30 20:58:54 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/MicroJava/J/JListExample.thy Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Mon May 30 20:58:54 2016 +0200
@@ -15,12 +15,29 @@
append_name :: mname
axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam
-where distinct_fields: "val_name \<noteq> next_name"
- and distinct_vars:
- "l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam"
- "l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam"
- "l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam"
- "l3_nam \<noteq> l4_nam"
+where distinct_fields: "val_nam \<noteq> next_nam"
+ and distinct_vars1: "l_nam \<noteq> l1_nam"
+ and distinct_vars2: "l_nam \<noteq> l2_nam"
+ and distinct_vars3: "l_nam \<noteq> l3_nam"
+ and distinct_vars4: "l_nam \<noteq> l4_nam"
+ and distinct_vars5: "l1_nam \<noteq> l2_nam"
+ and distinct_vars6: "l1_nam \<noteq> l3_nam"
+ and distinct_vars7: "l1_nam \<noteq> l4_nam"
+ and distinct_vars8: "l2_nam \<noteq> l3_nam"
+ and distinct_vars9: "l2_nam \<noteq> l4_nam"
+ and distinct_vars10: "l3_nam \<noteq> l4_nam"
+
+lemmas distinct_vars =
+ distinct_vars1
+ distinct_vars2
+ distinct_vars3
+ distinct_vars4
+ distinct_vars5
+ distinct_vars6
+ distinct_vars7
+ distinct_vars8
+ distinct_vars9
+ distinct_vars10
definition list_name :: cname where
"list_name = Cname list_nam"
--- a/src/HOL/Nominal/nominal_atoms.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon May 30 20:58:54 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 Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon May 30 20:58:54 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/Quickcheck_Examples/Hotel_Example.thy Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy Mon May 30 20:58:54 2016 +0200
@@ -109,9 +109,17 @@
axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
=> 'b list => 'a Quickcheck_Exhaustive.three_valued"
-where find_first'_code [code]:
- "find_first' f [] = Quickcheck_Exhaustive.No_value"
- "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))"
+where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
+ and find_first'_Cons: "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))"
+
+lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons
axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon May 30 20:58:54 2016 +0200
@@ -1020,7 +1020,7 @@
"\ndoes not match type " ^ ty' ^ " in definition");
val id' = mk_rulename id;
val ((t', (_, th)), lthy') = Named_Target.theory_init thy
- |> Specification.definition NONE []
+ |> Specification.definition NONE [] []
((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
val phi =
Proof_Context.export_morphism lthy'
--- a/src/HOL/Tools/BNF/bnf_axiomatization.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML Mon May 30 20:58:54 2016 +0200
@@ -81,8 +81,10 @@
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
- val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
- (Specification.axiomatization [] [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
+ val (((_, raw_thms)), lthy) = Local_Theory.background_theory_result
+ (Specification.axiomatization [] [] []
+ (map_index (fn (i, ax) =>
+ ((mk_b ("axiom" ^ string_of_int (i + 1)) Binding.empty, []), ax)) (flat all_goalss))) lthy;
fun mk_wit_thms set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon May 30 20:58:54 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 Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon May 30 20:58:54 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 Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon May 30 20:58:54 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/BNF/bnf_lfp_rec_sugar.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon May 30 20:58:54 2016 +0200
@@ -687,8 +687,7 @@
val _ = Outer_Syntax.local_theory @{command_keyword primrec}
"define primitive recursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
- --| @{keyword ")"}) []) --
- (Parse.fixes -- Parse_Spec.where_multi_specs)
+ --| @{keyword ")"}) []) -- Parse_Spec.specification
>> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon May 30 20:58:54 2016 +0200
@@ -623,11 +623,11 @@
else if Binding.eq_name (b, equal_binding) then
pair (Term.lambda u exist_xs_u_eq_ctr, refl)
else
- Specification.definition (SOME (b, NONE, NoSyn)) []
+ Specification.definition (SOME (b, NONE, NoSyn)) [] []
((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd)
ks exist_xs_u_eq_ctrs disc_bindings
||>> apfst split_list o fold_map (fn (b, proto_sels) =>
- Specification.definition (SOME (b, NONE, NoSyn)) []
+ Specification.definition (SOME (b, NONE, NoSyn)) [] []
((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos
||> `Local_Theory.close_target;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Mon May 30 20:58:54 2016 +0200
@@ -93,7 +93,7 @@
mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
|> Syntax.check_term lthy;
val ((_, (_, raw_def)), lthy') =
- Specification.definition NONE [] (Attrib.empty_binding, spec) lthy;
+ Specification.definition NONE [] [] (Attrib.empty_binding, spec) lthy;
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
in
--- a/src/HOL/Tools/Function/fun.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Function/fun.ML Mon May 30 20:58:54 2016 +0200
@@ -174,6 +174,6 @@
Outer_Syntax.local_theory' @{command_keyword fun}
"define general recursive functions (short version)"
(function_parser fun_config
- >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
+ >> (fn (config, (fixes, specs)) => add_fun_cmd fixes specs config))
end
--- a/src/HOL/Tools/Function/function.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon May 30 20:58:54 2016 +0200
@@ -274,7 +274,7 @@
Outer_Syntax.local_theory_to_proof' @{command_keyword function}
"define general recursive functions"
(function_parser default_config
- >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
+ >> (fn (config, (fixes, specs)) => function_cmd fixes specs config))
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword termination}
--- a/src/HOL/Tools/Function/function_common.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Mon May 30 20:58:54 2016 +0200
@@ -99,8 +99,7 @@
val import_last_function : Proof.context -> info option
val default_config : function_config
val function_parser : function_config ->
- ((function_config * (binding * string option * mixfix) list) *
- Specification.multi_specs_cmd) parser
+ (function_config * ((binding * string option * mixfix) list * Specification.multi_specs_cmd)) parser
end
structure Function_Common : FUNCTION_COMMON =
@@ -374,7 +373,7 @@
>> (fn opts => fold apply_opt opts default)
in
fun function_parser default_cfg =
- config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_multi_specs
+ config_parser default_cfg -- Parse_Spec.specification
end
--- a/src/HOL/Tools/Function/partial_function.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Mon May 30 20:58:54 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/Lifting/lifting_setup.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon May 30 20:58:54 2016 +0200
@@ -89,7 +89,7 @@
val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
val definition_term = Logic.mk_equals (lhs, rhs)
fun note_def lthy =
- Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) []
+ Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
fun raw_def lthy =
let
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon May 30 20:58:54 2016 +0200
@@ -56,7 +56,7 @@
thy
|> Class.instantiation ([tyco], vs, @{sort partial_term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
+ |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon May 30 20:58:54 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/HOL/Tools/Quickcheck/random_generators.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon May 30 20:58:54 2016 +0200
@@ -266,7 +266,7 @@
|> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
- Specification.definition NONE []
+ Specification.definition NONE [] []
((Binding.concealed Binding.empty, []), random_def)) random_defs')
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
--- a/src/HOL/Tools/code_evaluation.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Mon May 30 20:58:54 2016 +0200
@@ -43,7 +43,7 @@
thy
|> Class.instantiation ([tyco], vs, @{sort term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
+ |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
--- a/src/HOL/Tools/inductive.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/inductive.ML Mon May 30 20:58:54 2016 +0200
@@ -610,7 +610,7 @@
fun ind_cases_rules ctxt raw_props raw_fixes =
let
- val (props, ctxt' ) = Specification.read_props raw_props raw_fixes ctxt;
+ val (props, ctxt') = Specification.read_props raw_props raw_fixes ctxt;
val rules = Proof_Context.export ctxt' ctxt (map (mk_cases ctxt') props);
in rules end;
--- a/src/HOL/Tools/record.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/record.ML Mon May 30 20:58:54 2016 +0200
@@ -1734,7 +1734,7 @@
thy
|> Class.instantiation ([tyco], vs, sort)
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] ((Binding.concealed Binding.empty, []), eq))
+ |-> (fn eq => Specification.definition NONE [] [] ((Binding.concealed Binding.empty, []), eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
@@ -1781,7 +1781,7 @@
|> fold Code.add_default_eqn simps
|> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
+ |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
|-> (fn (_, (_, eq_def)) =>
Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
|-> (fn eq_def => fn thy =>
--- a/src/HOL/Typerep.thy Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Typerep.thy Mon May 30 20:58:54 2016 +0200
@@ -58,7 +58,7 @@
thy
|> Class.instantiation ([tyco], vs, @{sort typerep})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
+ |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
--- a/src/Pure/Isar/parse_spec.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Mon May 30 20:58:54 2016 +0200
@@ -12,10 +12,10 @@
val simple_spec: (Attrib.binding * string) parser
val simple_specs: (Attrib.binding * string list) parser
val if_assumes: string list parser
- val spec: (string list * (Attrib.binding * string)) parser
val multi_specs: Specification.multi_specs_cmd parser
val where_multi_specs: Specification.multi_specs_cmd parser
- val specification: (string list * (Attrib.binding * string list) list) parser
+ val specification:
+ ((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser
val constdecl: (binding * string option * mixfix) parser
val includes: (xstring * Position.T) list parser
val locale_fixes: (binding * string option * mixfix) list parser
@@ -60,17 +60,14 @@
Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat))
[];
-val spec = (opt_thm_name ":" -- Parse.prop) -- if_assumes >> swap;
-
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;
-val specification =
- Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.prop) -- if_assumes >> swap;
+val specification = Parse.fixes -- where_multi_specs;
(* basic constant specifications *)
--- a/src/Pure/Isar/specification.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/Pure/Isar/specification.ML Mon May 30 20:58:54 2016 +0200
@@ -9,43 +9,42 @@
sig
val read_props: string list -> (binding * string option * mixfix) list -> Proof.context ->
term list * Proof.context
- val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
- term * Proof.context
- val check_spec: (binding * typ option * mixfix) list ->
- term list -> Attrib.binding * term -> Proof.context ->
- ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
- * Proof.context
- val read_spec: (binding * string option * mixfix) list ->
- string list -> Attrib.binding * string -> Proof.context ->
- ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
- * Proof.context
- type multi_specs = ((Attrib.binding * term) * term list) list
- type multi_specs_cmd = ((Attrib.binding * string) * string list) list
+ val check_spec_open: (binding * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list -> term list -> term -> Proof.context ->
+ ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
+ Proof.context
+ val read_spec_open: (binding * string option * mixfix) list ->
+ (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 * (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 ->
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
- val check_specification: (binding * typ option * mixfix) list -> term list ->
- (Attrib.binding * term list) list -> Proof.context ->
- (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val read_specification: (binding * string option * mixfix) list -> string list ->
- (Attrib.binding * string list) list -> Proof.context ->
- (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val axiomatization: (binding * typ option * mixfix) list -> term list ->
- (Attrib.binding * term list) list -> theory -> (term list * thm list list) * theory
- val axiomatization_cmd: (binding * string option * mixfix) list -> string list ->
- (Attrib.binding * string list) list -> theory -> (term list * thm list list) * theory
+ val axiomatization: (binding * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list -> term list ->
+ (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
+ val axiomatization_cmd: (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list -> string list ->
+ (Attrib.binding * string) list -> theory -> (term list * thm list) * theory
val axiom: Attrib.binding * term -> theory -> thm * theory
- val definition: (binding * typ option * mixfix) option -> term list ->
- Attrib.binding * term -> local_theory -> (term * (string * thm)) * local_theory
- val definition': (binding * typ option * mixfix) option -> term list ->
- Attrib.binding * term -> bool -> local_theory -> (term * (string * thm)) * local_theory
- val definition_cmd: (binding * string option * mixfix) option -> string list ->
- Attrib.binding * string -> bool -> local_theory -> (term * (string * thm)) * local_theory
- val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option -> term ->
- bool -> local_theory -> local_theory
- val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> string ->
- bool -> local_theory -> local_theory
+ val definition: (binding * typ option * mixfix) option ->
+ (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
+ local_theory -> (term * (string * thm)) * local_theory
+ val definition': (binding * typ option * mixfix) option ->
+ (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
+ bool -> local_theory -> (term * (string * thm)) * local_theory
+ val definition_cmd: (binding * string option * mixfix) option ->
+ (binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
+ bool -> local_theory -> (term * (string * thm)) * local_theory
+ val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option ->
+ (binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory
+ val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
+ (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
local_theory -> local_theory
@@ -91,26 +90,35 @@
val ctxt3 = ctxt2 |> fold Variable.declare_term props3;
in (props3, ctxt3) end;
-fun read_prop raw_prop raw_fixes ctxt =
- let val ([prop], ctxt') = read_props [raw_prop] raw_fixes ctxt
- in (prop, ctxt') end;
-
(* prepare specification *)
local
-fun close_forms ctxt auto_close i prems concls =
- if not auto_close andalso null prems then concls
- else
- let
- val xs =
- if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) [])
- else [];
- val types =
- map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
- val uniform_typing = AList.lookup (op =) (xs ~~ types);
- in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
+fun prep_decls prep_var raw_vars ctxt =
+ let
+ val (vars, ctxt') = fold_map prep_var raw_vars ctxt;
+ val (xs, ctxt'') = ctxt'
+ |> Context_Position.set_visible false
+ |> Proof_Context.add_fixes vars
+ ||> Context_Position.restore_visible ctxt';
+ val _ =
+ Context_Position.reports ctxt''
+ (map (Binding.pos_of o #1) vars ~~
+ map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
+ in ((vars, xs), ctxt'') end;
+
+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 =
+ let
+ val names =
+ Variable.names_of ((fold o fold) Variable.declare_term tss ctxt)
+ |> fold Name.declare xs;
+ val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names;
+ in tss' end;
fun get_positions ctxt x =
let
@@ -125,99 +133,92 @@
| get _ _ = [];
in get [] end;
-fun prepare prep_var parse_prop prep_att auto_close raw_vars raw_specss ctxt =
+fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt =
let
- val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
- val (xs, params_ctxt) = vars_ctxt
- |> Context_Position.set_visible false
- |> Proof_Context.add_fixes vars
- ||> Context_Position.restore_visible vars_ctxt;
- val _ =
- Context_Position.reports params_ctxt
- (map (Binding.pos_of o #1) vars ~~
- map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
+ val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
+ val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes;
+
+ val props =
+ map (parse_prop params_ctxt) (raw_concl :: raw_prems)
+ |> singleton (dummy_frees params_ctxt (xs @ ys));
+
+ val concl :: prems = Syntax.check_props params_ctxt props;
+ val spec = Logic.list_implies (prems, concl);
+ val spec_ctxt = Variable.declare_term spec params_ctxt;
- val Asss0 =
- map (fn (raw_concls, raw_prems) => raw_prems :: map snd raw_concls) raw_specss
- |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
- val names =
- Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss0)
- |> fold Name.declare xs;
+ fun get_pos x =
+ (case maps (get_positions spec_ctxt x) props of
+ [] => Position.none
+ | pos :: _ => pos);
+ in ((vars, xs, get_pos, spec), spec_ctxt) end;
+
+fun prep_specs prep_var parse_prop prep_att raw_vars raw_specss ctxt =
+ let
+ val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
- val (Asss1, _) = (fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss0 names;
- val idx = (fold o fold o fold) Term.maxidx_term Asss1 ~1 + 1;
+ val propss0 =
+ 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 =
+ 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 (Asss2, _) =
- fold_map (fn prems :: conclss => fn i =>
- (burrow (close_forms params_ctxt auto_close i prems) conclss, i + 1)) Asss1 idx;
-
- val specs = burrow (Syntax.check_props params_ctxt) (flat Asss2);
- val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
+ val specs = Syntax.check_props vars_ctxt props;
+ val specs_ctxt = vars_ctxt |> fold Variable.declare_term specs;
val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
val name_atts: Attrib.binding list =
- map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (maps #1 raw_specss);
-
- fun get_pos x =
- (case (maps o maps o maps) (get_positions specs_ctxt x) Asss2 of
- [] => Position.none
- | pos :: _ => pos);
- in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
-
-
-fun single_spec ((a, B), As) = ([(a, [B])], As);
-fun the_spec (a, [prop]) = (a, prop);
-
-fun prep_specs prep_var parse_prop prep_att auto_close vars specs =
- prepare prep_var parse_prop prep_att auto_close
- vars (map single_spec specs) #>> (apfst o apsnd) (map the_spec);
+ map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (map #1 raw_specss);
+ in ((params, name_atts ~~ specs), specs_ctxt) end;
in
-fun check_spec xs As B =
- prep_specs Proof_Context.cert_var (K I) (K I) false xs [(B, As)] #>
- (apfst o apfst o apsnd) the_single;
+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;
-fun read_spec xs As B =
- prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src false xs [(B, As)] #>
- (apfst o apfst o apsnd) the_single;
-
-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) true xs specs #>> #1;
+ prep_specs Proof_Context.cert_var (K I) (K I) xs specs;
fun read_multi_specs xs specs =
- prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs specs #>> #1;
-
-fun check_specification xs As Bs =
- prepare Proof_Context.cert_var (K I) (K I) true xs [(Bs, As)] #>> #1;
-
-fun read_specification xs As Bs =
- prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs [(Bs, As)] #>> #1;
+ prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src xs specs;
end;
(* axiomatization -- within global theory *)
-fun gen_axioms prep raw_decls raw_prems raw_concls thy =
+fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy =
let
- val ((decls, specs), _) = prep raw_decls raw_prems raw_concls (Proof_Context.init_global thy);
- val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) decls;
+ (*specification*)
+ val ((vars, [prems, concls], _, _), vars_ctxt) =
+ Proof_Context.init_global thy
+ |> prep_stmt (raw_decls @ raw_fixes) ((map o map) (rpair []) [raw_prems, map snd raw_concls]);
+ val (decls, fixes) = chop (length raw_decls) vars;
+
+ val frees =
+ rev ((fold o fold) (Variable.add_frees vars_ctxt) [prems, concls] [])
+ |> map (fn (x, T) => (x, Free (x, T)));
+ val close = Logic.close_prop (map #2 fixes @ frees) prems;
+ val specs =
+ map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls;
(*consts*)
- val (consts, consts_thy) = thy |> fold_map Theory.specify_const decls;
- val subst = Term.subst_atomic (map Free xs ~~ consts);
+ val (consts, consts_thy) = thy
+ |> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls;
+ val subst = Term.subst_atomic (map (#2 o #2) decls ~~ consts);
(*axioms*)
- val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
- fold_map Thm.add_axiom_global
- (map (apfst (fn a => Binding.map_name (K a) b))
- (Global_Theory.name_multi (Binding.name_of b) (map subst props)))
- #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
+ val (axioms, axioms_thy) =
+ (specs, consts_thy) |-> fold_map (fn ((b, atts), prop) =>
+ Thm.add_axiom_global (b, subst prop) #>> (fn (_, th) => ((b, atts), [([th], [])])));
(*facts*)
val (facts, facts_lthy) = axioms_thy
@@ -225,33 +226,33 @@
|> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
|> Local_Theory.notes axioms;
- in ((consts, map #2 facts), Local_Theory.exit_global facts_lthy) end;
+ in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;
-val axiomatization = gen_axioms check_specification;
-val axiomatization_cmd = gen_axioms read_specification;
+val axiomatization = gen_axioms Proof_Context.cert_stmt (K I);
+val axiomatization_cmd = gen_axioms Proof_Context.read_stmt Attrib.check_src;
-fun axiom (b, ax) = axiomatization [] [] [(b, [ax])] #>> (hd o hd o snd);
+fun axiom (b, ax) = axiomatization [] [] [] [(b, ax)] #>> (hd o snd);
(* definition *)
-fun gen_def prep raw_var raw_prems raw_spec int lthy =
+fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy =
let
- val ((vars, ((raw_name, atts), prop)), get_pos) =
- fst (prep (the_list raw_var) raw_prems raw_spec lthy);
- val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} prop;
+ val atts = map (prep_att lthy) raw_atts;
+
+ val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
+ |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
+ val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} spec;
val _ = Name.reject_internal (x, []);
val (b, mx) =
- (case vars of
- [] => (Binding.make (x, get_pos x), NoSyn)
- | [((b, _), mx)] =>
- let
- val y = Variable.check_name b;
- val _ = x = y orelse
- error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
- Position.here (Binding.pos_of b));
- in (b, mx) end);
- val name = Thm.def_binding_optional b raw_name;
+ (case (vars, xs) of
+ ([], []) => (Binding.make (x, get_pos x), NoSyn)
+ | ([(b, _, mx)], [y]) =>
+ if x = y then (b, mx)
+ else
+ error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
+ Position.here (Binding.pos_of b)));
+ val name = Thm.def_binding_optional b a;
val ((lhs, (_, raw_th)), lthy2) = lthy
|> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
@@ -268,32 +269,29 @@
(member (op =) (Term.add_frees lhs' [])) [(x, T)];
in ((lhs, (def_name, th')), lthy4) end;
-val definition' = gen_def check_spec;
-fun definition xs As B = definition' xs As B false;
-val definition_cmd = gen_def read_spec;
+val definition' = gen_def check_spec_open (K I);
+fun definition xs ys As B = definition' xs ys As B false;
+val definition_cmd = gen_def read_spec_open Attrib.check_src;
(* abbreviation *)
-fun gen_abbrev prep mode raw_var raw_prop int lthy =
+fun gen_abbrev prep_spec mode raw_var raw_params raw_spec int lthy =
let
- val lthy1 = lthy
- |> Proof_Context.set_syntax_mode mode;
- val (((vars, (_, prop)), get_pos), _) =
- prep (the_list raw_var) [] (Attrib.empty_binding, raw_prop)
- (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
- val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
+ val lthy1 = lthy |> Proof_Context.set_syntax_mode mode;
+ val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
+ |> Proof_Context.set_mode Proof_Context.mode_abbrev
+ |> prep_spec (the_list raw_var) raw_params [] raw_spec;
+ val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 spec));
val _ = Name.reject_internal (x, []);
val (b, mx) =
- (case vars of
- [] => (Binding.make (x, get_pos x), NoSyn)
- | [((b, _), mx)] =>
- let
- val y = Variable.check_name b;
- val _ = x = y orelse
- error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
- Position.here (Binding.pos_of b));
- in (b, mx) end);
+ (case (vars, xs) of
+ ([], []) => (Binding.make (x, get_pos x), NoSyn)
+ | ([(b, _, mx)], [y]) =>
+ if x = y then (b, mx)
+ else
+ error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
+ Position.here (Binding.pos_of b)));
val lthy2 = lthy1
|> Local_Theory.abbrev mode ((b, mx), rhs) |> snd
|> Proof_Context.restore_syntax_mode lthy;
@@ -301,8 +299,8 @@
val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
in lthy2 end;
-val abbreviation = gen_abbrev check_spec;
-val abbreviation_cmd = gen_abbrev read_spec;
+val abbreviation = gen_abbrev check_spec_open;
+val abbreviation_cmd = gen_abbrev read_spec_open;
(* notation *)
--- a/src/Pure/Pure.thy Sun May 29 14:43:18 2016 +0200
+++ b/src/Pure/Pure.thy Mon May 30 20:58:54 2016 +0200
@@ -343,19 +343,24 @@
val _ =
Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
- (Scan.option Parse_Spec.constdecl -- Parse_Spec.spec
- >> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c));
+ (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
+ Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
+ #2 oo Specification.definition_cmd decl params prems spec));
val _ =
Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
- (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
- >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
+ (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
+ >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
+
+val axiomatization =
+ Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --
+ Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
val _ =
Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
(Scan.optional Parse.fixes [] --
- Scan.optional (Parse.where_ |-- Parse.!!! Parse_Spec.specification) ([], [])
- >> (fn (a, (b, c)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c)));
+ Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
+ >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
in end\<close>
--- a/src/Tools/Code/code_runtime.ML Sun May 29 14:43:18 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Mon May 30 20:58:54 2016 +0200
@@ -549,7 +549,7 @@
fun add_definiendum (ml_name, (b, T)) thy =
thy
|> Code_Target.add_reserved target ml_name
- |> Specification.axiomatization [(b, SOME T, NoSyn)] [] []
+ |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] []
|-> (fn ([Const (const, _)], _) =>
Code_Target.set_printings (Constant (const,
[(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))