more explicit indication of def names;
authorwenzelm
Tue Mar 13 20:04:24 2012 +0100 (2012-03-13)
changeset 469093c73a121a387
parent 46908 3553cb65c66c
child 46910 3e068ef04b42
more explicit indication of def names;
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/inductive_set.ML
src/Pure/Proof/extraction.ML
src/Tools/interpretation_with_defs.ML
src/Tools/misc_legacy.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 13 17:17:52 2012 +0000
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 13 20:04:24 2012 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4      fun mk_const (b, T, _) = Const (Sign.full_name thy b, T)
     1.5      val consts = map mk_const decls
     1.6      fun mk_def c (b, t, _) =
     1.7 -      (Binding.suffix_name "_def" b, Logic.mk_equals (c, t))
     1.8 +      (Thm.def_binding b, Logic.mk_equals (c, t))
     1.9      val defs = map2 mk_def consts specs
    1.10      val (def_thms, thy) =
    1.11        Global_Theory.add_defs false (map Thm.no_attributes defs) thy
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 13 17:17:52 2012 +0000
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 13 20:04:24 2012 +0100
     2.3 @@ -151,7 +151,7 @@
     2.4      (* register constant definitions *)
     2.5      val (fixdef_thms, thy) =
     2.6        (Global_Theory.add_defs false o map Thm.no_attributes)
     2.7 -        (map (Binding.suffix_name "_def") binds ~~ eqns) thy
     2.8 +        (map Thm.def_binding binds ~~ eqns) thy
     2.9  
    2.10      (* prove applied version of definitions *)
    2.11      fun prove_proj (lhs, rhs) =
    2.12 @@ -232,7 +232,7 @@
    2.13      val typ = Term.fastype_of rhs
    2.14      val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy
    2.15      val eqn = Logic.mk_equals (const, rhs)
    2.16 -    val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn)
    2.17 +    val def = Thm.no_attributes (Thm.def_binding bind, eqn)
    2.18      val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy
    2.19    in
    2.20      ((const, def_thm), thy)
     3.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Tue Mar 13 17:17:52 2012 +0000
     3.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Tue Mar 13 20:04:24 2012 +0100
     3.3 @@ -195,7 +195,7 @@
     3.4      val ((_, (_, below_ldef)), lthy) = thy
     3.5        |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
     3.6        |> Specification.definition (NONE,
     3.7 -          ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn))
     3.8 +          ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn))
     3.9      val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
    3.10      val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
    3.11      val thy = lthy
     4.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Tue Mar 13 17:17:52 2012 +0000
     4.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Tue Mar 13 20:04:24 2012 +0100
     4.3 @@ -134,7 +134,7 @@
     4.4          Abs ("t", Term.itselfT newT,
     4.5            mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT)))
     4.6  
     4.7 -    val name_def = Binding.suffix_name "_def" name
     4.8 +    val name_def = Thm.def_binding name
     4.9      val emb_bind = (Binding.prefix_name "emb_" name_def, [])
    4.10      val prj_bind = (Binding.prefix_name "prj_" name_def, [])
    4.11      val defl_bind = (Binding.prefix_name "defl_" name_def, [])
     5.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 13 17:17:52 2012 +0000
     5.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 13 20:04:24 2012 +0100
     5.3 @@ -141,7 +141,7 @@
     5.4  
     5.5      fun one_def (Free(n,_)) r =
     5.6            let val b = Long_Name.base_name n
     5.7 -          in ((Binding.name (b^"_def"), []), r) end
     5.8 +          in ((Binding.name (Thm.def_name b), []), r) end
     5.9        | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"
    5.10      fun defs [] _ = []
    5.11        | defs (l::[]) r = [one_def l r]
     6.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 13 17:17:52 2012 +0000
     6.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 13 20:04:24 2012 +0100
     6.3 @@ -394,7 +394,7 @@
     6.4      fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T);
     6.5      val consts = map mk_const decls;
     6.6      fun mk_def c (b, t, mx) =
     6.7 -      (Binding.suffix_name "_def" b, Logic.mk_equals (c, t));
     6.8 +      (Thm.def_binding b, Logic.mk_equals (c, t));
     6.9      val defs = map2 mk_def consts specs;
    6.10      val (def_thms, thy) =
    6.11        Global_Theory.add_defs false (map Thm.no_attributes defs) thy;
     7.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Mar 13 17:17:52 2012 +0000
     7.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Mar 13 20:04:24 2012 +0100
     7.3 @@ -235,7 +235,7 @@
     7.4          val lhs = list_comb (Const (cname, constrT), l_args);
     7.5          val rhs = mk_univ_inj r_args n i;
     7.6          val def = Logic.mk_equals (lhs, Const (Abs_name, Univ_elT --> T) $ rhs);
     7.7 -        val def_name = Long_Name.base_name cname ^ "_def";
     7.8 +        val def_name = Thm.def_name (Long_Name.base_name cname);
     7.9          val eqn =
    7.10            HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs));
    7.11          val ([def_thm], thy') =
    7.12 @@ -345,7 +345,7 @@
    7.13          val fTs = map fastype_of fs;
    7.14          val defs =
    7.15            map (fn (rec_name, (T, iso_name)) =>
    7.16 -            (Binding.name (Long_Name.base_name iso_name ^ "_def"),
    7.17 +            (Binding.name (Thm.def_name (Long_Name.base_name iso_name)),
    7.18                Logic.mk_equals (Const (iso_name, T --> Univ_elT),
    7.19                  list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
    7.20          val (def_thms, thy') =
     8.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Tue Mar 13 17:17:52 2012 +0000
     8.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Tue Mar 13 20:04:24 2012 +0100
     8.3 @@ -233,7 +233,7 @@
     8.4        |> (Global_Theory.add_defs false o map Thm.no_attributes)
     8.5            (map
     8.6              (fn ((((name, comb), set), T), T') =>
     8.7 -              (Binding.name (Long_Name.base_name name ^ "_def"),
     8.8 +              (Binding.name (Thm.def_name (Long_Name.base_name name)),
     8.9                  Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
    8.10                   (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
    8.11                     (set $ Free ("x", T) $ Free ("y", T')))))))
    8.12 @@ -314,7 +314,7 @@
    8.13              val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
    8.14              val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
    8.15              val def =
    8.16 -              (Binding.name (Long_Name.base_name name ^ "_def"),
    8.17 +              (Binding.name (Thm.def_name (Long_Name.base_name name)),
    8.18                  Logic.mk_equals (Const (name, caseT),
    8.19                    fold_rev lambda fns1
    8.20                      (list_comb (reccomb,
     9.1 --- a/src/HOL/Tools/Function/mutual.ML	Tue Mar 13 17:17:52 2012 +0000
     9.2 +++ b/src/HOL/Tools/Function/mutual.ML	Tue Mar 13 20:04:24 2012 +0100
     9.3 @@ -134,7 +134,7 @@
     9.4          val ((f, (_, f_defthm)), lthy') =
     9.5            Local_Theory.define
     9.6              ((Binding.name fname, mixfix),
     9.7 -              ((Binding.conceal (Binding.name (fname ^ "_def")), []),
     9.8 +              ((Binding.conceal (Binding.name (Thm.def_name fname)), []),
     9.9                Term.subst_bound (fsum, f_def))) lthy
    9.10        in
    9.11          (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
    10.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Mar 13 17:17:52 2012 +0000
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Mar 13 20:04:24 2012 +0100
    10.3 @@ -1152,7 +1152,7 @@
    10.4          val def = Logic.mk_equals (lhs, predterm)
    10.5          val ([definition], thy') = thy |>
    10.6            Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
    10.7 -          Global_Theory.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
    10.8 +          Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
    10.9          val ctxt' = Proof_Context.init_global thy'
   10.10          val rules as ((intro, elim), _) =
   10.11            create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Mar 13 17:17:52 2012 +0000
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Mar 13 20:04:24 2012 +0100
    11.3 @@ -87,7 +87,7 @@
    11.4        val def = Logic.mk_equals (lhs, atom)
    11.5        val ([definition], thy') = thy
    11.6          |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
    11.7 -        |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
    11.8 +        |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
    11.9      in
   11.10        (lhs, ((full_constname, [definition]) :: defs, thy'))
   11.11      end
   11.12 @@ -249,7 +249,7 @@
   11.13              val def = Logic.mk_equals (lhs, abs_arg')
   11.14              val ([definition], thy') = thy
   11.15                |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
   11.16 -              |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
   11.17 +              |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
   11.18            in
   11.19              (list_comb (Logic.varify_global const, vars),
   11.20                ((full_constname, [definition])::new_defs, thy'))
    12.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Mar 13 17:17:52 2012 +0000
    12.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Mar 13 20:04:24 2012 +0100
    12.3 @@ -45,7 +45,7 @@
    12.4        quote str ^ " differs from declaration " ^ name ^ pos)
    12.5    end
    12.6  
    12.7 -fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
    12.8 +fun gen_quotient_def prep_vars prep_term (raw_var, ((name, atts), (lhs_raw, rhs_raw))) lthy =
    12.9    let
   12.10      val (vars, ctxt) = prep_vars (the_list raw_var) lthy
   12.11      val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
   12.12 @@ -69,7 +69,8 @@
   12.13      val (_, prop') = Local_Defs.cert_def lthy prop
   12.14      val (_, newrhs) = Local_Defs.abs_def prop'
   12.15  
   12.16 -    val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy
   12.17 +    val ((trm, (_ , thm)), lthy') =
   12.18 +      Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
   12.19  
   12.20      (* data storage *)
   12.21      val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    13.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Tue Mar 13 17:17:52 2012 +0000
    13.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Mar 13 20:04:24 2012 +0100
    13.3 @@ -109,9 +109,9 @@
    13.4        | SOME morphs => morphs)
    13.5  
    13.6      val ((abs_t, (_, abs_def)), lthy2) = lthy1
    13.7 -      |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
    13.8 +      |> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm))
    13.9      val ((rep_t, (_, rep_def)), lthy3) = lthy2
   13.10 -      |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
   13.11 +      |> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm))
   13.12  
   13.13      (* quot_type theorem *)
   13.14      val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
    14.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Mar 13 17:17:52 2012 +0000
    14.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Tue Mar 13 20:04:24 2012 +0100
    14.3 @@ -371,7 +371,7 @@
    14.4        val (wfrec,_) = USyntax.strip_comb rhs
    14.5  in
    14.6  fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
    14.7 - let val def_name = Long_Name.base_name fid ^ "_def"
    14.8 + let val def_name = Thm.def_name (Long_Name.base_name fid)
    14.9       val wfrec_R_M =  map_types poly_tvars
   14.10                            (wfrec $ map_types poly_tvars R)
   14.11                        $ functional
   14.12 @@ -537,7 +537,7 @@
   14.13       val ([def0], theory) =
   14.14         thy
   14.15         |> Global_Theory.add_defs false
   14.16 -            [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
   14.17 +            [Thm.no_attributes (Binding.name (Thm.def_name fid), defn)]
   14.18       val def = Thm.unvarify_global def0;
   14.19       val dummy =
   14.20         if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
    15.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Mar 13 17:17:52 2012 +0000
    15.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Mar 13 20:04:24 2012 +0100
    15.3 @@ -498,7 +498,7 @@
    15.4      val (defs, lthy2) = lthy1
    15.5        |> Local_Theory.conceal  (* FIXME ?? *)
    15.6        |> fold_map Local_Theory.define
    15.7 -        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    15.8 +        (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
    15.9             fold_rev lambda params (HOLogic.Collect_const U $
   15.10               HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
   15.11             (cnames_syn ~~ cs_info ~~ preds))
    16.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 13 17:17:52 2012 +0000
    16.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 13 20:04:24 2012 +0100
    16.3 @@ -728,7 +728,7 @@
    16.4                         (chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
    16.5                           (chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
    16.6                             (chtype [T --> propT] Proofterm.reflexive_axm %> f) %%
    16.7 -                           PAxm (cname ^ "_def", eqn,
    16.8 +                           PAxm (Thm.def_name cname, eqn,
    16.9                               SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
   16.10                      val corr_prop = Reconstruct.prop_of corr_prf';
   16.11                      val corr_prf'' =
   16.12 @@ -792,7 +792,8 @@
   16.13               val (def_thms, thy') = if t = nullt then ([], thy) else
   16.14                 thy
   16.15                 |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
   16.16 -               |> Global_Theory.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
   16.17 +               |> Global_Theory.add_defs false
   16.18 +                  [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
   16.19                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
   16.20             in
   16.21               thy'
    17.1 --- a/src/Tools/interpretation_with_defs.ML	Tue Mar 13 17:17:52 2012 +0000
    17.2 +++ b/src/Tools/interpretation_with_defs.ML	Tue Mar 13 20:04:24 2012 +0100
    17.3 @@ -45,8 +45,8 @@
    17.4  
    17.5      val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs
    17.6        |> Syntax.check_terms defs_ctxt;
    17.7 -    val defs = map2 (fn (binding_thm, (binding_syn, _)) => fn rhs =>
    17.8 -      (binding_syn, (binding_thm, rhs))) raw_defs rhss;
    17.9 +    val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
   17.10 +      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
   17.11  
   17.12      val (def_eqns, theory') = theory
   17.13        |> Named_Target.theory_init
    18.1 --- a/src/Tools/misc_legacy.ML	Tue Mar 13 17:17:52 2012 +0000
    18.2 +++ b/src/Tools/misc_legacy.ML	Tue Mar 13 20:04:24 2012 +0100
    18.3 @@ -96,7 +96,7 @@
    18.4  fun mk_defpair (lhs, rhs) =
    18.5    (case Term.head_of lhs of
    18.6      Const (name, _) =>
    18.7 -      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
    18.8 +      (Thm.def_name (Long_Name.base_name name), Logic.mk_equals (lhs, rhs))
    18.9    | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   18.10  
   18.11