# HG changeset patch # User wenzelm # Date 1331997221 -3600 # Node ID b839e9fdf972badedeb449049382c0f9775912f1 # Parent 67cf9a6308f3be861caf68bcccee79010fdb2938# Parent eeea81b86b70516f9a641230e128b87591d5e758 merged diff -r 67cf9a6308f3 -r b839e9fdf972 NEWS --- 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. diff -r 67cf9a6308f3 -r b839e9fdf972 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- 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 \ 0\<^sub>p \ funpow n shift1 p \ 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) \ head p = p" by (induct p arbitrary: n rule: degree.induct, auto) diff -r 67cf9a6308f3 -r b839e9fdf972 src/HOL/Tools/record.ML --- 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; diff -r 67cf9a6308f3 -r b839e9fdf972 src/Pure/Isar/generic_target.ML --- 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; diff -r 67cf9a6308f3 -r b839e9fdf972 src/Pure/Isar/local_theory.ML --- 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; diff -r 67cf9a6308f3 -r b839e9fdf972 src/Pure/Isar/specification.ML --- 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]); diff -r 67cf9a6308f3 -r b839e9fdf972 src/Pure/Syntax/syntax.ML --- 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; diff -r 67cf9a6308f3 -r b839e9fdf972 src/Pure/Syntax/syntax_phases.ML --- 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');