--- a/NEWS Sat May 28 17:35:12 2016 +0200
+++ b/NEWS Sat May 28 21:38:58 2016 +0200
@@ -70,6 +70,10 @@
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.
+
* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called
--- a/src/Doc/Isar_Ref/Spec.thy Sat May 28 17:35:12 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Sat May 28 21:38:58 2016 +0200
@@ -337,9 +337,12 @@
\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')
+ prems @{syntax for_fixes}
+ ;
+ prems: (@'if' ((@{syntax prop}+) + @'and'))?
\<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 Sat May 28 17:35:12 2016 +0200
+++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy Sat May 28 21:38:58 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/Tools/BNF/bnf_axiomatization.ML Sat May 28 17:35:12 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML Sat May 28 21:38:58 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/Pure/Isar/parse_spec.ML Sat May 28 17:35:12 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Sat May 28 21:38:58 2016 +0200
@@ -15,7 +15,6 @@
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 constdecl: (binding * string option * mixfix) parser
val includes: (xstring * Position.T) list parser
val locale_fixes: (binding * string option * mixfix) list parser
@@ -69,9 +68,6 @@
val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
-val specification =
- Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.prop) -- if_assumes >> swap;
-
(* basic constant specifications *)
--- a/src/Pure/Isar/specification.ML Sat May 28 17:35:12 2016 +0200
+++ b/src/Pure/Isar/specification.ML Sat May 28 21:38:58 2016 +0200
@@ -25,16 +25,12 @@
(((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
@@ -192,32 +188,35 @@
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;
-
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,12 +224,12 @@
|> 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 *)
--- a/src/Pure/Pure.thy Sat May 28 17:35:12 2016 +0200
+++ b/src/Pure/Pure.thy Sat May 28 21:38:58 2016 +0200
@@ -351,11 +351,15 @@
(Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
>> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
+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 Sat May 28 17:35:12 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Sat May 28 21:38:58 2016 +0200
@@ -548,7 +548,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)))]))