--- a/src/HOL/Nominal/nominal_atoms.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Mar 07 22:17:25 2009 +0100
@@ -100,7 +100,7 @@
val (_,thy1) =
fold_map (fn ak => fn thy =>
- let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)])
+ let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
val inject_flat = Library.flat inject
val ak_type = Type (Sign.intern_type thy1 ak,[])
@@ -187,7 +187,7 @@
cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
in
- thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)]
+ thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)]
|> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
|> snd
|> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
@@ -217,7 +217,7 @@
(Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
in
- thy |> Sign.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)]
+ thy |> Sign.add_consts_i [(Binding.name prm_name, mk_permT T --> T --> T, NoSyn)]
|> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
end) ak_names_types thy3;
@@ -300,7 +300,7 @@
(HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
in
- AxClass.define_class (cl_name, ["HOL.type"]) []
+ AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
[((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
((Binding.name (cl_name ^ "2"), []), [axiom2]),
((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
@@ -349,7 +349,8 @@
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
in
- AxClass.define_class (cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
+ AxClass.define_class (Binding.name cl_name, [pt_name]) []
+ [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
end) ak_names_types thy8;
(* proves that every fs_<ak>-type together with <ak>-type *)
@@ -398,7 +399,7 @@
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
in
- AxClass.define_class (cl_name, ["HOL.type"]) []
+ AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
[((Binding.name (cl_name ^ "1"), []), [ax1])] thy'
end) ak_names_types thy) ak_names_types thy12;
--- a/src/HOL/Nominal/nominal_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -197,7 +197,7 @@
val tmp_thy = thy |>
Theory.copy |>
Sign.add_types (map (fn (tvs, tname, mx, _) =>
- (tname, length tvs, mx)) dts);
+ (Binding.name tname, length tvs, mx)) dts);
val atoms = atoms_of thy;
@@ -235,8 +235,8 @@
Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
| replace_types T = T;
- val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
- map (fn (cname, cargs, mx) => (cname ^ "_Rep",
+ val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
+ map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
map replace_types cargs, NoSyn)) constrs)) dts';
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
@@ -615,7 +615,8 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
- TypedefPackage.add_typedef false (SOME name') (name, map fst tvs, mx)
+ TypedefPackage.add_typedef false (SOME (Binding.name name'))
+ (Binding.name name, map fst tvs, mx)
(Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
@@ -800,7 +801,7 @@
(Const (rep_name, T --> T') $ lhs, rhs));
val def_name = (NameSpace.base_name cname) ^ "_def";
val ([def_thm], thy') = thy |>
- Sign.add_consts_i [(cname', constrT, mx)] |>
+ Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
(PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
in (thy', defs @ [def_thm], eqns @ [eqn]) end;
@@ -2012,7 +2013,7 @@
val (reccomb_defs, thy12) =
thy11
|> Sign.add_consts_i (map (fn ((name, T), T') =>
- (NameSpace.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
+ (Binding.name (NameSpace.base_name name), rec_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') =>
(Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
--- a/src/HOL/Tools/datatype_abs_proofs.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Sat Mar 07 22:17:25 2009 +0100
@@ -235,7 +235,7 @@
val (reccomb_defs, thy2) =
thy1
|> Sign.add_consts_i (map (fn ((name, T), T') =>
- (NameSpace.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
+ (Binding.name (NameSpace.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') =>
(Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
--- a/src/HOL/Tools/datatype_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -36,8 +36,8 @@
simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
-> theory -> Proof.state;
val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
- val add_datatype : bool -> bool -> string list -> (string list * bstring * mixfix *
- (bstring * typ list * mixfix) list) list -> theory ->
+ val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
+ (binding * typ list * mixfix) list) list -> theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -46,8 +46,8 @@
split_thms : (thm * thm) list,
induction : thm,
simps : thm list} * theory
- val add_datatype_cmd : bool -> string list -> (string list * bstring * mixfix *
- (bstring * string list * mixfix) list) list -> theory ->
+ val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
+ (binding * string list * mixfix) list) list -> theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -566,11 +566,11 @@
val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
- let val full_tname = Sign.full_bname tmp_thy (Syntax.type_name tname mx)
+ let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
in (case duplicates (op =) tvs of
[] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
else error ("Mutually recursive datatypes must have same type parameters")
- | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
+ | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
" : " ^ commas dups))
end) dts);
@@ -585,13 +585,14 @@
val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
- in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
- Sign.full_bname_path tmp_thy tname) (Syntax.const_name cname mx'),
+ in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
+ Sign.full_name_path tmp_thy (Binding.name_of tname))
+ (Binding.map_name (Syntax.const_name mx') cname),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
- end handle ERROR msg =>
- cat_error msg ("The error above occured in constructor " ^ cname ^
- " of datatype " ^ tname);
+ end handle ERROR msg => cat_error msg
+ ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
+ " of datatype " ^ quote (Binding.str_of tname));
val (constrs', constr_syntax', sorts') =
fold prep_constr constrs ([], [], sorts)
@@ -599,11 +600,11 @@
in
case duplicates (op =) (map fst constrs') of
[] =>
- (dts' @ [(i, (Sign.full_bname tmp_thy (Syntax.type_name tname mx),
+ (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
map DtTFree tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
| dups => error ("Duplicate constructors " ^ commas dups ^
- " in datatype " ^ tname)
+ " in datatype " ^ quote (Binding.str_of tname))
end;
val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
@@ -676,12 +677,13 @@
local structure P = OuterParse and K = OuterKeyword in
val datatype_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
- (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
+ (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix));
fun mk_datatype args =
let
- val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
+ val names = map
+ (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
val specs = map (fn ((((_, vs), t), mx), cons) =>
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
in snd o add_datatype_cmd false names specs end;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Sat Mar 07 22:17:25 2009 +0100
@@ -15,7 +15,7 @@
val distinctness_limit_setup : theory -> theory
val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
string list -> DatatypeAux.descr list -> (string * sort) list ->
- (string * mixfix) list -> (string * mixfix) list list -> attribute
+ (binding * mixfix) list -> (binding * mixfix) list list -> attribute
-> theory -> (thm list list * thm list list * thm list list *
DatatypeAux.simproc_dist list * thm) * theory
end;
@@ -192,7 +192,7 @@
val (typedefs, thy3) = thy2 |>
parent_path flat_names |>
fold_map (fn ((((name, mx), tvs), c), name') =>
- TypedefPackage.add_typedef false (SOME name') (name, tvs, mx)
+ TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
@@ -212,7 +212,7 @@
(* isomorphism declarations *)
- val iso_decls = map (fn (T, s) => (s, T --> Univ_elT, NoSyn))
+ val iso_decls = map (fn (T, s) => (Binding.name s, T --> Univ_elT, NoSyn))
(oldTs ~~ rep_names');
(* constructor definitions *)
--- a/src/HOL/Tools/function_package/size.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Sat Mar 07 22:17:25 2009 +0100
@@ -140,7 +140,7 @@
val ((size_def_thms, size_def_thms'), thy') =
thy
|> Sign.add_consts_i (map (fn (s, T) =>
- (NameSpace.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
+ (Binding.name (NameSpace.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
(size_names ~~ recTs1))
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
--- a/src/HOL/Tools/inductive_realizer.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Mar 07 22:17:25 2009 +0100
@@ -68,8 +68,8 @@
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
(Logic.strip_imp_concl (prop_of (hd intrs))));
val params = map dest_Var (Library.take (nparms, ts));
- val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs);
- fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr),
+ val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs));
+ fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)),
map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
filter_out (equal Extraction.nullT) (map
(Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
@@ -234,7 +234,7 @@
end;
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
- if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
+ if Binding.eq_name (name, s) then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
else x;
fun add_dummies f [] _ thy =
@@ -242,14 +242,14 @@
| add_dummies f dts used thy =
thy
|> f (map snd dts)
- |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
+ |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
handle DatatypeAux.Datatype_Empty name' =>
let
val name = NameSpace.base_name name';
- val dname = Name.variant used "Dummy"
+ val dname = Name.variant used "Dummy";
in
thy
- |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
+ |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
end;
fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
@@ -296,7 +296,7 @@
val thy1' = thy1 |>
Theory.copy |>
- Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |>
+ Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |>
fold (fn s => AxClass.axiomatize_arity
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
@@ -308,7 +308,7 @@
val ((dummies, dt_info), thy2) =
thy1
|> add_dummies
- (DatatypePackage.add_datatype false false (map #2 dts))
+ (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
(map (pair false) dts) []
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;
@@ -330,14 +330,17 @@
(if c = Extraction.nullt then c else list_comb (c, map Var (rev
(Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
(maps snd rss ~~ List.concat constrss);
- val (rlzpreds, rlzpreds') = split_list
- (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
+ val (rlzpreds, rlzpreds') =
+ rintrs |> map (fn rintr =>
let
- val Const (s, T) = head_of (HOLogic.dest_Trueprop
- (Logic.strip_assums_concl rintr));
+ val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
val s' = NameSpace.base_name s;
- val T' = Logic.unvarifyT T
- in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
+ val T' = Logic.unvarifyT T;
+ in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
+ |> distinct (op = o pairself (#1 o #1))
+ |> map (apfst (apfst (apfst Binding.name)))
+ |> split_list;
+
val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
(List.take (snd (strip_comb
(HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
--- a/src/HOL/Tools/inductive_set_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -464,7 +464,7 @@
| NONE => u)) |>
Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
eta_contract (member op = cs' orf is_pred pred_arities))) intros;
- val cnames_syn' = map (fn (b, _) => (Binding.map_name (suffix "p") b, NoSyn)) cnames_syn;
+ val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
InductivePackage.add_ind_def
--- a/src/HOL/Tools/record_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/record_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -1461,9 +1461,10 @@
Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
+ val tname = Binding.name (NameSpace.base_name name);
in
thy
- |> TypecopyPackage.add_typecopy (suffix ext_typeN (NameSpace.base_name name), alphas) repT NONE
+ |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
|-> (fn (name, _) => `(fn thy => get_thms thy name))
end;
@@ -1531,9 +1532,9 @@
(* 1st stage: defs_thy *)
fun mk_defs () =
thy
- |> extension_typedef name repT (alphas@[zeta])
+ |> extension_typedef name repT (alphas @ [zeta])
||> Sign.add_consts_i
- (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
+ (map (Syntax.no_syn o apfst Binding.name) (apfst base ext_decl :: dest_decls @ upd_decls))
||>> PureThy.add_defs false
(map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
||>> PureThy.add_defs false
@@ -1895,8 +1896,8 @@
(*record (scheme) type abbreviation*)
val recordT_specs =
- [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
- (bname, alphas, recT0, Syntax.NoSyn)];
+ [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
+ (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
(*selectors*)
fun mk_sel_spec (c,T) =
@@ -1937,8 +1938,9 @@
|> Sign.add_tyabbrs_i recordT_specs
|> Sign.add_path bname
|> Sign.add_consts_i
- (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
- |> (Sign.add_consts_i o map Syntax.no_syn)
+ (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx))
+ sel_decls (field_syntax @ [Syntax.NoSyn]))
+ |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
|> ((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)
--- a/src/HOL/Tools/typecopy_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/typecopy_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -14,7 +14,7 @@
proj: string * typ,
proj_def: thm
}
- val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
+ val add_typecopy: binding * string list -> typ -> (binding * binding) option
-> theory -> (string * info) * theory
val get_typecopies: theory -> string list
val get_info: theory -> string -> info option
--- a/src/HOL/Tools/typedef_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/typedef_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -13,12 +13,12 @@
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm}
val get_info: theory -> string -> info option
- val add_typedef: bool -> string option -> bstring * string list * mixfix ->
- term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
- val typedef: (bool * string) * (bstring * string list * mixfix) * term
- * (string * string) option -> theory -> Proof.state
- val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string
- * (string * string) option -> theory -> Proof.state
+ val add_typedef: bool -> binding option -> binding * string list * mixfix ->
+ term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
+ val typedef: (bool * binding) * (binding * string list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
val interpretation: (string -> theory -> theory) -> theory -> theory
val setup: theory -> theory
end;
@@ -51,9 +51,6 @@
(* prepare_typedef *)
-fun err_in_typedef msg name =
- cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
-
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
@@ -63,10 +60,12 @@
let
val _ = Theory.requires thy "Typedef" "typedefs";
val ctxt = ProofContext.init thy;
- val full = Sign.full_bname thy;
+
+ val full = Sign.full_name thy;
+ val full_name = full name;
+ val bname = Binding.name_of name;
(*rhs*)
- val full_name = full name;
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
val setT = Term.fastype_of set;
val rhs_tfrees = Term.add_tfrees set [];
@@ -81,11 +80,14 @@
|> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
|> map TFree;
- val tname = Syntax.type_name t mx;
+ val tname = Binding.map_name (Syntax.type_name mx) t;
val full_tname = full tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
- val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
+ val (Rep_name, Abs_name) =
+ (case opt_morphs of
+ NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+ | SOME morphs => morphs);
val setT' = map Term.itselfT args_setT ---> setT;
val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
val RepC = Const (full Rep_name, newT --> oldT);
@@ -97,15 +99,15 @@
val set' = if def then setC else set;
val goal' = mk_inhabited set';
val goal = mk_inhabited set;
- val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
+ val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
(*axiomatization*)
- val typedef_name = "type_definition_" ^ name;
+ val typedef_name = Binding.prefix_name "type_definition_" name;
val typedefC =
Const (@{const_name type_definition},
(newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
- val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
+ val typedef_deps = Term.add_consts set' [];
(*set definition*)
fun add_def theory =
@@ -131,7 +133,7 @@
(Abs_name, oldT --> newT, NoSyn)]
#> add_def
#-> (fn set_def =>
- PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
+ PureThy.add_axioms [((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
@@ -142,21 +144,21 @@
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
thy1
- |> Sign.add_path name
+ |> Sign.add_path (Binding.name_of name)
|> PureThy.add_thms
- ((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}), []),
- ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []),
- ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}),
- [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
- ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}),
- [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
- ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}),
- [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
- ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}),
- [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
+ [((Rep_name, make @{thm type_definition.Rep}), []),
+ ((Binding.suffix_name "_inverse" Rep_name, make @{thm type_definition.Rep_inverse}), []),
+ ((Binding.suffix_name "_inverse" Abs_name, make @{thm type_definition.Abs_inverse}), []),
+ ((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
+ ((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
+ ((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
+ [RuleCases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
+ ((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
+ [RuleCases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
+ ((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
+ [RuleCases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
+ ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
+ [RuleCases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
||> Sign.parent_path;
val info = {rep_type = oldT, abs_type = newT,
Rep_name = full Rep_name, Abs_name = full Abs_name,
@@ -201,7 +203,8 @@
|> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
in (set, goal, goal_pat, typedef_result) end
- handle ERROR msg => err_in_typedef msg name;
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
(* add_typedef: tactic interface *)
@@ -245,13 +248,14 @@
val typedef_decl =
Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+ ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
--| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
+ (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
- typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
+ typedef_cmd ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name),
+ (t, vs, mx), A, morphs);
val _ =
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
--- a/src/HOLCF/Tools/cont_consts.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Sat Mar 07 22:17:25 2009 +0100
@@ -52,11 +52,11 @@
is generated and connected to the other declaration via some translation.
*)
fun fix_mixfix (syn , T, mx as Infix p ) =
- (Syntax.const_name syn mx, T, InfixName (syn, p))
+ (Syntax.const_name mx syn, T, InfixName (syn, p))
| fix_mixfix (syn , T, mx as Infixl p ) =
- (Syntax.const_name syn mx, T, InfixlName (syn, p))
+ (Syntax.const_name mx syn, T, InfixlName (syn, p))
| fix_mixfix (syn , T, mx as Infixr p ) =
- (Syntax.const_name syn mx, T, InfixrName (syn, p))
+ (Syntax.const_name mx syn, T, InfixrName (syn, p))
| fix_mixfix decl = decl;
fun transform decl = let
val (c, T, mx) = fix_mixfix decl;
@@ -73,7 +73,7 @@
| is_contconst (_,_,Binder _) = false
| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
- quote (Syntax.const_name c mx));
+ quote (Syntax.const_name mx c));
(* add_consts(_i) *)
@@ -85,10 +85,9 @@
val transformed_decls = map transform contconst_decls;
in
thy
- |> Sign.add_consts_i normal_decls
- |> Sign.add_consts_i (map first transformed_decls)
- |> Sign.add_syntax_i (map second transformed_decls)
- |> Sign.add_trrules_i (List.concat (map third transformed_decls))
+ |> (Sign.add_consts_i o map (upd_first Binding.name))
+ (normal_decls @ map first transformed_decls @ map second transformed_decls)
+ |> Sign.add_trrules_i (maps third transformed_decls)
end;
val add_consts = gen_add_consts Syntax.read_typ_global;
--- a/src/HOLCF/Tools/domain/domain_extender.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Sat Mar 07 22:17:25 2009 +0100
@@ -103,7 +103,7 @@
(Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
o fst) eqs''';
val cons''' = map snd eqs''';
- fun thy_type (dname,tvars) = (NameSpace.base_name dname, length tvars, NoSyn);
+ fun thy_type (dname,tvars) = (Binding.name (NameSpace.base_name dname), length tvars, NoSyn);
fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
@@ -119,7 +119,7 @@
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
fun one_con (con,mx,args) =
- ((Syntax.const_name con mx),
+ ((Syntax.const_name mx con),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
find_index_eq tp dts,
DatatypeAux.dtyp_of_typ new_dts tp),
--- a/src/HOLCF/Tools/pcpodef_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -7,14 +7,14 @@
signature PCPODEF_PACKAGE =
sig
- val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
- * (string * string) option -> theory -> Proof.state
- val pcpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
- * (string * string) option -> theory -> Proof.state
- val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
- * (string * string) option -> theory -> Proof.state
- val cpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
- * (string * string) option -> theory -> Proof.state
+ val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
+ val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
end;
structure PcpodefPackage: PCPODEF_PACKAGE =
@@ -24,9 +24,6 @@
(* prepare_cpodef *)
-fun err_in_cpodef msg name =
- cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
-
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
@@ -36,10 +33,12 @@
let
val _ = Theory.requires thy "Pcpodef" "pcpodefs";
val ctxt = ProofContext.init thy;
- val full = Sign.full_bname thy;
+
+ val full = Sign.full_name thy;
+ val full_name = full name;
+ val bname = Binding.name_of name;
(*rhs*)
- val full_name = full name;
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
val setT = Term.fastype_of set;
val rhs_tfrees = Term.add_tfrees set [];
@@ -58,11 +57,14 @@
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
val lhs_sorts = map snd lhs_tfrees;
- val tname = Syntax.type_name t mx;
+ val tname = Binding.map_name (Syntax.type_name mx) t;
val full_tname = full tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
- val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
+ val (Rep_name, Abs_name) =
+ (case opt_morphs of
+ NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+ | SOME morphs => morphs);
val RepC = Const (full Rep_name, newT --> oldT);
fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
val less_def = Logic.mk_equals (lessC newT,
@@ -76,7 +78,8 @@
|> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
val less_def' = Syntax.check_term lthy3 less_def;
val ((_, (_, less_definition')), lthy4) = lthy3
- |> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def'));
+ |> Specification.definition (NONE,
+ ((Binding.prefix_name "less_" (Binding.suffix_name "_def" name), []), less_def'));
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
val thy5 = lthy4
@@ -95,14 +98,14 @@
val cpo_thms' = map (Thm.transfer theory') cpo_thms;
in
theory'
- |> Sign.add_path name
+ |> Sign.add_path (Binding.name_of name)
|> PureThy.add_thms
- ([((Binding.name ("adm_" ^ name), admissible'), []),
- ((Binding.name ("cont_" ^ Rep_name), @{thm typedef_cont_Rep} OF cpo_thms'), []),
- ((Binding.name ("cont_" ^ Abs_name), @{thm typedef_cont_Abs} OF cpo_thms'), []),
- ((Binding.name ("lub_" ^ name), @{thm typedef_lub} OF cpo_thms'), []),
- ((Binding.name ("thelub_" ^ name), @{thm typedef_thelub} OF cpo_thms'), []),
- ((Binding.name ("compact_" ^ name), @{thm typedef_compact} OF cpo_thms'), [])])
+ ([((Binding.prefix_name "adm_" name, admissible'), []),
+ ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
+ ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
+ ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
+ ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
+ ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
|> snd
|> Sign.parent_path
end;
@@ -117,15 +120,14 @@
val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
in
theory'
- |> Sign.add_path name
+ |> Sign.add_path (Binding.name_of name)
|> PureThy.add_thms
- ([((Binding.name (Rep_name ^ "_strict"), @{thm typedef_Rep_strict} OF pcpo_thms'), []),
- ((Binding.name (Abs_name ^ "_strict"), @{thm typedef_Abs_strict} OF pcpo_thms'), []),
- ((Binding.name (Rep_name ^ "_strict_iff"), @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
- ((Binding.name (Abs_name ^ "_strict_iff"), @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
- ((Binding.name (Rep_name ^ "_defined"), @{thm typedef_Rep_defined} OF pcpo_thms'), []),
- ((Binding.name (Abs_name ^ "_defined"), @{thm typedef_Abs_defined} OF pcpo_thms'), [])
- ])
+ ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
|> snd
|> Sign.parent_path
end;
@@ -142,7 +144,8 @@
then (goal_UU_mem, goal_admissible, pcpodef_result)
else (goal_nonempty, goal_admissible, cpodef_result)
end
- handle ERROR msg => err_in_cpodef msg name;
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
(* proof interface *)
@@ -174,14 +177,14 @@
val typedef_proof_decl =
Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+ ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
--| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
+ (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
- ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
+ ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
val _ =
OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
--- a/src/ZF/Tools/datatype_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -245,14 +245,14 @@
fun add_recursor thy =
if need_recursor then
thy |> Sign.add_consts_i
- [(recursor_base_name, recursor_typ, NoSyn)]
+ [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
|> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
else thy;
val (con_defs, thy0) = thy_path
|> Sign.add_consts_i
- ((case_base_name, case_typ, NoSyn) ::
- map #1 (List.concat con_ty_lists))
+ (map (fn (c, T, mx) => (Binding.name c, T, mx))
+ ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)))
|> PureThy.add_defs false
(map (Thm.no_attributes o apfst Binding.name)
(case_def ::
@@ -302,7 +302,7 @@
(*** Prove the recursor theorems ***)
- val recursor_eqns = case try (Thm.get_def thy1) recursor_base_name of
+ val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of
NONE => (writeln " [ No recursion operator ]";
[])
| SOME recursor_def =>
--- a/src/ZF/Tools/inductive_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -180,7 +180,7 @@
(*fetch fp definitions from the theory*)
val big_rec_def::part_rec_defs =
- map (Thm.get_def thy1)
+ map (Drule.get_def thy1)
(case rec_names of [_] => rec_names
| _ => big_rec_base_name::rec_names);
--- a/src/ZF/ind_syntax.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/ZF/ind_syntax.ML Sat Mar 07 22:17:25 2009 +0100
@@ -73,7 +73,7 @@
val T = (map (#2 o dest_Free) args) ---> iT
handle TERM _ => error
"Bad variable in constructor specification"
- val name = Syntax.const_name id syn (*handle infix constructors*)
+ val name = Syntax.const_name syn id
in ((id,T,syn), name, args, prems) end;
val read_constructs = map o map o read_construct;