1.1 --- a/NEWS Sat Mar 17 12:37:32 2012 +0000
1.2 +++ b/NEWS Sat Mar 17 16:13:41 2012 +0100
1.3 @@ -390,10 +390,13 @@
1.4 header declaration; it can be passed to Outer_Syntax.command etc.
1.5
1.6 * Local_Theory.define no longer hard-wires default theorem name
1.7 -"foo_def": definitional packages need to make this explicit, and may
1.8 -choose to omit theorem bindings for definitions by using
1.9 -Binding.empty/Attrib.empty_binding. Potential INCOMPATIBILITY for
1.10 -derived definitional packages.
1.11 +"foo_def", but retains the binding as given. If that is Binding.empty
1.12 +/ Attrib.empty_binding, the result is not registered as user-level
1.13 +fact. The Local_Theory.define_internal variant allows to specify a
1.14 +non-empty name (used for the foundation in the background theory),
1.15 +while omitting the fact binding in the user-context. Potential
1.16 +INCOMPATIBILITY for derived definitional packages: need to specify
1.17 +naming policy for primitive definitions more explicitly.
1.18
1.19 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
1.20 conformance with similar operations in structure Term and Logic.
2.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sat Mar 17 12:37:32 2012 +0000
2.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sat Mar 17 16:13:41 2012 +0100
2.3 @@ -1130,10 +1130,10 @@
2.4 lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
2.5 by (simp add: shift1_def)
2.6 lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
2.7 - by (induct k arbitrary: p, auto simp add: shift1_degree)
2.8 + by (induct k arbitrary: p) (auto simp add: shift1_degree)
2.9
2.10 lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
2.11 - by (induct n arbitrary: p, simp_all add: funpow_def)
2.12 + by (induct n arbitrary: p) (simp_all add: funpow.simps)
2.13
2.14 lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
2.15 by (induct p arbitrary: n rule: degree.induct, auto)
3.1 --- a/src/HOL/Tools/record.ML Sat Mar 17 12:37:32 2012 +0000
3.2 +++ b/src/HOL/Tools/record.ML Sat Mar 17 16:13:41 2012 +0100
3.3 @@ -2225,13 +2225,12 @@
3.4 Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
3.5 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
3.6
3.7 -fun prep_field prep (x, T, mx) = (x, prep T, mx)
3.8 - handle ERROR msg =>
3.9 - cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x);
3.10 -
3.11 -fun read_field raw_field ctxt =
3.12 - let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
3.13 - in (field, Variable.declare_typ T ctxt) end;
3.14 +fun read_fields raw_fields ctxt =
3.15 + let
3.16 + val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields);
3.17 + val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts;
3.18 + val ctxt' = fold Variable.declare_typ Ts ctxt;
3.19 + in (fields, ctxt') end;
3.20
3.21 in
3.22
3.23 @@ -2252,7 +2251,11 @@
3.24 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
3.25 val parents = get_parent_info thy parent;
3.26
3.27 - val bfields = map (prep_field cert_typ) raw_fields;
3.28 + val bfields =
3.29 + raw_fields |> map (fn (x, raw_T, mx) => (x, cert_typ raw_T, mx)
3.30 + handle ERROR msg =>
3.31 + cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x));
3.32 +
3.33
3.34 (* errors *)
3.35
3.36 @@ -2293,7 +2296,7 @@
3.37 val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
3.38 val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
3.39 val (parent, ctxt2) = read_parent raw_parent ctxt1;
3.40 - val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
3.41 + val (fields, ctxt3) = read_fields raw_fields ctxt2;
3.42 val params' = map (Proof_Context.check_tfree ctxt3) params;
3.43 in thy |> add_record (params', binding) parent fields end;
3.44
4.1 --- a/src/Pure/Isar/generic_target.ML Sat Mar 17 12:37:32 2012 +0000
4.2 +++ b/src/Pure/Isar/generic_target.ML Sat Mar 17 16:13:41 2012 +0100
4.3 @@ -9,7 +9,7 @@
4.4 sig
4.5 val define: (((binding * typ) * mixfix) * (binding * term) ->
4.6 term list * term list -> local_theory -> (term * thm) * local_theory) ->
4.7 - (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
4.8 + bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
4.9 (term * (string * thm)) * local_theory
4.10 val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
4.11 (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
4.12 @@ -48,7 +48,7 @@
4.13
4.14 (* define *)
4.15
4.16 -fun define foundation ((b, mx), ((b_def, atts), rhs)) lthy =
4.17 +fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
4.18 let
4.19 val thy = Proof_Context.theory_of lthy;
4.20 val thy_ctxt = Proof_Context.init_global thy;
4.21 @@ -88,7 +88,8 @@
4.22
4.23 (*note*)
4.24 val ([(res_name, [res])], lthy4) = lthy3
4.25 - |> Local_Theory.notes_kind "" [((b_def, atts), [([def], [])])];
4.26 + |> Local_Theory.notes_kind ""
4.27 + [((if internal then Binding.empty else b_def, atts), [([def], [])])];
4.28 in ((lhs, (res_name, res)), lthy4) end;
4.29
4.30
5.1 --- a/src/Pure/Isar/local_theory.ML Sat Mar 17 12:37:32 2012 +0000
5.2 +++ b/src/Pure/Isar/local_theory.ML Sat Mar 17 16:13:41 2012 +0100
5.3 @@ -32,6 +32,8 @@
5.4 val global_morphism: local_theory -> morphism
5.5 val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
5.6 (term * (string * thm)) * local_theory
5.7 + val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
5.8 + (term * (string * thm)) * local_theory
5.9 val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
5.10 val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
5.11 local_theory -> (string * thm list) list * local_theory
5.12 @@ -63,7 +65,7 @@
5.13 (* type lthy *)
5.14
5.15 type operations =
5.16 - {define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
5.17 + {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
5.18 (term * (string * thm)) * local_theory,
5.19 notes: string ->
5.20 (Attrib.binding * (thm list * Attrib.src list) list) list ->
5.21 @@ -195,7 +197,8 @@
5.22
5.23 val pretty = operation #pretty;
5.24 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
5.25 -val define = apsnd checkpoint oo operation1 #define;
5.26 +val define = apsnd checkpoint oo operation2 #define false;
5.27 +val define_internal = apsnd checkpoint oo operation2 #define true;
5.28 val notes_kind = apsnd checkpoint ooo operation2 #notes;
5.29 val declaration = checkpoint ooo operation2 #declaration;
5.30
6.1 --- a/src/Pure/Isar/specification.ML Sat Mar 17 12:37:32 2012 +0000
6.2 +++ b/src/Pure/Isar/specification.ML Sat Mar 17 16:13:41 2012 +0100
6.3 @@ -119,7 +119,8 @@
6.4
6.5 val Asss =
6.6 (map o map) snd raw_specss
6.7 - |> (burrow o burrow) (Par_List.map_name "Specification.parse_prop" (parse_prop params_ctxt));
6.8 + |> (burrow o burrow)
6.9 + (grouped 10 (Par_List.map_name "Specification.parse_prop") (parse_prop params_ctxt));
6.10 val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
6.11 |> fold Name.declare xs;
6.12 val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
6.13 @@ -213,7 +214,7 @@
6.14 in (b, mx) end);
6.15 val name = Thm.def_binding_optional b raw_name;
6.16 val ((lhs, (_, raw_th)), lthy2) = lthy
6.17 - |> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs));
6.18 + |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));
6.19
6.20 val th = prove lthy2 raw_th;
6.21 val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
7.1 --- a/src/Pure/Syntax/syntax.ML Sat Mar 17 12:37:32 2012 +0000
7.2 +++ b/src/Pure/Syntax/syntax.ML Sat Mar 17 16:13:41 2012 +0100
7.3 @@ -43,6 +43,7 @@
7.4 val read_typ: Proof.context -> string -> typ
7.5 val read_term: Proof.context -> string -> term
7.6 val read_prop: Proof.context -> string -> term
7.7 + val read_typs: Proof.context -> string list -> typ list
7.8 val read_terms: Proof.context -> string list -> term list
7.9 val read_props: Proof.context -> string list -> term list
7.10 val read_sort_global: theory -> string -> sort
7.11 @@ -265,11 +266,17 @@
7.12 (* read = parse + check *)
7.13
7.14 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
7.15 -fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
7.16
7.17 -fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt;
7.18 -fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt;
7.19 +fun read_typs ctxt =
7.20 + grouped 10 (Par_List.map_name "Syntax.read_typs") (parse_typ ctxt) #> check_typs ctxt;
7.21
7.22 +fun read_terms ctxt =
7.23 + grouped 10 (Par_List.map_name "Syntax.read_terms") (parse_term ctxt) #> check_terms ctxt;
7.24 +
7.25 +fun read_props ctxt =
7.26 + grouped 10 (Par_List.map_name "Syntax.read_props") (parse_prop ctxt) #> check_props ctxt;
7.27 +
7.28 +val read_typ = singleton o read_typs;
7.29 val read_term = singleton o read_terms;
7.30 val read_prop = singleton o read_props;
7.31
8.1 --- a/src/Pure/Syntax/syntax_phases.ML Sat Mar 17 12:37:32 2012 +0000
8.2 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Mar 17 16:13:41 2012 +0100
8.3 @@ -360,7 +360,7 @@
8.4
8.5 val results' =
8.6 if parsed_len > 1 then
8.7 - (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
8.8 + (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
8.9 check results
8.10 else results;
8.11 val reports' = fst (hd results');