# HG changeset patch # User wenzelm # Date 1464464338 -7200 # Node ID b9e1d53124f5348f090c98de1d61262b3eb827a8 # Parent 6c05c4632949059ce3693b10822475893618d7ef clarified 'axiomatization'; diff -r 6c05c4632949 -r b9e1d53124f5 NEWS --- 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 diff -r 6c05c4632949 -r b9e1d53124f5 src/Doc/Isar_Ref/Spec.thy --- 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 \ - @@{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'))? \} \<^descr> \<^theory_text>\axiomatization c\<^sub>1 \ c\<^sub>m where \\<^sub>1 \ \\<^sub>n\ introduces several constants diff -r 6c05c4632949 -r b9e1d53124f5 src/Doc/Tutorial/Misc/AdvancedInd.thy --- 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 \ 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} diff -r 6c05c4632949 -r b9e1d53124f5 src/HOL/Tools/BNF/bnf_axiomatization.ML --- 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) diff -r 6c05c4632949 -r b9e1d53124f5 src/Pure/Isar/parse_spec.ML --- 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 *) diff -r 6c05c4632949 -r b9e1d53124f5 src/Pure/Isar/specification.ML --- 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 *) diff -r 6c05c4632949 -r b9e1d53124f5 src/Pure/Pure.thy --- 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\ diff -r 6c05c4632949 -r b9e1d53124f5 src/Tools/Code/code_runtime.ML --- 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)))]))