# HG changeset patch # User wenzelm # Date 1220357445 -7200 # Node ID 103d9282a946a5b4e85b8b28e3547c3040e9f382 # Parent 37350f3011282c234c715f73fca1f6272b5711b4 explicit type Name.binding for higher-specification elements; diff -r 37350f301128 -r 103d9282a946 src/HOL/Library/Eval.thy --- 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 diff -r 37350f301128 -r 103d9282a946 src/HOL/Library/RType.thy --- 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 diff -r 37350f301128 -r 103d9282a946 src/HOL/Nominal/nominal_atoms.ML --- 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_-type together with -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_-type together with -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 -combination a cp___inst theorem; *) diff -r 37350f301128 -r 103d9282a946 src/HOL/Nominal/nominal_induct.ML --- 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.$$$ "\" || Args.$$$ "==")) >> SOME) + ((Scan.lift (Args.binding --| (Args.$$$ "\" || Args.$$$ "==")) >> SOME) -- Args.term) >> SOME || inst >> Option.map (pair NONE); diff -r 37350f301128 -r 103d9282a946 src/HOL/Nominal/nominal_package.ML --- 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 **) diff -r 37350f301128 -r 103d9282a946 src/HOL/Nominal/nominal_primrec.ML --- 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)) => diff -r 37350f301128 -r 103d9282a946 src/HOL/Statespace/state_space.ML --- 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) @ diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/datatype_abs_proofs.ML --- 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 *) diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/datatype_codegen.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/datatype_rep_proofs.ML --- 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 ********************************) diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/function_package/fundef_common.ML --- 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, diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/function_package/fundef_core.ML --- 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 diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/function_package/fundef_lib.ML --- 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" diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/function_package/fundef_package.ML --- 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 diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/function_package/inductive_wrap.ML --- 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 diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/function_package/mutual.ML --- 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, diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/function_package/size.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/inductive_package.ML --- 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 -- diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/inductive_realizer.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/inductive_set_package.ML --- 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) = diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/primrec_package.ML --- 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]))); diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/recdef_package.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/specification_package.ML --- 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 diff -r 37350f301128 -r 103d9282a946 src/HOL/Tools/typecopy_package.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/HOL/Typedef.thy --- 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 diff -r 37350f301128 -r 103d9282a946 src/HOL/ex/Quickcheck.thy --- 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 diff -r 37350f301128 -r 103d9282a946 src/HOLCF/Tools/fixrec_package.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/HOLCF/Tools/pcpodef_package.ML --- 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 diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/attrib.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/class.ML --- 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 diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/constdefs.ML --- 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' = diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/isar_cmd.ML --- 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); diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/isar_syn.ML --- 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.$$$ "\\" || 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.$$$ "\\" || P.$$$ "==") |-- P.!!! P.termp))) + ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\" || P.$$$ "==") |-- P.!!! P.termp))) >> (Toplevel.print oo (Toplevel.proof o Proof.def))); val _ = diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/local_defs.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/local_theory.ML --- 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, diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/locale.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/proof.ML --- 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 diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/rule_insts.ML --- 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 diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/spec_parse.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/Pure/Isar/theory_target.ML --- 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' diff -r 37350f301128 -r 103d9282a946 src/Pure/Tools/invoke.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/Pure/axclass.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/Tools/induct.ML --- 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.$$$ "\" || Args.$$$ "==")) >> SOME) + ((Scan.lift (Args.binding --| (Args.$$$ "\" || Args.$$$ "==")) >> SOME) -- Args.term) >> SOME || inst >> Option.map (pair NONE); diff -r 37350f301128 -r 103d9282a946 src/ZF/Tools/datatype_package.ML --- 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)) diff -r 37350f301128 -r 103d9282a946 src/ZF/Tools/ind_cases.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/ZF/Tools/inductive_package.ML --- 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; diff -r 37350f301128 -r 103d9282a946 src/ZF/Tools/primrec_package.ML --- 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])]