--- a/src/HOL/Library/Eval.thy Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Library/Eval.thy Tue Sep 02 14:10:45 2008 +0200
@@ -68,7 +68,7 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
+ |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit
--- a/src/HOL/Library/RType.thy Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Library/RType.thy Tue Sep 02 14:10:45 2008 +0200
@@ -67,7 +67,7 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort rtype})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
+ |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Sep 02 14:10:45 2008 +0200
@@ -265,9 +265,9 @@
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
in
AxClass.define_class (cl_name, ["HOL.type"]) []
- [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
- ((cl_name ^ "2", []), [axiom2]),
- ((cl_name ^ "3", []), [axiom3])] thy
+ [((Name.binding (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
+ ((Name.binding (cl_name ^ "2"), []), [axiom2]),
+ ((Name.binding (cl_name ^ "3"), []), [axiom3])] thy
end) ak_names_types thy6;
(* proves that every pt_<ak>-type together with <ak>-type *)
@@ -313,7 +313,7 @@
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
in
- AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy
+ AxClass.define_class (cl_name, [pt_name]) [] [((Name.binding (cl_name ^ "1"), []), [axiom1])] thy
end) ak_names_types thy8;
(* proves that every fs_<ak>-type together with <ak>-type *)
@@ -362,7 +362,8 @@
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
in
- AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'
+ AxClass.define_class (cl_name, ["HOL.type"]) []
+ [((Name.binding (cl_name ^ "1"), []), [ax1])] thy'
end) ak_names_types thy) ak_names_types thy12;
(* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem; *)
--- a/src/HOL/Nominal/nominal_induct.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Tue Sep 02 14:10:45 2008 +0200
@@ -6,7 +6,7 @@
structure NominalInduct:
sig
- val nominal_induct_tac: Proof.context -> (string option * term) option list list ->
+ val nominal_induct_tac: Proof.context -> (Name.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
@@ -31,7 +31,6 @@
fun inst_mutual_rule ctxt insts avoiding rules =
let
-
val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
val (cases, consumes) = RuleCases.get joined_rule;
@@ -132,7 +131,7 @@
val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
val def_inst =
- ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
+ ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
-- Args.term) >> SOME ||
inst >> Option.map (pair NONE);
--- a/src/HOL/Nominal/nominal_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -286,7 +286,7 @@
else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
end;
in
- (("", []), HOLogic.mk_Trueprop (HOLogic.mk_eq
+ ((Name.no_binding, []), HOLogic.mk_Trueprop (HOLogic.mk_eq
(Free (nth perm_names_types' i) $
Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
list_comb (c, args),
@@ -298,7 +298,7 @@
PrimrecPackage.add_primrec_overloaded
(map (fn (s, sT) => (s, sT, false))
(List.take (perm_names' ~~ perm_names_types, length new_type_names)))
- (map (fn s => (s, NONE, NoSyn)) perm_names') perm_eqs thy1;
+ (map (fn s => (Name.binding s, NONE, NoSyn)) perm_names') perm_eqs thy1;
(**** prove that permutation functions introduced by unfolding are ****)
(**** equivalent to already existing permutation functions ****)
@@ -559,11 +559,11 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = false, verbose = false, kind = Thm.internalK,
- alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false,
+ alt_name = Name.binding big_rep_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true}
- (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
+ (map (fn (s, T) => ((Name.binding s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
- [] (map (fn x => (("", []), x)) intr_ts) [] thy3;
+ [] (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy3;
(**** Prove that representing set is closed under permutation ****)
@@ -1476,11 +1476,11 @@
thy10 |>
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
- alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false,
+ alt_name = Name.binding big_rec_name, coind = false, no_elim = false, no_ind = false,
skip_mono = true}
- (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
+ (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (("", []), x)) rec_intr_ts) [] ||>
+ (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] ||>
PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
(** equivariance **)
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Sep 02 14:10:45 2008 +0200
@@ -9,13 +9,13 @@
signature NOMINAL_PRIMREC =
sig
val add_primrec: string -> string list option -> string option ->
- ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
+ ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
val add_primrec_unchecked: string -> string list option -> string option ->
- ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
+ ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
val add_primrec_i: string -> term list option -> term option ->
- ((bstring * term) * attribute list) list -> theory -> Proof.state
+ ((Name.binding * term) * attribute list) list -> theory -> Proof.state
val add_primrec_unchecked_i: string -> term list option -> term option ->
- ((bstring * term) * attribute list) list -> theory -> Proof.state
+ ((Name.binding * term) * attribute list) list -> theory -> Proof.state
end;
structure NominalPrimrec : NOMINAL_PRIMREC =
@@ -229,7 +229,8 @@
fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
let
- val (eqns, atts) = split_list eqns_atts;
+ val (raw_eqns, atts) = split_list eqns_atts;
+ val eqns = map (apfst Name.name_of) raw_eqns;
val dt_info = NominalPackage.get_nominal_datatypes thy;
val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
--- a/src/HOL/Statespace/state_space.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Statespace/state_space.ML Tue Sep 02 14:10:45 2008 +0200
@@ -61,7 +61,6 @@
val update_tr' : Proof.context -> term list -> term
end;
-
structure StateSpace: STATE_SPACE =
struct
@@ -303,7 +302,7 @@
val attr = Attrib.internal type_attr;
- val assumes = Element.Assumes [((dist_thm_name,[attr]),
+ val assumes = Element.Assumes [((Name.binding dist_thm_name,[attr]),
[(HOLogic.Trueprop $
(Const ("DistinctTreeProver.all_distinct",
Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $
@@ -445,7 +444,7 @@
NONE => []
| SOME s =>
let
- val fx = Element.Fixes [(s,SOME (string_of_typ stateT),NoSyn)];
+ val fx = Element.Fixes [(Name.binding s,SOME (string_of_typ stateT),NoSyn)];
val cs = Element.Constrains
(map (fn (n,T) => (n,string_of_typ T))
((map (fn (n,_) => (n,nameT)) all_comps) @
--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Sep 02 14:10:45 2008 +0200
@@ -156,11 +156,11 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
- alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true,
+ alt_name = Name.binding big_rec_name', coind = false, no_elim = false, no_ind = true,
skip_mono = true}
- (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
+ (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (("", []), x)) rec_intr_ts) [] thy0;
+ (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] thy0;
(* prove uniqueness and termination of primrec combinators *)
--- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 02 14:10:45 2008 +0200
@@ -442,7 +442,7 @@
(mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
val def' = Syntax.check_term lthy def;
val ((_, (_, thm)), lthy') = Specification.definition
- (NONE, (("", []), def')) lthy;
+ (NONE, ((Name.no_binding, []), def')) lthy;
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 02 14:10:45 2008 +0200
@@ -184,10 +184,10 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
- alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false,
+ alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true}
- (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
- (map (fn x => (("", []), x)) intr_ts) [] thy1;
+ (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
+ (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy1;
(********************************* typedef ********************************)
--- a/src/HOL/Tools/function_package/fundef_common.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Sep 02 14:10:45 2008 +0200
@@ -66,7 +66,7 @@
psimps, pinducts, termination, defname}) phi =
let
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
- val name = Morphism.name phi
+ val name = Name.name_of o Morphism.name phi o Name.binding
in
FundefCtxData { add_simps = add_simps, case_names = case_names,
fs = map term fs, R = term R, psimps = fact psimps,
--- a/src/HOL/Tools/function_package/fundef_core.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML Tue Sep 02 14:10:45 2008 +0200
@@ -10,8 +10,8 @@
sig
val prepare_fundef : FundefCommon.fundef_config
-> string (* defname *)
- -> ((string * typ) * mixfix) list (* defined symbol *)
- -> ((string * typ) list * term list * term * term) list (* specification *)
+ -> ((bstring * typ) * mixfix) list (* defined symbol *)
+ -> ((bstring * typ) list * term list * term * term) list (* specification *)
-> local_theory
-> (term (* f *)
@@ -31,22 +31,22 @@
open FundefCommon
datatype globals =
- Globals of {
- fvar: term,
- domT: typ,
+ Globals of {
+ fvar: term,
+ domT: typ,
ranT: typ,
- h: term,
- y: term,
- x: term,
- z: term,
- a: term,
- P: term,
- D: term,
+ h: term,
+ y: term,
+ x: term,
+ z: term,
+ a: term,
+ P: term,
+ D: term,
Pbool:term
}
-datatype rec_call_info =
+datatype rec_call_info =
RCInfo of
{
RIvs: (string * typ) list, (* Call context: fixes and assumes *)
@@ -55,7 +55,7 @@
llRI: thm,
h_assum: term
- }
+ }
datatype clause_context =
@@ -69,7 +69,7 @@
rhs: term,
cqs: cterm list,
- ags: thm list,
+ ags: thm list,
case_hyp : thm
}
@@ -80,7 +80,7 @@
datatype clause_info =
- ClauseInfo of
+ ClauseInfo of
{
no: int,
qglr : ((string * typ) list * term list * term * term),
@@ -166,16 +166,16 @@
val gs = map inst pre_gs
val lhs = inst pre_lhs
val rhs = inst pre_rhs
-
+
val cqs = map (cterm_of thy) qs
val ags = map (assume o cterm_of thy) gs
-
+
val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
in
- ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
+ ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
cqs = cqs, ags = ags, case_hyp = case_hyp }
end
-
+
(* lowlevel term function *)
fun abstract_over_list vs body =
@@ -188,7 +188,7 @@
Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
| t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
| _ => raise SAME);
- in
+ in
fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
end
@@ -233,7 +233,7 @@
cdata=cdata,
qglr=qglr,
- lGI=lGI,
+ lGI=lGI,
RCs=RC_infos,
tree=tree
}
@@ -260,11 +260,11 @@
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
(* if j < i, then turn around *)
-fun get_compat_thm thy cts i j ctxi ctxj =
+fun get_compat_thm thy cts i j ctxi ctxj =
let
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
-
+
val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
in if j < i then
let
@@ -324,14 +324,14 @@
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
- val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
+ val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
= mk_clause_context x ctxti cdescj
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
val compat = get_compat_thm thy compat_store i j cctxi cctxj
val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
- val RLj_import =
+ val RLj_import =
RLj |> fold forall_elim cqsj'
|> fold Thm.elim_implies agsj'
|> fold Thm.elim_implies Ghsj'
@@ -426,7 +426,7 @@
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
val _ = Output.debug (K "Proving cases for unique existence...")
- val (ex1s, values) =
+ val (ex1s, values) =
split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
val _ = Output.debug (K "Proving: Graph is a function")
@@ -466,10 +466,10 @@
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev Logic.all (fvar :: qs)
end
-
+
val G_intros = map2 mk_GIntro clauses RCss
-
- val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
+
+ val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
in
((G, GIntro_thms, G_elim, G_induct), lthy)
@@ -479,13 +479,13 @@
fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
let
- val f_def =
+ val f_def =
Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|> Syntax.check_term lthy
val ((f, (_, f_defthm)), lthy) =
- LocalTheory.define Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
+ LocalTheory.define Thm.internalK ((Name.binding (function_name fname), mixfix), ((Name.binding fdefname, []), f_def)) lthy
in
((f, f_defthm), lthy)
end
@@ -507,7 +507,7 @@
val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
- val (RIntro_thmss, (R, R_elim, _, lthy)) =
+ val (RIntro_thmss, (R, R_elim, _, lthy)) =
fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
in
((R, RIntro_thmss, R_elim), lthy)
@@ -516,7 +516,7 @@
fun fix_globals domT ranT fvar ctxt =
let
- val ([h, y, x, z, a, D, P, Pbool],ctxt') =
+ val ([h, y, x, z, a, D, P, Pbool],ctxt') =
Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
in
(Globals {h = Free (h, domT --> ranT),
@@ -546,13 +546,13 @@
(**********************************************************
- * PROVING THE RULES
+ * PROVING THE RULES
**********************************************************)
fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
let
val Globals {domT, z, ...} = globals
-
+
fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
let
val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
@@ -563,7 +563,7 @@
|> implies_intr z_smaller
|> forall_intr (cterm_of thy z)
|> (fn it => it COMP valthm)
- |> implies_intr lhs_acc
+ |> implies_intr lhs_acc
|> asm_simplify (HOL_basic_ss addsimps [f_iff])
|> fold_rev (implies_intr o cprop_of) ags
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
@@ -585,23 +585,23 @@
let
val Globals {domT, x, z, a, P, D, ...} = globals
val acc_R = mk_acc domT R
-
+
val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
-
+
val D_subset = cterm_of thy (Logic.all x
(Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
-
+
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
Logic.all x
(Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
HOLogic.mk_Trueprop (D $ z)))))
|> cterm_of thy
-
-
+
+
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
- val ihyp = Term.all domT $ Abs ("z", domT,
+ val ihyp = Term.all domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
HOLogic.mk_Trueprop (P $ Bound 0)))
|> cterm_of thy
@@ -610,36 +610,36 @@
fun prove_case clause =
let
- val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
+ val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
qglr = (oqs, _, _, _), ...} = clause
-
+
val case_hyp_conv = K (case_hyp RS eq_reflection)
- local open Conv in
+ local open Conv in
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
end
-
+
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
sih |> forall_elim (cterm_of thy rcarg)
|> Thm.elim_implies llRI
|> fold_rev (implies_intr o cprop_of) CCas
|> fold_rev (forall_intr o cterm_of thy o Free) RIvs
-
+
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
-
+
val step = HOLogic.mk_Trueprop (P $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs
|> fold_rev (curry Logic.mk_implies) gs
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|> cterm_of thy
-
+
val P_lhs = assume step
|> fold forall_elim cqs
- |> Thm.elim_implies lhs_D
+ |> Thm.elim_implies lhs_D
|> fold Thm.elim_implies ags
|> fold Thm.elim_implies P_recs
-
+
val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
|> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
|> symmetric (* P lhs == P x *)
@@ -650,17 +650,17 @@
in
(res, step)
end
-
+
val (cases, steps) = split_list (map prove_case clauses)
-
+
val istep = complete_thm
|> Thm.forall_elim_vars 0
|> fold (curry op COMP) cases (* P x *)
|> implies_intr ihyp
|> implies_intr (cprop_of x_D)
|> forall_intr (cterm_of thy x)
-
- val subset_induct_rule =
+
+ val subset_induct_rule =
acc_subset_induct
|> (curry op COMP) (assume D_subset)
|> (curry op COMP) (assume D_dcl)
@@ -694,13 +694,13 @@
(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
let
- val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
+ val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
qglr = (oqs, _, _, _), ...} = clause
val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
|> fold_rev (curry Logic.mk_implies) gs
|> cterm_of thy
in
- Goal.init goal
+ Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
|> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
|> (SINGLE (CLASIMPSET auto_tac)) |> the
@@ -721,26 +721,26 @@
val Globals {x, z, ...} = globals
val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
qglr=(oqs, _, _, _), ...} = clause
-
+
val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
-
- fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
+
+ fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
let
val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub)
-
+
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
- |> FundefCtxTree.export_term (fixes, assumes)
+ |> FundefCtxTree.export_term (fixes, assumes)
|> fold_rev (curry Logic.mk_implies o prop_of) ags
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|> cterm_of thy
-
+
val thm = assume hyp
|> fold forall_elim cqs
|> fold Thm.elim_implies ags
|> FundefCtxTree.import_thm thy (fixes, assumes)
|> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
-
+
val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
val acc = thm COMP ih_case
@@ -748,7 +748,7 @@
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
val ethm = z_acc_local
- |> FundefCtxTree.export_thm thy (fixes,
+ |> FundefCtxTree.export_thm thy (fixes,
z_eq_arg :: case_hyp :: ags @ assumes)
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
@@ -766,24 +766,24 @@
let
val Globals { domT, x, z, ... } = globals
val acc_R = mk_acc domT R
-
+
val R' = Free ("R", fastype_of R)
-
+
val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
-
+
val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
-
+
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
- val ihyp = Term.all domT $ Abs ("z", domT,
+ val ihyp = Term.all domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
HOLogic.mk_Trueprop (acc_R $ Bound 0)))
|> cterm_of thy
val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
-
- val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
-
+
+ val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
+
val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
in
R_cases
@@ -809,7 +809,7 @@
|> full_simplify (HOL_basic_ss addsimps [in_rel_def])
|> forall_intr (cterm_of thy Rrel)
end
-
+
(* Tail recursion (probably very fragile)
@@ -828,7 +828,7 @@
val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
(HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
- (fn {prems=[a], ...} =>
+ (fn {prems=[a], ...} =>
((rtac (G_induct OF [a]))
THEN_ALL_NEW (rtac accI)
THEN_ALL_NEW (etac R_cases)
@@ -841,13 +841,13 @@
val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
val thy = ProofContext.theory_of ctxt
val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
-
+
val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
in
Goal.prove ctxt [] [] trsimp
- (fn _ =>
+ (fn _ =>
rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
THEN (SIMPSET' simp_default_tac 1)
@@ -862,12 +862,12 @@
fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
let
- val FundefConfig {domintros, tailrec, default=default_str, ...} = config
-
+ val FundefConfig {domintros, tailrec, default=default_str, ...} = config
+
val fvar = Free (fname, fT)
val domT = domain_type fT
val ranT = range_type fT
-
+
val default = Syntax.parse_term lthy default_str
|> TypeInfer.constrain fT |> Syntax.check_term lthy
@@ -875,30 +875,30 @@
val Globals { x, h, ... } = globals
- val clauses = map (mk_clause_context x ctxt') abstract_qglrs
+ val clauses = map (mk_clause_context x ctxt') abstract_qglrs
val n = length abstract_qglrs
- fun build_tree (ClauseContext { ctxt, rhs, ...}) =
+ fun build_tree (ClauseContext { ctxt, rhs, ...}) =
FundefCtxTree.mk_tree (fname, fT) h ctxt rhs
val trees = map build_tree clauses
val RCss = map find_calls trees
- val ((G, GIntro_thms, G_elim, G_induct), lthy) =
+ val ((G, GIntro_thms, G_elim, G_induct), lthy) =
PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
- val ((f, f_defthm), lthy) =
+ val ((f, f_defthm), lthy) =
PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
- val ((R, RIntro_thmss, R_elim), lthy) =
+ val ((R, RIntro_thmss, R_elim), lthy) =
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
- val (_, lthy) =
- LocalTheory.abbrev Syntax.mode_default ((dom_name defname, NoSyn), mk_acc domT R) lthy
+ val (_, lthy) =
+ LocalTheory.abbrev Syntax.mode_default ((Name.binding (dom_name defname), NoSyn), mk_acc domT R) lthy
val newthy = ProofContext.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
@@ -918,31 +918,31 @@
fun mk_partial_rules provedgoal =
let
- val newthy = theory_of_thm provedgoal (*FIXME*)
+ val newthy = theory_of_thm provedgoal (*FIXME*)
- val (graph_is_function, complete_thm) =
+ val (graph_is_function, complete_thm) =
provedgoal
|> Conjunction.elim
|> apfst (Thm.forall_elim_vars 0)
-
+
val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
-
+
val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
-
- val simple_pinduct = PROFILE "Proving partial induction rule"
+
+ val simple_pinduct = PROFILE "Proving partial induction rule"
(mk_partial_induct_rule newthy globals R complete_thm) xclauses
-
-
+
+
val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
-
- val dom_intros = if domintros
+
+ val dom_intros = if domintros
then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
else NONE
val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
-
- in
- FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
- psimps=psimps, simple_pinducts=[simple_pinduct],
+
+ in
+ FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
+ psimps=psimps, simple_pinducts=[simple_pinduct],
termination=total_intro, trsimps=trsimps,
domintros=dom_intros}
end
@@ -951,6 +951,4 @@
end
-
-
end
--- a/src/HOL/Tools/function_package/fundef_lib.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Tue Sep 02 14:10:45 2008 +0200
@@ -56,7 +56,7 @@
fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
let
val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
- val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
+ val (_, ctx') = ProofContext.add_fixes_i [(Name.binding n', SOME T, NoSyn)] ctx
val (n'', body) = Term.dest_abs (n', T, b)
val _ = (n' = n'') orelse error "dest_all_ctx"
--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -9,15 +9,15 @@
signature FUNDEF_PACKAGE =
sig
- val add_fundef : (string * string option * mixfix) list
- -> ((bstring * Attrib.src list) * string) list
+ val add_fundef : (Name.binding * string option * mixfix) list
+ -> ((Name.binding * Attrib.src list) * string) list
-> FundefCommon.fundef_config
-> bool list
-> local_theory
-> Proof.state
- val add_fundef_i: (string * typ option * mixfix) list
- -> ((bstring * Attrib.src list) * term) list
+ val add_fundef_i: (Name.binding * typ option * mixfix) list
+ -> ((Name.binding * Attrib.src list) * term) list
-> FundefCommon.fundef_config
-> bool list
-> local_theory
@@ -36,7 +36,7 @@
open FundefLib
open FundefCommon
-val note_theorem = LocalTheory.note Thm.theoremK
+fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Name.binding name, atts), ths)
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
@@ -95,7 +95,9 @@
fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
let
- val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
+ val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
+ val fixes = map (apfst (apfst Name.name_of)) fixes0;
+ val spec = map (apfst (apfst Name.name_of)) spec0;
val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
val defname = mk_defname fixes
@@ -145,10 +147,10 @@
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
in
lthy
- |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss_i "" [(("", [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.rule_del]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
|> ProofContext.note_thmss_i ""
- [(("termination", [ContextRules.intro_bang (SOME 0)]),
+ [((Name.binding "termination", [ContextRules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
|> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
end
--- a/src/HOL/Tools/function_package/inductive_wrap.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML Tue Sep 02 14:10:45 2008 +0200
@@ -14,7 +14,7 @@
-> thm list * (term * thm * thm * local_theory)
end
-structure FundefInductiveWrap =
+structure FundefInductiveWrap: FUNDEF_INDUCTIVE_WRAP =
struct
open FundefLib
@@ -44,14 +44,14 @@
{quiet_mode = false,
verbose = ! Toplevel.debug,
kind = Thm.internalK,
- alt_name = "",
+ alt_name = Name.no_binding,
coind = false,
no_elim = false,
no_ind = false,
skip_mono = true}
- [((R, T), NoSyn)] (* the relation *)
+ [((Name.binding R, T), NoSyn)] (* the relation *)
[] (* no parameters *)
- (map (fn t => (("", []), t)) defs) (* the intros *)
+ (map (fn t => ((Name.no_binding, []), t)) defs) (* the intros *)
[] (* no special monos *)
lthy
--- a/src/HOL/Tools/function_package/mutual.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Tue Sep 02 14:10:45 2008 +0200
@@ -150,8 +150,8 @@
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
let
val ((f, (_, f_defthm)), lthy') =
- LocalTheory.define Thm.internalK ((fname, mixfix),
- ((fname ^ "_def", []), Term.subst_bound (fsum, f_def)))
+ LocalTheory.define Thm.internalK ((Name.binding fname, mixfix),
+ ((Name.binding (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
lthy
in
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
--- a/src/HOL/Tools/function_package/size.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/function_package/size.ML Tue Sep 02 14:10:45 2008 +0200
@@ -132,8 +132,8 @@
fun define_overloaded (def_name, eq) lthy =
let
val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
- val ((_, (_, thm)), lthy') = lthy
- |> LocalTheory.define Thm.definitionK ((c, NoSyn), ((def_name, []), rhs));
+ val ((_, (_, thm)), lthy') = lthy |> LocalTheory.define Thm.definitionK
+ ((Name.binding c, NoSyn), ((Name.binding def_name, []), rhs));
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
--- a/src/HOL/Tools/inductive_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -33,22 +33,25 @@
val inductive_forall_name: string
val inductive_forall_def: thm
val rulify: thm -> thm
- val inductive_cases: ((bstring * Attrib.src list) * string list) list ->
+ val inductive_cases: ((Name.binding * Attrib.src list) * string list) list ->
Proof.context -> thm list list * local_theory
- val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
+ val inductive_cases_i: ((Name.binding * Attrib.src list) * term list) list ->
Proof.context -> thm list list * local_theory
type inductive_flags
val add_inductive_i:
- inductive_flags -> ((string * typ) * mixfix) list ->
- (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
+ inductive_flags -> ((Name.binding * typ) * mixfix) list ->
+ (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
local_theory -> inductive_result * local_theory
- val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
- (string * string option * mixfix) list ->
- ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
+ val add_inductive: bool -> bool ->
+ (Name.binding * string option * mixfix) list ->
+ (Name.binding * string option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * string) list ->
+ (Facts.ref * Attrib.src list) list ->
local_theory -> inductive_result * local_theory
val add_inductive_global: string -> inductive_flags ->
- ((string * typ) * mixfix) list -> (string * typ) list ->
- ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
+ ((Name.binding * typ) * mixfix) list ->
+ (string * typ) list ->
+ ((Name.binding * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
val arities_of: thm -> (string * int) list
val params_of: thm -> term list
val partition_rules: thm -> thm list -> (string * thm list) list
@@ -62,18 +65,19 @@
sig
include BASIC_INDUCTIVE_PACKAGE
type add_ind_def
- val declare_rules: string -> bstring -> bool -> bool -> string list ->
- thm list -> bstring list -> Attrib.src list list -> (thm * string list) list ->
+ val declare_rules: string -> Name.binding -> bool -> bool -> string list ->
+ thm list -> Name.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 -> ((string * typ) * mixfix) list ->
- (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
- local_theory -> inductive_result * local_theory
- val gen_add_inductive: add_ind_def ->
- bool -> bool -> (string * string option * mixfix) list ->
- (string * string option * mixfix) list ->
- ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
+ val gen_add_inductive_i: add_ind_def -> inductive_flags ->
+ ((Name.binding * typ) * mixfix) list ->
+ (string * typ) list ->
+ ((Name.binding * Attrib.src list) * term) list -> thm list ->
+ local_theory -> inductive_result * local_theory
+ val gen_add_inductive: add_ind_def -> bool -> bool ->
+ (Name.binding * string option * mixfix) list ->
+ (Name.binding * string option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
local_theory -> inductive_result * local_theory
val gen_ind_decl: add_ind_def -> bool ->
OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
@@ -258,8 +262,9 @@
in
-fun check_rule ctxt cs params ((name, att), rule) =
+fun check_rule ctxt cs params ((binding, att), rule) =
let
+ val name = Name.name_of binding;
val params' = Term.variant_frees rule (Logic.strip_params rule);
val frees = rev (map Free params');
val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
@@ -294,7 +299,7 @@
List.app check_prem (prems ~~ aprems))
else err_in_rule ctxt name rule' bad_concl
| _ => err_in_rule ctxt name rule' bad_concl);
- ((name, att), arule)
+ ((binding, att), arule)
end;
val rulify =
@@ -635,13 +640,15 @@
(* add definiton of recursive predicates to theory *)
- val rec_name = if alt_name = "" then
- space_implode "_" (map fst cnames_syn) else alt_name;
+ val rec_name =
+ if Name.name_of alt_name = "" then
+ Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ else alt_name;
val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
LocalTheory.define Thm.internalK
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
- (("", []), fold_rev lambda params
+ ((Name.no_binding, []), fold_rev lambda params
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
(cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
@@ -652,7 +659,7 @@
val xs = map Free (Variable.variant_frees ctxt intr_ts
(mk_names "x" (length Ts) ~~ Ts))
in
- (name_mx, (("", []), fold_rev lambda (params @ xs)
+ (name_mx, ((Name.no_binding, []), fold_rev lambda (params @ xs)
(list_comb (rec_const, params @ make_bool_args' bs i @
make_args argTs (xs ~~ Ts)))))
end) (cnames_syn ~~ cs);
@@ -665,9 +672,12 @@
list_comb (rec_const, params), preds, argTs, bs, xs)
end;
-fun declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts
+fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
elims raw_induct ctxt =
let
+ val rec_name = Name.name_of rec_binding;
+ val rec_qualified = NameSpace.qualified rec_name;
+ val intr_names = map Name.name_of intr_bindings;
val ind_case_names = RuleCases.case_names intr_names;
val induct =
if coind then
@@ -681,28 +691,28 @@
val (intrs', ctxt1) =
ctxt |>
LocalTheory.notes kind
- (map (NameSpace.qualified rec_name) intr_names ~~
+ (map (Name.map_name rec_qualified) intr_bindings ~~
intr_atts ~~ map (fn th => [([th],
[Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), ctxt2) =
ctxt1 |>
- LocalTheory.note kind ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
+ LocalTheory.note kind ((Name.binding (rec_qualified "intros"), []), intrs') ||>>
fold_map (fn (name, (elim, cases)) =>
- LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
+ LocalTheory.note kind ((Name.binding (NameSpace.qualified (Sign.base_name name) "cases"),
[Attrib.internal (K (RuleCases.case_names cases)),
Attrib.internal (K (RuleCases.consumes 1)),
Attrib.internal (K (Induct.cases_pred name)),
Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
- LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
+ LocalTheory.note kind ((Name.binding (rec_qualified (coind_prefix coind ^ "induct")),
map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
val ctxt3 = if no_ind orelse coind then ctxt2 else
let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
in
ctxt2 |>
- LocalTheory.notes kind [((NameSpace.qualified rec_name "inducts", []),
+ LocalTheory.notes kind [((Name.binding (rec_qualified "inducts"), []),
inducts |> map (fn (name, th) => ([th],
[Attrib.internal (K ind_case_names),
Attrib.internal (K (RuleCases.consumes 1)),
@@ -711,24 +721,25 @@
in (intrs', elims', induct', ctxt3) end;
type inductive_flags =
- {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
+ {quiet_mode: bool, verbose: bool, kind: string, alt_name: Name.binding,
coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
type add_ind_def =
inductive_flags ->
- term list -> ((string * Attrib.src list) * term) list -> thm list ->
- term list -> (string * mixfix) list ->
+ term list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
+ term list -> (Name.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}
+fun (add_ind_def: add_ind_def)
+ {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
cs intros monos params cnames_syn ctxt =
let
val _ = null cnames_syn andalso error "No inductive predicates given";
+ val names = map (Name.name_of o fst) cnames_syn;
val _ = message (quiet_mode andalso not verbose)
- ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
- commas_quote (map fst cnames_syn));
+ ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
- val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; (* FIXME *)
+ val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn; (* FIXME *)
val ((intr_names, intr_atts), intr_ts) =
apfst split_list (split_list (map (check_rule ctxt cs params) intros));
@@ -739,7 +750,8 @@
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
params intr_ts rec_preds_defs ctxt1;
val elims = if no_elim then [] else
- prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt1;
+ prove_elims quiet_mode cs params intr_ts (map Name.name_of intr_names)
+ unfold rec_preds_defs ctxt1;
val raw_induct = zero_var_indexes
(if no_ind then Drule.asm_rl else
if coind then
@@ -755,7 +767,6 @@
val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
cnames intrs intr_names intr_atts elims raw_induct ctxt1;
- val names = map #1 cnames_syn;
val result =
{preds = preds,
intrs = intrs',
@@ -782,35 +793,35 @@
(* abbrevs *)
- val (_, ctxt1) = Variable.add_fixes (map (fst o fst) cnames_syn) lthy;
+ val (_, ctxt1) = Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn) lthy;
fun get_abbrev ((name, atts), t) =
if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
let
- val _ = name = "" andalso null atts orelse
+ val _ = Name.name_of name = "" andalso null atts orelse
error "Abbreviations may not have names or attributes";
val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
- val mx =
- (case find_first (fn ((c, _), _) => c = x) cnames_syn of
+ val var =
+ (case find_first (fn ((c, _), _) => Name.name_of c = x) cnames_syn of
NONE => error ("Undeclared head of abbreviation " ^ quote x)
- | SOME ((_, T'), mx) =>
+ | SOME ((b, T'), mx) =>
if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
- else mx);
- in SOME ((x, mx), rhs) end
+ else (b, mx));
+ in SOME (var, rhs) end
else NONE;
val abbrevs = map_filter get_abbrev spec;
- val bs = map (fst o fst) abbrevs;
+ val bs = map (Name.name_of o fst o fst) abbrevs;
(* predicates *)
val pre_intros = filter_out (is_some o get_abbrev) spec;
- val cnames_syn' = filter_out (member (op =) bs o fst o fst) cnames_syn;
- val cs = map (Free o fst) cnames_syn';
+ val cnames_syn' = filter_out (member (op =) bs o Name.name_of o fst o fst) cnames_syn;
+ val cs = map (Free o apfst Name.name_of o fst) cnames_syn';
val ps = map Free pnames;
- val (_, ctxt2) = lthy |> Variable.add_fixes (map (fst o fst) cnames_syn');
+ val (_, ctxt2) = lthy |> Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn');
val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
@@ -837,12 +848,12 @@
val (cs, ps) = chop (length cnames_syn) vars;
val intrs = map (apsnd the_single) specs;
val monos = Attrib.eval_thms lthy raw_monos;
- val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK, alt_name = "",
- coind = coind, no_elim = false, no_ind = false, skip_mono = false};
+ val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
+ alt_name = Name.no_binding, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
in
lthy
|> LocalTheory.set_group (serial_string ())
- |> gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos
+ |> gen_add_inductive_i mk_def flags cs (map (apfst Name.name_of o fst) ps) intrs monos
end;
val add_inductive_i = gen_add_inductive_i add_ind_def;
@@ -850,7 +861,7 @@
fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
let
- val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
+ val name = Sign.full_name thy (Name.name_of (fst (fst (hd cnames_syn))));
val ctxt' = thy
|> TheoryTarget.init NONE
|> LocalTheory.set_group group
@@ -934,14 +945,15 @@
val _ = OuterKeyword.keyword "monos";
+(* FIXME eliminate *)
fun flatten_specification specs = specs |> maps
(fn (a, (concl, [])) => concl |> map
(fn ((b, atts), [B]) =>
- if a = "" then ((b, atts), B)
- else if b = "" then ((a, atts), B)
- else error ("Illegal nested case names " ^ quote (NameSpace.append a b))
- | ((b, _), _) => error ("Illegal simultaneous specification " ^ quote b))
- | (a, _) => error ("Illegal local specification parameters for " ^ quote a));
+ if Name.name_of a = "" then ((b, atts), B)
+ else if Name.name_of b = "" then ((a, atts), B)
+ else error "Illegal nested case names"
+ | ((b, _), _) => error "Illegal simultaneous specification")
+ | (a, _) => error ("Illegal local specification parameters for " ^ quote (Name.name_of a)));
fun gen_ind_decl mk_def coind =
P.fixes -- P.for_fixes --
--- a/src/HOL/Tools/inductive_realizer.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Sep 02 14:10:45 2008 +0200
@@ -337,9 +337,7 @@
(Logic.strip_assums_concl rintr));
val s' = Sign.base_name s;
val T' = Logic.unvarifyT T
- in (((s', T'), NoSyn),
- (Const (s, T'), Free (s', T')))
- end) rintrs));
+ in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
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));
@@ -348,10 +346,10 @@
val (ind_info, thy3') = thy2 |>
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = "",
+ {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding,
coind = false, no_elim = false, no_ind = false, skip_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
- ((Sign.base_name (name_of_thm intr), []),
+ ((Name.binding (Sign.base_name (name_of_thm intr)), []),
subst_atomic rlzpreds' (Logic.unvarify rintr)))
(rintrs ~~ maps snd rss)) [] ||>
Sign.absolute_path;
--- a/src/HOL/Tools/inductive_set_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -13,12 +13,12 @@
val pred_set_conv_att: attribute
val add_inductive_i:
InductivePackage.inductive_flags ->
- ((string * typ) * mixfix) list ->
- (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
+ ((Name.binding * typ) * mixfix) list ->
+ (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
local_theory -> InductivePackage.inductive_result * local_theory
- val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
- (string * string option * mixfix) list ->
- ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
+ val add_inductive: bool -> bool -> (Name.binding * string option * mixfix) list ->
+ (Name.binding * string option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
local_theory -> InductivePackage.inductive_result * local_theory
val setup: theory -> theory
end;
@@ -461,16 +461,17 @@
| 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 (s, _) => (s ^ "p", NoSyn)) cnames_syn;
+ val cnames_syn' = map (fn (b, _) => (Name.map_name (suffix "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 {quiet_mode = quiet_mode, verbose = verbose, kind = kind,
- alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
+ InductivePackage.add_ind_def
+ {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Name.no_binding,
+ coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
cs' intros' monos' params1 cnames_syn' ctxt;
(* define inductive sets using previously defined predicates *)
val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
- (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []),
+ (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, ((Name.no_binding, []),
fold_rev lambda params (HOLogic.Collect_const U $
HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds)) ctxt1;
@@ -488,15 +489,17 @@
(K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
[def, mem_Collect_eq, split_conv]) 1))
in
- ctxt |> LocalTheory.note kind ((s ^ "p_" ^ s ^ "_eq",
+ ctxt |> LocalTheory.note kind ((Name.binding (s ^ "p_" ^ s ^ "_eq"),
[Attrib.internal (K pred_set_conv_att)]),
[conv_thm]) |> snd
end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
(* convert theorems to set notation *)
- val rec_name = if alt_name = "" then
- space_implode "_" (map fst cnames_syn) else alt_name;
- val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn; (* FIXME *)
+ val rec_name =
+ if Name.name_of alt_name = "" then
+ Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ else alt_name;
+ val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn; (* FIXME *)
val (intr_names, intr_atts) = split_list (map fst intros);
val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
val (intrs', elims', induct, ctxt4) =
--- a/src/HOL/Tools/primrec_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/primrec_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -8,13 +8,13 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec: (string * typ option * mixfix) list ->
- ((bstring * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
- val add_primrec_global: (string * typ option * mixfix) list ->
- ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory
+ val add_primrec: (Name.binding * typ option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
+ val add_primrec_global: (Name.binding * typ option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
val add_primrec_overloaded: (string * (string * typ) * bool) list ->
- (string * typ option * mixfix) list ->
- ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory
+ (Name.binding * typ option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -189,14 +189,14 @@
fun make_def ctxt fixes fs (fname, ls, rec_name, tname) =
let
val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t))
- ((map snd ls) @ [dummyT])
+ (map snd ls @ [dummyT])
(list_comb (Const (rec_name, dummyT),
- fs @ map Bound (0 ::(length ls downto 1))))
+ fs @ map Bound (0 :: (length ls downto 1))))
val def_name = Thm.def_name (Sign.base_name fname);
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
- val SOME mfx = get_first
- (fn ((v, _), mfx) => if v = fname then SOME mfx else NONE) fixes;
- in ((fname, mfx), ((def_name, []), rhs)) end;
+ val SOME var = get_first (fn ((b, _), mx) =>
+ if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
+ in (var, ((Name.binding def_name, []), rhs)) end;
(* find datatypes which contain all datatypes in tnames' *)
@@ -226,16 +226,15 @@
val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
- in map (fn (name_attr, t) => (name_attr, [Goal.prove ctxt [] [] t tac])) end;
+ in map (fn (a, t) => (a, [Goal.prove ctxt [] [] t tac])) end;
fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
let
val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
- orelse exists (fn ((w, _), _) => v = w) fixes) o snd) spec [];
+ orelse exists (fn ((w, _), _) => v = Name.name_of w) fixes) o snd) spec [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
- val dts = find_dts (DatatypePackage.get_datatypes
- (ProofContext.theory_of lthy)) tnames tnames;
+ val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
val main_fns = map (fn (tname, {index, ...}) =>
(index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
val {descr, rec_names, rec_rewrites, ...} =
@@ -251,7 +250,7 @@
"\nare not mutually recursive");
val qualify = NameSpace.qualified
(space_implode "_" (map (Sign.base_name o #1) defs));
- val spec' = (map o apfst o apfst) qualify spec;
+ val spec' = (map o apfst o apfst o Name.map_name) qualify spec;
val simp_atts = map (Attrib.internal o K)
[Simplifier.simp_add, RecfunCodegen.add NONE];
in
@@ -261,7 +260,7 @@
|-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
|-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
|-> (fn simps' => LocalTheory.note Thm.theoremK
- ((qualify "simps", simp_atts), maps snd simps'))
+ ((Name.binding (qualify "simps"), simp_atts), maps snd simps'))
|>> snd
end handle PrimrecError (msg, some_eqn) =>
error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
@@ -300,7 +299,7 @@
P.name >> pair false) --| P.$$$ ")")) (false, "");
val old_primrec_decl =
- opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
+ opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop);
fun pipe_error t = P.!!! (Scan.fail_with (K
(cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
--- a/src/HOL/Tools/recdef_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/recdef_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -268,8 +268,8 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- Specification.theorem Thm.internalK NONE (K I) (bname, atts)
- [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
+ Specification.theorem Thm.internalK NONE (K I) (Name.binding bname, atts)
+ [] (Element.Shows [((Name.no_binding, []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
end;
val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
@@ -299,7 +299,8 @@
val recdef_decl =
Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
+ P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
+ -- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
val _ =
@@ -319,7 +320,8 @@
val _ =
OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
K.thy_goal
- (SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
+ ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
+ Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
end;
--- a/src/HOL/Tools/specification_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/specification_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -233,7 +233,7 @@
val specification_decl =
P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+ Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
val _ =
OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -244,7 +244,7 @@
val ax_specification_decl =
P.name --
(P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
+ Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
val _ =
OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
--- a/src/HOL/Tools/typecopy_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -134,7 +134,7 @@
(mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
val def' = Syntax.check_term lthy def;
val ((_, (_, thm)), lthy') = Specification.definition
- (NONE, (("", []), def')) lthy;
+ (NONE, ((Name.no_binding, []), def')) lthy;
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
--- a/src/HOL/Typedef.thy Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Typedef.thy Tue Sep 02 14:10:45 2008 +0200
@@ -145,7 +145,7 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
+ |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit
--- a/src/HOL/ex/Quickcheck.thy Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy Tue Sep 02 14:10:45 2008 +0200
@@ -128,11 +128,11 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort random})
|> PrimrecPackage.add_primrec
- [(fst (dest_Free random'), SOME (snd (dest_Free random')), NoSyn)]
- (map (fn eq => (("", [del_func]), eq)) eqs')
+ [(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
+ (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
|-> add_code
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
+ |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit
@@ -261,7 +261,7 @@
in
thy
|> TheoryTarget.init NONE
- |> Specification.definition (NONE, (("", []), eq))
+ |> Specification.definition (NONE, ((Name.no_binding, []), eq))
|> snd
|> LocalTheory.exit
|> ProofContext.theory_of
--- a/src/HOLCF/Tools/fixrec_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -9,10 +9,10 @@
sig
val legacy_infer_term: theory -> term -> term
val legacy_infer_prop: theory -> term -> term
- val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
- val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
- val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
- val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
+ val add_fixrec: bool -> ((Name.binding * Attrib.src list) * string) list list -> theory -> theory
+ val add_fixrec_i: bool -> ((Name.binding * attribute list) * term) list list -> theory -> theory
+ val add_fixpat: (Name.binding * Attrib.src list) * string list -> theory -> theory
+ val add_fixpat_i: (Name.binding * attribute list) * term list -> theory -> theory
end;
structure FixrecPackage: FIXREC_PACKAGE =
@@ -226,7 +226,8 @@
val eqns = List.concat blocks;
val lengths = map length blocks;
- val ((names, srcss), strings) = apfst split_list (split_list eqns);
+ val ((bindings, srcss), strings) = apfst split_list (split_list eqns);
+ val names = map Name.name_of bindings;
val atts = map (map (prep_attrib thy)) srcss;
val eqn_ts = map (prep_prop thy) strings;
val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
@@ -278,7 +279,7 @@
val ts = map (prep_term thy) strings;
val simps = map (fix_pat thy) ts;
in
- (snd o PureThy.add_thmss [((name, simps), atts)]) thy
+ (snd o PureThy.add_thmss [((Name.name_of name, simps), atts)]) thy
end;
val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
--- a/src/HOLCF/Tools/pcpodef_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -94,7 +94,7 @@
|> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
val less_def' = Syntax.check_term lthy3 less_def;
val ((_, (_, less_definition')), lthy4) = lthy3
- |> Specification.definition (NONE, (("less_" ^ name ^ "_def", []), less_def'));
+ |> Specification.definition (NONE, ((Name.binding ("less_" ^ name ^ "_def"), []), 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
--- a/src/Pure/Isar/attrib.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Sep 02 14:10:45 2008 +0200
@@ -110,7 +110,8 @@
fun attribute thy = attribute_i thy o intern_src thy;
fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
- [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+ [((Name.no_binding, []),
+ map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
|> fst |> maps snd;
--- a/src/Pure/Isar/class.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/class.ML Tue Sep 02 14:10:45 2008 +0200
@@ -19,7 +19,7 @@
val abbrev: class -> Syntax.mode -> Properties.T
-> (string * mixfix) * term -> theory -> theory
val note: class -> string
- -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
+ -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
-> theory -> (bstring * thm list) list * theory
val declaration: class -> declaration -> theory -> theory
val refresh_syntax: class -> Proof.context -> Proof.context
@@ -48,7 +48,7 @@
(*old axclass layer*)
val axclass_cmd: bstring * xstring list
- -> ((bstring * Attrib.src list) * string list) list
+ -> ((Name.binding * Attrib.src list) * string list) list
-> theory -> class * theory
val classrel_cmd: xstring * xstring -> theory -> Proof.state
@@ -374,7 +374,7 @@
thy
|> fold2 add_constraint (map snd consts) no_constraints
|> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
- (inst, map (fn def => (("", []), def)) defs)
+ (inst, map (fn def => ((Name.no_binding, []), def)) defs)
|> fold2 add_constraint (map snd consts) constraints
end;
@@ -569,7 +569,7 @@
val constrain = Element.Constrains ((map o apsnd o map_atyps)
(K (TFree (Name.aT, base_sort))) supparams);
fun fork_syn (Element.Fixes xs) =
- fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
+ fold_map (fn (c, ty, syn) => cons (Name.name_of c, syn) #> pair (c, ty, NoSyn)) xs
#>> Element.Fixes
| fork_syn x = pair x;
fun fork_syntax elems =
@@ -628,7 +628,7 @@
|> add_consts ((snd o chop (length supparams)) all_params)
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
(map (fst o snd) params)
- [((bname ^ "_" ^ AxClass.axiomsN, []), map (globalize param_map) raw_pred)]
+ [((Name.binding (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
#> snd
#> `get_axiom
#-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
--- a/src/Pure/Isar/constdefs.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/constdefs.ML Tue Sep 02 14:10:45 2008 +0200
@@ -9,12 +9,12 @@
signature CONSTDEFS =
sig
- val add_constdefs: (string * string option) list *
- ((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
- theory -> theory
- val add_constdefs_i: (string * typ option) list *
- ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
- theory -> theory
+ val add_constdefs: (Name.binding * string option) list *
+ ((Name.binding * string option * mixfix) option *
+ ((Name.binding * Attrib.src list) * string)) list -> theory -> theory
+ val add_constdefs_i: (Name.binding * typ option) list *
+ ((Name.binding * typ option * mixfix) option *
+ ((Name.binding * attribute list) * term)) list -> theory -> theory
end;
structure Constdefs: CONSTDEFS =
@@ -38,13 +38,16 @@
val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
- val _ = (case d of NONE => () | SOME c' =>
- if c <> c' then
- err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
- else ());
+ val _ =
+ (case Option.map Name.name_of d of
+ NONE => ()
+ | SOME c' =>
+ if c <> c' then
+ err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
+ else ());
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
- val name = Thm.def_name_optional c raw_name;
+ val name = Thm.def_name_optional c (Name.name_of raw_name);
val atts = map (prep_att thy) raw_atts;
val thy' =
--- a/src/Pure/Isar/isar_cmd.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Sep 02 14:10:45 2008 +0200
@@ -15,19 +15,19 @@
val print_ast_translation: bool * (string * Position.T) -> theory -> theory
val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
theory -> theory
- val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
- val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
+ val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
+ val add_defs: (bool * bool) * ((Name.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
val hide_names: bool -> string * xstring list -> theory -> theory
- val have: ((string * Attrib.src list) * (string * string list) list) list ->
+ val have: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val hence: ((string * Attrib.src list) * (string * string list) list) list ->
+ val hence: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val show: ((string * Attrib.src list) * (string * string list) list) list ->
+ val show: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val thus: ((string * Attrib.src list) * (string * string list) list) list ->
+ val thus: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
val terminal_proof: Method.text * Method.text option ->
@@ -179,7 +179,7 @@
(* axioms *)
fun add_axms f args thy =
- f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
+ f (map (fn ((b, ax), srcs) => ((Name.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
--- a/src/Pure/Isar/isar_syn.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Sep 02 14:10:45 2008 +0200
@@ -203,10 +203,10 @@
(* old constdefs *)
val old_constdecl =
- P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
- P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
+ P.binding --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
+ P.binding -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
--| Scan.option P.where_ >> P.triple1 ||
- P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
+ P.binding -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
@@ -221,7 +221,7 @@
(* constant definitions and abbreviations *)
val constdecl =
- P.name --
+ P.binding --
(P.where_ >> K (NONE, NoSyn) ||
P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
@@ -272,7 +272,7 @@
val _ =
OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
(P.and_list1 SpecParse.xthms1
- >> (fn args => #2 o Specification.theorems_cmd "" [(("", []), flat args)]));
+ >> (fn args => #2 o Specification.theorems_cmd "" [((Name.no_binding, []), flat args)]));
(* name space entry path *)
@@ -396,16 +396,18 @@
(P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
>> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
- >> (fn ((x, y), z) => Toplevel.print o
- Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
+ >> (fn (((name, atts), expr), insts) => Toplevel.print o
+ Toplevel.theory_to_proof
+ (Locale.interpretation I ((true, Name.name_of name), atts) expr insts)));
val _ =
OuterSyntax.command "interpret"
"prove and register interpretation of locale expression in proof context"
(K.tag_proof K.prf_goal)
(SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
- >> (fn ((x, y), z) => Toplevel.print o
- Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
+ >> (fn (((name, atts), expr), insts) => Toplevel.print o
+ Toplevel.proof'
+ (Locale.interpret Seq.single ((true, Name.name_of name), atts) expr insts)));
(* classes *)
@@ -466,7 +468,7 @@
fun gen_theorem kind =
OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
(Scan.optional (SpecParse.opt_thm_name ":" --|
- Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
+ Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) (Name.no_binding, []) --
SpecParse.general_statement >> (fn (a, (elems, concl)) =>
(Specification.theorem_cmd kind NONE (K I) a elems concl)));
@@ -552,7 +554,7 @@
(K.tag_proof K.prf_asm)
(P.and_list1
(SpecParse.opt_thm_name ":" --
- ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
+ ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
>> (Toplevel.print oo (Toplevel.proof o Proof.def)));
val _ =
--- a/src/Pure/Isar/local_defs.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/local_defs.ML Tue Sep 02 14:10:45 2008 +0200
@@ -12,10 +12,11 @@
val mk_def: Proof.context -> (string * term) list -> term list
val expand: cterm list -> thm -> thm
val def_export: Assumption.export
- val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
- (term * (bstring * thm)) list * Proof.context
- val add_def: (string * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
- val fixed_abbrev: (string * mixfix) * term -> Proof.context -> (term * term) * Proof.context
+ val add_defs: ((Name.binding * mixfix) * ((Name.binding * attribute list) * term)) list ->
+ Proof.context -> (term * (string * thm)) list * Proof.context
+ val add_def: (Name.binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
+ val fixed_abbrev: (Name.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
val trans_terms: Proof.context -> thm list -> thm
@@ -88,22 +89,23 @@
fun add_defs defs ctxt =
let
- val ((xs, mxs), specs) = defs |> split_list |>> split_list;
- val ((names, atts), rhss) = specs |> split_list |>> split_list;
- val names' = map2 Thm.def_name_optional xs names;
+ val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
+ val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
+ val xs = map Name.name_of bvars;
+ val names = map2 (Name.map_name o Thm.def_name_optional) xs bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
in
ctxt
- |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
+ |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
|> fold Variable.declare_term eqs
|> ProofContext.add_assms_i def_export
- (map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs)
+ (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
|>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
end;
fun add_def (var, rhs) ctxt =
- let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (("", []), rhs))] ctxt
+ let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Name.no_binding, []), rhs))] ctxt
in ((lhs, th), ctxt') end;
--- a/src/Pure/Isar/local_theory.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/local_theory.ML Tue Sep 02 14:10:45 2008 +0200
@@ -26,16 +26,16 @@
val affirm: local_theory -> local_theory
val pretty: local_theory -> Pretty.T list
val axioms: string ->
- ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
- -> (term list * (bstring * thm list) list) * local_theory
- val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
+ ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
+ -> (term list * (string * thm list) list) * local_theory
+ val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
- (term * (bstring * thm)) * local_theory
- val note: string -> (bstring * Attrib.src list) * thm list ->
- local_theory -> (bstring * thm list) * local_theory
- val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
- local_theory -> (bstring * thm list) list * local_theory
+ val define: string -> (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
+ (term * (string * thm)) * local_theory
+ val note: string -> (Name.binding * Attrib.src list) * thm list ->
+ local_theory -> (string * thm list) * local_theory
+ val notes: string -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+ local_theory -> (string * thm list) list * local_theory
val type_syntax: declaration -> local_theory -> local_theory
val term_syntax: declaration -> local_theory -> local_theory
val declaration: declaration -> local_theory -> local_theory
@@ -57,15 +57,15 @@
type operations =
{pretty: local_theory -> Pretty.T list,
axioms: string ->
- ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
- -> (term list * (bstring * thm list) list) * local_theory,
- abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
+ ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
+ -> (term list * (string * thm list) list) * local_theory,
+ abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> (term * term) * local_theory,
define: string ->
- (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
- (term * (bstring * thm)) * local_theory,
+ (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
+ (term * (string * thm)) * local_theory,
notes: string ->
- ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
- local_theory -> (bstring * thm list) list * local_theory,
+ ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+ local_theory -> (string * thm list) list * local_theory,
type_syntax: declaration -> local_theory -> local_theory,
term_syntax: declaration -> local_theory -> local_theory,
declaration: declaration -> local_theory -> local_theory,
--- a/src/Pure/Isar/locale.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/locale.ML Tue Sep 02 14:10:45 2008 +0200
@@ -55,16 +55,16 @@
val parameters_of_expr: theory -> expr ->
((string * typ) * mixfix) list
val local_asms_of: theory -> string ->
- ((string * Attrib.src list) * term list) list
+ ((Name.binding * Attrib.src list) * term list) list
val global_asms_of: theory -> string ->
- ((string * Attrib.src list) * term list) list
+ ((Name.binding * Attrib.src list) * 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
- -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list list
+ -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list list
(* Processing of locale statements *)
val read_context_statement: xstring option -> Element.context element list ->
@@ -96,7 +96,7 @@
(* Storing results *)
val add_thmss: string -> string ->
- ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+ ((Name.binding * Attrib.src list) * (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
@@ -104,21 +104,21 @@
val interpretation_i: (Proof.context -> Proof.context) ->
(bool * string) * Attrib.src list -> expr ->
- term option list * ((bstring * Attrib.src list) * term) list ->
+ term option list * ((Name.binding * Attrib.src list) * term) list ->
theory -> Proof.state
val interpretation: (Proof.context -> Proof.context) ->
(bool * string) * Attrib.src list -> expr ->
- string option list * ((bstring * Attrib.src list) * string) list ->
+ string option list * ((Name.binding * Attrib.src list) * string) list ->
theory -> Proof.state
val interpretation_in_locale: (Proof.context -> Proof.context) ->
xstring * expr -> theory -> Proof.state
val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
(bool * string) * Attrib.src list -> expr ->
- term option list * ((bstring * Attrib.src list) * term) list ->
+ term option list * ((Name.binding * Attrib.src list) * term) list ->
bool -> Proof.state -> Proof.state
val interpret: (Proof.state -> Proof.state Seq.seq) ->
(bool * string) * Attrib.src list -> expr ->
- string option list * ((bstring * Attrib.src list) * string) list ->
+ string option list * ((Name.binding * Attrib.src list) * string) list ->
bool -> Proof.state -> Proof.state
end;
@@ -756,7 +756,7 @@
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 ren);
+ 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;
@@ -789,7 +789,7 @@
fun make_raw_params_elemss (params, tenv, syn) =
[((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
Int [Fixes (map (fn p =>
- (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
+ (Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
(* flatten_expr:
@@ -929,7 +929,7 @@
val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
val elem_morphism =
Element.rename_morphism ren $>
- Morphism.name_morphism (params_qualified params) $>
+ Morphism.name_morphism (Name.map_name (params_qualified params)) $>
Element.instT_morphism thy env;
val elems' = map (Element.morph_ctxt elem_morphism) elems;
in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
@@ -978,7 +978,7 @@
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', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
+ in (t', ((Name.map_name (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);
@@ -989,7 +989,7 @@
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
- in (if is_ext then res else [], (ctxt', mode)) end;
+ 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
@@ -1076,15 +1076,15 @@
*)
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
- val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
+ val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
in
((ids',
merge_syntax ctxt ids'
- (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
+ (syn, Symtab.make (map (fn fx => (Name.name_of (#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 #1) fixes), Assumed []), Ext (Fixes fixes))])
+ [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
end
| flatten _ ((ids, syn), Elem elem) =
((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
@@ -1104,7 +1104,7 @@
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) => (x, SOME T, NoSyn)) csts) ctxt
+ let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding 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)
@@ -1227,8 +1227,9 @@
end;
-fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
- (x, AList.lookup (op =) parms x, mx)) fixes)
+fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
+ let val x = Name.name_of binding
+ in (binding, 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))
@@ -1274,7 +1275,7 @@
list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
Term.fast_term_ord (d1, d2)) (defs1, defs2);
structure Defstab =
- TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
+ TableFun(type key = ((Name.binding * Attrib.src list) * (term * term list)) list
val ord = defs_ord);
fun rem_dup_defs es ds =
@@ -1387,7 +1388,7 @@
|> 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,
- name = prep_name,
+ name = Name.map_name prep_name,
fact = get ctxt,
attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
@@ -1572,8 +1573,8 @@
(* naming of interpreted theorems *)
fun add_param_prefixss s =
- (map o apfst o apfst) (NameSpace.qualified s);
-fun drop_param_prefixss args = (map o apfst o apfst)
+ (map o apfst o apfst o Name.map_name) (NameSpace.qualified s);
+fun drop_param_prefixss args = (map o apfst o apfst o Name.map_name)
(fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
@@ -1660,7 +1661,7 @@
fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
let
- val inst = Morphism.name_morphism (NameSpace.qualified prfx) $>
+ val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
(* need to add parameter prefix *) (* FIXME *)
Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
@@ -1724,7 +1725,7 @@
(fn (axiom, elems, params, decls, regs, intros, dests) =>
(axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
add_thmss loc Thm.internalK
- [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
+ [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
in
@@ -1864,12 +1865,13 @@
thy
|> def_pred aname parms defs exts exts';
val elemss' = change_assumes_elemss axioms elemss;
- val a_elem = [(("", []), [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
+ val a_elem = [(("", []),
+ [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
val (_, thy'') =
thy'
|> Sign.add_path aname
|> Sign.no_base_names
- |> PureThy.note_thmss Thm.internalK [((introN, []), [([intro], [])])]
+ |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
||> Sign.restore_naming thy';
in ((elemss', [statement]), a_elem, [intro], thy'') end;
val (predicate, stmt', elemss'', b_intro, thy'''') =
@@ -1882,14 +1884,15 @@
val cstatement = Thm.cterm_of thy''' statement;
val elemss'' = change_elemss_hyps axioms elemss';
val b_elem = [(("", []),
- [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
+ [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
val (_, thy'''') =
thy'''
|> Sign.add_path pname
|> Sign.no_base_names
|> PureThy.note_thmss Thm.internalK
- [((introN, []), [([intro], [])]),
- ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
+ [((Name.binding introN, []), [([intro], [])]),
+ ((Name.binding 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;
@@ -1905,7 +1908,7 @@
fun defines_to_notes is_ext thy (Defines defs) defns =
let
- val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
+ val defs' = map (fn (_, (def, _)) => ((Name.no_binding, []), (def, []))) defs
val notes = map (fn (a, (def, _)) =>
(a, [([assume (cterm_of thy def)], [])])) defs
in
@@ -1994,9 +1997,9 @@
end;
val _ = Context.>> (Context.map_theory
- (add_locale_i "" "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
+ (add_locale_i "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
snd #> ProofContext.theory_of #>
- add_locale_i "" "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
+ add_locale_i "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
snd #> ProofContext.theory_of));
@@ -2374,7 +2377,7 @@
fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
let
val att_morphism =
- Morphism.name_morphism (NameSpace.qualified prfx) $>
+ Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
Morphism.thm_morphism satisfy $>
Element.inst_morphism thy insts $>
Morphism.thm_morphism disch;
@@ -2435,7 +2438,7 @@
in
state
|> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
- "interpret" NONE after_qed' (map (pair ("", [])) (prep_propp propss))
+ "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
|> Element.refine_witness |> Seq.hd
end;
--- a/src/Pure/Isar/proof.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/proof.ML Tue Sep 02 14:10:45 2008 +0200
@@ -44,26 +44,30 @@
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: (string * string option * mixfix) list -> state -> state
- val fix_i: (string * typ option * mixfix) list -> state -> state
+ val fix: (Name.binding * string option * mixfix) list -> state -> state
+ val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
val assm: Assumption.export ->
- ((string * Attrib.src list) * (string * string list) list) list -> state -> state
+ ((Name.binding * Attrib.src list) * (string * string list) list) list -> state -> state
val assm_i: Assumption.export ->
- ((string * attribute list) * (term * term list) list) list -> state -> state
- val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
- val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
- val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
- val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
- val def: ((string * Attrib.src list) *
- ((string * mixfix) * (string * string list))) list -> state -> state
- val def_i: ((string * attribute list) *
- ((string * mixfix) * (term * term list))) list -> state -> state
+ ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
+ val assume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
+ state -> state
+ val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
+ state -> state
+ val presume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
+ state -> state
+ val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
+ state -> state
+ val def: ((Name.binding * Attrib.src list) *
+ ((Name.binding * mixfix) * (string * string list))) list -> state -> state
+ val def_i: ((Name.binding * attribute list) *
+ ((Name.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: ((string * Attrib.src list) *
+ val note_thmss: ((Name.binding * Attrib.src list) *
(Facts.ref * Attrib.src list) list) list -> state -> state
- val note_thmss_i: ((string * attribute list) *
+ val note_thmss_i: ((Name.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 +91,7 @@
(theory -> 'a -> attribute) ->
(context * 'b list -> context * (term list list * (context -> context))) ->
string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * 'a list) * 'b) list -> state -> state
+ ((Name.binding * 'a list) * 'b) list -> state -> state
val local_qed: Method.text option * bool -> state -> state Seq.seq
val theorem: Method.text option -> (thm list list -> context -> context) ->
(string * string list) list list -> context -> state
@@ -105,13 +109,13 @@
val global_done_proof: state -> context
val global_skip_proof: bool -> state -> context
val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
+ ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
+ ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
+ ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
+ ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
end;
structure Proof: PROOF =
@@ -610,7 +614,7 @@
(* note etc. *)
-fun no_binding args = map (pair ("", [])) args;
+fun no_binding args = map (pair (Name.no_binding, [])) args;
local
@@ -638,7 +642,7 @@
val local_results =
gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
-fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
+fun get_thmss state srcs = the_facts (note_thmss [((Name.no_binding, []), srcs)] state);
end;
@@ -682,14 +686,14 @@
val atts = map (prep_att (theory_of state)) raw_atts;
val (asms, state') = state |> map_context_result (fn ctxt =>
ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
- val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
+ val assumptions = asms |> map (fn (a, ts) => ((Name.binding a, atts), map (rpair []) ts));
in
state'
|> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
|> assume_i assumptions
|> add_binds_i AutoBind.no_facts
|> map_context (ProofContext.restore_naming (context_of state))
- |> `the_facts |-> (fn thms => note_thmss_i [((name, []), [(thms, [])])])
+ |> `the_facts |-> (fn thms => note_thmss_i [((Name.binding name, []), [(thms, [])])])
end;
in
--- a/src/Pure/Isar/rule_insts.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/rule_insts.ML Tue Sep 02 14:10:45 2008 +0200
@@ -284,7 +284,7 @@
val (param_names, ctxt') = ctxt
|> Variable.declare_thm thm
|> Thm.fold_terms Variable.declare_constraints st
- |> ProofContext.add_fixes_i (map (fn (x, T) => (x, SOME T, NoSyn)) params);
+ |> ProofContext.add_fixes_i (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) params);
(* Process type insts: Tinsts_env *)
fun absent xi = error
--- a/src/Pure/Isar/spec_parse.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/spec_parse.ML Tue Sep 02 14:10:45 2008 +0200
@@ -11,34 +11,34 @@
val attrib: OuterLex.token list -> Attrib.src * token list
val attribs: token list -> Attrib.src list * token list
val opt_attribs: token list -> Attrib.src list * token list
- val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
- val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
- val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
- val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
- val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
- val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
+ val thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
+ val opt_thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
+ val spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
+ val named_spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
+ val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
+ val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
val xthm: token list -> (Facts.ref * Attrib.src list) * token list
val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
val name_facts: token list ->
- ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
+ ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
val locale_mixfix: token list -> mixfix * token list
- val locale_fixes: token list -> (string * string option * mixfix) list * token list
+ val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list
val locale_insts: token list ->
- (string option list * ((bstring * Attrib.src list) * string) list) * token list
+ (string option list * ((Name.binding * Attrib.src list) * string) list) * token list
val class_expr: token list -> string list * token list
val locale_expr: token list -> Locale.expr * token list
val locale_keyword: token list -> string * token list
val locale_element: token list -> Element.context Locale.element * token list
val context_element: token list -> Element.context * token list
val statement: token list ->
- ((bstring * Attrib.src list) * (string * string list) list) list * token list
+ ((Name.binding * Attrib.src list) * (string * string list) list) list * token list
val general_statement: token list ->
(Element.context Locale.element list * Element.statement) * OuterLex.token list
val statement_keyword: token list -> string * token list
val specification: token list ->
- (string *
- (((bstring * Attrib.src list) * string list) list * (string * string option) list)) list *
- token list
+ (Name.binding *
+ (((Name.binding * Attrib.src list) * string list) list *
+ (Name.binding * string option) list)) list * token list
end;
structure SpecParse: SPEC_PARSE =
@@ -54,9 +54,11 @@
val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
val opt_attribs = Scan.optional attribs [];
-fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
+fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
+
fun opt_thm_name s =
- Scan.optional ((P.name -- opt_attribs || attribs >> pair "") --| P.$$$ s) ("", []);
+ Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s)
+ (Name.no_binding, []);
val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
@@ -79,7 +81,7 @@
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
val locale_fixes =
- P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
+ P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
>> (single o P.triple1) ||
P.params >> map Syntax.no_syn) >> flat;
@@ -134,7 +136,7 @@
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
val obtain_case =
- P.parname -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
+ P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
(P.and_list1 (Scan.repeat1 P.prop) >> flat));
val general_statement =
@@ -148,6 +150,6 @@
(* specifications *)
-val specification = P.enum1 "|" (P.parname -- (P.and_list1 spec -- P.for_simple_fixes));
+val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes));
end;
--- a/src/Pure/Isar/theory_target.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Isar/theory_target.ML Tue Sep 02 14:10:45 2008 +0200
@@ -48,8 +48,10 @@
let
val thy = ProofContext.theory_of ctxt;
val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
- val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
- val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
+ val fixes = map (fn (x, T) =>
+ (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
+ val assumes = map (fn A =>
+ ((Name.no_binding, []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
val elems =
(if null fixes then [] else [Element.Fixes fixes]) @
(if null assumes then [] else [Element.Assumes assumes]);
@@ -118,7 +120,7 @@
|> Drule.zero_var_indexes_list;
(*thm definition*)
- val result = PureThy.name_thm true true name th'';
+ val result = PureThy.name_thm true true Position.none name th'';
(*import fixes*)
val (tvars, vars) =
@@ -138,7 +140,7 @@
NONE => raise THM ("Failed to re-import result", 0, [result'])
| SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
|> Goal.norm_result
- |> PureThy.name_thm false false name;
+ |> PureThy.name_thm false false Position.none name;
in (result'', result) end;
@@ -154,7 +156,8 @@
val full = LocalTheory.full_name lthy;
val facts' = facts
- |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (full (fst a))) bs))
+ |> map (fn (a, bs) =>
+ (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs))
|> PureThy.map_facts (import_export_proof lthy);
val local_facts = PureThy.map_facts #1 facts'
|> Attrib.map_facts (Attrib.attribute_i thy);
@@ -185,11 +188,13 @@
let
val c' = Morphism.name phi c;
val rhs' = Morphism.term phi rhs;
- val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
- val arg = (c', Term.close_schematic_term rhs');
+ val name = Name.name_of c;
+ val name' = Name.name_of c'
+ val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
+ val arg = (name', Term.close_schematic_term rhs');
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
- val class_global = c' = NameSpace.qualified (Class.class_prefix target) c;
+ val class_global = name' = NameSpace.qualified (Class.class_prefix target) name;
in
not (is_class andalso (similar_body orelse class_global)) ?
(Context.mapping_result
@@ -201,8 +206,9 @@
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
end;
-fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
+fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
let
+ val c = Name.name_of b;
val tags = LocalTheory.group_position_of lthy;
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
val U = map #2 xs ---> T;
@@ -225,16 +231,17 @@
val t = Term.list_comb (const, map Free xs);
in
lthy'
- |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((c, mx2), t))
+ |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
|> is_class ? class_target ta (Class.declare target tags ((c, mx1), t))
- |> LocalDefs.add_def ((c, NoSyn), t)
+ |> LocalDefs.add_def ((b, NoSyn), t)
end;
(* abbrev *)
-fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
+fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
let
+ val c = Name.name_of b;
val tags = LocalTheory.group_position_of lthy;
val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
val target_ctxt = LocalTheory.target_of lthy;
@@ -251,7 +258,7 @@
LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs))
#-> (fn (lhs, _) =>
let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
- term_syntax ta (locale_const ta prmode tags ((c, mx2), lhs')) #>
+ term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
is_class ? class_target ta (Class.abbrev target prmode tags ((c, mx1), t'))
end)
else
@@ -259,26 +266,27 @@
(Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) =>
Sign.notation true prmode [(lhs, mx3)])))
|> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd
- |> LocalDefs.fixed_abbrev ((c, NoSyn), t)
+ |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
end;
(* define *)
fun define (ta as Target {target, is_locale, is_class, ...})
- kind ((c, mx), ((name, atts), rhs)) lthy =
+ kind ((b, mx), ((name, atts), rhs)) lthy =
let
val thy = ProofContext.theory_of lthy;
val thy_ctxt = ProofContext.init thy;
- val name' = Thm.def_name_optional c name;
+ val c = Name.name_of b;
+ val name' = Name.map_name (Thm.def_name_optional c) name;
val (rhs', rhs_conv) =
LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
val T = Term.fastype_of rhs;
(*const*)
- val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((c, T), mx);
+ val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((b, T), mx);
val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
(*def*)
@@ -291,7 +299,7 @@
then (fn name => fn eq => Thm.add_def false false (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 name' (lhs', rhs'));
+ |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
val def = LocalDefs.trans_terms lthy3
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
@@ -318,7 +326,7 @@
(*axioms*)
val hyps = map Thm.term_of (Assumption.assms_of lthy');
fun axiom ((name, atts), props) thy = thy
- |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
+ |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi (Name.name_of name) props)
|-> (fn ths => pair ((name, atts), [(ths, [])]));
in
lthy'
--- a/src/Pure/Tools/invoke.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/Tools/invoke.ML Tue Sep 02 14:10:45 2008 +0200
@@ -8,9 +8,9 @@
signature INVOKE =
sig
val invoke: string * Attrib.src list -> Locale.expr -> string option list ->
- (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+ (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
val invoke_i: string * attribute list -> Locale.expr -> term option list ->
- (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Invoke: INVOKE =
@@ -60,9 +60,9 @@
| NONE => Drule.termI)) params';
val propp =
- [(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
- (("", []), map (rpair [] o Logic.mk_term) params'),
- (("", []), map (rpair [] o Element.mark_witness) prems')];
+ [((Name.no_binding, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
+ ((Name.no_binding, []), map (rpair [] o Logic.mk_term) params'),
+ ((Name.no_binding, []), map (rpair [] o Element.mark_witness) prems')];
fun after_qed results =
Proof.end_block #>
Proof.map_context (fn ctxt =>
@@ -120,8 +120,8 @@
"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, expr), (insts, _)), fixes) =>
- Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
+ >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
+ Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes)));
end;
--- a/src/Pure/axclass.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Pure/axclass.ML Tue Sep 02 14:10:45 2008 +0200
@@ -9,7 +9,7 @@
signature AX_CLASS =
sig
val define_class: bstring * class list -> string list ->
- ((bstring * attribute list) * term list) list -> theory -> class * theory
+ ((Name.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
@@ -482,9 +482,10 @@
|> Sign.add_path bconst
|> Sign.no_base_names
|> PureThy.note_thmss ""
- [((introN, []), [([Drule.standard raw_intro], [])]),
- ((superN, []), [(map Drule.standard raw_classrel, [])]),
- ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
+ [((Name.binding introN, []), [([Drule.standard raw_intro], [])]),
+ ((Name.binding superN, []), [(map Drule.standard raw_classrel, [])]),
+ ((Name.binding axiomsN, []),
+ [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
||> Sign.restore_naming def_thy;
--- a/src/Tools/induct.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/Tools/induct.ML Tue Sep 02 14:10:45 2008 +0200
@@ -51,7 +51,7 @@
val setN: string
(*proof methods*)
val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
- val add_defs: (string option * term) option list -> Proof.context ->
+ val add_defs: (Name.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
@@ -63,7 +63,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 -> (string option * term) option list list ->
+ val induct_tac: Proof.context -> (Name.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 ->
@@ -552,7 +552,8 @@
fun add_defs def_insts =
let
fun add (SOME (SOME x, t)) ctxt =
- let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
+ let val ([(lhs, (_, th))], ctxt') =
+ LocalDefs.add_defs [((x, NoSyn), ((Name.no_binding, []), t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
| add NONE ctxt = ((NONE, []), ctxt);
@@ -716,7 +717,7 @@
val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
val def_inst =
- ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
+ ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
-- Args.term) >> SOME ||
inst >> Option.map (pair NONE);
--- a/src/ZF/Tools/datatype_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -262,7 +262,7 @@
||> add_recursor
||> Sign.parent_path
- val intr_names = map #2 (List.concat con_ty_lists);
+ val intr_names = map (Name.binding o #2) (List.concat con_ty_lists);
val (thy1, ind_result) =
thy0 |> Ind_Package.add_inductive_i
false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
--- a/src/ZF/Tools/ind_cases.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/ZF/Tools/ind_cases.ML Tue Sep 02 14:10:45 2008 +0200
@@ -8,7 +8,7 @@
signature IND_CASES =
sig
val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
- val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
+ val inductive_cases: ((Name.binding * Attrib.src list) * string list) list -> theory -> theory
val setup: theory -> theory
end;
--- a/src/ZF/Tools/inductive_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -29,10 +29,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 ->
- ((bstring * term) * attribute list) list ->
+ ((Name.binding * term) * attribute list) list ->
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
- ((bstring * string) * Attrib.src list) list ->
+ ((Name.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
@@ -62,11 +62,12 @@
(*internal version, accepting terms*)
fun add_inductive_i verbose (rec_tms, dom_sum)
- intr_specs (monos, con_defs, type_intrs, type_elims) thy =
+ raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
let
val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
val ctxt = ProofContext.init thy;
+ val intr_specs = map (apfst (apfst Name.name_of)) raw_intr_specs;
val (intr_names, intr_tms) = split_list (map fst intr_specs);
val case_names = RuleCases.case_names intr_names;
--- a/src/ZF/Tools/primrec_package.ML Tue Sep 02 14:10:32 2008 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Sep 02 14:10:45 2008 +0200
@@ -9,8 +9,8 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
- val add_primrec_i: ((bstring * term) * attribute list) list -> theory -> theory * thm list
+ val add_primrec: ((Name.binding * string) * Attrib.src list) list -> theory -> theory * thm list
+ val add_primrec_i: ((Name.binding * term) * attribute list) list -> theory -> theory * thm list
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -180,7 +180,7 @@
val (eqn_thms', thy2) =
thy1
- |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
+ |> PureThy.add_thms ((map Name.name_of eqn_names ~~ eqn_thms) ~~ eqn_atts);
val (_, thy3) =
thy2
|> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]