--- a/NEWS Sat Mar 17 12:37:32 2012 +0000
+++ b/NEWS Sat Mar 17 16:13:41 2012 +0100
@@ -390,10 +390,13 @@
header declaration; it can be passed to Outer_Syntax.command etc.
* Local_Theory.define no longer hard-wires default theorem name
-"foo_def": definitional packages need to make this explicit, and may
-choose to omit theorem bindings for definitions by using
-Binding.empty/Attrib.empty_binding. Potential INCOMPATIBILITY for
-derived definitional packages.
+"foo_def", but retains the binding as given. If that is Binding.empty
+/ Attrib.empty_binding, the result is not registered as user-level
+fact. The Local_Theory.define_internal variant allows to specify a
+non-empty name (used for the foundation in the background theory),
+while omitting the fact binding in the user-context. Potential
+INCOMPATIBILITY for derived definitional packages: need to specify
+naming policy for primitive definitions more explicitly.
* Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
conformance with similar operations in structure Term and Logic.
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sat Mar 17 12:37:32 2012 +0000
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sat Mar 17 16:13:41 2012 +0100
@@ -1130,10 +1130,10 @@
lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
by (simp add: shift1_def)
lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
- by (induct k arbitrary: p, auto simp add: shift1_degree)
+ by (induct k arbitrary: p) (auto simp add: shift1_degree)
lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
- by (induct n arbitrary: p, simp_all add: funpow_def)
+ by (induct n arbitrary: p) (simp_all add: funpow.simps)
lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
by (induct p arbitrary: n rule: degree.induct, auto)
--- a/src/HOL/Tools/record.ML Sat Mar 17 12:37:32 2012 +0000
+++ b/src/HOL/Tools/record.ML Sat Mar 17 16:13:41 2012 +0100
@@ -2225,13 +2225,12 @@
Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
| T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
-fun prep_field prep (x, T, mx) = (x, prep T, mx)
- handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x);
-
-fun read_field raw_field ctxt =
- let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
- in (field, Variable.declare_typ T ctxt) end;
+fun read_fields raw_fields ctxt =
+ let
+ val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields);
+ val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts;
+ val ctxt' = fold Variable.declare_typ Ts ctxt;
+ in (fields, ctxt') end;
in
@@ -2252,7 +2251,11 @@
val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
val parents = get_parent_info thy parent;
- val bfields = map (prep_field cert_typ) raw_fields;
+ val bfields =
+ raw_fields |> map (fn (x, raw_T, mx) => (x, cert_typ raw_T, mx)
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x));
+
(* errors *)
@@ -2293,7 +2296,7 @@
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
val (parent, ctxt2) = read_parent raw_parent ctxt1;
- val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
+ val (fields, ctxt3) = read_fields raw_fields ctxt2;
val params' = map (Proof_Context.check_tfree ctxt3) params;
in thy |> add_record (params', binding) parent fields end;
--- a/src/Pure/Isar/generic_target.ML Sat Mar 17 12:37:32 2012 +0000
+++ b/src/Pure/Isar/generic_target.ML Sat Mar 17 16:13:41 2012 +0100
@@ -9,7 +9,7 @@
sig
val define: (((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory) ->
- (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+ bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
(Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
@@ -48,7 +48,7 @@
(* define *)
-fun define foundation ((b, mx), ((b_def, atts), rhs)) lthy =
+fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
let
val thy = Proof_Context.theory_of lthy;
val thy_ctxt = Proof_Context.init_global thy;
@@ -88,7 +88,8 @@
(*note*)
val ([(res_name, [res])], lthy4) = lthy3
- |> Local_Theory.notes_kind "" [((b_def, atts), [([def], [])])];
+ |> Local_Theory.notes_kind ""
+ [((if internal then Binding.empty else b_def, atts), [([def], [])])];
in ((lhs, (res_name, res)), lthy4) end;
--- a/src/Pure/Isar/local_theory.ML Sat Mar 17 12:37:32 2012 +0000
+++ b/src/Pure/Isar/local_theory.ML Sat Mar 17 16:13:41 2012 +0100
@@ -32,6 +32,8 @@
val global_morphism: local_theory -> morphism
val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
+ val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+ (term * (string * thm)) * local_theory
val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
local_theory -> (string * thm list) list * local_theory
@@ -63,7 +65,7 @@
(* type lthy *)
type operations =
- {define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+ {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory,
notes: string ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -195,7 +197,8 @@
val pretty = operation #pretty;
val abbrev = apsnd checkpoint ooo operation2 #abbrev;
-val define = apsnd checkpoint oo operation1 #define;
+val define = apsnd checkpoint oo operation2 #define false;
+val define_internal = apsnd checkpoint oo operation2 #define true;
val notes_kind = apsnd checkpoint ooo operation2 #notes;
val declaration = checkpoint ooo operation2 #declaration;
--- a/src/Pure/Isar/specification.ML Sat Mar 17 12:37:32 2012 +0000
+++ b/src/Pure/Isar/specification.ML Sat Mar 17 16:13:41 2012 +0100
@@ -119,7 +119,8 @@
val Asss =
(map o map) snd raw_specss
- |> (burrow o burrow) (Par_List.map_name "Specification.parse_prop" (parse_prop params_ctxt));
+ |> (burrow o burrow)
+ (grouped 10 (Par_List.map_name "Specification.parse_prop") (parse_prop params_ctxt));
val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
|> fold Name.declare xs;
val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
@@ -213,7 +214,7 @@
in (b, mx) end);
val name = Thm.def_binding_optional b raw_name;
val ((lhs, (_, raw_th)), lthy2) = lthy
- |> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs));
+ |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));
val th = prove lthy2 raw_th;
val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
--- a/src/Pure/Syntax/syntax.ML Sat Mar 17 12:37:32 2012 +0000
+++ b/src/Pure/Syntax/syntax.ML Sat Mar 17 16:13:41 2012 +0100
@@ -43,6 +43,7 @@
val read_typ: Proof.context -> string -> typ
val read_term: Proof.context -> string -> term
val read_prop: Proof.context -> string -> term
+ val read_typs: Proof.context -> string list -> typ list
val read_terms: Proof.context -> string list -> term list
val read_props: Proof.context -> string list -> term list
val read_sort_global: theory -> string -> sort
@@ -265,11 +266,17 @@
(* read = parse + check *)
fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
-fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
+
+fun read_typs ctxt =
+ grouped 10 (Par_List.map_name "Syntax.read_typs") (parse_typ ctxt) #> check_typs ctxt;
-fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt;
-fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt;
+fun read_terms ctxt =
+ grouped 10 (Par_List.map_name "Syntax.read_terms") (parse_term ctxt) #> check_terms ctxt;
+fun read_props ctxt =
+ grouped 10 (Par_List.map_name "Syntax.read_props") (parse_prop ctxt) #> check_props ctxt;
+
+val read_typ = singleton o read_typs;
val read_term = singleton o read_terms;
val read_prop = singleton o read_props;
--- a/src/Pure/Syntax/syntax_phases.ML Sat Mar 17 12:37:32 2012 +0000
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Mar 17 16:13:41 2012 +0100
@@ -360,7 +360,7 @@
val results' =
if parsed_len > 1 then
- (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
+ (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
check results
else results;
val reports' = fst (hd results');