1.1 --- a/src/HOL/Library/Eval.thy Tue Sep 02 14:10:32 2008 +0200
1.2 +++ b/src/HOL/Library/Eval.thy Tue Sep 02 14:10:45 2008 +0200
1.3 @@ -68,7 +68,7 @@
1.4 thy
1.5 |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
1.6 |> `(fn lthy => Syntax.check_term lthy eq)
1.7 - |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
1.8 + |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
1.9 |> snd
1.10 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
1.11 |> LocalTheory.exit
2.1 --- a/src/HOL/Library/RType.thy Tue Sep 02 14:10:32 2008 +0200
2.2 +++ b/src/HOL/Library/RType.thy Tue Sep 02 14:10:45 2008 +0200
2.3 @@ -67,7 +67,7 @@
2.4 thy
2.5 |> TheoryTarget.instantiation ([tyco], vs, @{sort rtype})
2.6 |> `(fn lthy => Syntax.check_term lthy eq)
2.7 - |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
2.8 + |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
2.9 |> snd
2.10 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
2.11 |> LocalTheory.exit
3.1 --- a/src/HOL/Nominal/nominal_atoms.ML Tue Sep 02 14:10:32 2008 +0200
3.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Tue Sep 02 14:10:45 2008 +0200
3.3 @@ -265,9 +265,9 @@
3.4 HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
3.5 in
3.6 AxClass.define_class (cl_name, ["HOL.type"]) []
3.7 - [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
3.8 - ((cl_name ^ "2", []), [axiom2]),
3.9 - ((cl_name ^ "3", []), [axiom3])] thy
3.10 + [((Name.binding (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
3.11 + ((Name.binding (cl_name ^ "2"), []), [axiom2]),
3.12 + ((Name.binding (cl_name ^ "3"), []), [axiom3])] thy
3.13 end) ak_names_types thy6;
3.14
3.15 (* proves that every pt_<ak>-type together with <ak>-type *)
3.16 @@ -313,7 +313,7 @@
3.17 val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
3.18
3.19 in
3.20 - AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy
3.21 + AxClass.define_class (cl_name, [pt_name]) [] [((Name.binding (cl_name ^ "1"), []), [axiom1])] thy
3.22 end) ak_names_types thy8;
3.23
3.24 (* proves that every fs_<ak>-type together with <ak>-type *)
3.25 @@ -362,7 +362,8 @@
3.26 (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
3.27 cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
3.28 in
3.29 - AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'
3.30 + AxClass.define_class (cl_name, ["HOL.type"]) []
3.31 + [((Name.binding (cl_name ^ "1"), []), [ax1])] thy'
3.32 end) ak_names_types thy) ak_names_types thy12;
3.33
3.34 (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem; *)
4.1 --- a/src/HOL/Nominal/nominal_induct.ML Tue Sep 02 14:10:32 2008 +0200
4.2 +++ b/src/HOL/Nominal/nominal_induct.ML Tue Sep 02 14:10:45 2008 +0200
4.3 @@ -6,7 +6,7 @@
4.4
4.5 structure NominalInduct:
4.6 sig
4.7 - val nominal_induct_tac: Proof.context -> (string option * term) option list list ->
4.8 + val nominal_induct_tac: Proof.context -> (Name.binding option * term) option list list ->
4.9 (string * typ) list -> (string * typ) list list -> thm list ->
4.10 thm list -> int -> RuleCases.cases_tactic
4.11 val nominal_induct_method: Method.src -> Proof.context -> Method.method
4.12 @@ -31,7 +31,6 @@
4.13
4.14 fun inst_mutual_rule ctxt insts avoiding rules =
4.15 let
4.16 -
4.17 val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
4.18 val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
4.19 val (cases, consumes) = RuleCases.get joined_rule;
4.20 @@ -132,7 +131,7 @@
4.21 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
4.22
4.23 val def_inst =
4.24 - ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
4.25 + ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
4.26 -- Args.term) >> SOME ||
4.27 inst >> Option.map (pair NONE);
4.28
5.1 --- a/src/HOL/Nominal/nominal_package.ML Tue Sep 02 14:10:32 2008 +0200
5.2 +++ b/src/HOL/Nominal/nominal_package.ML Tue Sep 02 14:10:45 2008 +0200
5.3 @@ -286,7 +286,7 @@
5.4 else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
5.5 end;
5.6 in
5.7 - (("", []), HOLogic.mk_Trueprop (HOLogic.mk_eq
5.8 + ((Name.no_binding, []), HOLogic.mk_Trueprop (HOLogic.mk_eq
5.9 (Free (nth perm_names_types' i) $
5.10 Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
5.11 list_comb (c, args),
5.12 @@ -298,7 +298,7 @@
5.13 PrimrecPackage.add_primrec_overloaded
5.14 (map (fn (s, sT) => (s, sT, false))
5.15 (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
5.16 - (map (fn s => (s, NONE, NoSyn)) perm_names') perm_eqs thy1;
5.17 + (map (fn s => (Name.binding s, NONE, NoSyn)) perm_names') perm_eqs thy1;
5.18
5.19 (**** prove that permutation functions introduced by unfolding are ****)
5.20 (**** equivalent to already existing permutation functions ****)
5.21 @@ -559,11 +559,11 @@
5.22 val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
5.23 InductivePackage.add_inductive_global (serial_string ())
5.24 {quiet_mode = false, verbose = false, kind = Thm.internalK,
5.25 - alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false,
5.26 + alt_name = Name.binding big_rep_name, coind = false, no_elim = true, no_ind = false,
5.27 skip_mono = true}
5.28 - (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
5.29 + (map (fn (s, T) => ((Name.binding s, T --> HOLogic.boolT), NoSyn))
5.30 (rep_set_names' ~~ recTs'))
5.31 - [] (map (fn x => (("", []), x)) intr_ts) [] thy3;
5.32 + [] (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy3;
5.33
5.34 (**** Prove that representing set is closed under permutation ****)
5.35
5.36 @@ -1476,11 +1476,11 @@
5.37 thy10 |>
5.38 InductivePackage.add_inductive_global (serial_string ())
5.39 {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
5.40 - alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false,
5.41 + alt_name = Name.binding big_rec_name, coind = false, no_elim = false, no_ind = false,
5.42 skip_mono = true}
5.43 - (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
5.44 + (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
5.45 (map dest_Free rec_fns)
5.46 - (map (fn x => (("", []), x)) rec_intr_ts) [] ||>
5.47 + (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] ||>
5.48 PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
5.49
5.50 (** equivariance **)
6.1 --- a/src/HOL/Nominal/nominal_primrec.ML Tue Sep 02 14:10:32 2008 +0200
6.2 +++ b/src/HOL/Nominal/nominal_primrec.ML Tue Sep 02 14:10:45 2008 +0200
6.3 @@ -9,13 +9,13 @@
6.4 signature NOMINAL_PRIMREC =
6.5 sig
6.6 val add_primrec: string -> string list option -> string option ->
6.7 - ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
6.8 + ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
6.9 val add_primrec_unchecked: string -> string list option -> string option ->
6.10 - ((bstring * string) * Attrib.src list) list -> theory -> Proof.state
6.11 + ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
6.12 val add_primrec_i: string -> term list option -> term option ->
6.13 - ((bstring * term) * attribute list) list -> theory -> Proof.state
6.14 + ((Name.binding * term) * attribute list) list -> theory -> Proof.state
6.15 val add_primrec_unchecked_i: string -> term list option -> term option ->
6.16 - ((bstring * term) * attribute list) list -> theory -> Proof.state
6.17 + ((Name.binding * term) * attribute list) list -> theory -> Proof.state
6.18 end;
6.19
6.20 structure NominalPrimrec : NOMINAL_PRIMREC =
6.21 @@ -229,7 +229,8 @@
6.22
6.23 fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
6.24 let
6.25 - val (eqns, atts) = split_list eqns_atts;
6.26 + val (raw_eqns, atts) = split_list eqns_atts;
6.27 + val eqns = map (apfst Name.name_of) raw_eqns;
6.28 val dt_info = NominalPackage.get_nominal_datatypes thy;
6.29 val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
6.30 val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
7.1 --- a/src/HOL/Statespace/state_space.ML Tue Sep 02 14:10:32 2008 +0200
7.2 +++ b/src/HOL/Statespace/state_space.ML Tue Sep 02 14:10:45 2008 +0200
7.3 @@ -61,7 +61,6 @@
7.4 val update_tr' : Proof.context -> term list -> term
7.5 end;
7.6
7.7 -
7.8 structure StateSpace: STATE_SPACE =
7.9 struct
7.10
7.11 @@ -303,7 +302,7 @@
7.12
7.13 val attr = Attrib.internal type_attr;
7.14
7.15 - val assumes = Element.Assumes [((dist_thm_name,[attr]),
7.16 + val assumes = Element.Assumes [((Name.binding dist_thm_name,[attr]),
7.17 [(HOLogic.Trueprop $
7.18 (Const ("DistinctTreeProver.all_distinct",
7.19 Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $
7.20 @@ -445,7 +444,7 @@
7.21 NONE => []
7.22 | SOME s =>
7.23 let
7.24 - val fx = Element.Fixes [(s,SOME (string_of_typ stateT),NoSyn)];
7.25 + val fx = Element.Fixes [(Name.binding s,SOME (string_of_typ stateT),NoSyn)];
7.26 val cs = Element.Constrains
7.27 (map (fn (n,T) => (n,string_of_typ T))
7.28 ((map (fn (n,_) => (n,nameT)) all_comps) @
8.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Sep 02 14:10:32 2008 +0200
8.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Sep 02 14:10:45 2008 +0200
8.3 @@ -156,11 +156,11 @@
8.4 val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
8.5 InductivePackage.add_inductive_global (serial_string ())
8.6 {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
8.7 - alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true,
8.8 + alt_name = Name.binding big_rec_name', coind = false, no_elim = false, no_ind = true,
8.9 skip_mono = true}
8.10 - (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
8.11 + (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
8.12 (map dest_Free rec_fns)
8.13 - (map (fn x => (("", []), x)) rec_intr_ts) [] thy0;
8.14 + (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] thy0;
8.15
8.16 (* prove uniqueness and termination of primrec combinators *)
8.17
9.1 --- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 02 14:10:32 2008 +0200
9.2 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 02 14:10:45 2008 +0200
9.3 @@ -442,7 +442,7 @@
9.4 (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
9.5 val def' = Syntax.check_term lthy def;
9.6 val ((_, (_, thm)), lthy') = Specification.definition
9.7 - (NONE, (("", []), def')) lthy;
9.8 + (NONE, ((Name.no_binding, []), def')) lthy;
9.9 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
9.10 val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
9.11 in (thm', lthy') end;
10.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 02 14:10:32 2008 +0200
10.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 02 14:10:45 2008 +0200
10.3 @@ -184,10 +184,10 @@
10.4 val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
10.5 InductivePackage.add_inductive_global (serial_string ())
10.6 {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
10.7 - alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false,
10.8 + alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
10.9 skip_mono = true}
10.10 - (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
10.11 - (map (fn x => (("", []), x)) intr_ts) [] thy1;
10.12 + (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
10.13 + (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy1;
10.14
10.15 (********************************* typedef ********************************)
10.16
11.1 --- a/src/HOL/Tools/function_package/fundef_common.ML Tue Sep 02 14:10:32 2008 +0200
11.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Sep 02 14:10:45 2008 +0200
11.3 @@ -66,7 +66,7 @@
11.4 psimps, pinducts, termination, defname}) phi =
11.5 let
11.6 val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
11.7 - val name = Morphism.name phi
11.8 + val name = Name.name_of o Morphism.name phi o Name.binding
11.9 in
11.10 FundefCtxData { add_simps = add_simps, case_names = case_names,
11.11 fs = map term fs, R = term R, psimps = fact psimps,
12.1 --- a/src/HOL/Tools/function_package/fundef_core.ML Tue Sep 02 14:10:32 2008 +0200
12.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML Tue Sep 02 14:10:45 2008 +0200
12.3 @@ -10,8 +10,8 @@
12.4 sig
12.5 val prepare_fundef : FundefCommon.fundef_config
12.6 -> string (* defname *)
12.7 - -> ((string * typ) * mixfix) list (* defined symbol *)
12.8 - -> ((string * typ) list * term list * term * term) list (* specification *)
12.9 + -> ((bstring * typ) * mixfix) list (* defined symbol *)
12.10 + -> ((bstring * typ) list * term list * term * term) list (* specification *)
12.11 -> local_theory
12.12
12.13 -> (term (* f *)
12.14 @@ -31,22 +31,22 @@
12.15 open FundefCommon
12.16
12.17 datatype globals =
12.18 - Globals of {
12.19 - fvar: term,
12.20 - domT: typ,
12.21 + Globals of {
12.22 + fvar: term,
12.23 + domT: typ,
12.24 ranT: typ,
12.25 - h: term,
12.26 - y: term,
12.27 - x: term,
12.28 - z: term,
12.29 - a: term,
12.30 - P: term,
12.31 - D: term,
12.32 + h: term,
12.33 + y: term,
12.34 + x: term,
12.35 + z: term,
12.36 + a: term,
12.37 + P: term,
12.38 + D: term,
12.39 Pbool:term
12.40 }
12.41
12.42
12.43 -datatype rec_call_info =
12.44 +datatype rec_call_info =
12.45 RCInfo of
12.46 {
12.47 RIvs: (string * typ) list, (* Call context: fixes and assumes *)
12.48 @@ -55,7 +55,7 @@
12.49
12.50 llRI: thm,
12.51 h_assum: term
12.52 - }
12.53 + }
12.54
12.55
12.56 datatype clause_context =
12.57 @@ -69,7 +69,7 @@
12.58 rhs: term,
12.59
12.60 cqs: cterm list,
12.61 - ags: thm list,
12.62 + ags: thm list,
12.63 case_hyp : thm
12.64 }
12.65
12.66 @@ -80,7 +80,7 @@
12.67
12.68
12.69 datatype clause_info =
12.70 - ClauseInfo of
12.71 + ClauseInfo of
12.72 {
12.73 no: int,
12.74 qglr : ((string * typ) list * term list * term * term),
12.75 @@ -166,16 +166,16 @@
12.76 val gs = map inst pre_gs
12.77 val lhs = inst pre_lhs
12.78 val rhs = inst pre_rhs
12.79 -
12.80 +
12.81 val cqs = map (cterm_of thy) qs
12.82 val ags = map (assume o cterm_of thy) gs
12.83 -
12.84 +
12.85 val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
12.86 in
12.87 - ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
12.88 + ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
12.89 cqs = cqs, ags = ags, case_hyp = case_hyp }
12.90 end
12.91 -
12.92 +
12.93
12.94 (* lowlevel term function *)
12.95 fun abstract_over_list vs body =
12.96 @@ -188,7 +188,7 @@
12.97 Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
12.98 | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
12.99 | _ => raise SAME);
12.100 - in
12.101 + in
12.102 fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
12.103 end
12.104
12.105 @@ -233,7 +233,7 @@
12.106 cdata=cdata,
12.107 qglr=qglr,
12.108
12.109 - lGI=lGI,
12.110 + lGI=lGI,
12.111 RCs=RC_infos,
12.112 tree=tree
12.113 }
12.114 @@ -260,11 +260,11 @@
12.115
12.116 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
12.117 (* if j < i, then turn around *)
12.118 -fun get_compat_thm thy cts i j ctxi ctxj =
12.119 +fun get_compat_thm thy cts i j ctxi ctxj =
12.120 let
12.121 val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
12.122 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
12.123 -
12.124 +
12.125 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
12.126 in if j < i then
12.127 let
12.128 @@ -324,14 +324,14 @@
12.129 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
12.130 val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
12.131
12.132 - val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
12.133 + val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
12.134 = mk_clause_context x ctxti cdescj
12.135
12.136 val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
12.137 val compat = get_compat_thm thy compat_store i j cctxi cctxj
12.138 val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
12.139
12.140 - val RLj_import =
12.141 + val RLj_import =
12.142 RLj |> fold forall_elim cqsj'
12.143 |> fold Thm.elim_implies agsj'
12.144 |> fold Thm.elim_implies Ghsj'
12.145 @@ -426,7 +426,7 @@
12.146 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
12.147
12.148 val _ = Output.debug (K "Proving cases for unique existence...")
12.149 - val (ex1s, values) =
12.150 + val (ex1s, values) =
12.151 split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
12.152
12.153 val _ = Output.debug (K "Proving: Graph is a function")
12.154 @@ -466,10 +466,10 @@
12.155 |> fold_rev (curry Logic.mk_implies) gs
12.156 |> fold_rev Logic.all (fvar :: qs)
12.157 end
12.158 -
12.159 +
12.160 val G_intros = map2 mk_GIntro clauses RCss
12.161 -
12.162 - val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
12.163 +
12.164 + val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
12.165 FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
12.166 in
12.167 ((G, GIntro_thms, G_elim, G_induct), lthy)
12.168 @@ -479,13 +479,13 @@
12.169
12.170 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
12.171 let
12.172 - val f_def =
12.173 + val f_def =
12.174 Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
12.175 Abs ("y", ranT, G $ Bound 1 $ Bound 0))
12.176 |> Syntax.check_term lthy
12.177
12.178 val ((f, (_, f_defthm)), lthy) =
12.179 - LocalTheory.define Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
12.180 + LocalTheory.define Thm.internalK ((Name.binding (function_name fname), mixfix), ((Name.binding fdefname, []), f_def)) lthy
12.181 in
12.182 ((f, f_defthm), lthy)
12.183 end
12.184 @@ -507,7 +507,7 @@
12.185
12.186 val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
12.187
12.188 - val (RIntro_thmss, (R, R_elim, _, lthy)) =
12.189 + val (RIntro_thmss, (R, R_elim, _, lthy)) =
12.190 fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
12.191 in
12.192 ((R, RIntro_thmss, R_elim), lthy)
12.193 @@ -516,7 +516,7 @@
12.194
12.195 fun fix_globals domT ranT fvar ctxt =
12.196 let
12.197 - val ([h, y, x, z, a, D, P, Pbool],ctxt') =
12.198 + val ([h, y, x, z, a, D, P, Pbool],ctxt') =
12.199 Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
12.200 in
12.201 (Globals {h = Free (h, domT --> ranT),
12.202 @@ -546,13 +546,13 @@
12.203
12.204
12.205 (**********************************************************
12.206 - * PROVING THE RULES
12.207 + * PROVING THE RULES
12.208 **********************************************************)
12.209
12.210 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
12.211 let
12.212 val Globals {domT, z, ...} = globals
12.213 -
12.214 +
12.215 fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
12.216 let
12.217 val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
12.218 @@ -563,7 +563,7 @@
12.219 |> implies_intr z_smaller
12.220 |> forall_intr (cterm_of thy z)
12.221 |> (fn it => it COMP valthm)
12.222 - |> implies_intr lhs_acc
12.223 + |> implies_intr lhs_acc
12.224 |> asm_simplify (HOL_basic_ss addsimps [f_iff])
12.225 |> fold_rev (implies_intr o cprop_of) ags
12.226 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
12.227 @@ -585,23 +585,23 @@
12.228 let
12.229 val Globals {domT, x, z, a, P, D, ...} = globals
12.230 val acc_R = mk_acc domT R
12.231 -
12.232 +
12.233 val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
12.234 val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
12.235 -
12.236 +
12.237 val D_subset = cterm_of thy (Logic.all x
12.238 (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
12.239 -
12.240 +
12.241 val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
12.242 Logic.all x
12.243 (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
12.244 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
12.245 HOLogic.mk_Trueprop (D $ z)))))
12.246 |> cterm_of thy
12.247 -
12.248 -
12.249 +
12.250 +
12.251 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
12.252 - val ihyp = Term.all domT $ Abs ("z", domT,
12.253 + val ihyp = Term.all domT $ Abs ("z", domT,
12.254 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
12.255 HOLogic.mk_Trueprop (P $ Bound 0)))
12.256 |> cterm_of thy
12.257 @@ -610,36 +610,36 @@
12.258
12.259 fun prove_case clause =
12.260 let
12.261 - val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
12.262 + val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
12.263 qglr = (oqs, _, _, _), ...} = clause
12.264 -
12.265 +
12.266 val case_hyp_conv = K (case_hyp RS eq_reflection)
12.267 - local open Conv in
12.268 + local open Conv in
12.269 val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
12.270 val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
12.271 end
12.272 -
12.273 +
12.274 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
12.275 sih |> forall_elim (cterm_of thy rcarg)
12.276 |> Thm.elim_implies llRI
12.277 |> fold_rev (implies_intr o cprop_of) CCas
12.278 |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
12.279 -
12.280 +
12.281 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
12.282 -
12.283 +
12.284 val step = HOLogic.mk_Trueprop (P $ lhs)
12.285 |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
12.286 |> fold_rev (curry Logic.mk_implies) gs
12.287 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
12.288 |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
12.289 |> cterm_of thy
12.290 -
12.291 +
12.292 val P_lhs = assume step
12.293 |> fold forall_elim cqs
12.294 - |> Thm.elim_implies lhs_D
12.295 + |> Thm.elim_implies lhs_D
12.296 |> fold Thm.elim_implies ags
12.297 |> fold Thm.elim_implies P_recs
12.298 -
12.299 +
12.300 val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
12.301 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
12.302 |> symmetric (* P lhs == P x *)
12.303 @@ -650,17 +650,17 @@
12.304 in
12.305 (res, step)
12.306 end
12.307 -
12.308 +
12.309 val (cases, steps) = split_list (map prove_case clauses)
12.310 -
12.311 +
12.312 val istep = complete_thm
12.313 |> Thm.forall_elim_vars 0
12.314 |> fold (curry op COMP) cases (* P x *)
12.315 |> implies_intr ihyp
12.316 |> implies_intr (cprop_of x_D)
12.317 |> forall_intr (cterm_of thy x)
12.318 -
12.319 - val subset_induct_rule =
12.320 +
12.321 + val subset_induct_rule =
12.322 acc_subset_induct
12.323 |> (curry op COMP) (assume D_subset)
12.324 |> (curry op COMP) (assume D_dcl)
12.325 @@ -694,13 +694,13 @@
12.326 (* FIXME: This should probably use fixed goals, to be more reliable and faster *)
12.327 fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
12.328 let
12.329 - val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
12.330 + val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
12.331 qglr = (oqs, _, _, _), ...} = clause
12.332 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
12.333 |> fold_rev (curry Logic.mk_implies) gs
12.334 |> cterm_of thy
12.335 in
12.336 - Goal.init goal
12.337 + Goal.init goal
12.338 |> (SINGLE (resolve_tac [accI] 1)) |> the
12.339 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
12.340 |> (SINGLE (CLASIMPSET auto_tac)) |> the
12.341 @@ -721,26 +721,26 @@
12.342 val Globals {x, z, ...} = globals
12.343 val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
12.344 qglr=(oqs, _, _, _), ...} = clause
12.345 -
12.346 +
12.347 val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
12.348 -
12.349 - fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
12.350 +
12.351 + fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
12.352 let
12.353 val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub)
12.354 -
12.355 +
12.356 val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
12.357 |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
12.358 - |> FundefCtxTree.export_term (fixes, assumes)
12.359 + |> FundefCtxTree.export_term (fixes, assumes)
12.360 |> fold_rev (curry Logic.mk_implies o prop_of) ags
12.361 |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
12.362 |> cterm_of thy
12.363 -
12.364 +
12.365 val thm = assume hyp
12.366 |> fold forall_elim cqs
12.367 |> fold Thm.elim_implies ags
12.368 |> FundefCtxTree.import_thm thy (fixes, assumes)
12.369 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
12.370 -
12.371 +
12.372 val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
12.373
12.374 val acc = thm COMP ih_case
12.375 @@ -748,7 +748,7 @@
12.376 |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
12.377
12.378 val ethm = z_acc_local
12.379 - |> FundefCtxTree.export_thm thy (fixes,
12.380 + |> FundefCtxTree.export_thm thy (fixes,
12.381 z_eq_arg :: case_hyp :: ags @ assumes)
12.382 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
12.383
12.384 @@ -766,24 +766,24 @@
12.385 let
12.386 val Globals { domT, x, z, ... } = globals
12.387 val acc_R = mk_acc domT R
12.388 -
12.389 +
12.390 val R' = Free ("R", fastype_of R)
12.391 -
12.392 +
12.393 val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
12.394 val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
12.395 -
12.396 +
12.397 val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
12.398 -
12.399 +
12.400 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
12.401 - val ihyp = Term.all domT $ Abs ("z", domT,
12.402 + val ihyp = Term.all domT $ Abs ("z", domT,
12.403 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
12.404 HOLogic.mk_Trueprop (acc_R $ Bound 0)))
12.405 |> cterm_of thy
12.406
12.407 val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
12.408 -
12.409 - val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
12.410 -
12.411 +
12.412 + val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
12.413 +
12.414 val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
12.415 in
12.416 R_cases
12.417 @@ -809,7 +809,7 @@
12.418 |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
12.419 |> forall_intr (cterm_of thy Rrel)
12.420 end
12.421 -
12.422 +
12.423
12.424
12.425 (* Tail recursion (probably very fragile)
12.426 @@ -828,7 +828,7 @@
12.427 val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
12.428 Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
12.429 (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
12.430 - (fn {prems=[a], ...} =>
12.431 + (fn {prems=[a], ...} =>
12.432 ((rtac (G_induct OF [a]))
12.433 THEN_ALL_NEW (rtac accI)
12.434 THEN_ALL_NEW (etac R_cases)
12.435 @@ -841,13 +841,13 @@
12.436 val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
12.437 val thy = ProofContext.theory_of ctxt
12.438 val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
12.439 -
12.440 +
12.441 val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
12.442 val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
12.443 fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
12.444 in
12.445 Goal.prove ctxt [] [] trsimp
12.446 - (fn _ =>
12.447 + (fn _ =>
12.448 rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
12.449 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
12.450 THEN (SIMPSET' simp_default_tac 1)
12.451 @@ -862,12 +862,12 @@
12.452
12.453 fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
12.454 let
12.455 - val FundefConfig {domintros, tailrec, default=default_str, ...} = config
12.456 -
12.457 + val FundefConfig {domintros, tailrec, default=default_str, ...} = config
12.458 +
12.459 val fvar = Free (fname, fT)
12.460 val domT = domain_type fT
12.461 val ranT = range_type fT
12.462 -
12.463 +
12.464 val default = Syntax.parse_term lthy default_str
12.465 |> TypeInfer.constrain fT |> Syntax.check_term lthy
12.466
12.467 @@ -875,30 +875,30 @@
12.468
12.469 val Globals { x, h, ... } = globals
12.470
12.471 - val clauses = map (mk_clause_context x ctxt') abstract_qglrs
12.472 + val clauses = map (mk_clause_context x ctxt') abstract_qglrs
12.473
12.474 val n = length abstract_qglrs
12.475
12.476 - fun build_tree (ClauseContext { ctxt, rhs, ...}) =
12.477 + fun build_tree (ClauseContext { ctxt, rhs, ...}) =
12.478 FundefCtxTree.mk_tree (fname, fT) h ctxt rhs
12.479
12.480 val trees = map build_tree clauses
12.481 val RCss = map find_calls trees
12.482
12.483 - val ((G, GIntro_thms, G_elim, G_induct), lthy) =
12.484 + val ((G, GIntro_thms, G_elim, G_induct), lthy) =
12.485 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
12.486
12.487 - val ((f, f_defthm), lthy) =
12.488 + val ((f, f_defthm), lthy) =
12.489 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
12.490
12.491 val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
12.492 val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
12.493
12.494 - val ((R, RIntro_thmss, R_elim), lthy) =
12.495 + val ((R, RIntro_thmss, R_elim), lthy) =
12.496 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
12.497
12.498 - val (_, lthy) =
12.499 - LocalTheory.abbrev Syntax.mode_default ((dom_name defname, NoSyn), mk_acc domT R) lthy
12.500 + val (_, lthy) =
12.501 + LocalTheory.abbrev Syntax.mode_default ((Name.binding (dom_name defname), NoSyn), mk_acc domT R) lthy
12.502
12.503 val newthy = ProofContext.theory_of lthy
12.504 val clauses = map (transfer_clause_ctx newthy) clauses
12.505 @@ -918,31 +918,31 @@
12.506
12.507 fun mk_partial_rules provedgoal =
12.508 let
12.509 - val newthy = theory_of_thm provedgoal (*FIXME*)
12.510 + val newthy = theory_of_thm provedgoal (*FIXME*)
12.511
12.512 - val (graph_is_function, complete_thm) =
12.513 + val (graph_is_function, complete_thm) =
12.514 provedgoal
12.515 |> Conjunction.elim
12.516 |> apfst (Thm.forall_elim_vars 0)
12.517 -
12.518 +
12.519 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
12.520 -
12.521 +
12.522 val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
12.523 -
12.524 - val simple_pinduct = PROFILE "Proving partial induction rule"
12.525 +
12.526 + val simple_pinduct = PROFILE "Proving partial induction rule"
12.527 (mk_partial_induct_rule newthy globals R complete_thm) xclauses
12.528 -
12.529 -
12.530 +
12.531 +
12.532 val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
12.533 -
12.534 - val dom_intros = if domintros
12.535 +
12.536 + val dom_intros = if domintros
12.537 then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
12.538 else NONE
12.539 val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
12.540 -
12.541 - in
12.542 - FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
12.543 - psimps=psimps, simple_pinducts=[simple_pinduct],
12.544 +
12.545 + in
12.546 + FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
12.547 + psimps=psimps, simple_pinducts=[simple_pinduct],
12.548 termination=total_intro, trsimps=trsimps,
12.549 domintros=dom_intros}
12.550 end
12.551 @@ -951,6 +951,4 @@
12.552 end
12.553
12.554
12.555 -
12.556 -
12.557 end
13.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML Tue Sep 02 14:10:32 2008 +0200
13.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Tue Sep 02 14:10:45 2008 +0200
13.3 @@ -56,7 +56,7 @@
13.4 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
13.5 let
13.6 val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
13.7 - val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
13.8 + val (_, ctx') = ProofContext.add_fixes_i [(Name.binding n', SOME T, NoSyn)] ctx
13.9
13.10 val (n'', body) = Term.dest_abs (n', T, b)
13.11 val _ = (n' = n'') orelse error "dest_all_ctx"
14.1 --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 02 14:10:32 2008 +0200
14.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 02 14:10:45 2008 +0200
14.3 @@ -9,15 +9,15 @@
14.4
14.5 signature FUNDEF_PACKAGE =
14.6 sig
14.7 - val add_fundef : (string * string option * mixfix) list
14.8 - -> ((bstring * Attrib.src list) * string) list
14.9 + val add_fundef : (Name.binding * string option * mixfix) list
14.10 + -> ((Name.binding * Attrib.src list) * string) list
14.11 -> FundefCommon.fundef_config
14.12 -> bool list
14.13 -> local_theory
14.14 -> Proof.state
14.15
14.16 - val add_fundef_i: (string * typ option * mixfix) list
14.17 - -> ((bstring * Attrib.src list) * term) list
14.18 + val add_fundef_i: (Name.binding * typ option * mixfix) list
14.19 + -> ((Name.binding * Attrib.src list) * term) list
14.20 -> FundefCommon.fundef_config
14.21 -> bool list
14.22 -> local_theory
14.23 @@ -36,7 +36,7 @@
14.24 open FundefLib
14.25 open FundefCommon
14.26
14.27 -val note_theorem = LocalTheory.note Thm.theoremK
14.28 +fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Name.binding name, atts), ths)
14.29
14.30 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
14.31
14.32 @@ -95,7 +95,9 @@
14.33
14.34 fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
14.35 let
14.36 - val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
14.37 + val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
14.38 + val fixes = map (apfst (apfst Name.name_of)) fixes0;
14.39 + val spec = map (apfst (apfst Name.name_of)) spec0;
14.40 val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
14.41
14.42 val defname = mk_defname fixes
14.43 @@ -145,10 +147,10 @@
14.44 val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
14.45 in
14.46 lthy
14.47 - |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd
14.48 - |> ProofContext.note_thmss_i "" [(("", [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
14.49 + |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.rule_del]), [([allI], [])])] |> snd
14.50 + |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
14.51 |> ProofContext.note_thmss_i ""
14.52 - [(("termination", [ContextRules.intro_bang (SOME 0)]),
14.53 + [((Name.binding "termination", [ContextRules.intro_bang (SOME 0)]),
14.54 [([Goal.norm_result termination], [])])] |> snd
14.55 |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
14.56 end
15.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML Tue Sep 02 14:10:32 2008 +0200
15.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML Tue Sep 02 14:10:45 2008 +0200
15.3 @@ -14,7 +14,7 @@
15.4 -> thm list * (term * thm * thm * local_theory)
15.5 end
15.6
15.7 -structure FundefInductiveWrap =
15.8 +structure FundefInductiveWrap: FUNDEF_INDUCTIVE_WRAP =
15.9 struct
15.10
15.11 open FundefLib
15.12 @@ -44,14 +44,14 @@
15.13 {quiet_mode = false,
15.14 verbose = ! Toplevel.debug,
15.15 kind = Thm.internalK,
15.16 - alt_name = "",
15.17 + alt_name = Name.no_binding,
15.18 coind = false,
15.19 no_elim = false,
15.20 no_ind = false,
15.21 skip_mono = true}
15.22 - [((R, T), NoSyn)] (* the relation *)
15.23 + [((Name.binding R, T), NoSyn)] (* the relation *)
15.24 [] (* no parameters *)
15.25 - (map (fn t => (("", []), t)) defs) (* the intros *)
15.26 + (map (fn t => ((Name.no_binding, []), t)) defs) (* the intros *)
15.27 [] (* no special monos *)
15.28 lthy
15.29
16.1 --- a/src/HOL/Tools/function_package/mutual.ML Tue Sep 02 14:10:32 2008 +0200
16.2 +++ b/src/HOL/Tools/function_package/mutual.ML Tue Sep 02 14:10:45 2008 +0200
16.3 @@ -150,8 +150,8 @@
16.4 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
16.5 let
16.6 val ((f, (_, f_defthm)), lthy') =
16.7 - LocalTheory.define Thm.internalK ((fname, mixfix),
16.8 - ((fname ^ "_def", []), Term.subst_bound (fsum, f_def)))
16.9 + LocalTheory.define Thm.internalK ((Name.binding fname, mixfix),
16.10 + ((Name.binding (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
16.11 lthy
16.12 in
16.13 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
17.1 --- a/src/HOL/Tools/function_package/size.ML Tue Sep 02 14:10:32 2008 +0200
17.2 +++ b/src/HOL/Tools/function_package/size.ML Tue Sep 02 14:10:45 2008 +0200
17.3 @@ -132,8 +132,8 @@
17.4 fun define_overloaded (def_name, eq) lthy =
17.5 let
17.6 val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
17.7 - val ((_, (_, thm)), lthy') = lthy
17.8 - |> LocalTheory.define Thm.definitionK ((c, NoSyn), ((def_name, []), rhs));
17.9 + val ((_, (_, thm)), lthy') = lthy |> LocalTheory.define Thm.definitionK
17.10 + ((Name.binding c, NoSyn), ((Name.binding def_name, []), rhs));
17.11 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
17.12 val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
17.13 in (thm', lthy') end;
18.1 --- a/src/HOL/Tools/inductive_package.ML Tue Sep 02 14:10:32 2008 +0200
18.2 +++ b/src/HOL/Tools/inductive_package.ML Tue Sep 02 14:10:45 2008 +0200
18.3 @@ -33,22 +33,25 @@
18.4 val inductive_forall_name: string
18.5 val inductive_forall_def: thm
18.6 val rulify: thm -> thm
18.7 - val inductive_cases: ((bstring * Attrib.src list) * string list) list ->
18.8 + val inductive_cases: ((Name.binding * Attrib.src list) * string list) list ->
18.9 Proof.context -> thm list list * local_theory
18.10 - val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
18.11 + val inductive_cases_i: ((Name.binding * Attrib.src list) * term list) list ->
18.12 Proof.context -> thm list list * local_theory
18.13 type inductive_flags
18.14 val add_inductive_i:
18.15 - inductive_flags -> ((string * typ) * mixfix) list ->
18.16 - (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
18.17 + inductive_flags -> ((Name.binding * typ) * mixfix) list ->
18.18 + (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
18.19 local_theory -> inductive_result * local_theory
18.20 - val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
18.21 - (string * string option * mixfix) list ->
18.22 - ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
18.23 + val add_inductive: bool -> bool ->
18.24 + (Name.binding * string option * mixfix) list ->
18.25 + (Name.binding * string option * mixfix) list ->
18.26 + ((Name.binding * Attrib.src list) * string) list ->
18.27 + (Facts.ref * Attrib.src list) list ->
18.28 local_theory -> inductive_result * local_theory
18.29 val add_inductive_global: string -> inductive_flags ->
18.30 - ((string * typ) * mixfix) list -> (string * typ) list ->
18.31 - ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
18.32 + ((Name.binding * typ) * mixfix) list ->
18.33 + (string * typ) list ->
18.34 + ((Name.binding * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
18.35 val arities_of: thm -> (string * int) list
18.36 val params_of: thm -> term list
18.37 val partition_rules: thm -> thm list -> (string * thm list) list
18.38 @@ -62,18 +65,19 @@
18.39 sig
18.40 include BASIC_INDUCTIVE_PACKAGE
18.41 type add_ind_def
18.42 - val declare_rules: string -> bstring -> bool -> bool -> string list ->
18.43 - thm list -> bstring list -> Attrib.src list list -> (thm * string list) list ->
18.44 + val declare_rules: string -> Name.binding -> bool -> bool -> string list ->
18.45 + thm list -> Name.binding list -> Attrib.src list list -> (thm * string list) list ->
18.46 thm -> local_theory -> thm list * thm list * thm * local_theory
18.47 val add_ind_def: add_ind_def
18.48 - val gen_add_inductive_i: add_ind_def ->
18.49 - inductive_flags -> ((string * typ) * mixfix) list ->
18.50 - (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
18.51 - local_theory -> inductive_result * local_theory
18.52 - val gen_add_inductive: add_ind_def ->
18.53 - bool -> bool -> (string * string option * mixfix) list ->
18.54 - (string * string option * mixfix) list ->
18.55 - ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
18.56 + val gen_add_inductive_i: add_ind_def -> inductive_flags ->
18.57 + ((Name.binding * typ) * mixfix) list ->
18.58 + (string * typ) list ->
18.59 + ((Name.binding * Attrib.src list) * term) list -> thm list ->
18.60 + local_theory -> inductive_result * local_theory
18.61 + val gen_add_inductive: add_ind_def -> bool -> bool ->
18.62 + (Name.binding * string option * mixfix) list ->
18.63 + (Name.binding * string option * mixfix) list ->
18.64 + ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
18.65 local_theory -> inductive_result * local_theory
18.66 val gen_ind_decl: add_ind_def -> bool ->
18.67 OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
18.68 @@ -258,8 +262,9 @@
18.69
18.70 in
18.71
18.72 -fun check_rule ctxt cs params ((name, att), rule) =
18.73 +fun check_rule ctxt cs params ((binding, att), rule) =
18.74 let
18.75 + val name = Name.name_of binding;
18.76 val params' = Term.variant_frees rule (Logic.strip_params rule);
18.77 val frees = rev (map Free params');
18.78 val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
18.79 @@ -294,7 +299,7 @@
18.80 List.app check_prem (prems ~~ aprems))
18.81 else err_in_rule ctxt name rule' bad_concl
18.82 | _ => err_in_rule ctxt name rule' bad_concl);
18.83 - ((name, att), arule)
18.84 + ((binding, att), arule)
18.85 end;
18.86
18.87 val rulify =
18.88 @@ -635,13 +640,15 @@
18.89
18.90 (* add definiton of recursive predicates to theory *)
18.91
18.92 - val rec_name = if alt_name = "" then
18.93 - space_implode "_" (map fst cnames_syn) else alt_name;
18.94 + val rec_name =
18.95 + if Name.name_of alt_name = "" then
18.96 + Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
18.97 + else alt_name;
18.98
18.99 val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
18.100 LocalTheory.define Thm.internalK
18.101 ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
18.102 - (("", []), fold_rev lambda params
18.103 + ((Name.no_binding, []), fold_rev lambda params
18.104 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
18.105 val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
18.106 (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
18.107 @@ -652,7 +659,7 @@
18.108 val xs = map Free (Variable.variant_frees ctxt intr_ts
18.109 (mk_names "x" (length Ts) ~~ Ts))
18.110 in
18.111 - (name_mx, (("", []), fold_rev lambda (params @ xs)
18.112 + (name_mx, ((Name.no_binding, []), fold_rev lambda (params @ xs)
18.113 (list_comb (rec_const, params @ make_bool_args' bs i @
18.114 make_args argTs (xs ~~ Ts)))))
18.115 end) (cnames_syn ~~ cs);
18.116 @@ -665,9 +672,12 @@
18.117 list_comb (rec_const, params), preds, argTs, bs, xs)
18.118 end;
18.119
18.120 -fun declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts
18.121 +fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
18.122 elims raw_induct ctxt =
18.123 let
18.124 + val rec_name = Name.name_of rec_binding;
18.125 + val rec_qualified = NameSpace.qualified rec_name;
18.126 + val intr_names = map Name.name_of intr_bindings;
18.127 val ind_case_names = RuleCases.case_names intr_names;
18.128 val induct =
18.129 if coind then
18.130 @@ -681,28 +691,28 @@
18.131 val (intrs', ctxt1) =
18.132 ctxt |>
18.133 LocalTheory.notes kind
18.134 - (map (NameSpace.qualified rec_name) intr_names ~~
18.135 + (map (Name.map_name rec_qualified) intr_bindings ~~
18.136 intr_atts ~~ map (fn th => [([th],
18.137 [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
18.138 map (hd o snd);
18.139 val (((_, elims'), (_, [induct'])), ctxt2) =
18.140 ctxt1 |>
18.141 - LocalTheory.note kind ((NameSpace.qualified rec_name "intros", []), intrs') ||>>
18.142 + LocalTheory.note kind ((Name.binding (rec_qualified "intros"), []), intrs') ||>>
18.143 fold_map (fn (name, (elim, cases)) =>
18.144 - LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
18.145 + LocalTheory.note kind ((Name.binding (NameSpace.qualified (Sign.base_name name) "cases"),
18.146 [Attrib.internal (K (RuleCases.case_names cases)),
18.147 Attrib.internal (K (RuleCases.consumes 1)),
18.148 Attrib.internal (K (Induct.cases_pred name)),
18.149 Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
18.150 apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
18.151 - LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
18.152 + LocalTheory.note kind ((Name.binding (rec_qualified (coind_prefix coind ^ "induct")),
18.153 map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
18.154
18.155 val ctxt3 = if no_ind orelse coind then ctxt2 else
18.156 let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
18.157 in
18.158 ctxt2 |>
18.159 - LocalTheory.notes kind [((NameSpace.qualified rec_name "inducts", []),
18.160 + LocalTheory.notes kind [((Name.binding (rec_qualified "inducts"), []),
18.161 inducts |> map (fn (name, th) => ([th],
18.162 [Attrib.internal (K ind_case_names),
18.163 Attrib.internal (K (RuleCases.consumes 1)),
18.164 @@ -711,24 +721,25 @@
18.165 in (intrs', elims', induct', ctxt3) end;
18.166
18.167 type inductive_flags =
18.168 - {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
18.169 + {quiet_mode: bool, verbose: bool, kind: string, alt_name: Name.binding,
18.170 coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
18.171
18.172 type add_ind_def =
18.173 inductive_flags ->
18.174 - term list -> ((string * Attrib.src list) * term) list -> thm list ->
18.175 - term list -> (string * mixfix) list ->
18.176 + term list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
18.177 + term list -> (Name.binding * mixfix) list ->
18.178 local_theory -> inductive_result * local_theory
18.179
18.180 -fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
18.181 +fun (add_ind_def: add_ind_def)
18.182 + {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
18.183 cs intros monos params cnames_syn ctxt =
18.184 let
18.185 val _ = null cnames_syn andalso error "No inductive predicates given";
18.186 + val names = map (Name.name_of o fst) cnames_syn;
18.187 val _ = message (quiet_mode andalso not verbose)
18.188 - ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
18.189 - commas_quote (map fst cnames_syn));
18.190 + ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
18.191
18.192 - val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; (* FIXME *)
18.193 + val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn; (* FIXME *)
18.194 val ((intr_names, intr_atts), intr_ts) =
18.195 apfst split_list (split_list (map (check_rule ctxt cs params) intros));
18.196
18.197 @@ -739,7 +750,8 @@
18.198 val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
18.199 params intr_ts rec_preds_defs ctxt1;
18.200 val elims = if no_elim then [] else
18.201 - prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt1;
18.202 + prove_elims quiet_mode cs params intr_ts (map Name.name_of intr_names)
18.203 + unfold rec_preds_defs ctxt1;
18.204 val raw_induct = zero_var_indexes
18.205 (if no_ind then Drule.asm_rl else
18.206 if coind then
18.207 @@ -755,7 +767,6 @@
18.208 val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
18.209 cnames intrs intr_names intr_atts elims raw_induct ctxt1;
18.210
18.211 - val names = map #1 cnames_syn;
18.212 val result =
18.213 {preds = preds,
18.214 intrs = intrs',
18.215 @@ -782,35 +793,35 @@
18.216
18.217 (* abbrevs *)
18.218
18.219 - val (_, ctxt1) = Variable.add_fixes (map (fst o fst) cnames_syn) lthy;
18.220 + val (_, ctxt1) = Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn) lthy;
18.221
18.222 fun get_abbrev ((name, atts), t) =
18.223 if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
18.224 let
18.225 - val _ = name = "" andalso null atts orelse
18.226 + val _ = Name.name_of name = "" andalso null atts orelse
18.227 error "Abbreviations may not have names or attributes";
18.228 val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
18.229 - val mx =
18.230 - (case find_first (fn ((c, _), _) => c = x) cnames_syn of
18.231 + val var =
18.232 + (case find_first (fn ((c, _), _) => Name.name_of c = x) cnames_syn of
18.233 NONE => error ("Undeclared head of abbreviation " ^ quote x)
18.234 - | SOME ((_, T'), mx) =>
18.235 + | SOME ((b, T'), mx) =>
18.236 if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
18.237 - else mx);
18.238 - in SOME ((x, mx), rhs) end
18.239 + else (b, mx));
18.240 + in SOME (var, rhs) end
18.241 else NONE;
18.242
18.243 val abbrevs = map_filter get_abbrev spec;
18.244 - val bs = map (fst o fst) abbrevs;
18.245 + val bs = map (Name.name_of o fst o fst) abbrevs;
18.246
18.247
18.248 (* predicates *)
18.249
18.250 val pre_intros = filter_out (is_some o get_abbrev) spec;
18.251 - val cnames_syn' = filter_out (member (op =) bs o fst o fst) cnames_syn;
18.252 - val cs = map (Free o fst) cnames_syn';
18.253 + val cnames_syn' = filter_out (member (op =) bs o Name.name_of o fst o fst) cnames_syn;
18.254 + val cs = map (Free o apfst Name.name_of o fst) cnames_syn';
18.255 val ps = map Free pnames;
18.256
18.257 - val (_, ctxt2) = lthy |> Variable.add_fixes (map (fst o fst) cnames_syn');
18.258 + val (_, ctxt2) = lthy |> Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn');
18.259 val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
18.260 val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
18.261 val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
18.262 @@ -837,12 +848,12 @@
18.263 val (cs, ps) = chop (length cnames_syn) vars;
18.264 val intrs = map (apsnd the_single) specs;
18.265 val monos = Attrib.eval_thms lthy raw_monos;
18.266 - val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK, alt_name = "",
18.267 - coind = coind, no_elim = false, no_ind = false, skip_mono = false};
18.268 + val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
18.269 + alt_name = Name.no_binding, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
18.270 in
18.271 lthy
18.272 |> LocalTheory.set_group (serial_string ())
18.273 - |> gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos
18.274 + |> gen_add_inductive_i mk_def flags cs (map (apfst Name.name_of o fst) ps) intrs monos
18.275 end;
18.276
18.277 val add_inductive_i = gen_add_inductive_i add_ind_def;
18.278 @@ -850,7 +861,7 @@
18.279
18.280 fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
18.281 let
18.282 - val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
18.283 + val name = Sign.full_name thy (Name.name_of (fst (fst (hd cnames_syn))));
18.284 val ctxt' = thy
18.285 |> TheoryTarget.init NONE
18.286 |> LocalTheory.set_group group
18.287 @@ -934,14 +945,15 @@
18.288
18.289 val _ = OuterKeyword.keyword "monos";
18.290
18.291 +(* FIXME eliminate *)
18.292 fun flatten_specification specs = specs |> maps
18.293 (fn (a, (concl, [])) => concl |> map
18.294 (fn ((b, atts), [B]) =>
18.295 - if a = "" then ((b, atts), B)
18.296 - else if b = "" then ((a, atts), B)
18.297 - else error ("Illegal nested case names " ^ quote (NameSpace.append a b))
18.298 - | ((b, _), _) => error ("Illegal simultaneous specification " ^ quote b))
18.299 - | (a, _) => error ("Illegal local specification parameters for " ^ quote a));
18.300 + if Name.name_of a = "" then ((b, atts), B)
18.301 + else if Name.name_of b = "" then ((a, atts), B)
18.302 + else error "Illegal nested case names"
18.303 + | ((b, _), _) => error "Illegal simultaneous specification")
18.304 + | (a, _) => error ("Illegal local specification parameters for " ^ quote (Name.name_of a)));
18.305
18.306 fun gen_ind_decl mk_def coind =
18.307 P.fixes -- P.for_fixes --
19.1 --- a/src/HOL/Tools/inductive_realizer.ML Tue Sep 02 14:10:32 2008 +0200
19.2 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Sep 02 14:10:45 2008 +0200
19.3 @@ -337,9 +337,7 @@
19.4 (Logic.strip_assums_concl rintr));
19.5 val s' = Sign.base_name s;
19.6 val T' = Logic.unvarifyT T
19.7 - in (((s', T'), NoSyn),
19.8 - (Const (s, T'), Free (s', T')))
19.9 - end) rintrs));
19.10 + in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
19.11 val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
19.12 (List.take (snd (strip_comb
19.13 (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
19.14 @@ -348,10 +346,10 @@
19.15
19.16 val (ind_info, thy3') = thy2 |>
19.17 InductivePackage.add_inductive_global (serial_string ())
19.18 - {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = "",
19.19 + {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding,
19.20 coind = false, no_elim = false, no_ind = false, skip_mono = false}
19.21 rlzpreds rlzparams (map (fn (rintr, intr) =>
19.22 - ((Sign.base_name (name_of_thm intr), []),
19.23 + ((Name.binding (Sign.base_name (name_of_thm intr)), []),
19.24 subst_atomic rlzpreds' (Logic.unvarify rintr)))
19.25 (rintrs ~~ maps snd rss)) [] ||>
19.26 Sign.absolute_path;
20.1 --- a/src/HOL/Tools/inductive_set_package.ML Tue Sep 02 14:10:32 2008 +0200
20.2 +++ b/src/HOL/Tools/inductive_set_package.ML Tue Sep 02 14:10:45 2008 +0200
20.3 @@ -13,12 +13,12 @@
20.4 val pred_set_conv_att: attribute
20.5 val add_inductive_i:
20.6 InductivePackage.inductive_flags ->
20.7 - ((string * typ) * mixfix) list ->
20.8 - (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
20.9 + ((Name.binding * typ) * mixfix) list ->
20.10 + (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
20.11 local_theory -> InductivePackage.inductive_result * local_theory
20.12 - val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
20.13 - (string * string option * mixfix) list ->
20.14 - ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
20.15 + val add_inductive: bool -> bool -> (Name.binding * string option * mixfix) list ->
20.16 + (Name.binding * string option * mixfix) list ->
20.17 + ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
20.18 local_theory -> InductivePackage.inductive_result * local_theory
20.19 val setup: theory -> theory
20.20 end;
20.21 @@ -461,16 +461,17 @@
20.22 | NONE => u)) |>
20.23 Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
20.24 eta_contract (member op = cs' orf is_pred pred_arities))) intros;
20.25 - val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn;
20.26 + val cnames_syn' = map (fn (b, _) => (Name.map_name (suffix "p") b, NoSyn)) cnames_syn;
20.27 val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
20.28 val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
20.29 - InductivePackage.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, kind = kind,
20.30 - alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
20.31 + InductivePackage.add_ind_def
20.32 + {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Name.no_binding,
20.33 + coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
20.34 cs' intros' monos' params1 cnames_syn' ctxt;
20.35
20.36 (* define inductive sets using previously defined predicates *)
20.37 val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
20.38 - (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (("", []),
20.39 + (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, ((Name.no_binding, []),
20.40 fold_rev lambda params (HOLogic.Collect_const U $
20.41 HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
20.42 (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
20.43 @@ -488,15 +489,17 @@
20.44 (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
20.45 [def, mem_Collect_eq, split_conv]) 1))
20.46 in
20.47 - ctxt |> LocalTheory.note kind ((s ^ "p_" ^ s ^ "_eq",
20.48 + ctxt |> LocalTheory.note kind ((Name.binding (s ^ "p_" ^ s ^ "_eq"),
20.49 [Attrib.internal (K pred_set_conv_att)]),
20.50 [conv_thm]) |> snd
20.51 end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
20.52
20.53 (* convert theorems to set notation *)
20.54 - val rec_name = if alt_name = "" then
20.55 - space_implode "_" (map fst cnames_syn) else alt_name;
20.56 - val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn; (* FIXME *)
20.57 + val rec_name =
20.58 + if Name.name_of alt_name = "" then
20.59 + Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
20.60 + else alt_name;
20.61 + val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn; (* FIXME *)
20.62 val (intr_names, intr_atts) = split_list (map fst intros);
20.63 val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
20.64 val (intrs', elims', induct, ctxt4) =
21.1 --- a/src/HOL/Tools/primrec_package.ML Tue Sep 02 14:10:32 2008 +0200
21.2 +++ b/src/HOL/Tools/primrec_package.ML Tue Sep 02 14:10:45 2008 +0200
21.3 @@ -8,13 +8,13 @@
21.4
21.5 signature PRIMREC_PACKAGE =
21.6 sig
21.7 - val add_primrec: (string * typ option * mixfix) list ->
21.8 - ((bstring * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
21.9 - val add_primrec_global: (string * typ option * mixfix) list ->
21.10 - ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory
21.11 + val add_primrec: (Name.binding * typ option * mixfix) list ->
21.12 + ((Name.binding * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
21.13 + val add_primrec_global: (Name.binding * typ option * mixfix) list ->
21.14 + ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
21.15 val add_primrec_overloaded: (string * (string * typ) * bool) list ->
21.16 - (string * typ option * mixfix) list ->
21.17 - ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory
21.18 + (Name.binding * typ option * mixfix) list ->
21.19 + ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
21.20 end;
21.21
21.22 structure PrimrecPackage : PRIMREC_PACKAGE =
21.23 @@ -189,14 +189,14 @@
21.24 fun make_def ctxt fixes fs (fname, ls, rec_name, tname) =
21.25 let
21.26 val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t))
21.27 - ((map snd ls) @ [dummyT])
21.28 + (map snd ls @ [dummyT])
21.29 (list_comb (Const (rec_name, dummyT),
21.30 - fs @ map Bound (0 ::(length ls downto 1))))
21.31 + fs @ map Bound (0 :: (length ls downto 1))))
21.32 val def_name = Thm.def_name (Sign.base_name fname);
21.33 val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
21.34 - val SOME mfx = get_first
21.35 - (fn ((v, _), mfx) => if v = fname then SOME mfx else NONE) fixes;
21.36 - in ((fname, mfx), ((def_name, []), rhs)) end;
21.37 + val SOME var = get_first (fn ((b, _), mx) =>
21.38 + if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
21.39 + in (var, ((Name.binding def_name, []), rhs)) end;
21.40
21.41
21.42 (* find datatypes which contain all datatypes in tnames' *)
21.43 @@ -226,16 +226,15 @@
21.44 val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
21.45 fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
21.46 val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
21.47 - in map (fn (name_attr, t) => (name_attr, [Goal.prove ctxt [] [] t tac])) end;
21.48 + in map (fn (a, t) => (a, [Goal.prove ctxt [] [] t tac])) end;
21.49
21.50 fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
21.51 let
21.52 val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
21.53 val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
21.54 - orelse exists (fn ((w, _), _) => v = w) fixes) o snd) spec [];
21.55 + orelse exists (fn ((w, _), _) => v = Name.name_of w) fixes) o snd) spec [];
21.56 val tnames = distinct (op =) (map (#1 o snd) eqns);
21.57 - val dts = find_dts (DatatypePackage.get_datatypes
21.58 - (ProofContext.theory_of lthy)) tnames tnames;
21.59 + val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
21.60 val main_fns = map (fn (tname, {index, ...}) =>
21.61 (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
21.62 val {descr, rec_names, rec_rewrites, ...} =
21.63 @@ -251,7 +250,7 @@
21.64 "\nare not mutually recursive");
21.65 val qualify = NameSpace.qualified
21.66 (space_implode "_" (map (Sign.base_name o #1) defs));
21.67 - val spec' = (map o apfst o apfst) qualify spec;
21.68 + val spec' = (map o apfst o apfst o Name.map_name) qualify spec;
21.69 val simp_atts = map (Attrib.internal o K)
21.70 [Simplifier.simp_add, RecfunCodegen.add NONE];
21.71 in
21.72 @@ -261,7 +260,7 @@
21.73 |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
21.74 |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
21.75 |-> (fn simps' => LocalTheory.note Thm.theoremK
21.76 - ((qualify "simps", simp_atts), maps snd simps'))
21.77 + ((Name.binding (qualify "simps"), simp_atts), maps snd simps'))
21.78 |>> snd
21.79 end handle PrimrecError (msg, some_eqn) =>
21.80 error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
21.81 @@ -300,7 +299,7 @@
21.82 P.name >> pair false) --| P.$$$ ")")) (false, "");
21.83
21.84 val old_primrec_decl =
21.85 - opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
21.86 + opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop);
21.87
21.88 fun pipe_error t = P.!!! (Scan.fail_with (K
21.89 (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
22.1 --- a/src/HOL/Tools/recdef_package.ML Tue Sep 02 14:10:32 2008 +0200
22.2 +++ b/src/HOL/Tools/recdef_package.ML Tue Sep 02 14:10:45 2008 +0200
22.3 @@ -268,8 +268,8 @@
22.4 error ("No termination condition #" ^ string_of_int i ^
22.5 " in recdef definition of " ^ quote name);
22.6 in
22.7 - Specification.theorem Thm.internalK NONE (K I) (bname, atts)
22.8 - [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
22.9 + Specification.theorem Thm.internalK NONE (K I) (Name.binding bname, atts)
22.10 + [] (Element.Shows [((Name.no_binding, []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
22.11 end;
22.12
22.13 val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
22.14 @@ -299,7 +299,8 @@
22.15
22.16 val recdef_decl =
22.17 Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
22.18 - P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
22.19 + P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
22.20 + -- Scan.option hints
22.21 >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
22.22
22.23 val _ =
22.24 @@ -319,7 +320,8 @@
22.25 val _ =
22.26 OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
22.27 K.thy_goal
22.28 - (SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
22.29 + ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
22.30 + Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
22.31 >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
22.32
22.33 end;
23.1 --- a/src/HOL/Tools/specification_package.ML Tue Sep 02 14:10:32 2008 +0200
23.2 +++ b/src/HOL/Tools/specification_package.ML Tue Sep 02 14:10:45 2008 +0200
23.3 @@ -233,7 +233,7 @@
23.4
23.5 val specification_decl =
23.6 P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
23.7 - Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
23.8 + Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
23.9
23.10 val _ =
23.11 OuterSyntax.command "specification" "define constants by specification" K.thy_goal
23.12 @@ -244,7 +244,7 @@
23.13 val ax_specification_decl =
23.14 P.name --
23.15 (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
23.16 - Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
23.17 + Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
23.18
23.19 val _ =
23.20 OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
24.1 --- a/src/HOL/Tools/typecopy_package.ML Tue Sep 02 14:10:32 2008 +0200
24.2 +++ b/src/HOL/Tools/typecopy_package.ML Tue Sep 02 14:10:45 2008 +0200
24.3 @@ -134,7 +134,7 @@
24.4 (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
24.5 val def' = Syntax.check_term lthy def;
24.6 val ((_, (_, thm)), lthy') = Specification.definition
24.7 - (NONE, (("", []), def')) lthy;
24.8 + (NONE, ((Name.no_binding, []), def')) lthy;
24.9 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
24.10 val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
24.11 in (thm', lthy') end;
25.1 --- a/src/HOL/Typedef.thy Tue Sep 02 14:10:32 2008 +0200
25.2 +++ b/src/HOL/Typedef.thy Tue Sep 02 14:10:45 2008 +0200
25.3 @@ -145,7 +145,7 @@
25.4 thy
25.5 |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
25.6 |> `(fn lthy => Syntax.check_term lthy eq)
25.7 - |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
25.8 + |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
25.9 |> snd
25.10 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
25.11 |> LocalTheory.exit
26.1 --- a/src/HOL/ex/Quickcheck.thy Tue Sep 02 14:10:32 2008 +0200
26.2 +++ b/src/HOL/ex/Quickcheck.thy Tue Sep 02 14:10:45 2008 +0200
26.3 @@ -128,11 +128,11 @@
26.4 thy
26.5 |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
26.6 |> PrimrecPackage.add_primrec
26.7 - [(fst (dest_Free random'), SOME (snd (dest_Free random')), NoSyn)]
26.8 - (map (fn eq => (("", [del_func]), eq)) eqs')
26.9 + [(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
26.10 + (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
26.11 |-> add_code
26.12 |> `(fn lthy => Syntax.check_term lthy eq)
26.13 - |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
26.14 + |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
26.15 |> snd
26.16 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
26.17 |> LocalTheory.exit
26.18 @@ -261,7 +261,7 @@
26.19 in
26.20 thy
26.21 |> TheoryTarget.init NONE
26.22 - |> Specification.definition (NONE, (("", []), eq))
26.23 + |> Specification.definition (NONE, ((Name.no_binding, []), eq))
26.24 |> snd
26.25 |> LocalTheory.exit
26.26 |> ProofContext.theory_of
27.1 --- a/src/HOLCF/Tools/fixrec_package.ML Tue Sep 02 14:10:32 2008 +0200
27.2 +++ b/src/HOLCF/Tools/fixrec_package.ML Tue Sep 02 14:10:45 2008 +0200
27.3 @@ -9,10 +9,10 @@
27.4 sig
27.5 val legacy_infer_term: theory -> term -> term
27.6 val legacy_infer_prop: theory -> term -> term
27.7 - val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
27.8 - val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
27.9 - val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
27.10 - val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
27.11 + val add_fixrec: bool -> ((Name.binding * Attrib.src list) * string) list list -> theory -> theory
27.12 + val add_fixrec_i: bool -> ((Name.binding * attribute list) * term) list list -> theory -> theory
27.13 + val add_fixpat: (Name.binding * Attrib.src list) * string list -> theory -> theory
27.14 + val add_fixpat_i: (Name.binding * attribute list) * term list -> theory -> theory
27.15 end;
27.16
27.17 structure FixrecPackage: FIXREC_PACKAGE =
27.18 @@ -226,7 +226,8 @@
27.19 val eqns = List.concat blocks;
27.20 val lengths = map length blocks;
27.21
27.22 - val ((names, srcss), strings) = apfst split_list (split_list eqns);
27.23 + val ((bindings, srcss), strings) = apfst split_list (split_list eqns);
27.24 + val names = map Name.name_of bindings;
27.25 val atts = map (map (prep_attrib thy)) srcss;
27.26 val eqn_ts = map (prep_prop thy) strings;
27.27 val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
27.28 @@ -278,7 +279,7 @@
27.29 val ts = map (prep_term thy) strings;
27.30 val simps = map (fix_pat thy) ts;
27.31 in
27.32 - (snd o PureThy.add_thmss [((name, simps), atts)]) thy
27.33 + (snd o PureThy.add_thmss [((Name.name_of name, simps), atts)]) thy
27.34 end;
27.35
27.36 val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
28.1 --- a/src/HOLCF/Tools/pcpodef_package.ML Tue Sep 02 14:10:32 2008 +0200
28.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML Tue Sep 02 14:10:45 2008 +0200
28.3 @@ -94,7 +94,7 @@
28.4 |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
28.5 val less_def' = Syntax.check_term lthy3 less_def;
28.6 val ((_, (_, less_definition')), lthy4) = lthy3
28.7 - |> Specification.definition (NONE, (("less_" ^ name ^ "_def", []), less_def'));
28.8 + |> Specification.definition (NONE, ((Name.binding ("less_" ^ name ^ "_def"), []), less_def'));
28.9 val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
28.10 val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
28.11 val thy5 = lthy4
29.1 --- a/src/Pure/Isar/attrib.ML Tue Sep 02 14:10:32 2008 +0200
29.2 +++ b/src/Pure/Isar/attrib.ML Tue Sep 02 14:10:45 2008 +0200
29.3 @@ -110,7 +110,8 @@
29.4 fun attribute thy = attribute_i thy o intern_src thy;
29.5
29.6 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
29.7 - [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
29.8 + [((Name.no_binding, []),
29.9 + map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
29.10 |> fst |> maps snd;
29.11
29.12
30.1 --- a/src/Pure/Isar/class.ML Tue Sep 02 14:10:32 2008 +0200
30.2 +++ b/src/Pure/Isar/class.ML Tue Sep 02 14:10:45 2008 +0200
30.3 @@ -19,7 +19,7 @@
30.4 val abbrev: class -> Syntax.mode -> Properties.T
30.5 -> (string * mixfix) * term -> theory -> theory
30.6 val note: class -> string
30.7 - -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
30.8 + -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
30.9 -> theory -> (bstring * thm list) list * theory
30.10 val declaration: class -> declaration -> theory -> theory
30.11 val refresh_syntax: class -> Proof.context -> Proof.context
30.12 @@ -48,7 +48,7 @@
30.13
30.14 (*old axclass layer*)
30.15 val axclass_cmd: bstring * xstring list
30.16 - -> ((bstring * Attrib.src list) * string list) list
30.17 + -> ((Name.binding * Attrib.src list) * string list) list
30.18 -> theory -> class * theory
30.19 val classrel_cmd: xstring * xstring -> theory -> Proof.state
30.20
30.21 @@ -374,7 +374,7 @@
30.22 thy
30.23 |> fold2 add_constraint (map snd consts) no_constraints
30.24 |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
30.25 - (inst, map (fn def => (("", []), def)) defs)
30.26 + (inst, map (fn def => ((Name.no_binding, []), def)) defs)
30.27 |> fold2 add_constraint (map snd consts) constraints
30.28 end;
30.29
30.30 @@ -569,7 +569,7 @@
30.31 val constrain = Element.Constrains ((map o apsnd o map_atyps)
30.32 (K (TFree (Name.aT, base_sort))) supparams);
30.33 fun fork_syn (Element.Fixes xs) =
30.34 - fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
30.35 + fold_map (fn (c, ty, syn) => cons (Name.name_of c, syn) #> pair (c, ty, NoSyn)) xs
30.36 #>> Element.Fixes
30.37 | fork_syn x = pair x;
30.38 fun fork_syntax elems =
30.39 @@ -628,7 +628,7 @@
30.40 |> add_consts ((snd o chop (length supparams)) all_params)
30.41 |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
30.42 (map (fst o snd) params)
30.43 - [((bname ^ "_" ^ AxClass.axiomsN, []), map (globalize param_map) raw_pred)]
30.44 + [((Name.binding (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
30.45 #> snd
30.46 #> `get_axiom
30.47 #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
31.1 --- a/src/Pure/Isar/constdefs.ML Tue Sep 02 14:10:32 2008 +0200
31.2 +++ b/src/Pure/Isar/constdefs.ML Tue Sep 02 14:10:45 2008 +0200
31.3 @@ -9,12 +9,12 @@
31.4
31.5 signature CONSTDEFS =
31.6 sig
31.7 - val add_constdefs: (string * string option) list *
31.8 - ((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
31.9 - theory -> theory
31.10 - val add_constdefs_i: (string * typ option) list *
31.11 - ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
31.12 - theory -> theory
31.13 + val add_constdefs: (Name.binding * string option) list *
31.14 + ((Name.binding * string option * mixfix) option *
31.15 + ((Name.binding * Attrib.src list) * string)) list -> theory -> theory
31.16 + val add_constdefs_i: (Name.binding * typ option) list *
31.17 + ((Name.binding * typ option * mixfix) option *
31.18 + ((Name.binding * attribute list) * term)) list -> theory -> theory
31.19 end;
31.20
31.21 structure Constdefs: CONSTDEFS =
31.22 @@ -38,13 +38,16 @@
31.23
31.24 val prop = prep_prop var_ctxt raw_prop;
31.25 val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
31.26 - val _ = (case d of NONE => () | SOME c' =>
31.27 - if c <> c' then
31.28 - err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
31.29 - else ());
31.30 + val _ =
31.31 + (case Option.map Name.name_of d of
31.32 + NONE => ()
31.33 + | SOME c' =>
31.34 + if c <> c' then
31.35 + err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
31.36 + else ());
31.37
31.38 val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
31.39 - val name = Thm.def_name_optional c raw_name;
31.40 + val name = Thm.def_name_optional c (Name.name_of raw_name);
31.41 val atts = map (prep_att thy) raw_atts;
31.42
31.43 val thy' =
32.1 --- a/src/Pure/Isar/isar_cmd.ML Tue Sep 02 14:10:32 2008 +0200
32.2 +++ b/src/Pure/Isar/isar_cmd.ML Tue Sep 02 14:10:45 2008 +0200
32.3 @@ -15,19 +15,19 @@
32.4 val print_ast_translation: bool * (string * Position.T) -> theory -> theory
32.5 val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
32.6 theory -> theory
32.7 - val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
32.8 - val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
32.9 + val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
32.10 + val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory
32.11 val declaration: string * Position.T -> local_theory -> local_theory
32.12 val simproc_setup: string -> string list -> string * Position.T -> string list ->
32.13 local_theory -> local_theory
32.14 val hide_names: bool -> string * xstring list -> theory -> theory
32.15 - val have: ((string * Attrib.src list) * (string * string list) list) list ->
32.16 + val have: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
32.17 bool -> Proof.state -> Proof.state
32.18 - val hence: ((string * Attrib.src list) * (string * string list) list) list ->
32.19 + val hence: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
32.20 bool -> Proof.state -> Proof.state
32.21 - val show: ((string * Attrib.src list) * (string * string list) list) list ->
32.22 + val show: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
32.23 bool -> Proof.state -> Proof.state
32.24 - val thus: ((string * Attrib.src list) * (string * string list) list) list ->
32.25 + val thus: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
32.26 bool -> Proof.state -> Proof.state
32.27 val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
32.28 val terminal_proof: Method.text * Method.text option ->
32.29 @@ -179,7 +179,7 @@
32.30 (* axioms *)
32.31
32.32 fun add_axms f args thy =
32.33 - f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
32.34 + f (map (fn ((b, ax), srcs) => ((Name.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
32.35
32.36 val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
32.37
33.1 --- a/src/Pure/Isar/isar_syn.ML Tue Sep 02 14:10:32 2008 +0200
33.2 +++ b/src/Pure/Isar/isar_syn.ML Tue Sep 02 14:10:45 2008 +0200
33.3 @@ -203,10 +203,10 @@
33.4 (* old constdefs *)
33.5
33.6 val old_constdecl =
33.7 - P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
33.8 - P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
33.9 + P.binding --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
33.10 + P.binding -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
33.11 --| Scan.option P.where_ >> P.triple1 ||
33.12 - P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
33.13 + P.binding -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
33.14
33.15 val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
33.16
33.17 @@ -221,7 +221,7 @@
33.18 (* constant definitions and abbreviations *)
33.19
33.20 val constdecl =
33.21 - P.name --
33.22 + P.binding --
33.23 (P.where_ >> K (NONE, NoSyn) ||
33.24 P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
33.25 Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
33.26 @@ -272,7 +272,7 @@
33.27 val _ =
33.28 OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
33.29 (P.and_list1 SpecParse.xthms1
33.30 - >> (fn args => #2 o Specification.theorems_cmd "" [(("", []), flat args)]));
33.31 + >> (fn args => #2 o Specification.theorems_cmd "" [((Name.no_binding, []), flat args)]));
33.32
33.33
33.34 (* name space entry path *)
33.35 @@ -396,16 +396,18 @@
33.36 (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
33.37 >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
33.38 SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
33.39 - >> (fn ((x, y), z) => Toplevel.print o
33.40 - Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
33.41 + >> (fn (((name, atts), expr), insts) => Toplevel.print o
33.42 + Toplevel.theory_to_proof
33.43 + (Locale.interpretation I ((true, Name.name_of name), atts) expr insts)));
33.44
33.45 val _ =
33.46 OuterSyntax.command "interpret"
33.47 "prove and register interpretation of locale expression in proof context"
33.48 (K.tag_proof K.prf_goal)
33.49 (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
33.50 - >> (fn ((x, y), z) => Toplevel.print o
33.51 - Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
33.52 + >> (fn (((name, atts), expr), insts) => Toplevel.print o
33.53 + Toplevel.proof'
33.54 + (Locale.interpret Seq.single ((true, Name.name_of name), atts) expr insts)));
33.55
33.56
33.57 (* classes *)
33.58 @@ -466,7 +468,7 @@
33.59 fun gen_theorem kind =
33.60 OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
33.61 (Scan.optional (SpecParse.opt_thm_name ":" --|
33.62 - Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
33.63 + Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) (Name.no_binding, []) --
33.64 SpecParse.general_statement >> (fn (a, (elems, concl)) =>
33.65 (Specification.theorem_cmd kind NONE (K I) a elems concl)));
33.66
33.67 @@ -552,7 +554,7 @@
33.68 (K.tag_proof K.prf_asm)
33.69 (P.and_list1
33.70 (SpecParse.opt_thm_name ":" --
33.71 - ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
33.72 + ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
33.73 >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
33.74
33.75 val _ =
34.1 --- a/src/Pure/Isar/local_defs.ML Tue Sep 02 14:10:32 2008 +0200
34.2 +++ b/src/Pure/Isar/local_defs.ML Tue Sep 02 14:10:45 2008 +0200
34.3 @@ -12,10 +12,11 @@
34.4 val mk_def: Proof.context -> (string * term) list -> term list
34.5 val expand: cterm list -> thm -> thm
34.6 val def_export: Assumption.export
34.7 - val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
34.8 - (term * (bstring * thm)) list * Proof.context
34.9 - val add_def: (string * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
34.10 - val fixed_abbrev: (string * mixfix) * term -> Proof.context -> (term * term) * Proof.context
34.11 + val add_defs: ((Name.binding * mixfix) * ((Name.binding * attribute list) * term)) list ->
34.12 + Proof.context -> (term * (string * thm)) list * Proof.context
34.13 + val add_def: (Name.binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
34.14 + val fixed_abbrev: (Name.binding * mixfix) * term -> Proof.context ->
34.15 + (term * term) * Proof.context
34.16 val export: Proof.context -> Proof.context -> thm -> thm list * thm
34.17 val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
34.18 val trans_terms: Proof.context -> thm list -> thm
34.19 @@ -88,22 +89,23 @@
34.20
34.21 fun add_defs defs ctxt =
34.22 let
34.23 - val ((xs, mxs), specs) = defs |> split_list |>> split_list;
34.24 - val ((names, atts), rhss) = specs |> split_list |>> split_list;
34.25 - val names' = map2 Thm.def_name_optional xs names;
34.26 + val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
34.27 + val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
34.28 + val xs = map Name.name_of bvars;
34.29 + val names = map2 (Name.map_name o Thm.def_name_optional) xs bfacts;
34.30 val eqs = mk_def ctxt (xs ~~ rhss);
34.31 val lhss = map (fst o Logic.dest_equals) eqs;
34.32 in
34.33 ctxt
34.34 - |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
34.35 + |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
34.36 |> fold Variable.declare_term eqs
34.37 |> ProofContext.add_assms_i def_export
34.38 - (map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs)
34.39 + (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
34.40 |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
34.41 end;
34.42
34.43 fun add_def (var, rhs) ctxt =
34.44 - let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (("", []), rhs))] ctxt
34.45 + let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Name.no_binding, []), rhs))] ctxt
34.46 in ((lhs, th), ctxt') end;
34.47
34.48
35.1 --- a/src/Pure/Isar/local_theory.ML Tue Sep 02 14:10:32 2008 +0200
35.2 +++ b/src/Pure/Isar/local_theory.ML Tue Sep 02 14:10:45 2008 +0200
35.3 @@ -26,16 +26,16 @@
35.4 val affirm: local_theory -> local_theory
35.5 val pretty: local_theory -> Pretty.T list
35.6 val axioms: string ->
35.7 - ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
35.8 - -> (term list * (bstring * thm list) list) * local_theory
35.9 - val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
35.10 + ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
35.11 + -> (term list * (string * thm list) list) * local_theory
35.12 + val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
35.13 (term * term) * local_theory
35.14 - val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
35.15 - (term * (bstring * thm)) * local_theory
35.16 - val note: string -> (bstring * Attrib.src list) * thm list ->
35.17 - local_theory -> (bstring * thm list) * local_theory
35.18 - val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
35.19 - local_theory -> (bstring * thm list) list * local_theory
35.20 + val define: string -> (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
35.21 + (term * (string * thm)) * local_theory
35.22 + val note: string -> (Name.binding * Attrib.src list) * thm list ->
35.23 + local_theory -> (string * thm list) * local_theory
35.24 + val notes: string -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
35.25 + local_theory -> (string * thm list) list * local_theory
35.26 val type_syntax: declaration -> local_theory -> local_theory
35.27 val term_syntax: declaration -> local_theory -> local_theory
35.28 val declaration: declaration -> local_theory -> local_theory
35.29 @@ -57,15 +57,15 @@
35.30 type operations =
35.31 {pretty: local_theory -> Pretty.T list,
35.32 axioms: string ->
35.33 - ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
35.34 - -> (term list * (bstring * thm list) list) * local_theory,
35.35 - abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
35.36 + ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
35.37 + -> (term list * (string * thm list) list) * local_theory,
35.38 + abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> (term * term) * local_theory,
35.39 define: string ->
35.40 - (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
35.41 - (term * (bstring * thm)) * local_theory,
35.42 + (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
35.43 + (term * (string * thm)) * local_theory,
35.44 notes: string ->
35.45 - ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
35.46 - local_theory -> (bstring * thm list) list * local_theory,
35.47 + ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
35.48 + local_theory -> (string * thm list) list * local_theory,
35.49 type_syntax: declaration -> local_theory -> local_theory,
35.50 term_syntax: declaration -> local_theory -> local_theory,
35.51 declaration: declaration -> local_theory -> local_theory,
36.1 --- a/src/Pure/Isar/locale.ML Tue Sep 02 14:10:32 2008 +0200
36.2 +++ b/src/Pure/Isar/locale.ML Tue Sep 02 14:10:45 2008 +0200
36.3 @@ -55,16 +55,16 @@
36.4 val parameters_of_expr: theory -> expr ->
36.5 ((string * typ) * mixfix) list
36.6 val local_asms_of: theory -> string ->
36.7 - ((string * Attrib.src list) * term list) list
36.8 + ((Name.binding * Attrib.src list) * term list) list
36.9 val global_asms_of: theory -> string ->
36.10 - ((string * Attrib.src list) * term list) list
36.11 + ((Name.binding * Attrib.src list) * term list) list
36.12
36.13 (* Theorems *)
36.14 val intros: theory -> string -> thm list * thm list
36.15 val dests: theory -> string -> thm list
36.16 (* Not part of the official interface. DO NOT USE *)
36.17 val facts_of: theory -> string
36.18 - -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list list
36.19 + -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list list
36.20
36.21 (* Processing of locale statements *)
36.22 val read_context_statement: xstring option -> Element.context element list ->
36.23 @@ -96,7 +96,7 @@
36.24
36.25 (* Storing results *)
36.26 val add_thmss: string -> string ->
36.27 - ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
36.28 + ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
36.29 Proof.context -> Proof.context
36.30 val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
36.31 val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
36.32 @@ -104,21 +104,21 @@
36.33
36.34 val interpretation_i: (Proof.context -> Proof.context) ->
36.35 (bool * string) * Attrib.src list -> expr ->
36.36 - term option list * ((bstring * Attrib.src list) * term) list ->
36.37 + term option list * ((Name.binding * Attrib.src list) * term) list ->
36.38 theory -> Proof.state
36.39 val interpretation: (Proof.context -> Proof.context) ->
36.40 (bool * string) * Attrib.src list -> expr ->
36.41 - string option list * ((bstring * Attrib.src list) * string) list ->
36.42 + string option list * ((Name.binding * Attrib.src list) * string) list ->
36.43 theory -> Proof.state
36.44 val interpretation_in_locale: (Proof.context -> Proof.context) ->
36.45 xstring * expr -> theory -> Proof.state
36.46 val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
36.47 (bool * string) * Attrib.src list -> expr ->
36.48 - term option list * ((bstring * Attrib.src list) * term) list ->
36.49 + term option list * ((Name.binding * Attrib.src list) * term) list ->
36.50 bool -> Proof.state -> Proof.state
36.51 val interpret: (Proof.state -> Proof.state Seq.seq) ->
36.52 (bool * string) * Attrib.src list -> expr ->
36.53 - string option list * ((bstring * Attrib.src list) * string) list ->
36.54 + string option list * ((Name.binding * Attrib.src list) * string) list ->
36.55 bool -> Proof.state -> Proof.state
36.56 end;
36.57
36.58 @@ -756,7 +756,7 @@
36.59 val ren = renaming xs parms';
36.60 (* renaming may reduce number of parameters *)
36.61 val new_parms = map (Element.rename ren) parms' |> distinct (op =);
36.62 - val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
36.63 + val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren);
36.64 val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
36.65 handle Symtab.DUP x =>
36.66 err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
36.67 @@ -789,7 +789,7 @@
36.68 fun make_raw_params_elemss (params, tenv, syn) =
36.69 [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
36.70 Int [Fixes (map (fn p =>
36.71 - (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
36.72 + (Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
36.73
36.74
36.75 (* flatten_expr:
36.76 @@ -929,7 +929,7 @@
36.77 val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
36.78 val elem_morphism =
36.79 Element.rename_morphism ren $>
36.80 - Morphism.name_morphism (params_qualified params) $>
36.81 + Morphism.name_morphism (Name.map_name (params_qualified params)) $>
36.82 Element.instT_morphism thy env;
36.83 val elems' = map (Element.morph_ctxt elem_morphism) elems;
36.84 in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
36.85 @@ -978,7 +978,7 @@
36.86 val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
36.87 val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
36.88 let val ((c, _), t') = LocalDefs.cert_def ctxt t
36.89 - in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
36.90 + in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
36.91 val (_, ctxt') =
36.92 ctxt |> fold (Variable.auto_fixes o #1) asms
36.93 |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
36.94 @@ -989,7 +989,7 @@
36.95 let
36.96 val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
36.97 val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
36.98 - in (if is_ext then res else [], (ctxt', mode)) end;
36.99 + in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end;
36.100
36.101 fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
36.102 let
36.103 @@ -1076,15 +1076,15 @@
36.104 *)
36.105
36.106 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
36.107 - val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
36.108 + val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
36.109 in
36.110 ((ids',
36.111 merge_syntax ctxt ids'
36.112 - (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
36.113 + (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
36.114 handle Symtab.DUP x => err_in_locale ctxt
36.115 ("Conflicting syntax for parameter: " ^ quote x)
36.116 (map #1 ids')),
36.117 - [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
36.118 + [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
36.119 end
36.120 | flatten _ ((ids, syn), Elem elem) =
36.121 ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
36.122 @@ -1104,7 +1104,7 @@
36.123 let val (vars, _) = prep_vars fixes ctxt
36.124 in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
36.125 | declare_ext_elem prep_vars (Constrains csts) ctxt =
36.126 - let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
36.127 + let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
36.128 in ([], ctxt') end
36.129 | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
36.130 | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
36.131 @@ -1227,8 +1227,9 @@
36.132 end;
36.133
36.134
36.135 -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
36.136 - (x, AList.lookup (op =) parms x, mx)) fixes)
36.137 +fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
36.138 + let val x = Name.name_of binding
36.139 + in (binding, AList.lookup (op =) parms x, mx) end) fixes)
36.140 | finish_ext_elem parms _ (Constrains _, _) = Constrains []
36.141 | finish_ext_elem _ close (Assumes asms, propp) =
36.142 close (Assumes (map #1 asms ~~ propp))
36.143 @@ -1274,7 +1275,7 @@
36.144 list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
36.145 Term.fast_term_ord (d1, d2)) (defs1, defs2);
36.146 structure Defstab =
36.147 - TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
36.148 + TableFun(type key = ((Name.binding * Attrib.src list) * (term * term list)) list
36.149 val ord = defs_ord);
36.150
36.151 fun rem_dup_defs es ds =
36.152 @@ -1387,7 +1388,7 @@
36.153 |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
36.154 | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
36.155 {var = I, typ = I, term = I,
36.156 - name = prep_name,
36.157 + name = Name.map_name prep_name,
36.158 fact = get ctxt,
36.159 attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
36.160
36.161 @@ -1572,8 +1573,8 @@
36.162 (* naming of interpreted theorems *)
36.163
36.164 fun add_param_prefixss s =
36.165 - (map o apfst o apfst) (NameSpace.qualified s);
36.166 -fun drop_param_prefixss args = (map o apfst o apfst)
36.167 + (map o apfst o apfst o Name.map_name) (NameSpace.qualified s);
36.168 +fun drop_param_prefixss args = (map o apfst o apfst o Name.map_name)
36.169 (fn "" => "" | s => (NameSpace.implode o tl o NameSpace.explode) s) args;
36.170
36.171 fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
36.172 @@ -1660,7 +1661,7 @@
36.173
36.174 fun interpret_args thy prfx insts prems eqns atts2 exp attrib args =
36.175 let
36.176 - val inst = Morphism.name_morphism (NameSpace.qualified prfx) $>
36.177 + val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
36.178 (* need to add parameter prefix *) (* FIXME *)
36.179 Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
36.180 Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
36.181 @@ -1724,7 +1725,7 @@
36.182 (fn (axiom, elems, params, decls, regs, intros, dests) =>
36.183 (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
36.184 add_thmss loc Thm.internalK
36.185 - [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
36.186 + [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
36.187
36.188 in
36.189
36.190 @@ -1864,12 +1865,13 @@
36.191 thy
36.192 |> def_pred aname parms defs exts exts';
36.193 val elemss' = change_assumes_elemss axioms elemss;
36.194 - val a_elem = [(("", []), [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
36.195 + val a_elem = [(("", []),
36.196 + [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
36.197 val (_, thy'') =
36.198 thy'
36.199 |> Sign.add_path aname
36.200 |> Sign.no_base_names
36.201 - |> PureThy.note_thmss Thm.internalK [((introN, []), [([intro], [])])]
36.202 + |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
36.203 ||> Sign.restore_naming thy';
36.204 in ((elemss', [statement]), a_elem, [intro], thy'') end;
36.205 val (predicate, stmt', elemss'', b_intro, thy'''') =
36.206 @@ -1882,14 +1884,15 @@
36.207 val cstatement = Thm.cterm_of thy''' statement;
36.208 val elemss'' = change_elemss_hyps axioms elemss';
36.209 val b_elem = [(("", []),
36.210 - [Assumes [((pname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
36.211 + [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
36.212 val (_, thy'''') =
36.213 thy'''
36.214 |> Sign.add_path pname
36.215 |> Sign.no_base_names
36.216 |> PureThy.note_thmss Thm.internalK
36.217 - [((introN, []), [([intro], [])]),
36.218 - ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
36.219 + [((Name.binding introN, []), [([intro], [])]),
36.220 + ((Name.binding axiomsN, []),
36.221 + [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
36.222 ||> Sign.restore_naming thy''';
36.223 in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
36.224 in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end;
36.225 @@ -1905,7 +1908,7 @@
36.226
36.227 fun defines_to_notes is_ext thy (Defines defs) defns =
36.228 let
36.229 - val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
36.230 + val defs' = map (fn (_, (def, _)) => ((Name.no_binding, []), (def, []))) defs
36.231 val notes = map (fn (a, (def, _)) =>
36.232 (a, [([assume (cterm_of thy def)], [])])) defs
36.233 in
36.234 @@ -1994,9 +1997,9 @@
36.235 end;
36.236
36.237 val _ = Context.>> (Context.map_theory
36.238 - (add_locale_i "" "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
36.239 + (add_locale_i "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
36.240 snd #> ProofContext.theory_of #>
36.241 - add_locale_i "" "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
36.242 + add_locale_i "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
36.243 snd #> ProofContext.theory_of));
36.244
36.245
36.246 @@ -2374,7 +2377,7 @@
36.247 fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
36.248 let
36.249 val att_morphism =
36.250 - Morphism.name_morphism (NameSpace.qualified prfx) $>
36.251 + Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $>
36.252 Morphism.thm_morphism satisfy $>
36.253 Element.inst_morphism thy insts $>
36.254 Morphism.thm_morphism disch;
36.255 @@ -2435,7 +2438,7 @@
36.256 in
36.257 state
36.258 |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
36.259 - "interpret" NONE after_qed' (map (pair ("", [])) (prep_propp propss))
36.260 + "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
36.261 |> Element.refine_witness |> Seq.hd
36.262 end;
36.263
37.1 --- a/src/Pure/Isar/proof.ML Tue Sep 02 14:10:32 2008 +0200
37.2 +++ b/src/Pure/Isar/proof.ML Tue Sep 02 14:10:45 2008 +0200
37.3 @@ -44,26 +44,30 @@
37.4 val match_bind_i: (term list * term) list -> state -> state
37.5 val let_bind: (string list * string) list -> state -> state
37.6 val let_bind_i: (term list * term) list -> state -> state
37.7 - val fix: (string * string option * mixfix) list -> state -> state
37.8 - val fix_i: (string * typ option * mixfix) list -> state -> state
37.9 + val fix: (Name.binding * string option * mixfix) list -> state -> state
37.10 + val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
37.11 val assm: Assumption.export ->
37.12 - ((string * Attrib.src list) * (string * string list) list) list -> state -> state
37.13 + ((Name.binding * Attrib.src list) * (string * string list) list) list -> state -> state
37.14 val assm_i: Assumption.export ->
37.15 - ((string * attribute list) * (term * term list) list) list -> state -> state
37.16 - val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
37.17 - val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
37.18 - val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
37.19 - val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
37.20 - val def: ((string * Attrib.src list) *
37.21 - ((string * mixfix) * (string * string list))) list -> state -> state
37.22 - val def_i: ((string * attribute list) *
37.23 - ((string * mixfix) * (term * term list))) list -> state -> state
37.24 + ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
37.25 + val assume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
37.26 + state -> state
37.27 + val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
37.28 + state -> state
37.29 + val presume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
37.30 + state -> state
37.31 + val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
37.32 + state -> state
37.33 + val def: ((Name.binding * Attrib.src list) *
37.34 + ((Name.binding * mixfix) * (string * string list))) list -> state -> state
37.35 + val def_i: ((Name.binding * attribute list) *
37.36 + ((Name.binding * mixfix) * (term * term list))) list -> state -> state
37.37 val chain: state -> state
37.38 val chain_facts: thm list -> state -> state
37.39 val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
37.40 - val note_thmss: ((string * Attrib.src list) *
37.41 + val note_thmss: ((Name.binding * Attrib.src list) *
37.42 (Facts.ref * Attrib.src list) list) list -> state -> state
37.43 - val note_thmss_i: ((string * attribute list) *
37.44 + val note_thmss_i: ((Name.binding * attribute list) *
37.45 (thm list * attribute list) list) list -> state -> state
37.46 val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
37.47 val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
37.48 @@ -87,7 +91,7 @@
37.49 (theory -> 'a -> attribute) ->
37.50 (context * 'b list -> context * (term list list * (context -> context))) ->
37.51 string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
37.52 - ((string * 'a list) * 'b) list -> state -> state
37.53 + ((Name.binding * 'a list) * 'b) list -> state -> state
37.54 val local_qed: Method.text option * bool -> state -> state Seq.seq
37.55 val theorem: Method.text option -> (thm list list -> context -> context) ->
37.56 (string * string list) list list -> context -> state
37.57 @@ -105,13 +109,13 @@
37.58 val global_done_proof: state -> context
37.59 val global_skip_proof: bool -> state -> context
37.60 val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
37.61 - ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
37.62 + ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
37.63 val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
37.64 - ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
37.65 + ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
37.66 val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
37.67 - ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
37.68 + ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
37.69 val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
37.70 - ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
37.71 + ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
37.72 end;
37.73
37.74 structure Proof: PROOF =
37.75 @@ -610,7 +614,7 @@
37.76
37.77 (* note etc. *)
37.78
37.79 -fun no_binding args = map (pair ("", [])) args;
37.80 +fun no_binding args = map (pair (Name.no_binding, [])) args;
37.81
37.82 local
37.83
37.84 @@ -638,7 +642,7 @@
37.85 val local_results =
37.86 gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
37.87
37.88 -fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
37.89 +fun get_thmss state srcs = the_facts (note_thmss [((Name.no_binding, []), srcs)] state);
37.90
37.91 end;
37.92
37.93 @@ -682,14 +686,14 @@
37.94 val atts = map (prep_att (theory_of state)) raw_atts;
37.95 val (asms, state') = state |> map_context_result (fn ctxt =>
37.96 ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
37.97 - val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
37.98 + val assumptions = asms |> map (fn (a, ts) => ((Name.binding a, atts), map (rpair []) ts));
37.99 in
37.100 state'
37.101 |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
37.102 |> assume_i assumptions
37.103 |> add_binds_i AutoBind.no_facts
37.104 |> map_context (ProofContext.restore_naming (context_of state))
37.105 - |> `the_facts |-> (fn thms => note_thmss_i [((name, []), [(thms, [])])])
37.106 + |> `the_facts |-> (fn thms => note_thmss_i [((Name.binding name, []), [(thms, [])])])
37.107 end;
37.108
37.109 in
38.1 --- a/src/Pure/Isar/rule_insts.ML Tue Sep 02 14:10:32 2008 +0200
38.2 +++ b/src/Pure/Isar/rule_insts.ML Tue Sep 02 14:10:45 2008 +0200
38.3 @@ -284,7 +284,7 @@
38.4 val (param_names, ctxt') = ctxt
38.5 |> Variable.declare_thm thm
38.6 |> Thm.fold_terms Variable.declare_constraints st
38.7 - |> ProofContext.add_fixes_i (map (fn (x, T) => (x, SOME T, NoSyn)) params);
38.8 + |> ProofContext.add_fixes_i (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) params);
38.9
38.10 (* Process type insts: Tinsts_env *)
38.11 fun absent xi = error
39.1 --- a/src/Pure/Isar/spec_parse.ML Tue Sep 02 14:10:32 2008 +0200
39.2 +++ b/src/Pure/Isar/spec_parse.ML Tue Sep 02 14:10:45 2008 +0200
39.3 @@ -11,34 +11,34 @@
39.4 val attrib: OuterLex.token list -> Attrib.src * token list
39.5 val attribs: token list -> Attrib.src list * token list
39.6 val opt_attribs: token list -> Attrib.src list * token list
39.7 - val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
39.8 - val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
39.9 - val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
39.10 - val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
39.11 - val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
39.12 - val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
39.13 + val thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
39.14 + val opt_thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
39.15 + val spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
39.16 + val named_spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
39.17 + val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
39.18 + val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
39.19 val xthm: token list -> (Facts.ref * Attrib.src list) * token list
39.20 val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
39.21 val name_facts: token list ->
39.22 - ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
39.23 + ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
39.24 val locale_mixfix: token list -> mixfix * token list
39.25 - val locale_fixes: token list -> (string * string option * mixfix) list * token list
39.26 + val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list
39.27 val locale_insts: token list ->
39.28 - (string option list * ((bstring * Attrib.src list) * string) list) * token list
39.29 + (string option list * ((Name.binding * Attrib.src list) * string) list) * token list
39.30 val class_expr: token list -> string list * token list
39.31 val locale_expr: token list -> Locale.expr * token list
39.32 val locale_keyword: token list -> string * token list
39.33 val locale_element: token list -> Element.context Locale.element * token list
39.34 val context_element: token list -> Element.context * token list
39.35 val statement: token list ->
39.36 - ((bstring * Attrib.src list) * (string * string list) list) list * token list
39.37 + ((Name.binding * Attrib.src list) * (string * string list) list) list * token list
39.38 val general_statement: token list ->
39.39 (Element.context Locale.element list * Element.statement) * OuterLex.token list
39.40 val statement_keyword: token list -> string * token list
39.41 val specification: token list ->
39.42 - (string *
39.43 - (((bstring * Attrib.src list) * string list) list * (string * string option) list)) list *
39.44 - token list
39.45 + (Name.binding *
39.46 + (((Name.binding * Attrib.src list) * string list) list *
39.47 + (Name.binding * string option) list)) list * token list
39.48 end;
39.49
39.50 structure SpecParse: SPEC_PARSE =
39.51 @@ -54,9 +54,11 @@
39.52 val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
39.53 val opt_attribs = Scan.optional attribs [];
39.54
39.55 -fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
39.56 +fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
39.57 +
39.58 fun opt_thm_name s =
39.59 - Scan.optional ((P.name -- opt_attribs || attribs >> pair "") --| P.$$$ s) ("", []);
39.60 + Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s)
39.61 + (Name.no_binding, []);
39.62
39.63 val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
39.64 val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
39.65 @@ -79,7 +81,7 @@
39.66 val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
39.67
39.68 val locale_fixes =
39.69 - P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
39.70 + P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
39.71 >> (single o P.triple1) ||
39.72 P.params >> map Syntax.no_syn) >> flat;
39.73
39.74 @@ -134,7 +136,7 @@
39.75 val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
39.76
39.77 val obtain_case =
39.78 - P.parname -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
39.79 + P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
39.80 (P.and_list1 (Scan.repeat1 P.prop) >> flat));
39.81
39.82 val general_statement =
39.83 @@ -148,6 +150,6 @@
39.84
39.85 (* specifications *)
39.86
39.87 -val specification = P.enum1 "|" (P.parname -- (P.and_list1 spec -- P.for_simple_fixes));
39.88 +val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes));
39.89
39.90 end;
40.1 --- a/src/Pure/Isar/theory_target.ML Tue Sep 02 14:10:32 2008 +0200
40.2 +++ b/src/Pure/Isar/theory_target.ML Tue Sep 02 14:10:45 2008 +0200
40.3 @@ -48,8 +48,10 @@
40.4 let
40.5 val thy = ProofContext.theory_of ctxt;
40.6 val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
40.7 - val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
40.8 - val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
40.9 + val fixes = map (fn (x, T) =>
40.10 + (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
40.11 + val assumes = map (fn A =>
40.12 + ((Name.no_binding, []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
40.13 val elems =
40.14 (if null fixes then [] else [Element.Fixes fixes]) @
40.15 (if null assumes then [] else [Element.Assumes assumes]);
40.16 @@ -118,7 +120,7 @@
40.17 |> Drule.zero_var_indexes_list;
40.18
40.19 (*thm definition*)
40.20 - val result = PureThy.name_thm true true name th'';
40.21 + val result = PureThy.name_thm true true Position.none name th'';
40.22
40.23 (*import fixes*)
40.24 val (tvars, vars) =
40.25 @@ -138,7 +140,7 @@
40.26 NONE => raise THM ("Failed to re-import result", 0, [result'])
40.27 | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
40.28 |> Goal.norm_result
40.29 - |> PureThy.name_thm false false name;
40.30 + |> PureThy.name_thm false false Position.none name;
40.31
40.32 in (result'', result) end;
40.33
40.34 @@ -154,7 +156,8 @@
40.35 val full = LocalTheory.full_name lthy;
40.36
40.37 val facts' = facts
40.38 - |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (full (fst a))) bs))
40.39 + |> map (fn (a, bs) =>
40.40 + (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs))
40.41 |> PureThy.map_facts (import_export_proof lthy);
40.42 val local_facts = PureThy.map_facts #1 facts'
40.43 |> Attrib.map_facts (Attrib.attribute_i thy);
40.44 @@ -185,11 +188,13 @@
40.45 let
40.46 val c' = Morphism.name phi c;
40.47 val rhs' = Morphism.term phi rhs;
40.48 - val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
40.49 - val arg = (c', Term.close_schematic_term rhs');
40.50 + val name = Name.name_of c;
40.51 + val name' = Name.name_of c'
40.52 + val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
40.53 + val arg = (name', Term.close_schematic_term rhs');
40.54 val similar_body = Type.similar_types (rhs, rhs');
40.55 (* FIXME workaround based on educated guess *)
40.56 - val class_global = c' = NameSpace.qualified (Class.class_prefix target) c;
40.57 + val class_global = name' = NameSpace.qualified (Class.class_prefix target) name;
40.58 in
40.59 not (is_class andalso (similar_body orelse class_global)) ?
40.60 (Context.mapping_result
40.61 @@ -201,8 +206,9 @@
40.62 Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
40.63 end;
40.64
40.65 -fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
40.66 +fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
40.67 let
40.68 + val c = Name.name_of b;
40.69 val tags = LocalTheory.group_position_of lthy;
40.70 val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
40.71 val U = map #2 xs ---> T;
40.72 @@ -225,16 +231,17 @@
40.73 val t = Term.list_comb (const, map Free xs);
40.74 in
40.75 lthy'
40.76 - |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((c, mx2), t))
40.77 + |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
40.78 |> is_class ? class_target ta (Class.declare target tags ((c, mx1), t))
40.79 - |> LocalDefs.add_def ((c, NoSyn), t)
40.80 + |> LocalDefs.add_def ((b, NoSyn), t)
40.81 end;
40.82
40.83
40.84 (* abbrev *)
40.85
40.86 -fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
40.87 +fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
40.88 let
40.89 + val c = Name.name_of b;
40.90 val tags = LocalTheory.group_position_of lthy;
40.91 val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
40.92 val target_ctxt = LocalTheory.target_of lthy;
40.93 @@ -251,7 +258,7 @@
40.94 LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs))
40.95 #-> (fn (lhs, _) =>
40.96 let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
40.97 - term_syntax ta (locale_const ta prmode tags ((c, mx2), lhs')) #>
40.98 + term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
40.99 is_class ? class_target ta (Class.abbrev target prmode tags ((c, mx1), t'))
40.100 end)
40.101 else
40.102 @@ -259,26 +266,27 @@
40.103 (Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) =>
40.104 Sign.notation true prmode [(lhs, mx3)])))
40.105 |> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd
40.106 - |> LocalDefs.fixed_abbrev ((c, NoSyn), t)
40.107 + |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
40.108 end;
40.109
40.110
40.111 (* define *)
40.112
40.113 fun define (ta as Target {target, is_locale, is_class, ...})
40.114 - kind ((c, mx), ((name, atts), rhs)) lthy =
40.115 + kind ((b, mx), ((name, atts), rhs)) lthy =
40.116 let
40.117 val thy = ProofContext.theory_of lthy;
40.118 val thy_ctxt = ProofContext.init thy;
40.119
40.120 - val name' = Thm.def_name_optional c name;
40.121 + val c = Name.name_of b;
40.122 + val name' = Name.map_name (Thm.def_name_optional c) name;
40.123 val (rhs', rhs_conv) =
40.124 LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
40.125 val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
40.126 val T = Term.fastype_of rhs;
40.127
40.128 (*const*)
40.129 - val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((c, T), mx);
40.130 + val ((lhs, local_def), lthy2) = lthy |> declare_const ta (member (op =) xs) ((b, T), mx);
40.131 val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
40.132
40.133 (*def*)
40.134 @@ -291,7 +299,7 @@
40.135 then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
40.136 else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
40.137 val (global_def, lthy3) = lthy2
40.138 - |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
40.139 + |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
40.140 val def = LocalDefs.trans_terms lthy3
40.141 [(*c == global.c xs*) local_def,
40.142 (*global.c xs == rhs'*) global_def,
40.143 @@ -318,7 +326,7 @@
40.144 (*axioms*)
40.145 val hyps = map Thm.term_of (Assumption.assms_of lthy');
40.146 fun axiom ((name, atts), props) thy = thy
40.147 - |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
40.148 + |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi (Name.name_of name) props)
40.149 |-> (fn ths => pair ((name, atts), [(ths, [])]));
40.150 in
40.151 lthy'
41.1 --- a/src/Pure/Tools/invoke.ML Tue Sep 02 14:10:32 2008 +0200
41.2 +++ b/src/Pure/Tools/invoke.ML Tue Sep 02 14:10:45 2008 +0200
41.3 @@ -8,9 +8,9 @@
41.4 signature INVOKE =
41.5 sig
41.6 val invoke: string * Attrib.src list -> Locale.expr -> string option list ->
41.7 - (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
41.8 + (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
41.9 val invoke_i: string * attribute list -> Locale.expr -> term option list ->
41.10 - (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
41.11 + (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
41.12 end;
41.13
41.14 structure Invoke: INVOKE =
41.15 @@ -60,9 +60,9 @@
41.16 | NONE => Drule.termI)) params';
41.17
41.18 val propp =
41.19 - [(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
41.20 - (("", []), map (rpair [] o Logic.mk_term) params'),
41.21 - (("", []), map (rpair [] o Element.mark_witness) prems')];
41.22 + [((Name.no_binding, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
41.23 + ((Name.no_binding, []), map (rpair [] o Logic.mk_term) params'),
41.24 + ((Name.no_binding, []), map (rpair [] o Element.mark_witness) prems')];
41.25 fun after_qed results =
41.26 Proof.end_block #>
41.27 Proof.map_context (fn ctxt =>
41.28 @@ -120,8 +120,8 @@
41.29 "schematic invocation of locale expression in proof context"
41.30 (K.tag_proof K.prf_goal)
41.31 (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
41.32 - >> (fn (((name, expr), (insts, _)), fixes) =>
41.33 - Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
41.34 + >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
41.35 + Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes)));
41.36
41.37 end;
41.38
42.1 --- a/src/Pure/axclass.ML Tue Sep 02 14:10:32 2008 +0200
42.2 +++ b/src/Pure/axclass.ML Tue Sep 02 14:10:45 2008 +0200
42.3 @@ -9,7 +9,7 @@
42.4 signature AX_CLASS =
42.5 sig
42.6 val define_class: bstring * class list -> string list ->
42.7 - ((bstring * attribute list) * term list) list -> theory -> class * theory
42.8 + ((Name.binding * attribute list) * term list) list -> theory -> class * theory
42.9 val add_classrel: thm -> theory -> theory
42.10 val add_arity: thm -> theory -> theory
42.11 val prove_classrel: class * class -> tactic -> theory -> theory
42.12 @@ -482,9 +482,10 @@
42.13 |> Sign.add_path bconst
42.14 |> Sign.no_base_names
42.15 |> PureThy.note_thmss ""
42.16 - [((introN, []), [([Drule.standard raw_intro], [])]),
42.17 - ((superN, []), [(map Drule.standard raw_classrel, [])]),
42.18 - ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
42.19 + [((Name.binding introN, []), [([Drule.standard raw_intro], [])]),
42.20 + ((Name.binding superN, []), [(map Drule.standard raw_classrel, [])]),
42.21 + ((Name.binding axiomsN, []),
42.22 + [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
42.23 ||> Sign.restore_naming def_thy;
42.24
42.25
43.1 --- a/src/Tools/induct.ML Tue Sep 02 14:10:32 2008 +0200
43.2 +++ b/src/Tools/induct.ML Tue Sep 02 14:10:45 2008 +0200
43.3 @@ -51,7 +51,7 @@
43.4 val setN: string
43.5 (*proof methods*)
43.6 val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
43.7 - val add_defs: (string option * term) option list -> Proof.context ->
43.8 + val add_defs: (Name.binding option * term) option list -> Proof.context ->
43.9 (term option list * thm list) * Proof.context
43.10 val atomize_term: theory -> term -> term
43.11 val atomize_tac: int -> tactic
43.12 @@ -63,7 +63,7 @@
43.13 val cases_tac: Proof.context -> term option list list -> thm option ->
43.14 thm list -> int -> cases_tactic
43.15 val get_inductT: Proof.context -> term option list list -> thm list list
43.16 - val induct_tac: Proof.context -> (string option * term) option list list ->
43.17 + val induct_tac: Proof.context -> (Name.binding option * term) option list list ->
43.18 (string * typ) list list -> term option list -> thm list option ->
43.19 thm list -> int -> cases_tactic
43.20 val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
43.21 @@ -552,7 +552,8 @@
43.22 fun add_defs def_insts =
43.23 let
43.24 fun add (SOME (SOME x, t)) ctxt =
43.25 - let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (("", []), t))] ctxt
43.26 + let val ([(lhs, (_, th))], ctxt') =
43.27 + LocalDefs.add_defs [((x, NoSyn), ((Name.no_binding, []), t))] ctxt
43.28 in ((SOME lhs, [th]), ctxt') end
43.29 | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
43.30 | add NONE ctxt = ((NONE, []), ctxt);
43.31 @@ -716,7 +717,7 @@
43.32 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
43.33
43.34 val def_inst =
43.35 - ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
43.36 + ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
43.37 -- Args.term) >> SOME ||
43.38 inst >> Option.map (pair NONE);
43.39
44.1 --- a/src/ZF/Tools/datatype_package.ML Tue Sep 02 14:10:32 2008 +0200
44.2 +++ b/src/ZF/Tools/datatype_package.ML Tue Sep 02 14:10:45 2008 +0200
44.3 @@ -262,7 +262,7 @@
44.4 ||> add_recursor
44.5 ||> Sign.parent_path
44.6
44.7 - val intr_names = map #2 (List.concat con_ty_lists);
44.8 + val intr_names = map (Name.binding o #2) (List.concat con_ty_lists);
44.9 val (thy1, ind_result) =
44.10 thy0 |> Ind_Package.add_inductive_i
44.11 false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
45.1 --- a/src/ZF/Tools/ind_cases.ML Tue Sep 02 14:10:32 2008 +0200
45.2 +++ b/src/ZF/Tools/ind_cases.ML Tue Sep 02 14:10:45 2008 +0200
45.3 @@ -8,7 +8,7 @@
45.4 signature IND_CASES =
45.5 sig
45.6 val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
45.7 - val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
45.8 + val inductive_cases: ((Name.binding * Attrib.src list) * string list) list -> theory -> theory
45.9 val setup: theory -> theory
45.10 end;
45.11
46.1 --- a/src/ZF/Tools/inductive_package.ML Tue Sep 02 14:10:32 2008 +0200
46.2 +++ b/src/ZF/Tools/inductive_package.ML Tue Sep 02 14:10:45 2008 +0200
46.3 @@ -29,10 +29,10 @@
46.4 (*Insert definitions for the recursive sets, which
46.5 must *already* be declared as constants in parent theory!*)
46.6 val add_inductive_i: bool -> term list * term ->
46.7 - ((bstring * term) * attribute list) list ->
46.8 + ((Name.binding * term) * attribute list) list ->
46.9 thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
46.10 val add_inductive: string list * string ->
46.11 - ((bstring * string) * Attrib.src list) list ->
46.12 + ((Name.binding * string) * Attrib.src list) list ->
46.13 (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
46.14 (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
46.15 theory -> theory * inductive_result
46.16 @@ -62,11 +62,12 @@
46.17
46.18 (*internal version, accepting terms*)
46.19 fun add_inductive_i verbose (rec_tms, dom_sum)
46.20 - intr_specs (monos, con_defs, type_intrs, type_elims) thy =
46.21 + raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
46.22 let
46.23 val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
46.24 val ctxt = ProofContext.init thy;
46.25
46.26 + val intr_specs = map (apfst (apfst Name.name_of)) raw_intr_specs;
46.27 val (intr_names, intr_tms) = split_list (map fst intr_specs);
46.28 val case_names = RuleCases.case_names intr_names;
46.29
47.1 --- a/src/ZF/Tools/primrec_package.ML Tue Sep 02 14:10:32 2008 +0200
47.2 +++ b/src/ZF/Tools/primrec_package.ML Tue Sep 02 14:10:45 2008 +0200
47.3 @@ -9,8 +9,8 @@
47.4
47.5 signature PRIMREC_PACKAGE =
47.6 sig
47.7 - val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
47.8 - val add_primrec_i: ((bstring * term) * attribute list) list -> theory -> theory * thm list
47.9 + val add_primrec: ((Name.binding * string) * Attrib.src list) list -> theory -> theory * thm list
47.10 + val add_primrec_i: ((Name.binding * term) * attribute list) list -> theory -> theory * thm list
47.11 end;
47.12
47.13 structure PrimrecPackage : PRIMREC_PACKAGE =
47.14 @@ -180,7 +180,7 @@
47.15
47.16 val (eqn_thms', thy2) =
47.17 thy1
47.18 - |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
47.19 + |> PureThy.add_thms ((map Name.name_of eqn_names ~~ eqn_thms) ~~ eqn_atts);
47.20 val (_, thy3) =
47.21 thy2
47.22 |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]