--- a/doc-src/IsarImplementation/Thy/ML.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 21 16:51:45 2009 +0100
@@ -317,7 +317,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- @{ML "Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix
+ @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
-> theory -> term * theory"} \\
@{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Jan 20 19:09:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 21 16:51:45 2009 +0100
@@ -366,7 +366,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline%
+ \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
\verb| -> theory -> term * theory| \\
\verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Tue Jan 20 19:09:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Wed Jan 21 16:51:45 2009 +0100
@@ -325,9 +325,9 @@
\indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
- \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix ->|\isasep\isanewline%
+ \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
\verb| theory -> term * theory| \\
- \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Binding.T * term ->|\isasep\isanewline%
+ \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
\verb| theory -> (term * term) * theory| \\
\indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
\indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Jan 20 19:09:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Wed Jan 21 16:51:45 2009 +0100
@@ -816,13 +816,13 @@
\indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
\indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
\indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
- \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> Binding.T -> string| \\
+ \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
\end{mldecls}
\begin{mldecls}
\indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
\indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
\indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
- \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T| \\
+ \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
\indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
\indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/logic.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy Wed Jan 21 16:51:45 2009 +0100
@@ -323,9 +323,9 @@
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
- @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix ->
+ @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->
theory -> term * theory"} \\
- @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * term ->
+ @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->
theory -> (term * term) * theory"} \\
@{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
@{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
--- a/doc-src/IsarImplementation/Thy/prelim.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Wed Jan 21 16:51:45 2009 +0100
@@ -707,13 +707,13 @@
@{index_ML_type NameSpace.naming} \\
@{index_ML NameSpace.default_naming: NameSpace.naming} \\
@{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
- @{index_ML NameSpace.full_name: "NameSpace.naming -> Binding.T -> string"} \\
+ @{index_ML NameSpace.full_name: "NameSpace.naming -> binding -> string"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML_type NameSpace.T} \\
@{index_ML NameSpace.empty: NameSpace.T} \\
@{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
- @{index_ML NameSpace.declare: "NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T"} \\
+ @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T"} \\
@{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
@{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
\end{mldecls}
--- a/src/HOL/ATP_Linkup.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ATP_Linkup.thy
- ID: $Id$
Author: Lawrence C Paulson
Author: Jia Meng, NICTA
Author: Fabian Immler, TUM
--- a/src/HOL/Code_Eval.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Code_Eval.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Code_Eval.thy
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
*)
@@ -24,7 +23,7 @@
code_datatype Const App
class term_of = typerep +
- fixes term_of :: "'a \<Rightarrow> term"
+ fixes term_of :: "'a::{} \<Rightarrow> term"
lemma term_of_anything: "term_of x \<equiv> t"
by (rule eq_reflection) (cases "term_of x", cases t, simp)
--- a/src/HOL/Datatype.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Datatype.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Datatype.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
--- a/src/HOL/Finite_Set.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Finite_Set.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Finite_Set.thy
- ID: $Id$
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
with contributions by Jeremy Avigad
*)
--- a/src/HOL/FunDef.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/FunDef.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/FunDef.thy
- ID: $Id$
Author: Alexander Krauss, TU Muenchen
*)
--- a/src/HOL/Lattices.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Lattices.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Lattices.thy
- ID: $Id$
Author: Tobias Nipkow
*)
--- a/src/HOL/Nominal/nominal_induct.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Wed Jan 21 16:51:45 2009 +0100
@@ -6,7 +6,7 @@
structure NominalInduct:
sig
- val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list ->
+ val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
(string * typ) list -> (string * typ) list list -> thm list ->
thm list -> int -> RuleCases.cases_tactic
val nominal_induct_method: Method.src -> Proof.context -> Method.method
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Jan 21 16:51:45 2009 +0100
@@ -9,8 +9,8 @@
signature NOMINAL_PRIMREC =
sig
val add_primrec: term list option -> term option ->
- (Binding.T * typ option * mixfix) list ->
- (Binding.T * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> local_theory -> Proof.state
end;
--- a/src/HOL/Orderings.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Orderings.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Orderings.thy
- ID: $Id$
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson
*)
--- a/src/HOL/Tools/TFL/tfl.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Jan 21 16:51:45 2009 +0100
@@ -390,7 +390,7 @@
(wfrec $ map_types poly_tvars R)
$ functional
val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
- val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy
+ val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
in (thy', def) end;
end;
@@ -549,7 +549,7 @@
val ([def0], theory) =
thy
|> PureThy.add_defs false
- [Thm.no_attributes (fid ^ "_def", defn)]
+ [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
val def = Thm.freezeT def0;
val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
else ()
--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Jan 21 16:51:45 2009 +0100
@@ -238,7 +238,7 @@
(Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
- ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
+ (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
@@ -262,7 +262,7 @@
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
- |> PureThy.add_thmss [(("recs", rec_thms), [])]
+ |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [])]
||> Sign.parent_path
||> Theory.checkpoint
|-> (fn thms => pair (reccomb_names, Library.flat thms))
@@ -316,7 +316,7 @@
fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn);
- val def = ((Sign.base_name name) ^ "_def",
+ val def = (Binding.name (Sign.base_name name ^ "_def"),
Logic.mk_equals (list_comb (Const (name, caseT), fns1),
list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
--- a/src/HOL/Tools/datatype_aux.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Wed Jan 21 16:51:45 2009 +0100
@@ -76,7 +76,7 @@
fun store_thmss_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
Sign.add_path tname
- #> PureThy.add_thmss [((label, thms), atts)]
+ #> PureThy.add_thmss [((Binding.name label, thms), atts)]
#-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
@@ -85,7 +85,7 @@
fun store_thms_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
Sign.add_path tname
- #> PureThy.add_thms [((label, thms), atts)]
+ #> PureThy.add_thms [((Binding.name label, thms), atts)]
#-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
--- a/src/HOL/Tools/datatype_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -196,13 +196,13 @@
fun add_rules simps case_thms rec_thms inject distinct
weak_case_congs cong_att =
- PureThy.add_thmss [(("simps", simps), []),
- (("", flat case_thms @
+ PureThy.add_thmss [((Binding.name "simps", simps), []),
+ ((Binding.empty, flat case_thms @
flat distinct @ rec_thms), [Simplifier.simp_add]),
- (("", rec_thms), [Code.add_default_eqn_attribute]),
- (("", flat inject), [iff_add]),
- (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
- (("", weak_case_congs), [cong_att])]
+ ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
+ ((Binding.empty, flat inject), [iff_add]),
+ ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
+ ((Binding.empty, weak_case_congs), [cong_att])]
#> snd;
@@ -213,15 +213,15 @@
val inducts = ProjectRule.projections (ProofContext.init thy) induction;
fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
- [(("", nth inducts index), [Induct.induct_type name]),
- (("", exhaustion), [Induct.cases_type name])];
+ [((Binding.empty, nth inducts index), [Induct.induct_type name]),
+ ((Binding.empty, exhaustion), [Induct.cases_type name])];
fun unnamed_rule i =
- (("", nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
+ ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
in
thy |> PureThy.add_thms
(maps named_rules infos @
map unnamed_rule (length infos upto length inducts - 1)) |> snd
- |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd
+ |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
end;
@@ -451,7 +451,7 @@
|> store_thmss "inject" new_type_names inject
||>> store_thmss "distinct" new_type_names distinct
||> Sign.add_path (space_implode "_" new_type_names)
- ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])];
+ ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
--- a/src/HOL/Tools/datatype_realizer.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Jan 21 16:51:45 2009 +0100
@@ -130,7 +130,7 @@
val vs = map (fn i => List.nth (pnames, i)) is;
val (thm', thy') = thy
|> Sign.absolute_path
- |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm)
+ |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
@@ -196,7 +196,7 @@
val exh_name = Thm.get_name exhaustion;
val (thm', thy') = thy
|> Sign.absolute_path
- |> PureThy.store_thm (exh_name ^ "_P_correctness", thm)
+ |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm)
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Jan 21 16:51:45 2009 +0100
@@ -242,7 +242,7 @@
val ([def_thm], thy') =
thy
|> Sign.add_consts_i [(cname', constrT, mx)]
- |> (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)];
+ |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
@@ -343,7 +343,7 @@
val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
val fTs = map fastype_of fs;
- val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
+ val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Sign.base_name iso_name ^ "_def"),
Logic.mk_equals (Const (iso_name, T --> Univ_elT),
list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
val (def_thms, thy') =
@@ -631,7 +631,7 @@
val ([dt_induct'], thy7) =
thy6
|> Sign.add_path big_name
- |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
+ |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
||> Sign.parent_path
||> Theory.checkpoint;
--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -9,14 +9,14 @@
signature FUNDEF_PACKAGE =
sig
- val add_fundef : (Binding.T * string option * mixfix) list
+ val add_fundef : (binding * string option * mixfix) list
-> (Attrib.binding * string) list
-> FundefCommon.fundef_config
-> bool list
-> local_theory
-> Proof.state
- val add_fundef_i: (Binding.T * typ option * mixfix) list
+ val add_fundef_i: (binding * typ option * mixfix) list
-> (Attrib.binding * term) list
-> FundefCommon.fundef_config
-> bool list
--- a/src/HOL/Tools/function_package/size.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Wed Jan 21 16:51:45 2009 +0100
@@ -144,7 +144,7 @@
(size_names ~~ recTs1))
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
- (def_names ~~ (size_fns ~~ rec_combs1)))
+ (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
||> TheoryTarget.instantiation
(map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
||>> fold_map define_overloaded
@@ -208,7 +208,7 @@
prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
val ([size_thms], thy'') = PureThy.add_thmss
- [(("size", size_eqns),
+ [((Binding.name "size", size_eqns),
[Simplifier.simp_add, Thm.declaration_attribute
(fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
--- a/src/HOL/Tools/inductive_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -38,17 +38,17 @@
thm list list * local_theory
type inductive_flags
val add_inductive_i:
- inductive_flags -> ((Binding.T * typ) * mixfix) list ->
+ inductive_flags -> ((binding * typ) * mixfix) list ->
(string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
inductive_result * local_theory
val add_inductive: bool -> bool ->
- (Binding.T * string option * mixfix) list ->
- (Binding.T * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
(Attrib.binding * string) list ->
(Facts.ref * Attrib.src list) list ->
bool -> local_theory -> inductive_result * local_theory
val add_inductive_global: string -> inductive_flags ->
- ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+ ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> theory -> inductive_result * theory
val arities_of: thm -> (string * int) list
val params_of: thm -> term list
@@ -63,16 +63,16 @@
sig
include BASIC_INDUCTIVE_PACKAGE
type add_ind_def
- val declare_rules: string -> Binding.T -> bool -> bool -> string list ->
- thm list -> Binding.T list -> Attrib.src list list -> (thm * string list) list ->
+ val declare_rules: string -> binding -> bool -> bool -> string list ->
+ thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
thm -> local_theory -> thm list * thm list * thm * local_theory
val add_ind_def: add_ind_def
val gen_add_inductive_i: add_ind_def -> inductive_flags ->
- ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+ ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> local_theory -> inductive_result * local_theory
val gen_add_inductive: add_ind_def -> bool -> bool ->
- (Binding.T * string option * mixfix) list ->
- (Binding.T * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
bool -> local_theory -> inductive_result * local_theory
val gen_ind_decl: add_ind_def -> bool ->
@@ -720,13 +720,13 @@
in (intrs', elims', induct', ctxt3) end;
type inductive_flags =
- {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
+ {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
type add_ind_def =
inductive_flags ->
term list -> (Attrib.binding * term) list -> thm list ->
- term list -> (Binding.T * mixfix) list ->
+ term list -> (binding * mixfix) list ->
local_theory -> inductive_result * local_theory
fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Jan 21 16:51:45 2009 +0100
@@ -391,14 +391,14 @@
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
[K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
- val (thm', thy') = PureThy.store_thm (space_implode "_"
- (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
+ val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
+ (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
(DatatypeAux.split_conj_thm thm');
val ([thms'], thy'') = PureThy.add_thmss
- [((space_implode "_"
+ [((Binding.name (space_implode "_"
(NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
- ["correctness"]), thms), [])] thy';
+ ["correctness"])), thms), [])] thy';
val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
in
Extraction.add_realizers_i
@@ -451,8 +451,8 @@
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
- val (thm', thy') = PureThy.store_thm (space_implode "_"
- (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
+ val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
+ (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
in
Extraction.add_realizers_i
[mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
--- a/src/HOL/Tools/inductive_set_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -12,13 +12,13 @@
val pred_set_conv_att: attribute
val add_inductive_i:
InductivePackage.inductive_flags ->
- ((Binding.T * typ) * mixfix) list ->
+ ((binding * typ) * mixfix) list ->
(string * typ) list ->
(Attrib.binding * term) list -> thm list ->
local_theory -> InductivePackage.inductive_result * local_theory
val add_inductive: bool -> bool ->
- (Binding.T * string option * mixfix) list ->
- (Binding.T * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
bool -> local_theory -> InductivePackage.inductive_result * local_theory
val codegen_preproc: theory -> thm list -> thm list
--- a/src/HOL/Tools/old_primrec_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -305,11 +305,11 @@
end;
fun thy_note ((name, atts), thms) =
- PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
+ PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
fun thy_def false ((name, atts), t) =
- PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+ PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
| thy_def true ((name, atts), t) =
- PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+ PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
in
--- a/src/HOL/Tools/primrec_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -7,12 +7,12 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec: (Binding.T * typ option * mixfix) list ->
+ val add_primrec: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> local_theory -> thm list * local_theory
- val add_primrec_global: (Binding.T * typ option * mixfix) list ->
+ val add_primrec_global: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
val add_primrec_overloaded: (string * (string * typ) * bool) list ->
- (Binding.T * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
end;
--- a/src/HOL/Tools/recdef_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/recdef_package.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Wrapper module for Konrad Slind's TFL package.
@@ -16,10 +15,10 @@
val cong_del: attribute
val wf_add: attribute
val wf_del: attribute
- val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
+ val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
Attrib.src option -> theory -> theory
* {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
- val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
+ val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
-> theory -> theory * {induct_rules: thm}
@@ -214,8 +213,8 @@
thy
|> Sign.add_path bname
|> PureThy.add_thmss
- ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
- ||>> PureThy.add_thms [(("induct", induct), [])];
+ (((Binding.name "simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
+ ||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy =
thy
@@ -243,7 +242,7 @@
val ([induct_rules'], thy3) =
thy2
|> Sign.add_path bname
- |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
+ |> PureThy.add_thms [((Binding.name "induct_rules", induct_rules), [])]
||> Sign.parent_path;
in (thy3, {induct_rules = induct_rules'}) end;
@@ -299,7 +298,7 @@
val recdef_decl =
Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
+ P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
-- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
--- a/src/HOL/Tools/record_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/record_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1534,8 +1534,10 @@
|> extension_typedef name repT (alphas@[zeta])
||> Sign.add_consts_i
(map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
- ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
- ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
+ ||>> PureThy.add_defs false
+ (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
+ ||>> PureThy.add_defs false
+ (map (Thm.no_attributes o apfst Binding.name) upd_specs)
|-> (fn args as ((_, dest_defs), upd_defs) =>
fold Code.add_default_eqn dest_defs
#> fold Code.add_default_eqn upd_defs
@@ -1693,14 +1695,14 @@
[dest_convs',upd_convs']),
thm_thy) =
defs_thy
- |> (PureThy.add_thms o map Thm.no_attributes)
+ |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
[("ext_inject", inject),
("ext_induct", induct),
("ext_cases", cases),
("ext_surjective", surjective),
("ext_split", split_meta)]
- ||>> (PureThy.add_thmss o map Thm.no_attributes)
- [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)]
+ ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
+ [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)]
in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
end;
@@ -1938,9 +1940,9 @@
(map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
|> (Sign.add_consts_i o map Syntax.no_syn)
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
- |> ((PureThy.add_defs false o map Thm.no_attributes) sel_specs)
- ||>> ((PureThy.add_defs false o map Thm.no_attributes) upd_specs)
- ||>> ((PureThy.add_defs false o map Thm.no_attributes)
+ |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
+ ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
+ ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
[make_spec, fields_spec, extend_spec, truncate_spec])
|-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
fold Code.add_default_eqn sel_defs
@@ -2164,17 +2166,17 @@
val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'],
[surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) =
defs_thy
- |> (PureThy.add_thmss o map Thm.no_attributes)
+ |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
[("select_convs", sel_convs_standard),
("update_convs", upd_convs),
("select_defs", sel_defs),
("update_defs", upd_defs),
("splits", [split_meta_standard,split_object,split_ex]),
("defs", derived_defs)]
- ||>> (PureThy.add_thms o map Thm.no_attributes)
+ ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
[("surjective", surjective),
("equality", equality)]
- ||>> PureThy.add_thms
+ ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name)
[(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
(("induct", induct), induct_type_global name),
(("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
@@ -2186,8 +2188,8 @@
val final_thy =
thms_thy
|> (snd oo PureThy.add_thmss)
- [(("simps", sel_upd_simps), [Simplifier.simp_add]),
- (("iffs",iffs), [iff_add])]
+ [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
+ ((Binding.name "iffs", iffs), [iff_add])]
|> put_record name (make_record_info args parent fields extension induct_scheme')
|> put_sel_upd (names @ [full_moreN]) sel_upd_simps
|> add_record_equalities extension_id equality'
--- a/src/HOL/Tools/res_axioms.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Wed Jan 21 16:51:45 2009 +0100
@@ -84,7 +84,7 @@
val (c, thy') =
Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy
val cdef = cname ^ "_def"
- val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
+ val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
| dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
--- a/src/HOL/Tools/specification_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -28,7 +28,7 @@
else thname
val def_eq = Logic.mk_equals (Const(cname_full,ctype),
HOLogic.choice_const ctype $ P)
- val (thms, thy') = PureThy.add_defs covld [((cdefname,def_eq),[])] thy
+ val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
val thm' = [thm,hd thms] MRS @{thm exE_some}
in
mk_definitional cos (thy',thm')
@@ -39,7 +39,7 @@
let
fun process [] (thy,tm) =
let
- val (thms, thy') = PureThy.add_axioms [((axname,HOLogic.mk_Trueprop tm),[])] thy
+ val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy
in
(thy',hd thms)
end
@@ -184,7 +184,7 @@
if name = ""
then arg |> Library.swap
else (writeln (" " ^ name ^ ": " ^ (Display.string_of_thm thm));
- PureThy.store_thm (name, thm) thy)
+ PureThy.store_thm (Binding.name name, thm) thy)
in
args |> apsnd (remove_alls frees)
|> apsnd undo_imps
--- a/src/HOL/Tools/typedef_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Tools/typedef_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -112,7 +112,8 @@
if def then
theory
|> Sign.add_consts_i [(name, setT', NoSyn)]
- |> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))]
+ |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
+ (PrimitiveDefs.mk_defpair (setC, set)))]
|-> (fn [th] => pair (SOME th))
else (NONE, theory);
fun contract_def NONE th = th
@@ -130,7 +131,7 @@
(Abs_name, oldT --> newT, NoSyn)]
#> add_def
#-> (fn set_def =>
- PureThy.add_axioms [((typedef_name, typedef_prop),
+ PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
[Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
##>> pair set_def)
##> Theory.add_deps "" (dest_Const RepC) typedef_deps
@@ -143,7 +144,7 @@
thy1
|> Sign.add_path name
|> PureThy.add_thms
- ([((Rep_name, make @{thm type_definition.Rep}), []),
+ ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []),
((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
--- a/src/HOL/Typerep.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Typerep.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
-(* Title: HOL/Library/RType.thy
- ID: $Id$
+(* Title: HOL/Typerep.thy
Author: Florian Haftmann, TU Muenchen
*)
@@ -15,9 +14,7 @@
fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep"
begin
-definition
- typerep_of :: "'a \<Rightarrow> typerep"
-where
+definition typerep_of :: "'a \<Rightarrow> typerep" where
[simp]: "typerep_of x = typerep TYPE('a)"
end
--- a/src/HOL/Wellfounded.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/Wellfounded.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
-(* ID: $Id$
- Author: Tobias Nipkow
+(* Author: Tobias Nipkow
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Konrad Slind, Alexander Krauss
Copyright 1992-2008 University of Cambridge and TU Muenchen
--- a/src/HOL/ex/Quickcheck.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOL/ex/Quickcheck.thy Wed Jan 21 16:51:45 2009 +0100
@@ -200,7 +200,7 @@
in
lthy
|> LocalTheory.theory (Code.del_eqns c
- #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
+ #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal])
#-> Code.add_eqn)
end;
in
--- a/src/HOLCF/Tools/fixrec_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -9,9 +9,9 @@
val legacy_infer_term: theory -> term -> term
val legacy_infer_prop: theory -> term -> term
val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
- val add_fixrec_i: bool -> ((Binding.T * attribute list) * term) list list -> theory -> theory
+ val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory
val add_fixpat: Attrib.binding * string list -> theory -> theory
- val add_fixpat_i: (Binding.T * attribute list) * term list -> theory -> theory
+ val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
end;
structure FixrecPackage: FIXREC_PACKAGE =
--- a/src/Pure/General/binding.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/General/binding.ML Wed Jan 21 16:51:45 2009 +0100
@@ -6,6 +6,7 @@
signature BASIC_BINDING =
sig
+ type binding
val long_names: bool ref
val short_names: bool ref
val unique_names: bool ref
@@ -92,6 +93,8 @@
else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
end;
+type binding = T;
+
end;
structure Basic_Binding : BASIC_BINDING = Binding;
--- a/src/Pure/General/name_space.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/General/name_space.ML Wed Jan 21 16:51:45 2009 +0100
@@ -3,9 +3,10 @@
Generic name spaces with declared and hidden entries. Unknown names
are considered global; no support for absolute addressing.
+Cf. Pure/General/binding.ML
*)
-type bstring = string; (*names to be bound*)
+type bstring = string; (*simple names to be bound -- legacy*)
type xstring = string; (*external names*)
signature NAME_SPACE =
@@ -31,8 +32,8 @@
val merge: T * T -> T
type naming
val default_naming: naming
- val declare: naming -> Binding.T -> T -> string * T
- val full_name: naming -> Binding.T -> string
+ val declare: naming -> binding -> T -> string * T
+ val full_name: naming -> binding -> string
val external_names: naming -> string -> string list
val path_of: naming -> string
val add_path: string -> naming -> naming
@@ -41,7 +42,7 @@
val sticky_prefix: string -> naming -> naming
type 'a table = T * 'a Symtab.table
val empty_table: 'a table
- val bind: naming -> Binding.T * 'a
+ val bind: naming -> binding * 'a
-> 'a table -> string * 'a table (*exception Symtab.DUP*)
val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
val join_tables: (string -> 'a * 'a -> 'a)
--- a/src/Pure/IsaMakefile Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/IsaMakefile Wed Jan 21 16:51:45 2009 +0100
@@ -41,7 +41,7 @@
Isar/expression.ML Isar/find_theorems.ML Isar/isar.ML \
Isar/isar_document.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
- Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/old_locale.ML \
+ Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
@@ -75,7 +75,7 @@
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \
Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML \
- Thy/thy_syntax.ML Tools/ROOT.ML Tools/invoke.ML \
+ Thy/thy_syntax.ML Tools/ROOT.ML \
Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \
assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
--- a/src/Pure/Isar/ROOT.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/ROOT.ML Wed Jan 21 16:51:45 2009 +0100
@@ -53,7 +53,6 @@
(*local theories and targets*)
use "local_theory.ML";
use "overloading.ML";
-use "old_locale.ML";
use "locale.ML";
use "class_target.ML";
use "theory_target.ML";
--- a/src/Pure/Isar/args.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/args.ML Wed Jan 21 16:51:45 2009 +0100
@@ -35,7 +35,7 @@
val name_source: T list -> string * T list
val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
val name: T list -> string * T list
- val binding: T list -> Binding.T * T list
+ val binding: T list -> binding * T list
val alt_name: T list -> string * T list
val symbol: T list -> string * T list
val liberal_name: T list -> string * T list
@@ -66,8 +66,8 @@
val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
val attribs: (string -> string) -> T list -> src list * T list
val opt_attribs: (string -> string) -> T list -> src list * T list
- val thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
- val opt_thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
+ val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
+ val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
src -> Proof.context -> 'a * Proof.context
--- a/src/Pure/Isar/attrib.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Jan 21 16:51:45 2009 +0100
@@ -7,7 +7,7 @@
signature ATTRIB =
sig
type src = Args.src
- type binding = Binding.T * src list
+ type binding = binding * src list
val empty_binding: binding
val print_attributes: theory -> unit
val intern: theory -> xstring -> string
@@ -54,7 +54,7 @@
type src = Args.src;
-type binding = Binding.T * src list;
+type binding = binding * src list;
val empty_binding: binding = (Binding.empty, []);
--- a/src/Pure/Isar/calculation.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Jan 21 16:51:45 2009 +0100
@@ -98,8 +98,8 @@
("sym", sym_att, "declaration of symmetry rule"),
("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
PureThy.add_thms
- [(("", transitive_thm), [trans_add]),
- (("", symmetric_thm), [sym_add])] #> snd));
+ [((Binding.empty, transitive_thm), [trans_add]),
+ ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
--- a/src/Pure/Isar/class.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/class.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/Isar/ML
Author: Florian Haftmann, TU Muenchen
-Type classes derived from primitive axclasses and locales - interfaces
+Type classes derived from primitive axclasses and locales - interfaces.
*)
signature CLASS =
@@ -34,7 +34,7 @@
(* instantiation of canonical interpretation *)
(*FIXME inst_morph should be calculated manually and not instantiate constraint*)
- val aT = TFree ("'a", base_sort);
+ val aT = TFree (Name.aT, base_sort);
val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
|> Expression.cert_goal_expression ([(class, (("", false),
Expression.Named ((map o apsnd) Const param_map)))], []);
@@ -89,7 +89,88 @@
in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
-fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
+fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
+ let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
+
+fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
+ if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort)
+ else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi)
+ (*FIXME does not occur*)
+ | T as TFree (v, sort) =>
+ if v = Name.aT then T
+ else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification"));
+
+val singleton_fixate = (map o map_atyps) (fn TVar (vi, sort)
+ => TFree (Name.aT, sort) | T => T);
+
+fun add_tfrees_of_element (Element.Fixes fxs) = fold (fn (_, SOME T, _) => Term.add_tfreesT T
+ | _ => I) fxs
+ | add_tfrees_of_element (Element.Constrains cnstrs) = fold (Term.add_tfreesT o snd) cnstrs
+ | add_tfrees_of_element (Element.Assumes assms) = fold (fold (fn (t, ts) =>
+ Term.add_tfrees t #> fold Term.add_tfrees ts) o snd) assms
+ | add_tfrees_of_element _ = I;
+
+fun fork_syn (Element.Fixes xs) =
+ fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
+ #>> Element.Fixes
+ | fork_syn x = pair x;
+
+fun prep_class_spec prep_class prep_decl thy raw_supclasses raw_elems =
+ let
+ (* prepare import *)
+ val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
+ val (sups, others_basesort) = map (prep_class thy) raw_supclasses
+ |> Sign.minimize_sort thy
+ |> List.partition (is_class thy);
+
+ val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+ val supparam_names = map fst supparams;
+ val _ = if has_duplicates (op =) supparam_names
+ then error ("Duplicate parameter(s) in superclasses: "
+ ^ (commas o map quote o duplicates (op =)) supparam_names)
+ else ();
+ val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
+ sups, []);
+ val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort;
+
+ (* infer types and base sort *)
+ val base_constraints = (map o apsnd)
+ (map_type_tfree (K (TVar ((Name.aT, 0), given_basesort))) o fst o snd)
+ (these_operations thy sups);
+ val ((_, _, inferred_elems), _) = ProofContext.init thy
+ |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
+ |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort))
+ |> add_typ_check ~2 "singleton_fixate" singleton_fixate
+ |> prep_decl supexpr raw_elems;
+ (*FIXME propagation of given base sort into class spec broken*)
+ (*FIXME check for *all* side conditions here, extra check function for elements,
+ less side-condition checks in check phase*)
+ val base_sort = if null inferred_elems then given_basesort else
+ case fold add_tfrees_of_element inferred_elems []
+ of [] => error "No type variable in class specification"
+ | [(_, sort)] => sort
+ | _ => error "Multiple type variables in class specification"
+ val sup_sort = inter_sort base_sort sups
+
+ (* process elements as class specification *)
+ val begin_ctxt = begin sups base_sort
+ #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
+ (K (TFree (Name.aT, base_sort))) supparams)
+ (*FIXME should constraints be issued in begin?*)
+ val ((_, _, syntax_elems), _) = ProofContext.init thy
+ |> begin_ctxt
+ |> Expression.cert_declaration supexpr inferred_elems;
+ val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
+ val constrain = Element.Constrains ((map o apsnd o map_atyps)
+ (K (TFree (Name.aT, base_sort))) supparams);
+ (*FIXME 2009 perhaps better: control type variable by explicit
+ parameter instantiation of import expression*)
+ in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
+
+val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
+val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
+
+(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
let
(*FIXME 2009 simplify*)
val supclasses = map (prep_class thy) raw_supclasses;
@@ -126,7 +207,7 @@
in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
-val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
+val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*)
fun add_consts bname class base_sort sups supparams global_syntax thy =
let
@@ -235,19 +316,13 @@
#> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
in do_proof after_qed some_prop goal_ctxt end;
-fun user_proof after_qed NONE =
- Proof.theorem_i NONE (K (after_qed NONE)) [[]]
- #> Element.refine_witness #> Seq.hd
- | user_proof after_qed (SOME prop) =
- Proof.theorem_i NONE (after_qed o SOME o Element.make_witness prop
- o Thm.close_derivation o the_single o the_single)
- [[(Element.mark_witness prop, [])]]
- #> Element.refine_witness #> Seq.hd;
+fun user_proof after_qed some_prop =
+ Element.witness_proof (after_qed o try the_single o the_single)
+ [the_list some_prop];
-fun tactic_proof tac after_qed NONE ctxt =
- after_qed NONE ctxt
- | tactic_proof tac after_qed (SOME prop) ctxt =
- after_qed (SOME (Element.prove_witness ctxt prop tac)) ctxt;
+fun tactic_proof tac after_qed some_prop ctxt =
+ after_qed (Option.map
+ (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt;
in
--- a/src/Pure/Isar/class_target.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Wed Jan 21 16:51:45 2009 +0100
@@ -18,6 +18,7 @@
val rules: theory -> class -> thm option * thm
val these_params: theory -> sort -> (string * (class * (string * typ))) list
val these_defs: theory -> sort -> thm list
+ val these_operations: theory -> sort -> (string * (class * (typ * term))) list
val print_classes: theory -> unit
val begin: class list -> sort -> Proof.context -> Proof.context
@@ -253,7 +254,6 @@
in fold amend (heritage thy [class]) thy end;
fun register_operation class (c, (t, some_def)) thy =
- (*FIXME 2009 does this still also work for abbrevs?*)
let
val base_sort = base_sort thy class;
val prep_typ = map_type_tfree
@@ -297,11 +297,14 @@
(* class context syntax *)
-fun synchronize_class_syntax sups base_sort ctxt =
+fun these_unchecks thy =
+ map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
+
+fun synchronize_class_syntax sort base_sort ctxt =
let
val thy = ProofContext.theory_of ctxt;
val algebra = Sign.classes_of thy;
- val operations = these_operations thy sups;
+ val operations = these_operations thy sort;
fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
val primary_constraints =
(map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
@@ -322,7 +325,7 @@
| NONE => NONE)
| NONE => NONE)
fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
- val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
+ val unchecks = these_unchecks thy sort;
in
ctxt
|> fold declare_const primary_constraints
@@ -337,11 +340,11 @@
val base_sort = base_sort thy class;
in synchronize_class_syntax [class] base_sort ctxt end;
-fun begin sups base_sort ctxt =
+fun begin sort base_sort ctxt =
ctxt
|> Variable.declare_term
(Logic.mk_type (TFree (Name.aT, base_sort)))
- |> synchronize_class_syntax sups base_sort
+ |> synchronize_class_syntax sort base_sort
|> Overloading.add_improvable_syntax;
fun init class thy =
@@ -356,52 +359,42 @@
fun declare class pos ((c, mx), dict) thy =
let
- val prfx = class_prefix class;
- val thy' = thy |> Sign.add_path prfx;
- (*FIXME 2009 use proper name morphism*)
- val morph = morphism thy' class;
- val params = map (apsnd fst o snd) (these_params thy' [class]);
-
- val c' = Sign.full_bname thy' c;
+ val morph = morphism thy class;
+ val b = Morphism.binding morph (Binding.name c);
+ val b_def = Morphism.binding morph (Binding.name (c ^ "_dict"));
+ val c' = Sign.full_name thy b;
val dict' = Morphism.term morph dict;
val ty' = Term.fastype_of dict';
- val ty'' = Type.strip_sorts ty';
- (*FIXME 2009 the tinkering with theorems here is a mess*)
- val def_eq = Logic.mk_equals (Const (c', ty'), dict');
- fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
+ val def_eq = Logic.mk_equals (Const (c', ty'), dict')
+ |> map_types Type.strip_sorts;
in
- thy'
- |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
- |> Thm.add_def false false (c, def_eq) (*FIXME 2009 name of theorem*)
- (*FIXME 2009 add_def should accept binding*)
- |>> Thm.symmetric
- ||>> get_axiom
- |-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def')))
- #> PureThy.store_thm (c ^ "_raw", def') (*FIXME 2009 name of theorem*)
- (*FIXME 2009 store_thm etc. should accept binding*)
- #> snd)
- |> Sign.restore_naming thy
+ thy
+ |> Sign.declare_const pos ((b, Type.strip_sorts ty'), mx)
+ |> snd
+ |> Thm.add_def false false (b_def, def_eq)
+ |>> Thm.varifyT
+ |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
+ #> snd
+ #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
|> Sign.add_const_constraint (c', SOME ty')
end;
fun abbrev class prmode pos ((c, mx), rhs) thy =
let
- val prfx = class_prefix class;
- val thy' = thy |> Sign.add_path prfx;
-
- val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
- (these_operations thy [class]);
- val c' = Sign.full_bname thy' c;
+ val morph = morphism thy class;
+ val unchecks = these_unchecks thy [class];
+ val b = Morphism.binding morph (Binding.name c);
+ val c' = Sign.full_name thy b;
val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
- val rhs'' = map_types Logic.varifyT rhs';
val ty' = Term.fastype_of rhs';
+ val rhs'' = map_types ((*Type.strip_sorts o *)Logic.varifyT) rhs';
in
- thy'
- |> Sign.add_abbrev (#1 prmode) pos (Binding.name c, map_types Type.strip_sorts rhs'') |> snd
+ thy
+ |> Sign.add_abbrev (#1 prmode) pos (b, rhs'')
+ |> snd
|> Sign.add_const_constraint (c', SOME ty')
|> Sign.notation true prmode [(Const (c', ty'), mx)]
|> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
- |> Sign.restore_naming thy
end;
@@ -610,8 +603,7 @@
end;
fun default_intro_tac ctxt [] =
- intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
- Locale.intro_locales_tac true ctxt []
+ intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
| default_intro_tac _ _ = no_tac;
fun default_tac rules ctxt facts =
--- a/src/Pure/Isar/constdefs.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Wed Jan 21 16:51:45 2009 +0100
@@ -8,12 +8,12 @@
signature CONSTDEFS =
sig
- val add_constdefs: (Binding.T * string option) list *
- ((Binding.T * string option * mixfix) option *
+ val add_constdefs: (binding * string option) list *
+ ((binding * string option * mixfix) option *
(Attrib.binding * string)) list -> theory -> theory
- val add_constdefs_i: (Binding.T * typ option) list *
- ((Binding.T * typ option * mixfix) option *
- ((Binding.T * attribute list) * term)) list -> theory -> theory
+ val add_constdefs_i: (binding * typ option) list *
+ ((binding * typ option * mixfix) option *
+ ((binding * attribute list) * term)) list -> theory -> theory
end;
structure Constdefs: CONSTDEFS =
@@ -52,7 +52,7 @@
val thy' =
thy
|> Sign.add_consts_i [(c, T, mx)]
- |> PureThy.add_defs false [((name, def), atts)]
+ |> PureThy.add_defs false [((Binding.name name, def), atts)]
|-> (fn [thm] => Code.add_default_eqn thm);
in ((c, T), thy') end;
--- a/src/Pure/Isar/context_rules.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML Wed Jan 21 16:51:45 2009 +0100
@@ -199,7 +199,7 @@
val dest_query = rule_add elim_queryK Tactic.make_elim;
val _ = Context.>> (Context.map_theory
- (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]));
+ (snd o PureThy.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
(* concrete syntax *)
--- a/src/Pure/Isar/element.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/element.ML Wed Jan 21 16:51:45 2009 +0100
@@ -9,11 +9,11 @@
sig
datatype ('typ, 'term) stmt =
Shows of (Attrib.binding * ('term * 'term list) list) list |
- Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list
+ Obtains of (binding * ((binding * 'typ option) list * 'term list)) list
type statement = (string, string) stmt
type statement_i = (typ, term) stmt
datatype ('typ, 'term, 'fact) ctxt =
- Fixes of (Binding.T * 'typ option * mixfix) list |
+ Fixes of (binding * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
@@ -23,12 +23,12 @@
val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
(Attrib.binding * ('fact * Attrib.src list) list) list ->
(Attrib.binding * ('c * Attrib.src list) list) list
- val map_ctxt': {binding: Binding.T -> Binding.T,
- var: Binding.T * mixfix -> Binding.T * mixfix,
+ val map_ctxt': {binding: binding -> binding,
+ var: binding * mixfix -> binding * mixfix,
typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c,
attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
- val map_ctxt: {binding: Binding.T -> Binding.T,
- var: Binding.T * mixfix -> Binding.T * mixfix,
+ val map_ctxt: {binding: binding -> binding,
+ var: binding * mixfix -> binding * mixfix,
typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
@@ -41,25 +41,21 @@
val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
val pretty_statement: Proof.context -> string -> thm -> Pretty.T
type witness
- val map_witness: (term * thm -> term * thm) -> witness -> witness
+ val prove_witness: Proof.context -> term -> tactic -> witness
+ val witness_proof: (witness list list -> Proof.context -> Proof.context) ->
+ term list list -> Proof.context -> Proof.state
+ val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) ->
+ term list list -> term list -> Proof.context -> Proof.state
+ val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
+ string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
val morph_witness: morphism -> witness -> witness
- val witness_prop: witness -> term
- val witness_hyps: witness -> term list
- val assume_witness: theory -> term -> witness
- val prove_witness: Proof.context -> term -> tactic -> witness
- val close_witness: witness -> witness
val conclude_witness: witness -> thm
- val mark_witness: term -> term
- val make_witness: term -> thm -> witness
- val dest_witness: witness -> term * thm
- val transfer_witness: theory -> witness -> witness
- val refine_witness: Proof.state -> Proof.state Seq.seq
val pretty_witness: Proof.context -> witness -> Pretty.T
val rename: (string * (string * mixfix option)) list -> string -> string
val rename_var_name: (string * (string * mixfix option)) list ->
string * mixfix -> string * mixfix
val rename_var: (string * (string * mixfix option)) list ->
- Binding.T * mixfix -> Binding.T * mixfix
+ binding * mixfix -> binding * mixfix
val rename_term: (string * (string * mixfix option)) list -> term -> term
val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
val rename_morphism: (string * (string * mixfix option)) list -> morphism
@@ -93,7 +89,7 @@
datatype ('typ, 'term) stmt =
Shows of (Attrib.binding * ('term * 'term list) list) list |
- Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list;
+ Obtains of (binding * ((binding * 'typ option) list * 'term list)) list;
type statement = (string, string) stmt;
type statement_i = (typ, term) stmt;
@@ -102,7 +98,7 @@
(* context *)
datatype ('typ, 'term, 'fact) ctxt =
- Fixes of (Binding.T * 'typ option * mixfix) list |
+ Fixes of (binding * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
@@ -300,24 +296,51 @@
datatype witness = Witness of term * thm;
+val mark_witness = Logic.protect;
+fun witness_prop (Witness (t, _)) = t;
+fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
fun map_witness f (Witness witn) = Witness (f witn);
fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
-fun witness_prop (Witness (t, _)) = t;
-fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
-
-fun assume_witness thy t =
- Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
-
fun prove_witness ctxt t tac =
- Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
+ Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
Tactic.rtac Drule.protectI 1 THEN tac)));
-val close_witness = map_witness (fn (t, th) => (t, Thm.close_derivation th));
+local
+
+val refine_witness =
+ Proof.refine (Method.Basic (K (Method.RAW_METHOD
+ (K (ALLGOALS
+ (CONJUNCTS (ALLGOALS
+ (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
-fun conclude_witness (Witness (_, th)) =
- Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
+fun gen_witness_proof proof after_qed wit_propss eq_props =
+ let
+ val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss
+ @ [map (rpair []) eq_props];
+ fun after_qed' thmss =
+ let
+ val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
+ in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
+ in proof after_qed' propss #> refine_witness #> Seq.hd end;
+
+in
+
+fun witness_proof after_qed wit_propss =
+ gen_witness_proof (Proof.theorem_i NONE) (fn wits => fn _ => after_qed wits)
+ wit_propss [];
+
+val witness_proof_eqs = gen_witness_proof (Proof.theorem_i NONE);
+
+fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
+ gen_witness_proof (fn after_qed' => fn propss =>
+ Proof.map_context (K goal_ctxt)
+ #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+ cmd NONE after_qed' (map (pair (Binding.empty, [])) propss))
+ (fn wits => fn _ => after_qed wits) wit_propss [];
+
+end; (*local*)
fun compose_witness (Witness (_, th)) r =
let
@@ -330,18 +353,8 @@
(Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
end;
-val mark_witness = Logic.protect;
-
-fun make_witness t th = Witness (t, th);
-fun dest_witness (Witness w) = w;
-
-fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th);
-
-val refine_witness =
- Proof.refine (Method.Basic (K (Method.RAW_METHOD
- (K (ALLGOALS
- (CONJUNCTS (ALLGOALS
- (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
+fun conclude_witness (Witness (_, th)) =
+ Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
fun pretty_witness ctxt witn =
let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
--- a/src/Pure/Isar/expression.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/expression.ML Wed Jan 21 16:51:45 2009 +0100
@@ -9,8 +9,8 @@
(* Locale expressions *)
datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
type 'term expr = (string * ((string * bool) * 'term map)) list
- type expression_i = term expr * (Binding.T * typ option * mixfix) list
- type expression = string expr * (Binding.T * string option * mixfix) list
+ type expression_i = term expr * (binding * typ option * mixfix) list
+ type expression = string expr * (binding * string option * mixfix) list
(* Processing of context statements *)
val cert_statement: Element.context_i list -> (term * term list) list list ->
@@ -20,14 +20,14 @@
(* Declaring locales *)
val cert_declaration: expression_i -> Element.context_i list -> Proof.context ->
- ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ ((binding * typ option * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
val cert_read_declaration: expression_i -> Element.context list -> Proof.context ->
- ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ ((binding * typ option * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
(*FIXME*)
val read_declaration: expression -> Element.context list -> Proof.context ->
- ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ ((binding * typ option * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
theory -> string * local_theory
@@ -64,8 +64,8 @@
type 'term expr = (string * ((string * bool) * 'term map)) list;
-type expression = string expr * (Binding.T * string option * mixfix) list;
-type expression_i = term expr * (Binding.T * typ option * mixfix) list;
+type expression = string expr * (binding * string option * mixfix) list;
+type expression_i = term expr * (binding * typ option * mixfix) list;
(** Internalise locale names in expr **)
@@ -640,7 +640,7 @@
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
|> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
- [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
+ [((Binding.name (Thm.def_name bname), Logic.mk_equals (head, body)), [Thm.kind_internal])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
@@ -786,41 +786,23 @@
(*** Interpretation ***)
-(** Witnesses and goals **)
-
-fun prep_propp propss = propss |> map (map (rpair [] o Element.mark_witness));
-
-val prep_result = map2 (fn props => fn thms =>
- map2 Element.make_witness props (map Thm.close_derivation thms));
-
-
(** Interpretation between locales: declaring sublocale relationships **)
local
-fun gen_sublocale prep_expr intern
- raw_target expression thy =
+fun gen_sublocale prep_expr intern raw_target expression thy =
let
val target = intern thy raw_target;
val target_ctxt = Locale.init target thy;
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
- fun store_dep (name, morph) thms =
- Locale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
-
- fun after_qed results =
- ProofContext.theory (
- (* store dependencies *)
- fold2 store_dep deps (prep_result propss results) #>
- (* propagate registrations *)
- (fn thy => fold_rev Locale.activate_global_facts
+ fun after_qed witss = ProofContext.theory (
+ fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
+ (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
+ (fn thy => fold_rev Locale.activate_global_facts
(Locale.get_registrations thy) thy));
- in
- goal_ctxt |>
- Proof.theorem_i NONE after_qed (prep_propp propss) |>
- Element.refine_witness |> Seq.hd
- end;
+ in Element.witness_proof after_qed propss goal_ctxt end;
in
@@ -845,10 +827,10 @@
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- fun store_reg ((name, morph), thms) thy =
+ fun store_reg ((name, morph), wits) thy =
let
- val thms' = map (Element.morph_witness export') thms;
- val morph' = morph $> Element.satisfy_morphism thms';
+ val wits' = map (Element.morph_witness export') wits;
+ val morph' = morph $> Element.satisfy_morphism wits';
in
thy
|> Locale.add_registration (name, (morph', export))
@@ -859,35 +841,26 @@
thy
|> fold (fn (name, morph) =>
Locale.activate_global_facts (name, morph $> export)) regs
- | store_eqns_activate regs thms thy =
+ | store_eqns_activate regs eqs thy =
let
- val thms' = thms |> map (Element.conclude_witness #>
- Morphism.thm (export' $> export) #>
+ val eqs' = eqs |> map (Morphism.thm (export' $> export) #>
LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
Drule.abs_def);
- val eq_morph = Element.eq_morphism thy thms';
+ val eq_morph = Element.eq_morphism thy eqs';
val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
in
thy
|> fold (fn (name, morph) =>
Locale.amend_registration eq_morph (name, morph) #>
Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
- |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn th => [([th], [])]) thms')
+ |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
|> snd
end;
- fun after_qed results =
- let
- val (wits_reg, wits_eq) = split_last (prep_result (propss @ [eqns]) results);
- in ProofContext.theory (fold_map store_reg (regs ~~ wits_reg)
- #-> (fn regs => store_eqns_activate regs wits_eq))
- end;
+ fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
+ #-> (fn regs => store_eqns_activate regs eqs));
- in
- goal_ctxt |>
- Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |>
- Element.refine_witness |> Seq.hd
- end;
+ in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
in
@@ -910,20 +883,16 @@
val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
- fun store_reg ((name, morph), thms) =
+ fun store_reg (name, morph) thms =
let
val morph' = morph $> Element.satisfy_morphism thms $> export;
- in
- Locale.activate_local_facts (name, morph')
- end;
+ in Locale.activate_local_facts (name, morph') end;
- fun after_qed results =
- Proof.map_context (fold store_reg (regs ~~ prep_result propss results));
+ fun after_qed wits =
+ Proof.map_context (fold2 store_reg regs wits);
in
- state |> Proof.map_context (K goal_ctxt) |>
- Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
- "interpret" NONE after_qed (map (pair (Binding.empty, [])) (prep_propp propss)) |>
- Element.refine_witness |> Seq.hd
+ state
+ |> Element.witness_local_proof after_qed "interpret" propss goal_ctxt int
end;
in
--- a/src/Pure/Isar/isar_cmd.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Wed Jan 21 16:51:45 2009 +0100
@@ -13,8 +13,8 @@
val typed_print_translation: bool * (string * Position.T) -> theory -> theory
val print_ast_translation: bool * (string * Position.T) -> theory -> theory
val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
- val add_axioms: ((Binding.T * string) * Attrib.src list) list -> theory -> theory
- val add_defs: (bool * bool) * ((Binding.T * string) * Attrib.src list) list -> theory -> theory
+ val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
+ val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
val declaration: string * Position.T -> local_theory -> local_theory
val simproc_setup: string -> string list -> string * Position.T -> string list ->
local_theory -> local_theory
@@ -53,7 +53,6 @@
val print_theorems: Toplevel.transition -> Toplevel.transition
val print_locales: Toplevel.transition -> Toplevel.transition
val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
- val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
val print_attributes: Toplevel.transition -> Toplevel.transition
val print_simpset: Toplevel.transition -> Toplevel.transition
val print_rules: Toplevel.transition -> Toplevel.transition
@@ -359,12 +358,6 @@
Toplevel.keep (fn state =>
Locale.print_locale (Toplevel.theory_of state) show_facts name);
-fun print_registrations show_wits name = Toplevel.unknown_context o
- Toplevel.keep (Toplevel.node_case
- (Context.cases (Old_Locale.print_registrations show_wits name o ProofContext.init)
- (Old_Locale.print_registrations show_wits name))
- (Old_Locale.print_registrations show_wits name o Proof.context_of));
-
val print_attributes = Toplevel.unknown_theory o
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
--- a/src/Pure/Isar/isar_syn.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Jan 21 16:51:45 2009 +0100
@@ -418,45 +418,6 @@
>> (fn expr => Toplevel.print o
Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
-local
-
-val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
-
-in
-
-val locale_val =
- SpecParse.locale_expr --
- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
- Scan.repeat1 SpecParse.context_element >> pair Old_Locale.empty;
-
-val _ =
- OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl
- (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Old_Locale.empty, []) -- P.opt_begin
- >> (fn ((name, (expr, elems)), begin) =>
- (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
- (Old_Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
-
-val _ =
- OuterSyntax.command "class_interpretation"
- "prove and register interpretation of locale expression in theory or locale" K.thy_goal
- (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
- >> (Toplevel.print oo (Toplevel.theory_to_proof o Old_Locale.interpretation_in_locale I)) ||
- opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
- >> (fn ((name, expr), insts) => Toplevel.print o
- Toplevel.theory_to_proof
- (Old_Locale.interpretation_cmd (Binding.base_name name) expr insts)));
-
-val _ =
- OuterSyntax.command "class_interpret"
- "prove and register interpretation of locale expression in proof context"
- (K.tag_proof K.prf_goal)
- (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
- >> (fn ((name, expr), insts) => Toplevel.print o
- Toplevel.proof'
- (fn int => Old_Locale.interpret_cmd (Binding.base_name name) expr insts int)));
-
-end;
-
(* classes *)
@@ -857,12 +818,6 @@
(opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
val _ =
- OuterSyntax.improper_command "print_interps"
- "print interpretations of named locale" K.diag
- (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
- >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
-
-val _ =
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
--- a/src/Pure/Isar/local_defs.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Wed Jan 21 16:51:45 2009 +0100
@@ -11,10 +11,10 @@
val mk_def: Proof.context -> (string * term) list -> term list
val expand: cterm list -> thm -> thm
val def_export: Assumption.export
- val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list ->
+ val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list ->
Proof.context -> (term * (string * thm)) list * Proof.context
- val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
- val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context ->
+ val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
+ val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
(term * term) * Proof.context
val export: Proof.context -> Proof.context -> thm -> thm list * thm
val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
--- a/src/Pure/Isar/local_theory.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML Wed Jan 21 16:51:45 2009 +0100
@@ -18,16 +18,16 @@
val raw_theory: (theory -> theory) -> local_theory -> local_theory
val checkpoint: local_theory -> local_theory
val full_naming: local_theory -> NameSpace.naming
- val full_name: local_theory -> Binding.T -> string
+ val full_name: local_theory -> binding -> string
val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val theory: (theory -> theory) -> local_theory -> local_theory
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
val affirm: local_theory -> local_theory
val pretty: local_theory -> Pretty.T list
- val abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
+ val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val define: string -> (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
+ val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -55,10 +55,10 @@
type operations =
{pretty: local_theory -> Pretty.T list,
- abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
+ abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory,
define: string ->
- (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
+ (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory,
notes: string ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
--- a/src/Pure/Isar/locale.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/locale.ML Wed Jan 21 16:51:45 2009 +0100
@@ -29,23 +29,18 @@
signature LOCALE =
sig
- type locale
-
+ (* Locale specification *)
val register_locale: bstring ->
- (string * sort) list * (Binding.T * typ option * mixfix) list ->
+ (string * sort) list * (binding * typ option * mixfix) list ->
term option * term list ->
thm option * thm option -> thm list ->
(declaration * stamp) list * (declaration * stamp) list ->
((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
((string * morphism) * stamp) list -> theory -> theory
-
- (* Locale name space *)
val intern: theory -> xstring -> string
val extern: theory -> string -> xstring
-
- (* Specification *)
val defined: theory -> string -> bool
- val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
+ val params_of: theory -> string -> (binding * typ option * mixfix) list
val intros_of: theory -> string -> thm option * thm option
val axioms_of: theory -> string -> thm list
val instance_of: theory -> string -> morphism -> term list
@@ -112,13 +107,25 @@
datatype ctxt = datatype Element.ctxt;
+fun global_note_qualified kind facts thy = (*FIXME*)
+ thy
+ |> Sign.qualified_names
+ |> PureThy.note_thmss kind facts
+ ||> Sign.restore_naming thy;
+
+fun local_note_qualified kind facts ctxt = (*FIXME*)
+ ctxt
+ |> ProofContext.qualified_names
+ |> ProofContext.note_thmss_i kind facts
+ ||> ProofContext.restore_naming ctxt;
+
(*** Theory data ***)
datatype locale = Loc of {
(** static part **)
- parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
+ parameters: (string * sort) list * (binding * typ option * mixfix) list,
(* type and term parameters *)
spec: term option * term list,
(* assumptions (as a single predicate expression) and defines *)
@@ -330,7 +337,7 @@
fun init_global_elem (Notes (kind, facts)) thy =
let
val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
- in Old_Locale.global_note_qualified kind facts' thy |> snd end
+ in global_note_qualified kind facts' thy |> snd end
fun init_local_elem (Fixes fixes) ctxt = ctxt |>
ProofContext.add_fixes_i fixes |> snd
@@ -352,7 +359,7 @@
| init_local_elem (Notes (kind, facts)) ctxt =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
- in Old_Locale.local_note_qualified kind facts' ctxt |> snd end
+ in local_note_qualified kind facts' ctxt |> snd end
fun cons_elem false (Notes notes) elems = elems
| cons_elem _ elem elems = elem :: elems
@@ -445,7 +452,7 @@
let
val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
Attrib.map_facts (Attrib.attribute_i thy)
- in Old_Locale.global_note_qualified kind args'' #> snd end)
+ in global_note_qualified kind args'' #> snd end)
(get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
in ctxt'' end;
@@ -496,12 +503,10 @@
val _ = Context.>> (Context.map_theory
(Method.add_methods
[("intro_locales",
- Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt ORELSE'
- Old_Locale.intro_locales_tac false ctxt)),
+ Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
"back-chain introduction rules of locales without unfolding predicates"),
("unfold_locales",
- Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE'
- Old_Locale.intro_locales_tac true ctxt)),
+ Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
"back-chain all introduction rules of locales")]));
end;
--- a/src/Pure/Isar/obtain.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/obtain.ML Wed Jan 21 16:51:45 2009 +0100
@@ -39,16 +39,16 @@
signature OBTAIN =
sig
val thatN: string
- val obtain: string -> (Binding.T * string option * mixfix) list ->
+ val obtain: string -> (binding * string option * mixfix) list ->
(Attrib.binding * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val obtain_i: string -> (Binding.T * typ option * mixfix) list ->
- ((Binding.T * attribute list) * (term * term list) list) list ->
+ val obtain_i: string -> (binding * typ option * mixfix) list ->
+ ((binding * attribute list) * (term * term list) list) list ->
bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
(cterm list * thm list) * Proof.context
- val guess: (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
- val guess_i: (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Obtain: OBTAIN =
--- a/src/Pure/Isar/old_locale.ML Tue Jan 20 19:09:19 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2485 +0,0 @@
-(* Title: Pure/Isar/locale.ML
- Author: Clemens Ballarin, TU Muenchen
- Author: Markus Wenzel, LMU/TU Muenchen
-
-Locales -- Isar proof contexts as meta-level predicates, with local
-syntax and implicit structures.
-
-Draws basic ideas from Florian Kammueller's original version of
-locales, but uses the richer infrastructure of Isar instead of the raw
-meta-logic. Furthermore, structured import of contexts (with merge
-and rename operations) are provided, as well as type-inference of the
-signature parts, and predicate definitions of the specification text.
-
-Interpretation enables the reuse of theorems of locales in other
-contexts, namely those defined by theories, structured proofs and
-locales themselves.
-
-See also:
-
-[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
- In Stefano Berardi et al., Types for Proofs and Programs: International
- Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
-[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
- Dependencies between Locales. Technical Report TUM-I0607, Technische
- Universitaet Muenchen, 2006.
-[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
- Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
- pages 31-43, 2006.
-*)
-
-(* TODO:
-- beta-eta normalisation of interpretation parameters
-- dangling type frees in locales
-- test subsumption of interpretations when merging theories
-*)
-
-signature OLD_LOCALE =
-sig
- datatype expr =
- Locale of string |
- Rename of expr * (string * mixfix option) option list |
- Merge of expr list
- val empty: expr
-
- val intern: theory -> xstring -> string
- val intern_expr: theory -> expr -> expr
- val extern: theory -> string -> xstring
- val init: string -> theory -> Proof.context
-
- (* The specification of a locale *)
- val parameters_of: theory -> string -> ((string * typ) * mixfix) list
- val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list
- val local_asms_of: theory -> string -> (Attrib.binding * term list) list
- val global_asms_of: theory -> string -> (Attrib.binding * term list) list
-
- (* Theorems *)
- val intros: theory -> string -> thm list * thm list
- val dests: theory -> string -> thm list
- (* Not part of the official interface. DO NOT USE *)
- val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
-
- (* Not part of the official interface. DO NOT USE *)
- val declarations_of: theory -> string -> declaration list * declaration list;
-
- (* Processing of locale statements *)
- val read_context_statement: string option -> Element.context list ->
- (string * string list) list list -> Proof.context ->
- string option * Proof.context * Proof.context * (term * term list) list list
- val read_context_statement_cmd: xstring option -> Element.context list ->
- (string * string list) list list -> Proof.context ->
- string option * Proof.context * Proof.context * (term * term list) list list
- val cert_context_statement: string option -> Element.context_i list ->
- (term * term list) list list -> Proof.context ->
- string option * Proof.context * Proof.context * (term * term list) list list
- val read_expr: expr -> Element.context list -> Proof.context ->
- Element.context_i list * Proof.context
- val cert_expr: expr -> Element.context_i list -> Proof.context ->
- Element.context_i list * Proof.context
-
- (* Diagnostic functions *)
- val print_locales: theory -> unit
- val print_locale: theory -> bool -> expr -> Element.context list -> unit
- val print_registrations: bool -> string -> Proof.context -> unit
-
- val add_locale: string -> bstring -> expr -> Element.context_i list -> theory
- -> string * Proof.context
- val add_locale_cmd: bstring -> expr -> Element.context list -> theory
- -> string * Proof.context
-
- (* Tactics *)
- val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
-
- (* Storing results *)
- val global_note_qualified: string ->
- ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
- theory -> (string * thm list) list * theory
- val local_note_qualified: string ->
- ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
- Proof.context -> (string * thm list) list * Proof.context
- val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
- Proof.context -> Proof.context
- val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
- val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
- val add_declaration: string -> declaration -> Proof.context -> Proof.context
-
- (* Interpretation *)
- val get_interpret_morph: theory -> (Binding.T -> Binding.T) -> string * string ->
- (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
- string -> term list -> Morphism.morphism
- val interpretation: (Proof.context -> Proof.context) ->
- (Binding.T -> Binding.T) -> expr ->
- term option list * (Attrib.binding * term) list ->
- theory ->
- (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
- val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
- theory -> Proof.state
- val interpretation_in_locale: (Proof.context -> Proof.context) ->
- xstring * expr -> theory -> Proof.state
- val interpret: (Proof.state -> Proof.state) ->
- (Binding.T -> Binding.T) -> expr ->
- term option list * (Attrib.binding * term) list ->
- bool -> Proof.state ->
- (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
- val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list ->
- bool -> Proof.state -> Proof.state
-end;
-
-structure Old_Locale: OLD_LOCALE =
-struct
-
-(* legacy operations *)
-
-fun merge_lists _ xs [] = xs
- | merge_lists _ [] ys = ys
- | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
-
-fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
-
-
-(* auxiliary: noting name bindings with qualified base names *)
-
-fun global_note_qualified kind facts thy =
- thy
- |> Sign.qualified_names
- |> PureThy.note_thmss kind facts
- ||> Sign.restore_naming thy;
-
-fun local_note_qualified kind facts ctxt =
- ctxt
- |> ProofContext.qualified_names
- |> ProofContext.note_thmss_i kind facts
- ||> ProofContext.restore_naming ctxt;
-
-
-(** locale elements and expressions **)
-
-datatype ctxt = datatype Element.ctxt;
-
-datatype expr =
- Locale of string |
- Rename of expr * (string * mixfix option) option list |
- Merge of expr list;
-
-val empty = Merge [];
-
-datatype 'a element =
- Elem of 'a | Expr of expr;
-
-fun map_elem f (Elem e) = Elem (f e)
- | map_elem _ (Expr e) = Expr e;
-
-type decl = declaration * stamp;
-
-type locale =
- {axiom: Element.witness list,
- (* For locales that define predicates this is [A [A]], where A is the locale
- specification. Otherwise [].
- Only required to generate the right witnesses for locales with predicates. *)
- elems: (Element.context_i * stamp) list,
- (* Static content, neither Fixes nor Constrains elements *)
- params: ((string * typ) * mixfix) list, (*all term params*)
- decls: decl list * decl list, (*type/term_syntax declarations*)
- regs: ((string * string list) * Element.witness list) list,
- (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
- intros: thm list * thm list,
- (* Introduction rules: of delta predicate and locale predicate. *)
- dests: thm list}
- (* Destruction rules: projections from locale predicate to predicates of fragments. *)
-
-(* CB: an internal (Int) locale element was either imported or included,
- an external (Ext) element appears directly in the locale text. *)
-
-datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
-
-
-
-(** substitutions on Vars -- clone from element.ML **)
-
-(* instantiate types *)
-
-fun var_instT_type env =
- if Vartab.is_empty env then I
- else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x));
-
-fun var_instT_term env =
- if Vartab.is_empty env then I
- else Term.map_types (var_instT_type env);
-
-fun var_inst_term (envT, env) =
- if Vartab.is_empty env then var_instT_term envT
- else
- let
- val instT = var_instT_type envT;
- fun inst (Const (x, T)) = Const (x, instT T)
- | inst (Free (x, T)) = Free(x, instT T)
- | inst (Var (xi, T)) =
- (case Vartab.lookup env xi of
- NONE => Var (xi, instT T)
- | SOME t => t)
- | inst (b as Bound _) = b
- | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
- | inst (t $ u) = inst t $ inst u;
- in Envir.beta_norm o inst end;
-
-
-(** management of registrations in theories and proof contexts **)
-
-type registration =
- {prfx: (Binding.T -> Binding.T) * (string * string),
- (* first component: interpretation name morphism;
- second component: parameter prefix *)
- exp: Morphism.morphism,
- (* maps content to its originating context *)
- imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
- (* inverse of exp *)
- wits: Element.witness list,
- (* witnesses of the registration *)
- eqns: thm Termtab.table,
- (* theorems (equations) interpreting derived concepts and indexed by lhs *)
- morph: unit
- (* interpreting morphism *)
- }
-
-structure Registrations :
- sig
- type T
- val empty: T
- val join: T * T -> T
- val dest: theory -> T ->
- (term list *
- (((Binding.T -> Binding.T) * (string * string)) *
- (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
- Element.witness list *
- thm Termtab.table)) list
- val test: theory -> T * term list -> bool
- val lookup: theory ->
- T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
- (((Binding.T -> Binding.T) * (string * string)) * Element.witness list * thm Termtab.table) option
- val insert: theory -> term list -> ((Binding.T -> Binding.T) * (string * string)) ->
- (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
- T ->
- T * (term list * (((Binding.T -> Binding.T) * (string * string)) * Element.witness list)) list
- val add_witness: term list -> Element.witness -> T -> T
- val add_equation: term list -> thm -> T -> T
-(*
- val update_morph: term list -> Morphism.morphism -> T -> T
- val get_morph: theory -> T ->
- term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) ->
- Morphism.morphism
-*)
- end =
-struct
- (* A registration is indexed by parameter instantiation.
- NB: index is exported whereas content is internalised. *)
- type T = registration Termtab.table;
-
- fun mk_reg prfx exp imp wits eqns morph =
- {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph};
-
- fun map_reg f reg =
- let
- val {prfx, exp, imp, wits, eqns, morph} = reg;
- val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph);
- in mk_reg prfx' exp' imp' wits' eqns' morph' end;
-
- val empty = Termtab.empty;
-
- (* term list represented as single term, for simultaneous matching *)
- fun termify ts =
- Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
- fun untermify t =
- let fun ut (Const _) ts = ts
- | ut (s $ t) ts = ut s (t::ts)
- in ut t [] end;
-
- (* joining of registrations:
- - prefix and morphisms of right theory;
- - witnesses are equal, no attempt to subsumption testing;
- - union of equalities, if conflicting (i.e. two eqns with equal lhs)
- eqn of right theory takes precedence *)
- fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) =>
- mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2);
-
- fun dest_transfer thy regs =
- Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) =>
- (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m))));
-
- fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
- map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns)));
-
- (* registrations that subsume t *)
- fun subsumers thy t regs =
- filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
-
- (* test if registration that subsumes the query is present *)
- fun test thy (regs, ts) =
- not (null (subsumers thy (termify ts) regs));
-
- (* look up registration, pick one that subsumes the query *)
- fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) =
- let
- val t = termify ts;
- val subs = subsumers thy t regs;
- in
- (case subs of
- [] => NONE
- | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) =>
- let
- val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
- val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
- (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst
- |> var_instT_type impT)) |> Symtab.make;
- val inst' = dom' |> map (fn (t as Free (x, _)) =>
- (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst)
- |> var_inst_term (impT, imp))) |> Symtab.make;
- val inst'_morph = Element.inst_morphism thy (tinst', inst');
- in SOME (prfx,
- map (Element.morph_witness inst'_morph) wits,
- Termtab.map (Morphism.thm inst'_morph) eqns)
- end)
- end;
-
- (* add registration if not subsumed by ones already present,
- additionally returns registrations that are strictly subsumed *)
- fun insert thy ts prfx (exp, imp) regs =
- let
- val t = termify ts;
- val subs = subsumers thy t regs ;
- in (case subs of
- [] => let
- val sups =
- filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
- val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
- in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end
- | _ => (regs, []))
- end;
-
- fun gen_add f ts regs =
- let
- val t = termify ts;
- in
- Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs
- end;
-
- (* add witness theorem to registration,
- only if instantiation is exact, otherwise exception Option raised *)
- fun add_witness ts wit regs =
- gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m))
- ts regs;
-
- (* add equation to registration, replaces previous equation with same lhs;
- only if instantiation is exact, otherwise exception Option raised;
- exception TERM raised if not a meta equality *)
- fun add_equation ts thm regs =
- gen_add (fn (x, e, i, thms, eqns, m) =>
- (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
- ts regs;
-
-end;
-
-
-(** theory data : locales **)
-
-structure LocalesData = TheoryDataFun
-(
- type T = NameSpace.T * locale Symtab.table;
- (* 1st entry: locale namespace,
- 2nd entry: locales of the theory *)
-
- val empty = NameSpace.empty_table;
- val copy = I;
- val extend = I;
-
- fun join_locales _
- ({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale,
- {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
- {axiom = axiom,
- elems = merge_lists (eq_snd (op =)) elems elems',
- params = params,
- decls =
- (Library.merge (eq_snd (op =)) (decls1, decls1'),
- Library.merge (eq_snd (op =)) (decls2, decls2')),
- regs = merge_alists (op =) regs regs',
- intros = intros,
- dests = dests};
- fun merge _ = NameSpace.join_tables join_locales;
-);
-
-
-
-(** context data : registrations **)
-
-structure RegistrationsData = GenericDataFun
-(
- type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*)
- val empty = Symtab.empty;
- val extend = I;
- fun merge _ = Symtab.join (K Registrations.join);
-);
-
-
-(** access locales **)
-
-val intern = NameSpace.intern o #1 o LocalesData.get;
-val extern = NameSpace.extern o #1 o LocalesData.get;
-
-fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
-
-fun the_locale thy name = case get_locale thy name
- of SOME loc => loc
- | NONE => error ("Unknown locale " ^ quote name);
-
-fun register_locale bname loc thy =
- thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy)
- (Binding.name bname, loc) #> snd);
-
-fun change_locale name f thy =
- let
- val {axiom, elems, params, decls, regs, intros, dests} =
- the_locale thy name;
- val (axiom', elems', params', decls', regs', intros', dests') =
- f (axiom, elems, params, decls, regs, intros, dests);
- in
- thy
- |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
- elems = elems', params = params',
- decls = decls', regs = regs', intros = intros', dests = dests'}))
- end;
-
-fun print_locales thy =
- let val (space, locs) = LocalesData.get thy in
- Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
- |> Pretty.writeln
- end;
-
-
-(* access registrations *)
-
-(* retrieve registration from theory or context *)
-
-fun get_registrations ctxt name =
- case Symtab.lookup (RegistrationsData.get ctxt) name of
- NONE => []
- | SOME reg => Registrations.dest (Context.theory_of ctxt) reg;
-
-fun get_global_registrations thy = get_registrations (Context.Theory thy);
-fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt);
-
-
-fun get_registration ctxt imprt (name, ps) =
- case Symtab.lookup (RegistrationsData.get ctxt) name of
- NONE => NONE
- | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt));
-
-fun get_global_registration thy = get_registration (Context.Theory thy);
-fun get_local_registration ctxt = get_registration (Context.Proof ctxt);
-
-
-fun test_registration ctxt (name, ps) =
- case Symtab.lookup (RegistrationsData.get ctxt) name of
- NONE => false
- | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps);
-
-fun test_global_registration thy = test_registration (Context.Theory thy);
-fun test_local_registration ctxt = test_registration (Context.Proof ctxt);
-
-
-(* add registration to theory or context, ignored if subsumed *)
-
-fun put_registration (name, ps) prfx morphs ctxt =
- RegistrationsData.map (fn regs =>
- let
- val thy = Context.theory_of ctxt;
- val reg = the_default Registrations.empty (Symtab.lookup regs name);
- val (reg', sups) = Registrations.insert thy ps prfx morphs reg;
- val _ = if not (null sups) then warning
- ("Subsumed interpretation(s) of locale " ^
- quote (extern thy name) ^
- "\nwith the following prefix(es):" ^
- commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups))
- else ();
- in Symtab.update (name, reg') regs end) ctxt;
-
-fun put_global_registration id prfx morphs =
- Context.theory_map (put_registration id prfx morphs);
-fun put_local_registration id prfx morphs =
- Context.proof_map (put_registration id prfx morphs);
-
-fun put_registration_in_locale name id =
- change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
- (axiom, elems, params, decls, regs @ [(id, [])], intros, dests));
-
-
-(* add witness theorem to registration, ignored if registration not present *)
-
-fun add_witness (name, ps) thm =
- RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm));
-
-fun add_global_witness id thm = Context.theory_map (add_witness id thm);
-fun add_local_witness id thm = Context.proof_map (add_witness id thm);
-
-
-fun add_witness_in_locale name id thm =
- change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) =>
- let
- fun add (id', thms) =
- if id = id' then (id', thm :: thms) else (id', thms);
- in (axiom, elems, params, decls, map add regs, intros, dests) end);
-
-
-(* add equation to registration, ignored if registration not present *)
-
-fun add_equation (name, ps) thm =
- RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm));
-
-fun add_global_equation id thm = Context.theory_map (add_equation id thm);
-fun add_local_equation id thm = Context.proof_map (add_equation id thm);
-
-(*
-(* update morphism of registration, ignored if registration not present *)
-
-fun update_morph (name, ps) morph =
- RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph));
-
-fun update_global_morph id morph = Context.theory_map (update_morph id morph);
-fun update_local_morph id morph = Context.proof_map (update_morph id morph);
-*)
-
-
-(* printing of registrations *)
-
-fun print_registrations show_wits loc ctxt =
- let
- val thy = ProofContext.theory_of ctxt;
- val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
- fun prt_term' t = if !show_types
- then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
- Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
- else prt_term t;
- val prt_thm = prt_term o prop_of;
- fun prt_inst ts =
- Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
- fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx]
- | prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx];
- fun prt_eqns [] = Pretty.str "no equations."
- | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
- Pretty.breaks (map prt_thm eqns));
- fun prt_core ts eqns =
- [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];
- fun prt_witns [] = Pretty.str "no witnesses."
- | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
- Pretty.breaks (map (Element.pretty_witness ctxt) witns))
- fun prt_reg (ts, (_, _, witns, eqns)) =
- if show_wits
- then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
- else Pretty.block (prt_core ts eqns)
-
- val loc_int = intern thy loc;
- val regs = RegistrationsData.get (Context.Proof ctxt);
- val loc_regs = Symtab.lookup regs loc_int;
- in
- (case loc_regs of
- NONE => Pretty.str ("no interpretations")
- | SOME r => let
- val r' = Registrations.dest thy r;
- val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r';
- in Pretty.big_list ("interpretations:") (map prt_reg r'') end)
- |> Pretty.writeln
- end;
-
-
-(* diagnostics *)
-
-fun err_in_locale ctxt msg ids =
- let
- val thy = ProofContext.theory_of ctxt;
- fun prt_id (name, parms) =
- [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
- val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
- val err_msg =
- if forall (fn (s, _) => s = "") ids then msg
- else msg ^ "\n" ^ Pretty.string_of (Pretty.block
- (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
- in error err_msg end;
-
-fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
-
-
-fun pretty_ren NONE = Pretty.str "_"
- | pretty_ren (SOME (x, NONE)) = Pretty.str x
- | pretty_ren (SOME (x, SOME syn)) =
- Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
-
-fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
- | pretty_expr thy (Rename (expr, xs)) =
- Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
- | pretty_expr thy (Merge es) =
- Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
-
-fun err_in_expr _ msg (Merge []) = error msg
- | err_in_expr ctxt msg expr =
- error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
- [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
- pretty_expr (ProofContext.theory_of ctxt) expr]));
-
-
-(** structured contexts: rename + merge + implicit type instantiation **)
-
-(* parameter types *)
-
-fun frozen_tvars ctxt Ts =
- #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
- |> map (fn ((xi, S), T) => (xi, (S, T)));
-
-fun unify_frozen ctxt maxidx Ts Us =
- let
- fun paramify NONE i = (NONE, i)
- | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
-
- val (Ts', maxidx') = fold_map paramify Ts maxidx;
- val (Us', maxidx'') = fold_map paramify Us maxidx';
- val thy = ProofContext.theory_of ctxt;
-
- fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
- handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
- | unify _ env = env;
- val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
- val Vs = map (Option.map (Envir.norm_type unifier)) Us';
- val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
- in map (Option.map (Envir.norm_type unifier')) Vs end;
-
-fun params_of elemss =
- distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
-
-fun params_of' elemss =
- distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
-
-fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params);
-
-
-(* CB: param_types has the following type:
- ('a * 'b option) list -> ('a * 'b) list *)
-fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
-
-
-fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
- handle Symtab.DUP x => err_in_locale ctxt
- ("Conflicting syntax for parameter: " ^ quote x) (map fst ids);
-
-
-(* Distinction of assumed vs. derived identifiers.
- The former may have axioms relating assumptions of the context to
- assumptions of the specification fragment (for locales with
- predicates). The latter have witnesses relating assumptions of the
- specification fragment to assumptions of other (assumed) specification
- fragments. *)
-
-datatype 'a mode = Assumed of 'a | Derived of 'a;
-
-fun map_mode f (Assumed x) = Assumed (f x)
- | map_mode f (Derived x) = Derived (f x);
-
-
-(* flatten expressions *)
-
-local
-
-fun unify_parms ctxt fixed_parms raw_parmss =
- let
- val thy = ProofContext.theory_of ctxt;
- val maxidx = length raw_parmss;
- val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
-
- fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
- fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
- val parms = fixed_parms @ maps varify_parms idx_parmss;
-
- fun unify T U envir = Sign.typ_unify thy (U, T) envir
- handle Type.TUNIFY =>
- let
- val T' = Envir.norm_type (fst envir) T;
- val U' = Envir.norm_type (fst envir) U;
- val prt = Syntax.string_of_typ ctxt;
- in
- raise TYPE ("unify_parms: failed to unify types " ^
- prt U' ^ " and " ^ prt T', [U', T'], [])
- end;
- fun unify_list (T :: Us) = fold (unify T) Us
- | unify_list [] = I;
- val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
- (Vartab.empty, maxidx);
-
- val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
- val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
-
- fun inst_parms (i, ps) =
- List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps)
- |> map_filter (fn (a, S) =>
- let val T = Envir.norm_type unifier' (TVar ((a, i), S))
- in if T = TFree (a, S) then NONE else SOME (a, T) end)
- |> Symtab.make;
- in map inst_parms idx_parmss end;
-
-in
-
-fun unify_elemss _ _ [] = []
- | unify_elemss _ [] [elems] = [elems]
- | unify_elemss ctxt fixed_parms elemss =
- let
- val thy = ProofContext.theory_of ctxt;
- val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
- |> map (Element.instT_morphism thy);
- fun inst ((((name, ps), mode), elems), phi) =
- (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
- map_mode (map (Element.morph_witness phi)) mode),
- map (Element.morph_ctxt phi) elems);
- in map inst (elemss ~~ phis) end;
-
-
-fun renaming xs parms = zip_options parms xs
- handle Library.UnequalLengths =>
- error ("Too many arguments in renaming: " ^
- commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
-
-
-(* params_of_expr:
- Compute parameters (with types and syntax) of locale expression.
-*)
-
-fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
- let
- val thy = ProofContext.theory_of ctxt;
-
- fun merge_tenvs fixed tenv1 tenv2 =
- let
- val [env1, env2] = unify_parms ctxt fixed
- [tenv1 |> Symtab.dest |> map (apsnd SOME),
- tenv2 |> Symtab.dest |> map (apsnd SOME)]
- in
- Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
- Symtab.map (Element.instT_type env2) tenv2)
- end;
-
- fun merge_syn expr syn1 syn2 =
- Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
- handle Symtab.DUP x => err_in_expr ctxt
- ("Conflicting syntax for parameter: " ^ quote x) expr;
-
- fun params_of (expr as Locale name) =
- let
- val {params, ...} = the_locale thy name;
- in (map (fst o fst) params, params |> map fst |> Symtab.make,
- params |> map (apfst fst) |> Symtab.make) end
- | params_of (expr as Rename (e, xs)) =
- let
- val (parms', types', syn') = params_of e;
- val ren = renaming xs parms';
- (* renaming may reduce number of parameters *)
- val new_parms = map (Element.rename ren) parms' |> distinct (op =);
- val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren);
- val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
- handle Symtab.DUP x =>
- err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
- val syn_types = map (apsnd (fn mx =>
- SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0)))))
- (Symtab.dest new_syn);
- val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
- val (env :: _) = unify_parms ctxt []
- ((ren_types |> map (apsnd SOME)) :: map single syn_types);
- val new_types = fold (Symtab.insert (op =))
- (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
- in (new_parms, new_types, new_syn) end
- | params_of (Merge es) =
- fold (fn e => fn (parms, types, syn) =>
- let
- val (parms', types', syn') = params_of e
- in
- (merge_lists (op =) parms parms', merge_tenvs [] types types',
- merge_syn e syn syn')
- end)
- es ([], Symtab.empty, Symtab.empty)
-
- val (parms, types, syn) = params_of expr;
- in
- (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types,
- merge_syn expr prev_syn syn)
- end;
-
-fun make_params_ids params = [(("", params), ([], Assumed []))];
-fun make_raw_params_elemss (params, tenv, syn) =
- [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
- Int [Fixes (map (fn p =>
- (Binding.name p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
-
-
-(* flatten_expr:
- Extend list of identifiers by those new in locale expression expr.
- Compute corresponding list of lists of locale elements (one entry per
- identifier).
-
- Identifiers represent locale fragments and are in an extended form:
- ((name, ps), (ax_ps, axs))
- (name, ps) is the locale name with all its parameters.
- (ax_ps, axs) is the locale axioms with its parameters;
- axs are always taken from the top level of the locale hierarchy,
- hence axioms may contain additional parameters from later fragments:
- ps subset of ax_ps. axs is either singleton or empty.
-
- Elements are enriched by identifier-like information:
- (((name, ax_ps), axs), elems)
- The parameters in ax_ps are the axiom parameters, but enriched by type
- info: now each entry is a pair of string and typ option. Axioms are
- type-instantiated.
-
-*)
-
-fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
- let
- val thy = ProofContext.theory_of ctxt;
-
- fun rename_parms top ren ((name, ps), (parms, mode)) =
- ((name, map (Element.rename ren) ps),
- if top
- then (map (Element.rename ren) parms,
- map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
- else (parms, mode));
-
- (* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *)
-
- fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
- if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
- then (wits, ids, visited)
- else
- let
- val {params, regs, ...} = the_locale thy name;
- val pTs' = map #1 params;
- val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
- (* dummy syntax, since required by rename *)
- val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
- val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
- (* propagate parameter types, to keep them consistent *)
- val regs' = map (fn ((name, ps), wits) =>
- ((name, map (Element.rename ren) ps),
- map (Element.transfer_witness thy) wits)) regs;
- val new_regs = regs';
- val new_ids = map fst new_regs;
- val new_idTs =
- map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
-
- val new_wits = new_regs |> map (#2 #> map
- (Element.morph_witness
- (Element.instT_morphism thy env $>
- Element.rename_morphism ren $>
- Element.satisfy_morphism wits)
- #> Element.close_witness));
- val new_ids' = map (fn (id, wits) =>
- (id, ([], Derived wits))) (new_ids ~~ new_wits);
- val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
- ((n, pTs), mode)) (new_idTs ~~ new_ids');
- val new_id = ((name, map #1 pTs), ([], mode));
- val (wits', ids', visited') = fold add_with_regs new_idTs'
- (wits @ flat new_wits, ids, visited @ [new_id]);
- in
- (wits', ids' @ [new_id], visited')
- end;
-
- (* distribute top-level axioms over assumed ids *)
-
- fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
- let
- val {elems, ...} = the_locale thy name;
- val ts = maps
- (fn (Assumes asms, _) => maps (map #1 o #2) asms
- | _ => [])
- elems;
- val (axs1, axs2) = chop (length ts) axioms;
- in (((name, parms), (all_ps, Assumed axs1)), axs2) end
- | axiomify all_ps (id, (_, Derived ths)) axioms =
- ((id, (all_ps, Derived ths)), axioms);
-
- (* identifiers of an expression *)
-
- fun identify top (Locale name) =
- (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
- where name is a locale name, ps a list of parameter names and axs
- a list of axioms relating to the identifier, axs is empty unless
- identify at top level (top = true);
- parms is accumulated list of parameters *)
- let
- val {axiom, params, ...} = the_locale thy name;
- val ps = map (#1 o #1) params;
- val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []);
- val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
- in (ids_ax, ps) end
- | identify top (Rename (e, xs)) =
- let
- val (ids', parms') = identify top e;
- val ren = renaming xs parms'
- handle ERROR msg => err_in_locale' ctxt msg ids';
-
- val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
- val parms'' = distinct (op =) (maps (#2 o #1) ids'');
- in (ids'', parms'') end
- | identify top (Merge es) =
- fold (fn e => fn (ids, parms) =>
- let
- val (ids', parms') = identify top e
- in
- (merge_alists (op =) ids ids', merge_lists (op =) parms parms')
- end)
- es ([], []);
-
- fun inst_wit all_params (t, th) = let
- val {hyps, prop, ...} = Thm.rep_thm th;
- val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
- val [env] = unify_parms ctxt all_params [ps];
- val t' = Element.instT_term env t;
- val th' = Element.instT_thm thy env th;
- in (t', th') end;
-
- fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
- let
- val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
- val elems = map fst elems_stamped;
- val ps = map fst ps_mx;
- fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
- val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
- val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
- val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
- val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
- val (lprfx, pprfx) = param_prefix name params;
- val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
- #> Binding.add_prefix false lprfx;
- val elem_morphism =
- Element.rename_morphism ren $>
- Morphism.binding_morphism add_prefices $>
- Element.instT_morphism thy env;
- val elems' = map (Element.morph_ctxt elem_morphism) elems;
- in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
-
- (* parameters, their types and syntax *)
- val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
- val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
- (* compute identifiers and syntax, merge with previous ones *)
- val (ids, _) = identify true expr;
- val idents = subtract (eq_fst (op =)) prev_idents ids;
- val syntax = merge_syntax ctxt ids (syn, prev_syntax);
- (* type-instantiate elements *)
- val final_elemss = map (eval all_params tenv syntax) idents;
- in ((prev_idents @ idents, syntax), final_elemss) end;
-
-end;
-
-
-(* activate elements *)
-
-local
-
-fun axioms_export axs _ As =
- (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
-
-
-(* NB: derived ids contain only facts at this stage *)
-
-fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =
- ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))
- | activate_elem _ _ (Constrains _) (ctxt, mode) =
- ([], (ctxt, mode))
- | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =
- let
- val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
- val ts = maps (map #1 o #2) asms';
- val (ps, qs) = chop (length ts) axs;
- val (_, ctxt') =
- ctxt |> fold Variable.auto_fixes ts
- |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
- in ([], (ctxt', Assumed qs)) end
- | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =
- ([], (ctxt, Derived ths))
- | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =
- let
- val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
- val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
- let val ((c, _), t') = LocalDefs.cert_def ctxt t
- in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
- val (_, ctxt') =
- ctxt |> fold (Variable.auto_fixes o #1) asms
- |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
- in ([], (ctxt', Assumed axs)) end
- | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =
- ([], (ctxt, Derived ths))
- | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
- let
- val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
- val (res, ctxt') = ctxt |> local_note_qualified kind facts';
- in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
-
-fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
- let
- val thy = ProofContext.theory_of ctxt;
- val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = ""))
- elems (ProofContext.qualified_names ctxt, mode)
- handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
- val ctxt'' = if name = "" then ctxt'
- else let
- val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
- in if test_local_registration ctxt' (name, ps') then ctxt'
- else let
- val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, ""))
- (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
- in case mode of
- Assumed axs =>
- fold (add_local_witness (name, ps') o
- Element.assume_witness thy o Element.witness_prop) axs ctxt''
- | Derived ths =>
- fold (add_local_witness (name, ps')) ths ctxt''
- end
- end
- in (ProofContext.restore_naming ctxt ctxt'', res) end;
-
-fun activate_elemss ax_in_ctxt prep_facts =
- fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
- let
- val elems = map (prep_facts ctxt) raw_elems;
- val (ctxt', res) = apsnd flat
- (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
- val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
- in (((((name, ps), mode), elems'), res), ctxt') end);
-
-in
-
-(* CB: activate_facts prep_facts elemss ctxt,
- where elemss is a list of pairs consisting of identifiers and
- context elements, extends ctxt by the context elements yielding
- ctxt' and returns ((elemss', facts), ctxt').
- Identifiers in the argument are of the form ((name, ps), axs) and
- assumptions use the axioms in the identifiers to set up exporters
- in ctxt'. elemss' does not contain identifiers and is obtained
- from elemss and the intermediate context with prep_facts.
- If read_facts or cert_facts is used for prep_facts, these also remove
- the internal/external markers from elemss. *)
-
-fun activate_facts ax_in_ctxt prep_facts args =
- activate_elemss ax_in_ctxt prep_facts args
- #>> (apsnd flat o split_list);
-
-end;
-
-
-
-(** prepare locale elements **)
-
-(* expressions *)
-
-fun intern_expr thy (Locale xname) = Locale (intern thy xname)
- | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
- | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
-
-
-(* propositions and bindings *)
-
-(* flatten (ctxt, prep_expr) ((ids, syn), expr)
- normalises expr (which is either a locale
- expression or a single context element) wrt.
- to the list ids of already accumulated identifiers.
- It returns ((ids', syn'), elemss) where ids' is an extension of ids
- with identifiers generated for expr, and elemss is the list of
- context elements generated from expr.
- syn and syn' are symtabs mapping parameter names to their syntax. syn'
- is an extension of syn.
- For details, see flatten_expr.
-
- Additionally, for a locale expression, the elems are grouped into a single
- Int; individual context elements are marked Ext. In this case, the
- identifier-like information of the element is as follows:
- - for Fixes: (("", ps), []) where the ps have type info NONE
- - for other elements: (("", []), []).
- The implementation of activate_facts relies on identifier names being
- empty strings for external elements.
-*)
-
-fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
- val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
- in
- ((ids',
- merge_syntax ctxt ids'
- (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
- handle Symtab.DUP x => err_in_locale ctxt
- ("Conflicting syntax for parameter: " ^ quote x)
- (map #1 ids')),
- [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
- end
- | flatten _ ((ids, syn), Elem elem) =
- ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
- | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
- apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
-
-local
-
-local
-
-fun declare_int_elem (Fixes fixes) ctxt =
- ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
- (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd)
- | declare_int_elem _ ctxt = ([], ctxt);
-
-fun declare_ext_elem prep_vars (Fixes fixes) ctxt =
- let val (vars, _) = prep_vars fixes ctxt
- in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
- | declare_ext_elem prep_vars (Constrains csts) ctxt =
- let val (_, ctxt') = prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) ctxt
- in ([], ctxt') end
- | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
- | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
- | declare_ext_elem _ (Notes _) ctxt = ([], ctxt);
-
-fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems
- of Int es => fold_map declare_int_elem es ctxt
- | Ext e => declare_ext_elem prep_vars e ctxt |>> single)
- handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)])
- | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt);
-
-in
-
-fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
- let
- (* CB: fix of type bug of goal in target with context elements.
- Parameters new in context elements must receive types that are
- distinct from types of parameters in target (fixed_params). *)
- val ctxt_with_fixed =
- fold Variable.declare_term (map Free fixed_params) ctxt;
- val int_elemss =
- raw_elemss
- |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
- |> unify_elemss ctxt_with_fixed fixed_params;
- val (raw_elemss', _) =
- fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x))
- raw_elemss int_elemss;
- in fold_map (declare_elems prep_vars) raw_elemss' ctxt end;
-
-end;
-
-local
-
-val norm_term = Envir.beta_norm oo Term.subst_atomic;
-
-fun abstract_thm thy eq =
- Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
-
-fun bind_def ctxt (name, ps) eq (xs, env, ths) =
- let
- val ((y, T), b) = LocalDefs.abs_def eq;
- val b' = norm_term env b;
- val th = abstract_thm (ProofContext.theory_of ctxt) eq;
- fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
- in
- exists (fn (x, _) => x = y) xs andalso
- err "Attempt to define previously specified variable";
- exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
- err "Attempt to redefine variable";
- (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
- end;
-
-
-(* CB: for finish_elems (Int and Ext),
- extracts specification, only of assumed elements *)
-
-fun eval_text _ _ _ (Fixes _) text = text
- | eval_text _ _ _ (Constrains _) text = text
- | eval_text _ (_, Assumed _) is_ext (Assumes asms)
- (((exts, exts'), (ints, ints')), (xs, env, defs)) =
- let
- val ts = maps (map #1 o #2) asms;
- val ts' = map (norm_term env) ts;
- val spec' =
- if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
- else ((exts, exts'), (ints @ ts, ints' @ ts'));
- in (spec', (fold Term.add_frees ts' xs, env, defs)) end
- | eval_text _ (_, Derived _) _ (Assumes _) text = text
- | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
- (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
- | eval_text _ (_, Derived _) _ (Defines _) text = text
- | eval_text _ _ _ (Notes _) text = text;
-
-
-(* for finish_elems (Int),
- remove redundant elements of derived identifiers,
- turn assumptions and definitions into facts,
- satisfy hypotheses of facts *)
-
-fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
- | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
- | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
- | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
-
- | finish_derived _ _ (Derived _) (Fixes _) = NONE
- | finish_derived _ _ (Derived _) (Constrains _) = NONE
- | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
- |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
- |> pair Thm.assumptionK |> Notes
- |> Element.morph_ctxt satisfy |> SOME
- | finish_derived sign satisfy (Derived _) (Defines defs) = defs
- |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
- |> pair Thm.definitionK |> Notes
- |> Element.morph_ctxt satisfy |> SOME
-
- | finish_derived _ satisfy _ (Notes facts) = Notes facts
- |> Element.morph_ctxt satisfy |> SOME;
-
-(* CB: for finish_elems (Ext) *)
-
-fun closeup _ false elem = elem
- | closeup ctxt true elem =
- let
- fun close_frees t =
- let
- val rev_frees =
- Term.fold_aterms (fn Free (x, T) =>
- if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
- in Term.list_all_free (rev rev_frees, t) end;
-
- fun no_binds [] = []
- | no_binds _ = error "Illegal term bindings in locale element";
- in
- (case elem of
- Assumes asms => Assumes (asms |> map (fn (a, propps) =>
- (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
- | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
- (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
- | e => e)
- end;
-
-
-fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
- let val x = Binding.base_name b
- in (b, AList.lookup (op =) parms x, mx) end) fixes)
- | finish_ext_elem parms _ (Constrains _, _) = Constrains []
- | finish_ext_elem _ close (Assumes asms, propp) =
- close (Assumes (map #1 asms ~~ propp))
- | finish_ext_elem _ close (Defines defs, propp) =
- close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
- | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
-
-
-(* CB: finish_parms introduces type info from parms to identifiers *)
-(* CB: only needed for types that have been NONE so far???
- If so, which are these??? *)
-
-fun finish_parms parms (((name, ps), mode), elems) =
- (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
-
-fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
- let
- val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
- val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
- val text' = fold (eval_text ctxt id' false) es text;
- val es' = map_filter
- (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
- in ((text', wits'), (id', map Int es')) end
- | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
- let
- val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
- val text' = eval_text ctxt id true e' text;
- in ((text', wits), (id, [Ext e'])) end
-
-in
-
-(* CB: only called by prep_elemss *)
-
-fun finish_elemss ctxt parms do_close =
- foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
-
-end;
-
-
-(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
-
-fun defs_ord (defs1, defs2) =
- list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
- TermOrd.fast_term_ord (d1, d2)) (defs1, defs2);
-structure Defstab =
- TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
-
-fun rem_dup_defs es ds =
- fold_map (fn e as (Defines defs) => (fn ds =>
- if Defstab.defined ds defs
- then (Defines [], ds)
- else (e, Defstab.update (defs, ()) ds))
- | e => (fn ds => (e, ds))) es ds;
-fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
- | rem_dup_elemss (Ext e) ds = (Ext e, ds);
-fun rem_dup_defines raw_elemss =
- fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
- apfst (pair id) (rem_dup_elemss es ds))
- | (id as (_, (Derived _)), es) => (fn ds =>
- ((id, es), ds))) raw_elemss Defstab.empty |> #1;
-
-(* CB: type inference and consistency checks for locales.
-
- Works by building a context (through declare_elemss), extracting the
- required information and adjusting the context elements (finish_elemss).
- Can also universally close free vars in assms and defs. This is only
- needed for Ext elements and controlled by parameter do_close.
-
- Only elements of assumed identifiers are considered.
-*)
-
-fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
- let
- (* CB: contexts computed in the course of this function are discarded.
- They are used for type inference and consistency checks only. *)
- (* CB: fixed_params are the parameters (with types) of the target locale,
- empty list if there is no target. *)
- (* CB: raw_elemss are list of pairs consisting of identifiers and
- context elements, the latter marked as internal or external. *)
- val raw_elemss = rem_dup_defines raw_elemss;
- val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context;
- (* CB: raw_ctxt is context with additional fixed variables derived from
- the fixes elements in raw_elemss,
- raw_proppss contains assumptions and definitions from the
- external elements in raw_elemss. *)
- fun prep_prop raw_propp (raw_ctxt, raw_concl) =
- let
- (* CB: add type information from fixed_params to context (declare_term) *)
- (* CB: process patterns (conclusion and external elements only) *)
- val (ctxt, all_propp) =
- prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
- (* CB: add type information from conclusion and external elements to context *)
- val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
- (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
- val all_propp' = map2 (curry (op ~~))
- (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
- val (concl, propp) = chop (length raw_concl) all_propp';
- in (propp, (ctxt, concl)) end
-
- val (proppss, (ctxt, concl)) =
- (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
-
- (* CB: obtain all parameters from identifier part of raw_elemss *)
- val xs = map #1 (params_of' raw_elemss);
- val typing = unify_frozen ctxt 0
- (map (Variable.default_type raw_ctxt) xs)
- (map (Variable.default_type ctxt) xs);
- val parms = param_types (xs ~~ typing);
- (* CB: parms are the parameters from raw_elemss, with correct typing. *)
-
- (* CB: extract information from assumes and defines elements
- (fixes, constrains and notes in raw_elemss don't have an effect on
- text and elemss), compute final form of context elements. *)
- val ((text, _), elemss) = finish_elemss ctxt parms do_close
- ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
- (* CB: text has the following structure:
- (((exts, exts'), (ints, ints')), (xs, env, defs))
- where
- exts: external assumptions (terms in external assumes elements)
- exts': dito, normalised wrt. env
- ints: internal assumptions (terms in internal assumes elements)
- ints': dito, normalised wrt. env
- xs: the free variables in exts' and ints' and rhss of definitions,
- this includes parameters except defined parameters
- env: list of term pairs encoding substitutions, where the first term
- is a free variable; substitutions represent defines elements and
- the rhs is normalised wrt. the previous env
- defs: theorems representing the substitutions from defines elements
- (thms are normalised wrt. env).
- elemss is an updated version of raw_elemss:
- - type info added to Fixes and modified in Constrains
- - axiom and definition statement replaced by corresponding one
- from proppss in Assumes and Defines
- - Facts unchanged
- *)
- in ((parms, elemss, concl), text) end;
-
-in
-
-fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x;
-fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x;
-
-end;
-
-
-(* facts and attributes *)
-
-local
-
-fun check_name name =
- if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
- else name;
-
-fun prep_facts _ _ _ ctxt (Int elem) = elem
- |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
- | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
- {var = I, typ = I, term = I,
- binding = Binding.map_base prep_name,
- fact = get ctxt,
- attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
-
-in
-
-fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
-fun cert_facts x = prep_facts I (K I) (K I) x;
-
-end;
-
-
-(* Get the specification of a locale *)
-
-(*The global specification is made from the parameters and global
- assumptions, the local specification from the parameters and the
- local assumptions.*)
-
-local
-
-fun gen_asms_of get thy name =
- let
- val ctxt = ProofContext.init thy;
- val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
- val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
- in
- elemss |> get
- |> maps (fn (_, es) => map (fn Int e => e) es)
- |> maps (fn Assumes asms => asms | _ => [])
- |> map (apsnd (map fst))
- end;
-
-in
-
-fun parameters_of thy = #params o the_locale thy;
-
-fun intros thy = #intros o the_locale thy;
- (*returns introduction rule for delta predicate and locale predicate
- as a pair of singleton lists*)
-
-fun dests thy = #dests o the_locale thy;
-
-fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts
- | _ => NONE) o #elems o the_locale thy;
-
-fun parameters_of_expr thy expr =
- let
- val ctxt = ProofContext.init thy;
- val pts = params_of_expr ctxt [] (intern_expr thy expr)
- ([], Symtab.empty, Symtab.empty);
- val raw_params_elemss = make_raw_params_elemss pts;
- val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
- (([], Symtab.empty), Expr expr);
- val ((parms, _, _), _) =
- read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) [];
- in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end;
-
-fun local_asms_of thy name =
- gen_asms_of (single o Library.last_elem) thy name;
-
-fun global_asms_of thy name =
- gen_asms_of I thy name;
-
-end;
-
-
-(* full context statements: imports + elements + conclusion *)
-
-local
-
-fun prep_context_statement prep_expr prep_elemss prep_facts
- do_close fixed_params imports elements raw_concl context =
- let
- val thy = ProofContext.theory_of context;
-
- val (import_params, import_tenv, import_syn) =
- params_of_expr context fixed_params (prep_expr thy imports)
- ([], Symtab.empty, Symtab.empty);
- val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
- val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
- (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
-
- val ((import_ids, _), raw_import_elemss) =
- flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports);
- (* CB: normalise "includes" among elements *)
- val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
- ((import_ids, incl_syn), elements);
-
- val raw_elemss = flat raw_elemsss;
- (* CB: raw_import_elemss @ raw_elemss is the normalised list of
- context elements obtained from import and elements. *)
- (* Now additional elements for parameters are inserted. *)
- val import_params_ids = make_params_ids import_params;
- val incl_params_ids =
- make_params_ids (incl_params \\ import_params);
- val raw_import_params_elemss =
- make_raw_params_elemss (import_params, incl_tenv, incl_syn);
- val raw_incl_params_elemss =
- make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn);
- val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
- context fixed_params
- (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
-
- (* replace extended ids (for axioms) by ids *)
- val (import_ids', incl_ids) = chop (length import_ids) ids;
- val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
- val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
- (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
- (all_ids ~~ all_elemss);
- (* CB: all_elemss and parms contain the correct parameter types *)
-
- val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
- val ((import_elemss, _), import_ctxt) =
- activate_facts false prep_facts ps context;
-
- val ((elemss, _), ctxt) =
- activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt);
- in
- ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
- (parms, spec, defs)), concl)
- end;
-
-fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
- let
- val thy = ProofContext.theory_of ctxt;
- val locale = Option.map (prep_locale thy) raw_locale;
- val (fixed_params, imports) =
- (case locale of
- NONE => ([], empty)
- | SOME name =>
- let val {params = ps, ...} = the_locale thy name
- in (map fst ps, Locale name) end);
- val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
- prep_ctxt false fixed_params imports (map Elem elems) concl ctxt;
- in (locale, locale_ctxt, elems_ctxt, concl') end;
-
-fun prep_expr prep imports body ctxt =
- let
- val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt;
- val all_elems = maps snd (import_elemss @ elemss);
- in (all_elems, ctxt') end;
-
-in
-
-val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
-val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
-
-fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt);
-fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt);
-
-val read_expr = prep_expr read_context;
-val cert_expr = prep_expr cert_context;
-
-fun read_context_statement loc = prep_statement (K I) read_ctxt loc;
-fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc;
-fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc;
-
-end;
-
-
-(* init *)
-
-fun init loc =
- ProofContext.init
- #> #2 o cert_context_statement (SOME loc) [] [];
-
-
-(* print locale *)
-
-fun print_locale thy show_facts imports body =
- let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in
- Pretty.big_list "locale elements:" (all_elems
- |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
- |> map (Element.pretty_ctxt ctxt) |> filter_out null
- |> map Pretty.chunks)
- |> Pretty.writeln
- end;
-
-
-
-(** store results **)
-
-(* join equations of an id with already accumulated ones *)
-
-fun join_eqns get_reg id eqns =
- let
- val eqns' = case get_reg id
- of NONE => eqns
- | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns')
- (* prefer equations from eqns' *)
- in ((id, eqns'), eqns') end;
-
-
-(* collect witnesses and equations up to a particular target for a
- registration; requires parameters and flattened list of identifiers
- instead of recomputing it from the target *)
-
-fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let
-
- val thy = ProofContext.theory_of ctxt;
-
- val ts = map (var_inst_term (impT, imp)) ext_ts;
- val (parms, parmTs) = split_list parms;
- val parmvTs = map Logic.varifyT parmTs;
- val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
- val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
- |> Symtab.make;
- val inst = Symtab.make (parms ~~ ts);
-
- (* instantiate parameter names in ids *)
- val ext_inst = Symtab.make (parms ~~ ext_ts);
- fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps;
- val inst_ids = map (apfst (apsnd ext_inst_names)) ids;
- val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
- val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids;
- val eqns =
- fold_map (join_eqns (get_local_registration ctxt imprt))
- (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd;
- in ((tinst, inst), wits, eqns) end;
-
-
-(* compute and apply morphism *)
-
-fun name_morph phi_name (lprfx, pprfx) b =
- b
- |> (if not (Binding.is_empty b) andalso pprfx <> ""
- then Binding.add_prefix false pprfx else I)
- |> (if not (Binding.is_empty b)
- then Binding.add_prefix false lprfx else I)
- |> phi_name;
-
-fun inst_morph thy phi_name param_prfx insts prems eqns export =
- let
- (* standardise export morphism *)
- val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
- val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
- (* FIXME sync with exp_fact *)
- val exp_typ = Logic.type_map exp_term;
- val export' =
- Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
- in
- Morphism.binding_morphism (name_morph phi_name param_prfx) $>
- Element.inst_morphism thy insts $>
- Element.satisfy_morphism prems $>
- Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
- Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $>
- export'
- end;
-
-fun activate_note thy phi_name param_prfx attrib insts prems eqns exp =
- (Element.facts_map o Element.morph_ctxt)
- (inst_morph thy phi_name param_prfx insts prems eqns exp)
- #> Attrib.map_facts attrib;
-
-
-(* public interface to interpretation morphism *)
-
-fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts =
- let
- val parms = the_locale thy target |> #params |> map fst;
- val ids = flatten (ProofContext.init thy, intern_expr thy)
- (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
- val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
- in
- inst_morph thy phi_name param_prfx insts prems eqns exp
- end;
-
-(* store instantiations of args for all registered interpretations
- of the theory *)
-
-fun note_thmss_registrations target (kind, args) thy =
- let
- val parms = the_locale thy target |> #params |> map fst;
- val ids = flatten (ProofContext.init thy, intern_expr thy)
- (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
-
- val regs = get_global_registrations thy target;
- (* add args to thy for all registrations *)
-
- fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
- let
- val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
- val args' = args
- |> activate_note thy phi_name param_prfx
- (Attrib.attribute_i thy) insts prems eqns exp;
- in
- thy
- |> global_note_qualified kind args'
- |> snd
- end;
- in fold activate regs thy end;
-
-
-(* locale results *)
-
-fun add_thmss loc kind args ctxt =
- let
- val (([(_, [Notes args'])], _), ctxt') =
- activate_facts true cert_facts
- [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
- val ctxt'' = ctxt' |> ProofContext.theory
- (change_locale loc
- (fn (axiom, elems, params, decls, regs, intros, dests) =>
- (axiom, elems @ [(Notes args', stamp ())],
- params, decls, regs, intros, dests))
- #> note_thmss_registrations loc args');
- in ctxt'' end;
-
-
-(* declarations *)
-
-local
-
-fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
-
-fun add_decls add loc decl =
- ProofContext.theory (change_locale loc
- (fn (axiom, elems, params, decls, regs, intros, dests) =>
- (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
- add_thmss loc Thm.internalK
- [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
-
-in
-
-val add_type_syntax = add_decls (apfst o cons);
-val add_term_syntax = add_decls (apsnd o cons);
-val add_declaration = add_decls (K I);
-
-fun declarations_of thy loc =
- the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst);
-
-end;
-
-
-
-(** define locales **)
-
-(* predicate text *)
-(* CB: generate locale predicates and delta predicates *)
-
-local
-
-(* introN: name of theorems for introduction rules of locale and
- delta predicates;
- axiomsN: name of theorem set with destruct rules for locale predicates,
- also name suffix of delta predicates. *)
-
-val introN = "intro";
-val axiomsN = "axioms";
-
-fun atomize_spec thy ts =
- let
- val t = Logic.mk_conjunction_balanced ts;
- val body = ObjectLogic.atomize_term thy t;
- val bodyT = Term.fastype_of body;
- in
- if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
- else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
- end;
-
-fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
- if length args = n then
- Syntax.const "_aprop" $
- Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
- else raise Match);
-
-(* CB: define one predicate including its intro rule and axioms
- - bname: predicate name
- - parms: locale parameters
- - defs: thms representing substitutions from defines elements
- - ts: terms representing locale assumptions (not normalised wrt. defs)
- - norm_ts: terms representing locale assumptions (normalised wrt. defs)
- - thy: the theory
-*)
-
-fun def_pred bname parms defs ts norm_ts thy =
- let
- val name = Sign.full_bname thy bname;
-
- val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
- val env = Term.add_free_names body [];
- val xs = filter (member (op =) env o #1) parms;
- val Ts = map #2 xs;
- val extraTs =
- (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
- |> Library.sort_wrt #1 |> map TFree;
- val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
-
- val args = map Logic.mk_type extraTs @ map Free xs;
- val head = Term.list_comb (Const (name, predT), args);
- val statement = ObjectLogic.ensure_propT thy head;
-
- val ([pred_def], defs_thy) =
- thy
- |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
- |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
- |> PureThy.add_defs false
- [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
- val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
-
- val cert = Thm.cterm_of defs_thy;
-
- val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
- MetaSimplifier.rewrite_goals_tac [pred_def] THEN
- Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
- Tactic.compose_tac (false,
- Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
-
- val conjuncts =
- (Drule.equal_elim_rule2 OF [body_eq,
- MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
- |> Conjunction.elim_balanced (length ts);
- val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
- Element.prove_witness defs_ctxt t
- (MetaSimplifier.rewrite_goals_tac defs THEN
- Tactic.compose_tac (false, ax, 0) 1));
- in ((statement, intro, axioms), defs_thy) end;
-
-fun assumes_to_notes (Assumes asms) axms =
- fold_map (fn (a, spec) => fn axs =>
- let val (ps, qs) = chop (length spec) axs
- in ((a, [(ps, [])]), qs) end) asms axms
- |> apfst (curry Notes Thm.assumptionK)
- | assumes_to_notes e axms = (e, axms);
-
-(* CB: the following two change only "new" elems, these have identifier ("", _). *)
-
-(* turn Assumes into Notes elements *)
-
-fun change_assumes_elemss axioms elemss =
- let
- val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
- fun change (id as ("", _), es) =
- fold_map assumes_to_notes (map satisfy es)
- #-> (fn es' => pair (id, es'))
- | change e = pair e;
- in
- fst (fold_map change elemss (map Element.conclude_witness axioms))
- end;
-
-(* adjust hyps of Notes elements *)
-
-fun change_elemss_hyps axioms elemss =
- let
- val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
- fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
- | change e = e;
- in map change elemss end;
-
-in
-
-(* CB: main predicate definition function *)
-
-fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
- let
- val ((elemss', more_ts), a_elem, a_intro, thy'') =
- if null exts then ((elemss, []), [], [], thy)
- else
- let
- val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
- val ((statement, intro, axioms), thy') =
- thy
- |> def_pred aname parms defs exts exts';
- val elemss' = change_assumes_elemss axioms elemss;
- val a_elem = [(("", []),
- [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
- val (_, thy'') =
- thy'
- |> Sign.add_path aname
- |> Sign.no_base_names
- |> PureThy.note_thmss Thm.internalK [((Binding.name introN, []), [([intro], [])])]
- ||> Sign.restore_naming thy';
- in ((elemss', [statement]), a_elem, [intro], thy'') end;
- val (predicate, stmt', elemss'', b_intro, thy'''') =
- if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'')
- else
- let
- val ((statement, intro, axioms), thy''') =
- thy''
- |> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts);
- val cstatement = Thm.cterm_of thy''' statement;
- val elemss'' = change_elemss_hyps axioms elemss';
- val b_elem = [(("", []),
- [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
- val (_, thy'''') =
- thy'''
- |> Sign.add_path pname
- |> Sign.no_base_names
- |> PureThy.note_thmss Thm.internalK
- [((Binding.name introN, []), [([intro], [])]),
- ((Binding.name axiomsN, []),
- [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
- ||> Sign.restore_naming thy''';
- in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
- in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
-
-end;
-
-
-(* add_locale(_i) *)
-
-local
-
-(* turn Defines into Notes elements, accumulate definition terms *)
-
-fun defines_to_notes is_ext thy (Defines defs) defns =
- let
- val defs' = map (fn (_, (def, _)) => (Attrib.empty_binding, (def, []))) defs
- val notes = map (fn (a, (def, _)) =>
- (a, [([assume (cterm_of thy def)], [])])) defs
- in
- (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
- end
- | defines_to_notes _ _ e defns = (SOME e, defns);
-
-fun change_defines_elemss thy elemss defns =
- let
- fun change (id as (n, _), es) defns =
- let
- val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns
- in ((id, map_filter I es'), defns') end
- in fold_map change elemss defns end;
-
-fun gen_add_locale prep_ctxt prep_expr
- predicate_name bname raw_imports raw_body thy =
- (* predicate_name: "" - locale with predicate named as locale
- "name" - locale with predicate named "name" *)
- let
- val thy_ctxt = ProofContext.init thy;
- val name = Sign.full_bname thy bname;
- val _ = is_some (get_locale thy name) andalso
- error ("Duplicate definition of locale " ^ quote name);
-
- val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
- text as (parms, ((_, exts'), _), defs)) =
- prep_ctxt raw_imports raw_body thy_ctxt;
- val elemss = import_elemss @ body_elemss |>
- map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
-
- val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\
- List.foldr OldTerm.add_typ_tfrees [] (map snd parms);
- val _ = if null extraTs then ()
- else warning ("Additional type variable(s) in locale specification " ^ quote bname);
-
- val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
- val (elemss', defns) = change_defines_elemss thy elemss [];
- val elemss'' = elemss' @ [(("", []), defns)];
- val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
- define_preds predicate_name' text elemss'' thy;
- val regs = pred_axioms
- |> fold_map (fn (id, elems) => fn wts => let
- val ts = flat (map_filter (fn (Assumes asms) =>
- SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
- val (wts1, wts2) = chop (length ts) wts;
- in ((apsnd (map fst) id, wts1), wts2) end) elemss'''
- |> fst
- |> map_filter (fn (("", _), _) => NONE | e => SOME e);
- fun axiomify axioms elemss =
- (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
- val ts = flat (map_filter (fn (Assumes asms) =>
- SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
- val (axs1, axs2) = chop (length ts) axs;
- in (axs2, ((id, Assumed axs1), elems)) end)
- |> snd;
- val ((_, facts), ctxt) = activate_facts true (K I)
- (axiomify pred_axioms elemss''') (ProofContext.init thy');
- val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
- val export = Thm.close_derivation o Goal.norm_result o
- singleton (ProofContext.export view_ctxt thy_ctxt);
- val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
- val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss''');
- val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
- val axs' = map (Element.assume_witness thy') stmt';
- val loc_ctxt = thy'
- |> Sign.add_path bname
- |> Sign.no_base_names
- |> PureThy.note_thmss Thm.assumptionK facts' |> snd
- |> Sign.restore_naming thy'
- |> register_locale bname {axiom = axs',
- elems = map (fn e => (e, stamp ())) elems'',
- params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
- decls = ([], []),
- regs = regs,
- intros = intros,
- dests = map Element.conclude_witness pred_axioms}
- |> init name;
- in (name, loc_ctxt) end;
-
-in
-
-val add_locale = gen_add_locale cert_context (K I);
-val add_locale_cmd = gen_add_locale read_context intern_expr "";
-
-end;
-
-val _ = Context.>> (Context.map_theory
- (add_locale "" "var" empty [Fixes [(Binding.name (Name.internal "x"), NONE, NoSyn)]] #>
- snd #> ProofContext.theory_of #>
- add_locale "" "struct" empty [Fixes [(Binding.name (Name.internal "S"), NONE, Structure)]] #>
- snd #> ProofContext.theory_of));
-
-
-
-
-(** Normalisation of locale statements ---
- discharges goals implied by interpretations **)
-
-local
-
-fun locale_assm_intros thy =
- Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros))
- (#2 (LocalesData.get thy)) [];
-fun locale_base_intros thy =
- Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros))
- (#2 (LocalesData.get thy)) [];
-
-fun all_witnesses ctxt =
- let
- val thy = ProofContext.theory_of ctxt;
- fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
- (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) =>
- map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms)
- registrations [];
- in get (RegistrationsData.get (Context.Proof ctxt)) end;
-
-in
-
-fun intro_locales_tac eager ctxt facts st =
- let
- val wits = all_witnesses ctxt;
- val thy = ProofContext.theory_of ctxt;
- val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []);
- in
- Method.intros_tac (wits @ intros) facts st
- end;
-
-end;
-
-
-(** Interpretation commands **)
-
-local
-
-(* extract proof obligations (assms and defs) from elements *)
-
-fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
- | extract_asms_elems ((id, Derived _), _) = (id, []);
-
-
-(* activate instantiated facts in theory or context *)
-
-fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn
- phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
- let
- val ctxt = mk_ctxt thy_ctxt;
- fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt);
- fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt);
-
- val (all_propss, eq_props) = chop (length all_elemss) propss;
- val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
-
- (* Filter out fragments already registered. *)
-
- val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
- test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss))));
- val (new_pss, ys) = split_list xs;
- val (new_propss, new_thmss) = split_list ys;
-
- val thy_ctxt' = thy_ctxt
- (* add registrations *)
- |> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp))
- new_elemss new_pss
- (* add witnesses of Assumed elements (only those generate proof obligations) *)
- |> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss
- (* add equations *)
- |> fold2 (fn (id, _) => fold (add_eqn id)) eq_props
- ((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o
- Element.conclude_witness) eq_thms);
-
- val prems = flat (map_filter
- (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
- | ((_, Derived _), _) => NONE) all_elemss);
-
- val thy_ctxt'' = thy_ctxt'
- (* add witnesses of Derived elements *)
- |> fold (fn (id, thms) => fold
- (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
- (map_filter (fn ((_, Assumed _), _) => NONE
- | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
-
- fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt =
- let
- val ctxt = mk_ctxt thy_ctxt;
- val thy = ProofContext.theory_of ctxt;
- val facts' = facts
- |> activate_note thy phi_name param_prfx
- (attrib thy_ctxt) insts prems eqns exp;
- in
- thy_ctxt
- |> note kind facts'
- |> snd
- end
- | activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt;
-
- fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt =
- let
- val ctxt = mk_ctxt thy_ctxt;
- val thy = ProofContext.theory_of ctxt;
- val {params, elems, ...} = the_locale thy loc;
- val parms = map fst params;
- val param_prfx = param_prefix loc ps;
- val ids = flatten (ProofContext.init thy, intern_expr thy)
- (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
- val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
- in
- thy_ctxt
- |> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems
- end;
-
- in
- thy_ctxt''
- (* add equations as lemmas to context *)
- |> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK)
- ((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])]))
- (unflat eq_thms eq_attns) eq_thms
- (* add interpreted facts *)
- |> fold2 activate_elems new_elemss new_pss
- end;
-
-fun global_activate_facts_elemss x = gen_activate_facts_elemss
- ProofContext.init
- global_note_qualified
- Attrib.attribute_i
- put_global_registration
- add_global_witness
- add_global_equation
- x;
-
-fun local_activate_facts_elemss x = gen_activate_facts_elemss
- I
- local_note_qualified
- (Attrib.attribute_i o ProofContext.theory_of)
- put_local_registration
- add_local_witness
- add_local_equation
- x;
-
-fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
- let
- (* parameters *)
- val (parm_names, parm_types) = parms |> split_list
- ||> map (TypeInfer.paramify_vars o Logic.varifyT);
- val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar);
- val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst;
-
- (* parameter instantiations *)
- val d = length parms - length insts;
- val insts =
- if d < 0 then error "More arguments than parameters in instantiation."
- else insts @ replicate d NONE;
- val (given_ps, given_insts) =
- ((parm_names ~~ parm_types) ~~ insts) |> map_filter
- (fn (_, NONE) => NONE
- | ((n, T), SOME inst) => SOME ((n, T), inst))
- |> split_list;
- val (given_parm_names, given_parm_types) = given_ps |> split_list;
-
- (* parse insts / eqns *)
- val given_insts' = map (parse_term ctxt) given_insts;
- val eqns' = map (parse_prop ctxt) eqns;
-
- (* type inference and contexts *)
- val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns';
- val res = Syntax.check_terms ctxt arg;
- val ctxt' = ctxt |> fold Variable.auto_fixes res;
-
- (* instantiation *)
- val (type_parms'', res') = chop (length type_parms) res;
- val (given_insts'', eqns'') = chop (length given_insts) res';
- val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
- val inst = Symtab.make (given_parm_names ~~ given_insts'');
-
- (* export from eigencontext *)
- val export = Variable.export_morphism ctxt' ctxt;
-
- (* import, its inverse *)
- val domT = fold Term.add_tfrees res [] |> map TFree;
- val importT = domT |> map (fn x => (Morphism.typ export x, x))
- |> map_filter (fn (TFree _, _) => NONE (* fixed point of export *)
- | (TVar y, x) => SOME (fst y, x)
- | _ => error "internal: illegal export in interpretation")
- |> Vartab.make;
- val dom = fold Term.add_frees res [] |> map Free;
- val imprt = dom |> map (fn x => (Morphism.term export x, x))
- |> map_filter (fn (Free _, _) => NONE (* fixed point of export *)
- | (Var y, x) => SOME (fst y, x)
- | _ => error "internal: illegal export in interpretation")
- |> Vartab.make;
- in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end;
-
-val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
-val check_instantiations = prep_instantiations (K I) (K I);
-
-fun gen_prep_registration mk_ctxt test_reg activate
- prep_attr prep_expr prep_insts
- thy_ctxt phi_name raw_expr raw_insts =
- let
- val ctxt = mk_ctxt thy_ctxt;
- val thy = ProofContext.theory_of ctxt;
- val ctxt' = ProofContext.init thy;
- fun prep_attn attn = (apsnd o map)
- (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn;
-
- val expr = prep_expr thy raw_expr;
-
- val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty);
- val params_ids = make_params_ids (#1 pts);
- val raw_params_elemss = make_raw_params_elemss pts;
- val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr);
- val ((parms, all_elemss, _), (_, (_, defs, _))) =
- read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) [];
-
- (** compute instantiation **)
-
- (* consistency check: equations need to be stored in a particular locale,
- therefore if equations are present locale expression must be a name *)
-
- val _ = case (expr, snd raw_insts) of
- (Locale _, _) => () | (_, []) => ()
- | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name.";
-
- (* read or certify instantiation *)
- val (raw_insts', raw_eqns) = raw_insts;
- val (raw_eq_attns, raw_eqns') = split_list raw_eqns;
- val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns');
- val eq_attns = map prep_attn raw_eq_attns;
-
- (* defined params without given instantiation *)
- val not_given = filter_out (Symtab.defined inst1 o fst) parms;
- fun add_def (p, pT) inst =
- let
- val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
- NONE => error ("Instance missing for parameter " ^ quote p)
- | SOME (Free (_, T), t) => (t, T);
- val d = Element.inst_term (instT, inst) t;
- in Symtab.update_new (p, d) inst end;
- val inst2 = fold add_def not_given inst1;
- val inst_morphism = Element.inst_morphism thy (instT, inst2);
- (* Note: insts contain no vars. *)
-
- (** compute proof obligations **)
-
- (* restore "small" ids *)
- val ids' = map (fn ((n, ps), (_, mode)) =>
- ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode))
- ids;
- val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
- (* instantiate ids and elements *)
- val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
- ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
- map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
- |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
-
- (* equations *)
- val eqn_elems = if null eqns then []
- else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
-
- val propss = map extract_asms_elems inst_elemss @ eqn_elems;
-
- in
- (propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs)
- end;
-
-fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
- test_global_registration
- global_activate_facts_elemss mk_ctxt;
-
-fun gen_prep_local_registration mk_ctxt = gen_prep_registration I
- test_local_registration
- local_activate_facts_elemss mk_ctxt;
-
-val prep_global_registration = gen_prep_global_registration
- (K I) (K I) check_instantiations;
-val prep_global_registration_cmd = gen_prep_global_registration
- Attrib.intern_src intern_expr read_instantiations;
-
-val prep_local_registration = gen_prep_local_registration
- (K I) (K I) check_instantiations;
-val prep_local_registration_cmd = gen_prep_local_registration
- Attrib.intern_src intern_expr read_instantiations;
-
-fun prep_registration_in_locale target expr thy =
- (* target already in internal form *)
- let
- val ctxt = ProofContext.init thy;
- val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
- (([], Symtab.empty), Expr (Locale target));
- val fixed = the_locale thy target |> #params |> map #1;
- val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
- ((raw_target_ids, target_syn), Expr expr);
- val (target_ids, ids) = chop (length raw_target_ids) all_ids;
- val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];
-
- (** compute proof obligations **)
-
- (* restore "small" ids, with mode *)
- val ids' = map (apsnd snd) ids;
- (* remove Int markers *)
- val elemss' = map (fn (_, es) =>
- map (fn Int e => e) es) elemss
- (* extract assumptions and defs *)
- val ids_elemss = ids' ~~ elemss';
- val propss = map extract_asms_elems ids_elemss;
-
- (** activation function:
- - add registrations to the target locale
- - add induced registrations for all global registrations of
- the target, unless already present
- - add facts of induced registrations to theory **)
-
- fun activate thmss thy =
- let
- val satisfy = Element.satisfy_thm (flat thmss);
- val ids_elemss_thmss = ids_elemss ~~ thmss;
- val regs = get_global_registrations thy target;
-
- fun activate_id (((id, Assumed _), _), thms) thy =
- thy |> put_registration_in_locale target id
- |> fold (add_witness_in_locale target id) thms
- | activate_id _ thy = thy;
-
- fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy =
- let
- val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
- val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts));
- val disch = Element.satisfy_thm wits;
- val new_elemss = filter (fn (((name, ps), _), _) =>
- not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
- fun activate_assumed_id (((_, Derived _), _), _) thy = thy
- | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
- val ps' = inst_parms ps;
- in
- if test_global_registration thy (name, ps')
- then thy
- else thy
- |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
- |> fold (fn witn => fn thy => add_global_witness (name, ps')
- (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
- end;
-
- fun activate_derived_id ((_, Assumed _), _) thy = thy
- | activate_derived_id (((name, ps), Derived ths), _) thy = let
- val ps' = inst_parms ps;
- in
- if test_global_registration thy (name, ps')
- then thy
- else thy
- |> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp)
- |> fold (fn witn => fn thy => add_global_witness (name, ps')
- (witn |> Element.map_witness (fn (t, th) => (* FIXME *)
- (Element.inst_term insts t,
- disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
- end;
-
- fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
- let
- val att_morphism =
- Morphism.binding_morphism (name_morph phi_name param_prfx) $>
- Morphism.thm_morphism satisfy $>
- Element.inst_morphism thy insts $>
- Morphism.thm_morphism disch;
- val facts' = facts
- |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
- |> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy)
- |> (map o apfst o apfst) (name_morph phi_name param_prfx);
- in
- thy
- |> global_note_qualified kind facts'
- |> snd
- end
- | activate_elem _ _ thy = thy;
-
- fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;
-
- in thy |> fold activate_assumed_id ids_elemss_thmss
- |> fold activate_derived_id ids_elemss
- |> fold activate_elems new_elemss end;
- in
- thy |> fold activate_id ids_elemss_thmss
- |> fold activate_reg regs
- end;
-
- in (propss, activate) end;
-
-fun prep_propp propss = propss |> map (fn (_, props) =>
- map (rpair [] o Element.mark_witness) props);
-
-fun prep_result propps thmss =
- ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
-
-fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy =
- let
- val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts;
- fun after_qed' results =
- ProofContext.theory (activate (prep_result propss results))
- #> after_qed;
- in
- thy
- |> ProofContext.init
- |> Proof.theorem_i NONE after_qed' (prep_propp propss)
- |> Element.refine_witness
- |> Seq.hd
- |> pair morphs
- end;
-
-fun gen_interpret prep_registration after_qed name_morph expr insts int state =
- let
- val _ = Proof.assert_forward_or_chain state;
- val ctxt = Proof.context_of state;
- val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts;
- fun after_qed' results =
- Proof.map_context (K (ctxt |> activate (prep_result propss results)))
- #> Proof.put_facts NONE
- #> after_qed;
- in
- state
- |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
- "interpret" NONE after_qed' (map (pair (Binding.empty, [])) (prep_propp propss))
- |> Element.refine_witness |> Seq.hd
- |> pair morphs
- end;
-
-fun standard_name_morph interp_prfx b =
- if Binding.is_empty b then b
- else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
- fold (Binding.add_prefix false o fst) pprfx
- #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
- #> Binding.add_prefix false lprfx
- ) b;
-
-in
-
-val interpretation = gen_interpretation prep_global_registration;
-fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd
- I (standard_name_morph interp_prfx);
-
-fun interpretation_in_locale after_qed (raw_target, expr) thy =
- let
- val target = intern thy raw_target;
- val (propss, activate) = prep_registration_in_locale target expr thy;
- val raw_propp = prep_propp propss;
-
- val (_, _, goal_ctxt, propp) = thy
- |> ProofContext.init
- |> cert_context_statement (SOME target) [] raw_propp;
-
- fun after_qed' results =
- ProofContext.theory (activate (prep_result propss results))
- #> after_qed;
- in
- goal_ctxt
- |> Proof.theorem_i NONE after_qed' propp
- |> Element.refine_witness |> Seq.hd
- end;
-
-val interpret = gen_interpret prep_local_registration;
-fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
- I (standard_name_morph interp_prfx);
-
-end;
-
-end;
--- a/src/Pure/Isar/outer_parse.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML Wed Jan 21 16:51:45 2009 +0100
@@ -61,12 +61,12 @@
val list: 'a parser -> 'a list parser
val list1: 'a parser -> 'a list parser
val name: bstring parser
- val binding: Binding.T parser
+ val binding: binding parser
val xname: xstring parser
val text: string parser
val path: Path.T parser
val parname: string parser
- val parbinding: Binding.T parser
+ val parbinding: binding parser
val sort: string parser
val arity: (string * string list * string) parser
val multi_arity: (string list * string list * string) parser
@@ -81,11 +81,11 @@
val opt_mixfix': mixfix parser
val where_: string parser
val const: (string * string * mixfix) parser
- val params: (Binding.T * string option) list parser
- val simple_fixes: (Binding.T * string option) list parser
- val fixes: (Binding.T * string option * mixfix) list parser
- val for_fixes: (Binding.T * string option * mixfix) list parser
- val for_simple_fixes: (Binding.T * string option) list parser
+ val params: (binding * string option) list parser
+ val simple_fixes: (binding * string option) list parser
+ val fixes: (binding * string option * mixfix) list parser
+ val for_fixes: (binding * string option * mixfix) list parser
+ val for_simple_fixes: (binding * string option) list parser
val ML_source: (SymbolPos.text * Position.T) parser
val doc_source: (SymbolPos.text * Position.T) parser
val term_group: string parser
--- a/src/Pure/Isar/overloading.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/overloading.ML Wed Jan 21 16:51:45 2009 +0100
@@ -134,8 +134,8 @@
fun declare c_ty = pair (Const c_ty);
-fun define checked name (c, t) =
- Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t));
+fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name,
+ Logic.mk_equals (Const (c, Term.fastype_of t), t));
(* target *)
--- a/src/Pure/Isar/proof.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/proof.ML Wed Jan 21 16:51:45 2009 +0100
@@ -43,27 +43,27 @@
val match_bind_i: (term list * term) list -> state -> state
val let_bind: (string list * string) list -> state -> state
val let_bind_i: (term list * term) list -> state -> state
- val fix: (Binding.T * string option * mixfix) list -> state -> state
- val fix_i: (Binding.T * typ option * mixfix) list -> state -> state
+ val fix: (binding * string option * mixfix) list -> state -> state
+ val fix_i: (binding * typ option * mixfix) list -> state -> state
val assm: Assumption.export ->
(Attrib.binding * (string * string list) list) list -> state -> state
val assm_i: Assumption.export ->
- ((Binding.T * attribute list) * (term * term list) list) list -> state -> state
+ ((binding * attribute list) * (term * term list) list) list -> state -> state
val assume: (Attrib.binding * (string * string list) list) list -> state -> state
- val assume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
+ val assume_i: ((binding * attribute list) * (term * term list) list) list ->
state -> state
val presume: (Attrib.binding * (string * string list) list) list -> state -> state
- val presume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
+ val presume_i: ((binding * attribute list) * (term * term list) list) list ->
state -> state
- val def: (Attrib.binding * ((Binding.T * mixfix) * (string * string list))) list ->
+ val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list ->
state -> state
- val def_i: ((Binding.T * attribute list) *
- ((Binding.T * mixfix) * (term * term list))) list -> state -> state
+ val def_i: ((binding * attribute list) *
+ ((binding * mixfix) * (term * term list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
- val note_thmss_i: ((Binding.T * attribute list) *
+ val note_thmss_i: ((binding * attribute list) *
(thm list * attribute list) list) list -> state -> state
val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
@@ -87,7 +87,7 @@
(theory -> 'a -> attribute) ->
(context * 'b list -> context * (term list list * (context -> context))) ->
string -> Method.text option -> (thm list list -> state -> state) ->
- ((Binding.T * 'a list) * 'b) list -> state -> state
+ ((binding * 'a list) * 'b) list -> state -> state
val local_qed: Method.text option * bool -> state -> state
val theorem: Method.text option -> (thm list list -> context -> context) ->
(string * string list) list list -> context -> state
@@ -107,11 +107,11 @@
val have: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val have_i: Method.text option -> (thm list list -> state -> state) ->
- ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+ ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val show_i: Method.text option -> (thm list list -> state -> state) ->
- ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+ ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
val schematic_goal: state -> bool
val is_relevant: state -> bool
val local_future_proof: (state -> ('a * state) Future.future) ->
--- a/src/Pure/Isar/proof_context.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Jan 21 16:51:45 2009 +0100
@@ -23,7 +23,7 @@
val abbrev_mode: Proof.context -> bool
val set_stmt: bool -> Proof.context -> Proof.context
val naming_of: Proof.context -> NameSpace.naming
- val full_name: Proof.context -> Binding.T -> string
+ val full_name: Proof.context -> binding -> string
val full_bname: Proof.context -> bstring -> string
val consts_of: Proof.context -> Consts.T
val const_syntax_name: Proof.context -> string -> string
@@ -105,27 +105,27 @@
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
val note_thmss: string ->
- ((Binding.T * attribute list) * (Facts.ref * attribute list) list) list ->
+ ((binding * attribute list) * (Facts.ref * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val note_thmss_i: string ->
- ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
+ ((binding * attribute list) * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
- val read_vars: (Binding.T * string option * mixfix) list -> Proof.context ->
- (Binding.T * typ option * mixfix) list * Proof.context
- val cert_vars: (Binding.T * typ option * mixfix) list -> Proof.context ->
- (Binding.T * typ option * mixfix) list * Proof.context
- val add_fixes: (Binding.T * string option * mixfix) list ->
+ val read_vars: (binding * string option * mixfix) list -> Proof.context ->
+ (binding * typ option * mixfix) list * Proof.context
+ val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
+ (binding * typ option * mixfix) list * Proof.context
+ val add_fixes: (binding * string option * mixfix) list ->
Proof.context -> string list * Proof.context
- val add_fixes_i: (Binding.T * typ option * mixfix) list ->
+ val add_fixes_i: (binding * typ option * mixfix) list ->
Proof.context -> string list * Proof.context
val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
val add_assms: Assumption.export ->
- ((Binding.T * attribute list) * (string * string list) list) list ->
+ ((binding * attribute list) * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_assms_i: Assumption.export ->
- ((Binding.T * attribute list) * (term * term list) list) list ->
+ ((binding * attribute list) * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
@@ -135,7 +135,7 @@
Context.generic -> Context.generic
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
val add_abbrev: string -> Properties.T ->
- Binding.T * term -> Proof.context -> (term * term) * Proof.context
+ binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
val verbose: bool ref
val setmp_verbose: ('a -> 'b) -> 'a -> 'b
--- a/src/Pure/Isar/spec_parse.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML Wed Jan 21 16:51:45 2009 +0100
@@ -15,24 +15,23 @@
val opt_thm_name: string -> Attrib.binding parser
val spec: (Attrib.binding * string list) parser
val named_spec: (Attrib.binding * string list) parser
- val spec_name: ((Binding.T * string) * Attrib.src list) parser
- val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser
+ val spec_name: ((binding * string) * Attrib.src list) parser
+ val spec_opt_name: ((binding * string) * Attrib.src list) parser
val xthm: (Facts.ref * Attrib.src list) parser
val xthms1: (Facts.ref * Attrib.src list) list parser
val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
val locale_mixfix: mixfix parser
- val locale_fixes: (Binding.T * string option * mixfix) list parser
+ val locale_fixes: (binding * string option * mixfix) list parser
val locale_insts: (string option list * (Attrib.binding * string) list) parser
val class_expr: string list parser
- val locale_expr: Old_Locale.expr parser
- val locale_expression: Expression.expression parser
+ val locale_expression: Expression.expression parser
val locale_keyword: string parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
val specification:
- (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser
+ (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser
end;
structure SpecParse: SPEC_PARSE =
@@ -115,13 +114,6 @@
val class_expr = plus1_unless locale_keyword P.xname;
-val locale_expr =
- let
- fun expr2 x = (P.xname >> Old_Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
- and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Old_Locale.Rename || expr2) x
- and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Old_Locale.Merge es)) x;
- in expr0 end;
-
val locale_expression =
let
fun expr2 x = P.xname x;
--- a/src/Pure/Isar/specification.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/specification.ML Wed Jan 21 16:51:45 2009 +0100
@@ -9,33 +9,33 @@
signature SPECIFICATION =
sig
val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
- val check_specification: (Binding.T * typ option * mixfix) list ->
+ val check_specification: (binding * typ option * mixfix) list ->
(Attrib.binding * term list) list list -> Proof.context ->
- (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val read_specification: (Binding.T * string option * mixfix) list ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val read_specification: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list list -> Proof.context ->
- (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val check_free_specification: (Binding.T * typ option * mixfix) list ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val check_free_specification: (binding * typ option * mixfix) list ->
(Attrib.binding * term list) list -> Proof.context ->
- (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val read_free_specification: (Binding.T * string option * mixfix) list ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val read_free_specification: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list -> Proof.context ->
- (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val axiomatization: (Binding.T * typ option * mixfix) list ->
+ (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val axiomatization: (binding * typ option * mixfix) list ->
(Attrib.binding * term list) list -> theory ->
(term list * (string * thm list) list) * theory
- val axiomatization_cmd: (Binding.T * string option * mixfix) list ->
+ val axiomatization_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list -> theory ->
(term list * (string * thm list) list) * theory
val definition:
- (Binding.T * typ option * mixfix) option * (Attrib.binding * term) ->
+ (binding * typ option * mixfix) option * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory
val definition_cmd:
- (Binding.T * string option * mixfix) option * (Attrib.binding * string) ->
+ (binding * string option * mixfix) option * (Attrib.binding * string) ->
local_theory -> (term * (string * thm)) * local_theory
- val abbreviation: Syntax.mode -> (Binding.T * typ option * mixfix) option * term ->
+ val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
local_theory -> local_theory
- val abbreviation_cmd: Syntax.mode -> (Binding.T * string option * mixfix) option * string ->
+ val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
@@ -149,7 +149,8 @@
(*axioms*)
val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
- fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
+ fold_map Thm.add_axiom
+ ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props)))
#>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
(Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
--- a/src/Pure/Isar/theory_target.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Wed Jan 21 16:51:45 2009 +0100
@@ -6,7 +6,7 @@
signature THEORY_TARGET =
sig
- val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool,
+ val peek: local_theory -> {target: string, is_locale: bool,
is_class: bool, instantiation: string list * (string * sort) list * sort,
overloading: (string * (string * typ) * bool) list}
val init: string option -> theory -> local_theory
@@ -21,34 +21,17 @@
structure TheoryTarget: THEORY_TARGET =
struct
-(* new locales *)
-
-fun locale_extern new_locale x =
- if new_locale then Locale.extern x else Old_Locale.extern x;
-fun locale_add_type_syntax new_locale x =
- if new_locale then Locale.add_type_syntax x else Old_Locale.add_type_syntax x;
-fun locale_add_term_syntax new_locale x =
- if new_locale then Locale.add_term_syntax x else Old_Locale.add_term_syntax x;
-fun locale_add_declaration new_locale x =
- if new_locale then Locale.add_declaration x else Old_Locale.add_declaration x;
-fun locale_add_thmss new_locale x =
- if new_locale then Locale.add_thmss x else Old_Locale.add_thmss x;
-fun locale_init new_locale x =
- if new_locale then Locale.init x else Old_Locale.init x;
-fun locale_intern new_locale x =
- if new_locale then Locale.intern x else Old_Locale.intern x;
-
(* context data *)
-datatype target = Target of {target: string, new_locale: bool, is_locale: bool,
+datatype target = Target of {target: string, is_locale: bool,
is_class: bool, instantiation: string list * (string * sort) list * sort,
overloading: (string * (string * typ) * bool) list};
-fun make_target target new_locale is_locale is_class instantiation overloading =
- Target {target = target, new_locale = new_locale, is_locale = is_locale,
+fun make_target target is_locale is_class instantiation overloading =
+ Target {target = target, is_locale = is_locale,
is_class = is_class, instantiation = instantiation, overloading = overloading};
-val global_target = make_target "" false false false ([], [], []) [];
+val global_target = make_target "" false false ([], [], []) [];
structure Data = ProofDataFun
(
@@ -64,7 +47,7 @@
fun pretty_thy ctxt target is_locale is_class =
let
val thy = ProofContext.theory_of ctxt;
- val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
+ val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
(#1 (ProofContext.inferred_fixes ctxt));
val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
@@ -89,7 +72,7 @@
(* target declarations *)
-fun target_decl add (Target {target, new_locale, ...}) d lthy =
+fun target_decl add (Target {target, ...}) d lthy =
let
val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
val d0 = Morphism.form d';
@@ -100,12 +83,12 @@
|> LocalTheory.target (Context.proof_map d0)
else
lthy
- |> LocalTheory.target (add new_locale target d')
+ |> LocalTheory.target (add target d')
end;
-val type_syntax = target_decl locale_add_type_syntax;
-val term_syntax = target_decl locale_add_term_syntax;
-val declaration = target_decl locale_add_declaration;
+val type_syntax = target_decl Locale.add_type_syntax;
+val term_syntax = target_decl Locale.add_term_syntax;
+val declaration = target_decl Locale.add_declaration;
fun class_target (Target {target, ...}) f =
LocalTheory.raw_theory f #>
@@ -166,7 +149,7 @@
|> ProofContext.note_thmss_i kind facts
||> ProofContext.restore_naming ctxt;
-fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy =
+fun notes (Target {target, is_locale, ...}) kind facts lthy =
let
val thy = ProofContext.theory_of lthy;
val facts' = facts
@@ -185,7 +168,7 @@
#> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
#> Sign.restore_naming thy)
|> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
- |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts)
+ |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
|> note_local kind local_facts
end;
@@ -313,7 +296,7 @@
(fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
| NONE =>
if is_none (Class_Target.instantiation_param lthy c)
- then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
+ then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
val (global_def, lthy3) = lthy2
|> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
@@ -335,13 +318,13 @@
fun init_target _ NONE = global_target
| init_target thy (SOME target) =
make_target target (Locale.defined thy (Locale.intern thy target))
- true (Class_Target.is_class thy target) ([], [], []) [];
+ (Class_Target.is_class thy target) ([], [], []) [];
-fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
+fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
else if not (null overloading) then Overloading.init overloading
else if not is_locale then ProofContext.init
- else if not is_class then locale_init new_locale target
+ else if not is_class then Locale.init target
else Class_Target.init target;
fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
@@ -375,7 +358,7 @@
val ctxt = ProofContext.init thy;
val ops = raw_ops |> map (fn (name, const, checked) =>
(name, Term.dest_Const (prep_const ctxt const), checked));
- in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end;
+ in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
in
@@ -383,10 +366,9 @@
fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
fun context "-" thy = init NONE thy
- | context target thy = init (SOME (locale_intern
- (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
+ | context target thy = init (SOME (Locale.intern thy target)) thy;
-fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
+fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
fun instantiation_cmd raw_arities thy =
instantiation (read_multi_arity thy raw_arities) thy;
--- a/src/Pure/ML/ml_context.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Jan 21 16:51:45 2009 +0100
@@ -126,7 +126,8 @@
fun ml_store sel (name, ths) =
let
- val ths' = Context.>>> (Context.map_theory_result (PureThy.store_thms (name, ths)));
+ val ths' = Context.>>> (Context.map_theory_result
+ (PureThy.store_thms (Binding.name name, ths)));
val _ =
if name = "" then ()
else if not (ML_Syntax.is_identifier name) then
--- a/src/Pure/Proof/extraction.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Wed Jan 21 16:51:45 2009 +0100
@@ -733,11 +733,11 @@
val (def_thms, thy') = if t = nullt then ([], thy) else
thy
|> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
- |> PureThy.add_defs false [((extr_name s vs ^ "_def",
+ |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"),
Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
in
thy'
- |> PureThy.store_thm (corr_name s vs,
+ |> PureThy.store_thm (Binding.name (corr_name s vs),
Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
(Thm.forall_elim_var 0) (forall_intr_frees
(ProofChecker.thm_of_proof thy'
--- a/src/Pure/Tools/ROOT.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Tools/ROOT.ML Wed Jan 21 16:51:45 2009 +0100
@@ -9,8 +9,5 @@
(*basic XML support*)
use "xml_syntax.ML";
-(*derived theory and proof elements*)
-use "invoke.ML";
-
(*quickcheck needed here because of pg preferences*)
use "../../Tools/quickcheck.ML"
--- a/src/Pure/Tools/invoke.ML Tue Jan 20 19:09:19 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,127 +0,0 @@
-(* Title: Pure/Tools/invoke.ML
- Author: Makarius
-
-Schematic invocation of locale expression in proof context.
-*)
-
-signature INVOKE =
-sig
- val invoke: string * Attrib.src list -> Old_Locale.expr -> string option list ->
- (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
- val invoke_i: string * attribute list -> Old_Locale.expr -> term option list ->
- (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
-end;
-
-structure Invoke: INVOKE =
-struct
-
-
-(* invoke *)
-
-local
-
-fun gen_invoke prep_att prep_expr parse_term add_fixes
- (prfx, raw_atts) raw_expr raw_insts fixes int state =
- let
- val thy = Proof.theory_of state;
- val _ = Proof.assert_forward_or_chain state;
- val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
-
- val more_atts = map (prep_att thy) raw_atts;
- val (elems, _) = prep_expr raw_expr [] (ProofContext.init thy);
-
- val prems = maps Element.prems_of elems;
- val params = maps Element.params_of elems;
- val types = rev (fold Term.add_tfrees prems (fold (Term.add_tfreesT o #2) params []));
-
- val prems' = map Logic.varify prems;
- val params' = map (Logic.varify o Free) params;
- val types' = map (Logic.varifyT o TFree) types;
-
- val state' = state
- |> Proof.enter_forward
- |> Proof.begin_block
- |> Proof.map_context (snd o add_fixes fixes);
- val ctxt' = Proof.context_of state';
-
- val raw_insts' = zip_options params' raw_insts
- handle Library.UnequalLengths => error "Too many instantiations";
-
- fun prep_inst (t, u) =
- TypeInfer.constrain (TypeInfer.paramify_vars (Term.fastype_of t)) (parse_term ctxt' u);
- val insts = map #1 raw_insts' ~~
- Variable.polymorphic ctxt' (Syntax.check_terms ctxt' (map prep_inst raw_insts'));
- val inst_rules =
- replicate (length types') Drule.termI @
- map (fn t =>
- (case AList.lookup (op =) insts t of
- SOME u => Drule.mk_term (Thm.cterm_of thy u)
- | NONE => Drule.termI)) params';
-
- val propp =
- [((Binding.empty, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
- ((Binding.empty, []), map (rpair [] o Logic.mk_term) params'),
- ((Binding.empty, []), map (rpair [] o Element.mark_witness) prems')];
- fun after_qed results =
- Proof.end_block #>
- Proof.map_context (fn ctxt =>
- let
- val ([res_types, res_params, res_prems], ctxt'') =
- fold_burrow (apfst snd oo Variable.import_thms false) results ctxt';
-
- val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
- val params'' = map (Thm.term_of o Drule.dest_term) res_params;
- val inst = Element.morph_ctxt (Element.inst_morphism thy
- (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
- val elems' = map inst elems;
- val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
- val notes =
- maps (Element.facts_of thy) elems'
- |> Element.satisfy_facts prems''
- |> Element.generalize_facts ctxt'' ctxt
- |> Attrib.map_facts (Attrib.attribute_i thy)
- |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
- in
- ctxt
- |> ProofContext.sticky_prefix prfx
- |> ProofContext.qualified_names
- |> (snd o ProofContext.note_thmss_i "" notes)
- |> ProofContext.restore_naming ctxt
- end) #>
- Proof.put_facts NONE;
- in
- state'
- |> Proof.chain_facts chain_facts
- |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
- "invoke" NONE after_qed propp
- |> Element.refine_witness
- |> Seq.hd
- |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))),
- Position.none))
- |> Seq.hd
- end;
-
-in
-
-fun invoke x =
- gen_invoke Attrib.attribute Old_Locale.read_expr Syntax.parse_term ProofContext.add_fixes x;
-fun invoke_i x = gen_invoke (K I) Old_Locale.cert_expr (K I) ProofContext.add_fixes_i x;
-
-end;
-
-
-(* concrete syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ =
- OuterSyntax.command "invoke"
- "schematic invocation of locale expression in proof context"
- (K.tag_proof K.prf_goal)
- (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
- >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
- Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes)));
-
-end;
-
-end;
--- a/src/Pure/Tools/named_thms.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Tools/named_thms.ML
- ID: $Id$
Author: Makarius
Named collections of theorems in canonical order.
@@ -36,6 +35,6 @@
val setup =
Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
- PureThy.add_thms_dynamic (name, Data.get);
+ PureThy.add_thms_dynamic (Binding.name name, Data.get);
end;
--- a/src/Pure/assumption.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/assumption.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/assumption.ML
- ID: $Id$
Author: Makarius
Local assumptions, parameterized by export rules.
@@ -79,7 +78,7 @@
(* named prems -- legacy feature *)
val _ = Context.>>
- (Context.map_theory (PureThy.add_thms_dynamic ("prems",
+ (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
--- a/src/Pure/axclass.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/axclass.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/axclass.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Type classes defined as predicates, associated with a record of
@@ -9,7 +8,7 @@
signature AX_CLASS =
sig
val define_class: bstring * class list -> string list ->
- ((Binding.T * attribute list) * term list) list -> theory -> class * theory
+ ((binding * attribute list) * term list) list -> theory -> class * theory
val add_classrel: thm -> theory -> theory
val add_arity: thm -> theory -> theory
val prove_classrel: class * class -> tactic -> theory -> theory
@@ -329,7 +328,8 @@
quote (Syntax.string_of_classrel ctxt [c1, c2]));
in
thy
- |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])]
+ |> PureThy.add_thms [((Binding.name
+ (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
|-> (fn [th'] => add_classrel th')
end;
@@ -345,7 +345,7 @@
quote (Syntax.string_of_arity ctxt arity));
in
thy
- |> PureThy.add_thms (map (rpair []) (names ~~ ths))
+ |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
|-> fold add_arity
end;
@@ -372,10 +372,10 @@
|> Sign.no_base_names
|> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
|-> (fn const' as Const (c'', _) => Thm.add_def false true
- (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
+ (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
#>> Thm.varifyT
#-> (fn thm => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.add_thm ((c', thm), [Thm.kind_internal])
+ #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
#> snd
#> Sign.restore_naming thy
#> pair (Const (c, T))))
@@ -391,7 +391,7 @@
(NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
in
thy
- |> Thm.add_def false false (name', prop)
+ |> Thm.add_def false false (Binding.name name', prop)
|>> (fn thm => Drule.transitive_thm OF [eq, thm])
end;
@@ -469,7 +469,7 @@
val ([def], def_thy) =
thy
|> Sign.primitive_class (bclass, super)
- |> PureThy.add_defs false [((Thm.def_name bconst, class_eq), [])];
+ |> PureThy.add_defs false [((Binding.name (Thm.def_name bconst), class_eq), [])];
val (raw_intro, (raw_classrel, raw_axioms)) =
split_defined (length conjs) def ||> chop (length super);
@@ -515,7 +515,11 @@
val args = prep thy raw_args;
val specs = mk args;
val names = name args;
- in thy |> PureThy.add_axioms (map (rpair []) (names ~~ specs)) |-> fold add end;
+ in
+ thy
+ |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs))
+ |-> fold add
+ end;
fun ax_classrel prep =
axiomatize (map o prep) (map Logic.mk_classrel)
--- a/src/Pure/consts.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/consts.ML Wed Jan 21 16:51:45 2009 +0100
@@ -30,10 +30,10 @@
val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
- val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T
+ val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
val constrain: string * typ option -> T -> T
val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
- Binding.T * term -> T -> (term * term) * T
+ binding * term -> T -> (term * term) * T
val revert_abbrev: string -> string -> T -> T
val hide: bool -> string -> T -> T
val empty: T
--- a/src/Pure/drule.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/drule.ML Wed Jan 21 16:51:45 2009 +0100
@@ -460,10 +460,10 @@
val read_prop = certify o SimpleSyntax.read_prop;
fun store_thm name th =
- Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
+ Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
fun store_thm_open name th =
- Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
+ Context.>>> (Context.map_theory_result (PureThy.store_thm_open (Binding.name name, th)));
fun store_standard_thm name th = store_thm name (standard th);
fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
--- a/src/Pure/facts.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/facts.ML Wed Jan 21 16:51:45 2009 +0100
@@ -30,9 +30,9 @@
val props: T -> thm list
val could_unify: T -> term -> thm list
val merge: T * T -> T
- val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T
- val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T
- val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T
+ val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
+ val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
+ val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
end;
--- a/src/Pure/more_thm.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/more_thm.ML Wed Jan 21 16:51:45 2009 +0100
@@ -38,8 +38,8 @@
val forall_elim_vars: int -> thm -> thm
val unvarify: thm -> thm
val close_derivation: thm -> thm
- val add_axiom: bstring * term -> theory -> thm * theory
- val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
+ val add_axiom: binding * term -> theory -> thm * theory
+ val add_def: bool -> bool -> binding * term -> theory -> thm * theory
val rule_attribute: (Context.generic -> thm -> thm) -> attribute
val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
val theory_attributes: attribute list -> theory * thm -> theory * thm
@@ -276,14 +276,15 @@
(** specification primitives **)
-fun add_axiom (name, prop) thy =
+fun add_axiom (b, prop) thy =
let
- val name' = if name = "" then "axiom_" ^ serial_string () else name;
- val thy' = thy |> Theory.add_axioms_i [(name', prop)];
- val axm = unvarify (Thm.axiom thy' (Sign.full_bname thy' name'));
+ val b' = if Binding.is_empty b
+ then Binding.name ("axiom_" ^ serial_string ()) else b;
+ val thy' = thy |> Theory.add_axioms_i [(b', prop)];
+ val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b'));
in (axm, thy') end;
-fun add_def unchecked overloaded (name, prop) thy =
+fun add_def unchecked overloaded (b, prop) thy =
let
val tfrees = rev (map TFree (Term.add_tfrees prop []));
val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
@@ -291,8 +292,8 @@
val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
- val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
- val axm' = Thm.axiom thy' (Sign.full_bname thy' name);
+ val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
+ val axm' = Thm.axiom thy' (Sign.full_name thy' b);
val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
in (thm, thy') end;
--- a/src/Pure/morphism.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/morphism.ML Wed Jan 21 16:51:45 2009 +0100
@@ -16,21 +16,21 @@
signature MORPHISM =
sig
include BASIC_MORPHISM
- val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix
- val binding: morphism -> Binding.T -> Binding.T
+ val var: morphism -> binding * mixfix -> binding * mixfix
+ val binding: morphism -> binding -> binding
val typ: morphism -> typ -> typ
val term: morphism -> term -> term
val fact: morphism -> thm list -> thm list
val thm: morphism -> thm -> thm
val cterm: morphism -> cterm -> cterm
val morphism:
- {binding: Binding.T -> Binding.T,
- var: Binding.T * mixfix -> Binding.T * mixfix,
+ {binding: binding -> binding,
+ var: binding * mixfix -> binding * mixfix,
typ: typ -> typ,
term: term -> term,
fact: thm list -> thm list} -> morphism
- val binding_morphism: (Binding.T -> Binding.T) -> morphism
- val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism
+ val binding_morphism: (binding -> binding) -> morphism
+ val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism
val typ_morphism: (typ -> typ) -> morphism
val term_morphism: (term -> term) -> morphism
val fact_morphism: (thm list -> thm list) -> morphism
@@ -45,8 +45,8 @@
struct
datatype morphism = Morphism of
- {binding: Binding.T -> Binding.T,
- var: Binding.T * mixfix -> Binding.T * mixfix,
+ {binding: binding -> binding,
+ var: binding * mixfix -> binding * mixfix,
typ: typ -> typ,
term: term -> term,
fact: thm list -> thm list};
--- a/src/Pure/primitive_defs.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/primitive_defs.ML Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/primitive_defs.ML
- ID: $Id$
Author: Makarius
Primitive definition forms.
--- a/src/Pure/pure_thy.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/pure_thy.ML Wed Jan 21 16:51:45 2009 +0100
@@ -24,27 +24,27 @@
val name_thm: bool -> bool -> Position.T -> string -> thm -> thm
val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list
val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list
- val store_thms: bstring * thm list -> theory -> thm list * theory
- val store_thm: bstring * thm -> theory -> thm * theory
- val store_thm_open: bstring * thm -> theory -> thm * theory
- val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
- val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
- val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
- val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
- val note_thmss: string -> ((Binding.T * attribute list) *
+ val store_thms: binding * thm list -> theory -> thm list * theory
+ val store_thm: binding * thm -> theory -> thm * theory
+ val store_thm_open: binding * thm -> theory -> thm * theory
+ val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
+ val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
+ val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
+ val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
+ val note_thmss: string -> ((binding * attribute list) *
(thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
- val note_thmss_grouped: string -> string -> ((Binding.T * attribute list) *
+ val note_thmss_grouped: string -> string -> ((binding * attribute list) *
(thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
- val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
+ val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
- val add_defs: bool -> ((bstring * term) * attribute list) list ->
+ val add_defs: bool -> ((binding * term) * attribute list) list ->
theory -> thm list * theory
- val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list ->
+ val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
+ theory -> thm list * theory
+ val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
theory -> thm list * theory
val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
theory -> thm list * theory
- val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
- theory -> thm list * theory
val old_appl_syntax: theory -> bool
val old_appl_syntax_setup: theory -> theory
end;
@@ -163,21 +163,21 @@
(* store_thm(s) *)
-fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none)
- (name_thms false true Position.none) I (Binding.name bname, thms);
+fun store_thms (b, thms) = enter_thms (name_thms true true Position.none)
+ (name_thms false true Position.none) I (b, thms);
-fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single;
+fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
-fun store_thm_open (bname, th) =
+fun store_thm_open (b, th) =
enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
- (Binding.name bname, [th]) #>> the_single;
+ (b, [th]) #>> the_single;
(* add_thms(s) *)
-fun add_thms_atts pre_name ((bname, thms), atts) =
+fun add_thms_atts pre_name ((b, thms), atts) =
enter_thms pre_name (name_thms false true Position.none)
- (foldl_map (Thm.theory_attributes atts)) (Binding.name bname, thms);
+ (foldl_map (Thm.theory_attributes atts)) (b, thms);
fun gen_add_thmss pre_name =
fold_map (add_thms_atts pre_name);
@@ -192,9 +192,9 @@
(* add_thms_dynamic *)
-fun add_thms_dynamic (bname, f) thy = thy
+fun add_thms_dynamic (b, f) thy = thy
|> (FactsData.map o apfst)
- (Facts.add_dynamic (Sign.naming_of thy) (Binding.name bname, f) #> snd);
+ (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
(* note_thmss *)
@@ -224,21 +224,21 @@
(* store axioms as theorems *)
local
- fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_bname thy name);
+ fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
- fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
+ fun add_axm prep_b add = fold_map (fn ((b, ax), atts) => fn thy =>
let
- val named_ax = [(name, ax)];
+ val named_ax = [(b, ax)];
val thy' = add named_ax thy;
- val thm = hd (get_axs thy' named_ax);
- in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end);
+ val thm = hd (get_axs thy' ((map o apfst) prep_b named_ax));
+ in apfst hd (gen_add_thms (K I) [((prep_b b, thm), atts)] thy') end);
in
- val add_defs = add_axm o Theory.add_defs_i false;
- val add_defs_unchecked = add_axm o Theory.add_defs_i true;
- val add_axioms = add_axm Theory.add_axioms_i;
- val add_defs_cmd = add_axm o Theory.add_defs false;
- val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
- val add_axioms_cmd = add_axm Theory.add_axioms;
+ val add_defs = add_axm I o Theory.add_defs_i false;
+ val add_defs_unchecked = add_axm I o Theory.add_defs_i true;
+ val add_axioms = add_axm I Theory.add_axioms_i;
+ val add_defs_cmd = add_axm Binding.name o Theory.add_defs false;
+ val add_defs_unchecked_cmd = add_axm Binding.name o Theory.add_defs true;
+ val add_axioms_cmd = add_axm Binding.name Theory.add_axioms;
end;
@@ -378,16 +378,16 @@
("sort_constraint", typ "'a itself => prop", NoSyn),
("conjunction", typ "prop => prop => prop", NoSyn)]
#> (add_defs false o map Thm.no_attributes)
- [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
- ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
- ("sort_constraint_def",
+ [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
+ (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
+ (Binding.name "sort_constraint_def",
prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
\ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
- ("conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
+ (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
#> Sign.hide_const false "Pure.term"
#> Sign.hide_const false "Pure.sort_constraint"
#> Sign.hide_const false "Pure.conjunction"
- #> add_thmss [(("nothing", []), [])] #> snd
- #> Theory.add_axioms_i Proofterm.equality_axms));
+ #> add_thmss [((Binding.name "nothing", []), [])] #> snd
+ #> Theory.add_axioms_i ((map o apfst) Binding.name Proofterm.equality_axms)));
end;
--- a/src/Pure/sign.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/sign.ML Wed Jan 21 16:51:45 2009 +0100
@@ -14,7 +14,7 @@
tsig: Type.tsig,
consts: Consts.T}
val naming_of: theory -> NameSpace.naming
- val full_name: theory -> Binding.T -> string
+ val full_name: theory -> binding -> string
val base_name: string -> bstring
val full_bname: theory -> bstring -> string
val full_bname_path: theory -> string -> bstring -> string
@@ -91,10 +91,10 @@
val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
- val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
+ val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
val add_consts: (bstring * string * mixfix) list -> theory -> theory
val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
- val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory
+ val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
val revert_abbrev: string -> string -> theory -> theory
val add_const_constraint: string * typ option -> theory -> theory
val primitive_class: string * class list -> theory -> theory
--- a/src/Pure/theory.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Pure/theory.ML Wed Jan 21 16:51:45 2009 +0100
@@ -29,14 +29,14 @@
val at_end: (theory -> theory option) -> theory -> theory
val begin_theory: string -> theory list -> theory
val end_theory: theory -> theory
+ val add_axioms_i: (binding * term) list -> theory -> theory
val add_axioms: (bstring * string) list -> theory -> theory
- val add_axioms_i: (bstring * term) list -> theory -> theory
val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
+ val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
- val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
+ val add_finals_i: bool -> term list -> theory -> theory
val add_finals: bool -> string list -> theory -> theory
- val add_finals_i: bool -> term list -> theory -> theory
- val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
+ val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
end
structure Theory: THEORY =
@@ -157,19 +157,19 @@
fun err_in_axm msg name =
cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
-fun cert_axm thy (name, raw_tm) =
+fun cert_axm thy (b, raw_tm) =
let
val (t, T, _) = Sign.certify_prop thy raw_tm
handle TYPE (msg, _, _) => error msg
| TERM (msg, _) => error msg;
in
Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
- (name, Sign.no_vars (Syntax.pp_global thy) t)
+ (b, Sign.no_vars (Syntax.pp_global thy) t)
end;
-fun read_axm thy (name, str) =
- cert_axm thy (name, Syntax.read_prop_global thy str)
- handle ERROR msg => err_in_axm msg name;
+fun read_axm thy (bname, str) =
+ cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str)
+ handle ERROR msg => err_in_axm msg bname;
(* add_axioms(_i) *)
@@ -178,15 +178,15 @@
fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
let
- val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
+ val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
handle Symtab.DUP dup => err_dup_axm dup;
in axioms' end);
in
+val add_axioms_i = gen_add_axioms cert_axm;
val add_axioms = gen_add_axioms read_axm;
-val add_axioms_i = gen_add_axioms cert_axm;
end;
@@ -250,16 +250,16 @@
(* check_def *)
-fun check_def thy unchecked overloaded (bname, tm) defs =
+fun check_def thy unchecked overloaded (b, tm) defs =
let
val ctxt = ProofContext.init thy;
- val name = Sign.full_bname thy bname;
+ val name = Sign.full_name thy b;
val (lhs_const, rhs) = Sign.cert_def ctxt tm;
val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
val _ = check_overloading thy overloaded lhs_const;
in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
- [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
+ [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
@@ -298,8 +298,8 @@
in
+val add_finals_i = gen_add_finals (K I);
val add_finals = gen_add_finals Syntax.read_term_global;
-val add_finals_i = gen_add_finals (K I);
end;
--- a/src/Tools/induct.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/Tools/induct.ML Wed Jan 21 16:51:45 2009 +0100
@@ -50,7 +50,7 @@
val setN: string
(*proof methods*)
val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
- val add_defs: (Binding.T option * term) option list -> Proof.context ->
+ val add_defs: (binding option * term) option list -> Proof.context ->
(term option list * thm list) * Proof.context
val atomize_term: theory -> term -> term
val atomize_tac: int -> tactic
@@ -62,7 +62,7 @@
val cases_tac: Proof.context -> term option list list -> thm option ->
thm list -> int -> cases_tactic
val get_inductT: Proof.context -> term option list list -> thm list list
- val induct_tac: Proof.context -> (Binding.T option * term) option list list ->
+ val induct_tac: Proof.context -> (binding option * term) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
--- a/src/ZF/Inductive_ZF.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/ZF/Inductive_ZF.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,4 @@
(* Title: ZF/Inductive_ZF.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/ZF/Main_ZF.thy Tue Jan 20 19:09:19 2009 +0100
+++ b/src/ZF/Main_ZF.thy Wed Jan 21 16:51:45 2009 +0100
@@ -1,5 +1,3 @@
-(*$Id$*)
-
header{*Theory Main: Everything Except AC*}
theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
--- a/src/ZF/Tools/datatype_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -247,7 +247,7 @@
if need_recursor then
thy |> Sign.add_consts_i
[(recursor_base_name, recursor_typ, NoSyn)]
- |> (snd o PureThy.add_defs false [Thm.no_attributes recursor_def])
+ |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
else thy;
val (con_defs, thy0) = thy_path
@@ -255,7 +255,7 @@
((case_base_name, case_typ, NoSyn) ::
map #1 (List.concat con_ty_lists))
|> PureThy.add_defs false
- (map Thm.no_attributes
+ (map (Thm.no_attributes o apfst Binding.name)
(case_def ::
List.concat (ListPair.map mk_con_defs
(1 upto npart, con_ty_lists))))
@@ -383,13 +383,13 @@
(*Updating theory components: simprules and datatype info*)
(thy1 |> Sign.add_path big_rec_base_name
|> PureThy.add_thmss
- [(("simps", simps), [Simplifier.simp_add]),
- (("", intrs), [Classical.safe_intro NONE]),
- (("con_defs", con_defs), []),
- (("case_eqns", case_eqns), []),
- (("recursor_eqns", recursor_eqns), []),
- (("free_iffs", free_iffs), []),
- (("free_elims", free_SEs), [])] |> snd
+ [((Binding.name "simps", simps), [Simplifier.simp_add]),
+ ((Binding.empty , intrs), [Classical.safe_intro NONE]),
+ ((Binding.name "con_defs", con_defs), []),
+ ((Binding.name "case_eqns", case_eqns), []),
+ ((Binding.name "recursor_eqns", recursor_eqns), []),
+ ((Binding.name "free_iffs", free_iffs), []),
+ ((Binding.name "free_elims", free_SEs), [])] |> snd
|> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
|> ConstructorsData.map (fold Symtab.update con_pairs)
|> Sign.parent_path,
--- a/src/ZF/Tools/induct_tacs.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Wed Jan 21 16:51:45 2009 +0100
@@ -158,7 +158,7 @@
in
thy
|> Sign.add_path (Sign.base_name big_rec_name)
- |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
+ |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
|> Sign.parent_path
--- a/src/ZF/Tools/inductive_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -27,10 +27,10 @@
(*Insert definitions for the recursive sets, which
must *already* be declared as constants in parent theory!*)
val add_inductive_i: bool -> term list * term ->
- ((Binding.T * term) * attribute list) list ->
+ ((binding * term) * attribute list) list ->
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
- ((Binding.T * string) * Attrib.src list) list ->
+ ((binding * string) * Attrib.src list) list ->
(Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
(Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
theory -> theory * inductive_result
@@ -173,7 +173,7 @@
val (_, thy1) =
thy
|> Sign.add_path big_rec_base_name
- |> PureThy.add_defs false (map Thm.no_attributes axpairs);
+ |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
val ctxt1 = ProofContext.init thy1;
@@ -510,9 +510,9 @@
val ([induct', mutual_induct'], thy') =
thy
- |> PureThy.add_thms [((co_prefix ^ "induct", induct),
+ |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
[case_names, Induct.induct_pred big_rec_name]),
- (("mutual_induct", mutual_induct), [case_names])];
+ ((Binding.name "mutual_induct", mutual_induct), [case_names])];
in ((thy', induct'), mutual_induct')
end; (*of induction_rules*)
@@ -522,7 +522,7 @@
if not coind then induction_rules raw_induct thy1
else
(thy1
- |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])]
+ |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
|> apfst hd |> Library.swap, TrueI)
and defs = big_rec_def :: part_rec_defs
@@ -531,15 +531,15 @@
thy2
|> IndCases.declare big_rec_name make_cases
|> PureThy.add_thms
- [(("bnd_mono", bnd_mono), []),
- (("dom_subset", dom_subset), []),
- (("cases", elim), [case_names, Induct.cases_pred big_rec_name])]
+ [((Binding.name "bnd_mono", bnd_mono), []),
+ ((Binding.name "dom_subset", dom_subset), []),
+ ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
||>> (PureThy.add_thmss o map Thm.no_attributes)
- [("defs", defs),
- ("intros", intrs)];
+ [(Binding.name "defs", defs),
+ (Binding.name "intros", intrs)];
val (intrs'', thy4) =
thy3
- |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
+ |> PureThy.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
||> Sign.parent_path;
in
(thy4,
--- a/src/ZF/Tools/primrec_package.ML Tue Jan 20 19:09:19 2009 +0100
+++ b/src/ZF/Tools/primrec_package.ML Wed Jan 21 16:51:45 2009 +0100
@@ -8,8 +8,8 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec: ((Binding.T * string) * Attrib.src list) list -> theory -> theory * thm list
- val add_primrec_i: ((Binding.T * term) * attribute list) list -> theory -> theory * thm list
+ val add_primrec: ((binding * string) * Attrib.src list) list -> theory -> theory * thm list
+ val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -169,7 +169,7 @@
val ([def_thm], thy1) = thy
|> Sign.add_path (Sign.base_name fname)
- |> (PureThy.add_defs false o map Thm.no_attributes) [def];
+ |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
val eqn_thms =
@@ -179,10 +179,10 @@
val (eqn_thms', thy2) =
thy1
- |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts);
+ |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
val (_, thy3) =
thy2
- |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
+ |> PureThy.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
||> Sign.parent_path;
in (thy3, eqn_thms') end;