clarified 'axiomatization';
authorwenzelm
Sat May 28 21:38:58 2016 +0200 (2016-05-28)
changeset 63178b9e1d53124f5
parent 63177 6c05c4632949
child 63179 231e261fd6bc
clarified 'axiomatization';
NEWS
src/Doc/Isar_Ref/Spec.thy
src/Doc/Tutorial/Misc/AdvancedInd.thy
src/HOL/Tools/BNF/bnf_axiomatization.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/specification.ML
src/Pure/Pure.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/NEWS	Sat May 28 17:35:12 2016 +0200
     1.2 +++ b/NEWS	Sat May 28 21:38:58 2016 +0200
     1.3 @@ -70,6 +70,10 @@
     1.4  eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
     1.5  'function'.
     1.6  
     1.7 +* Command 'axiomatization' has become more restrictive to correspond
     1.8 +better to internal axioms as singleton facts with mandatory name. Minor
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Toplevel theorem statements support eigen-context notation with 'if' /
    1.12  'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
    1.13  traditional long statement form (in prefix). Local premises are called
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat May 28 17:35:12 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat May 28 21:38:58 2016 +0200
     2.3 @@ -337,9 +337,12 @@
     2.4    \end{matharray}
     2.5  
     2.6    @{rail \<open>
     2.7 -    @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
     2.8 +    @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
     2.9      ;
    2.10 -    specs: (@{syntax thmdecl}? @{syntax props} + @'and')
    2.11 +    axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
    2.12 +      prems @{syntax for_fixes}
    2.13 +    ;
    2.14 +    prems: (@'if' ((@{syntax prop}+) + @'and'))?
    2.15    \<close>}
    2.16  
    2.17    \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
     3.1 --- a/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sat May 28 17:35:12 2016 +0200
     3.2 +++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sat May 28 21:38:58 2016 +0200
     3.3 @@ -133,7 +133,7 @@
     3.4  *}
     3.5  
     3.6  axiomatization f :: "nat \<Rightarrow> nat"
     3.7 -  where f_ax: "f(f(n)) < f(Suc(n))"
     3.8 +  where f_ax: "f(f(n)) < f(Suc(n))" for n :: nat
     3.9  
    3.10  text{*
    3.11  \begin{warn}
     4.1 --- a/src/HOL/Tools/BNF/bnf_axiomatization.ML	Sat May 28 17:35:12 2016 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML	Sat May 28 21:38:58 2016 +0200
     4.3 @@ -81,8 +81,10 @@
     4.4      val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     4.5      val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
     4.6  
     4.7 -    val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
     4.8 -      (Specification.axiomatization [] [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
     4.9 +    val (((_, raw_thms)), lthy) = Local_Theory.background_theory_result
    4.10 +      (Specification.axiomatization [] [] []
    4.11 +        (map_index (fn (i, ax) =>
    4.12 +          ((mk_b ("axiom" ^ string_of_int (i + 1)) Binding.empty, []), ax)) (flat all_goalss))) lthy;
    4.13  
    4.14      fun mk_wit_thms set_maps =
    4.15        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
     5.1 --- a/src/Pure/Isar/parse_spec.ML	Sat May 28 17:35:12 2016 +0200
     5.2 +++ b/src/Pure/Isar/parse_spec.ML	Sat May 28 21:38:58 2016 +0200
     5.3 @@ -15,7 +15,6 @@
     5.4    val spec: (string list * (Attrib.binding * string)) parser
     5.5    val multi_specs: Specification.multi_specs_cmd parser
     5.6    val where_multi_specs: Specification.multi_specs_cmd parser
     5.7 -  val specification: (string list * (Attrib.binding * string list) list) parser
     5.8    val constdecl: (binding * string option * mixfix) parser
     5.9    val includes: (xstring * Position.T) list parser
    5.10    val locale_fixes: (binding * string option * mixfix) list parser
    5.11 @@ -69,9 +68,6 @@
    5.12  
    5.13  val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
    5.14  
    5.15 -val specification =
    5.16 -  Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.prop) -- if_assumes >> swap;
    5.17 -
    5.18  
    5.19  (* basic constant specifications *)
    5.20  
     6.1 --- a/src/Pure/Isar/specification.ML	Sat May 28 17:35:12 2016 +0200
     6.2 +++ b/src/Pure/Isar/specification.ML	Sat May 28 21:38:58 2016 +0200
     6.3 @@ -25,16 +25,12 @@
     6.4      (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
     6.5    val read_multi_specs: (binding * string option * mixfix) list -> multi_specs_cmd -> Proof.context ->
     6.6      (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
     6.7 -  val check_specification: (binding * typ option * mixfix) list -> term list ->
     6.8 -    (Attrib.binding * term list) list -> Proof.context ->
     6.9 -    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    6.10 -  val read_specification: (binding * string option * mixfix) list -> string list ->
    6.11 -    (Attrib.binding * string list) list -> Proof.context ->
    6.12 -    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
    6.13 -  val axiomatization: (binding * typ option * mixfix) list -> term list ->
    6.14 -    (Attrib.binding * term list) list -> theory -> (term list * thm list list) * theory
    6.15 -  val axiomatization_cmd: (binding * string option * mixfix) list -> string list ->
    6.16 -    (Attrib.binding * string list) list -> theory -> (term list * thm list list) * theory
    6.17 +  val axiomatization: (binding * typ option * mixfix) list ->
    6.18 +    (binding * typ option * mixfix) list -> term list ->
    6.19 +    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
    6.20 +  val axiomatization_cmd: (binding * string option * mixfix) list ->
    6.21 +    (binding * string option * mixfix) list -> string list ->
    6.22 +    (Attrib.binding * string) list -> theory -> (term list * thm list) * theory
    6.23    val axiom: Attrib.binding * term -> theory -> thm * theory
    6.24    val definition: (binding * typ option * mixfix) option -> term list ->
    6.25      Attrib.binding * term -> local_theory -> (term * (string * thm)) * local_theory
    6.26 @@ -192,32 +188,35 @@
    6.27  fun read_multi_specs xs specs =
    6.28    prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs specs #>> #1;
    6.29  
    6.30 -fun check_specification xs As Bs =
    6.31 -  prepare Proof_Context.cert_var (K I) (K I) true xs [(Bs, As)] #>> #1;
    6.32 -
    6.33 -fun read_specification xs As Bs =
    6.34 -  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs [(Bs, As)] #>> #1;
    6.35 -
    6.36  end;
    6.37  
    6.38  
    6.39  (* axiomatization -- within global theory *)
    6.40  
    6.41 -fun gen_axioms prep raw_decls raw_prems raw_concls thy =
    6.42 +fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy =
    6.43    let
    6.44 -    val ((decls, specs), _) = prep raw_decls raw_prems raw_concls (Proof_Context.init_global thy);
    6.45 -    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) decls;
    6.46 +    (*specification*)
    6.47 +    val ((vars, [prems, concls], _, _), vars_ctxt) =
    6.48 +      Proof_Context.init_global thy
    6.49 +      |> prep_stmt (raw_decls @ raw_fixes) ((map o map) (rpair []) [raw_prems, map snd raw_concls]);
    6.50 +    val (decls, fixes) = chop (length raw_decls) vars;
    6.51 +
    6.52 +    val frees =
    6.53 +      rev ((fold o fold) (Variable.add_frees vars_ctxt) [prems, concls] [])
    6.54 +      |> map (fn (x, T) => (x, Free (x, T)));
    6.55 +    val close = Logic.close_prop (map #2 fixes @ frees) prems;
    6.56 +    val specs =
    6.57 +      map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls;
    6.58  
    6.59      (*consts*)
    6.60 -    val (consts, consts_thy) = thy |> fold_map Theory.specify_const decls;
    6.61 -    val subst = Term.subst_atomic (map Free xs ~~ consts);
    6.62 +    val (consts, consts_thy) = thy
    6.63 +      |> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls;
    6.64 +    val subst = Term.subst_atomic (map (#2 o #2) decls ~~ consts);
    6.65  
    6.66      (*axioms*)
    6.67 -    val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
    6.68 -        fold_map Thm.add_axiom_global
    6.69 -          (map (apfst (fn a => Binding.map_name (K a) b))
    6.70 -            (Global_Theory.name_multi (Binding.name_of b) (map subst props)))
    6.71 -        #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
    6.72 +    val (axioms, axioms_thy) =
    6.73 +      (specs, consts_thy) |-> fold_map (fn ((b, atts), prop) =>
    6.74 +        Thm.add_axiom_global (b, subst prop) #>> (fn (_, th) => ((b, atts), [([th], [])])));
    6.75  
    6.76      (*facts*)
    6.77      val (facts, facts_lthy) = axioms_thy
    6.78 @@ -225,12 +224,12 @@
    6.79        |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
    6.80        |> Local_Theory.notes axioms;
    6.81  
    6.82 -  in ((consts, map #2 facts), Local_Theory.exit_global facts_lthy) end;
    6.83 +  in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;
    6.84  
    6.85 -val axiomatization = gen_axioms check_specification;
    6.86 -val axiomatization_cmd = gen_axioms read_specification;
    6.87 +val axiomatization = gen_axioms Proof_Context.cert_stmt (K I);
    6.88 +val axiomatization_cmd = gen_axioms Proof_Context.read_stmt Attrib.check_src;
    6.89  
    6.90 -fun axiom (b, ax) = axiomatization [] [] [(b, [ax])] #>> (hd o hd o snd);
    6.91 +fun axiom (b, ax) = axiomatization [] [] [] [(b, ax)] #>> (hd o snd);
    6.92  
    6.93  
    6.94  (* definition *)
     7.1 --- a/src/Pure/Pure.thy	Sat May 28 17:35:12 2016 +0200
     7.2 +++ b/src/Pure/Pure.thy	Sat May 28 21:38:58 2016 +0200
     7.3 @@ -351,11 +351,15 @@
     7.4      (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
     7.5        >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
     7.6  
     7.7 +val axiomatization =
     7.8 +  Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --
     7.9 +  Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
    7.10 +
    7.11  val _ =
    7.12    Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
    7.13      (Scan.optional Parse.fixes [] --
    7.14 -      Scan.optional (Parse.where_ |-- Parse.!!! Parse_Spec.specification) ([], [])
    7.15 -      >> (fn (a, (b, c)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c)));
    7.16 +      Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
    7.17 +      >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
    7.18  
    7.19  in end\<close>
    7.20  
     8.1 --- a/src/Tools/Code/code_runtime.ML	Sat May 28 17:35:12 2016 +0200
     8.2 +++ b/src/Tools/Code/code_runtime.ML	Sat May 28 21:38:58 2016 +0200
     8.3 @@ -548,7 +548,7 @@
     8.4  fun add_definiendum (ml_name, (b, T)) thy =
     8.5    thy
     8.6    |> Code_Target.add_reserved target ml_name
     8.7 -  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] []
     8.8 +  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] []
     8.9    |-> (fn ([Const (const, _)], _) =>
    8.10      Code_Target.set_printings (Constant (const,
    8.11        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))