# HG changeset patch # User wenzelm # Date 1460923809 -7200 # Node ID d743bb1b6c23461ecc024ab54d6f187d7fe55612 # Parent f507e6fe1d77cad334a62208f093de10f11998ef clarified bindings; diff -r f507e6fe1d77 -r d743bb1b6c23 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Sun Apr 17 20:54:17 2016 +0200 +++ b/src/HOL/Tools/Function/function.ML Sun Apr 17 22:10:09 2016 +0200 @@ -51,12 +51,10 @@ @{attributes [nitpick_psimp]} fun note_qualified suffix attrs (fname, thms) = - Local_Theory.note ((Binding.qualify_name true fname suffix, - map (Attrib.internal o K) attrs), thms) + Local_Theory.note ((derived_name fname suffix, map (Attrib.internal o K) attrs), thms) #> apfst snd -fun add_simps fnames post sort extra_qualify label mod_binding moreatts - simps lthy = +fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = let val spec = post simps |> map (apfst (apsnd (fn ats => moreatts @ ats))) @@ -69,7 +67,7 @@ val simps_by_f = sort saved_simps fun note fname simps = - Local_Theory.note ((mod_binding (Binding.qualify_name true fname label), []), simps) #> snd + Local_Theory.note ((mod_binding (derived_name fname label), []), simps) #> snd in (saved_simps, fold2 note fnames simps_by_f lthy) end fun prepare_function do_print prep fixspec eqns config lthy = @@ -103,7 +101,6 @@ val pelims = Function_Elims.mk_partial_elim_rules lthy result - val qualify = Binding.qualify_name true defname val concealed_partial = if partials then I else Binding.concealed val addsmps = add_simps fnames post sort_cont @@ -112,19 +109,20 @@ lthy |> addsmps (concealed_partial o Binding.qualify false "partial") "psimps" concealed_partial psimp_attribs psimps - ||>> Local_Theory.notes [((concealed_partial (qualify "pinduct"), []), + ||>> Local_Theory.notes [((concealed_partial (derived_name defname "pinduct"), []), simple_pinducts |> map (fn th => ([th], [Attrib.internal (K (Rule_Cases.case_names cnames)), Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), Attrib.internal (K (Induct.induct_pred ""))])))] ||>> (apfst snd o - Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination])) + Local_Theory.note + ((Binding.concealed (derived_name defname "termination"), []), [termination])) ||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) (fnames ~~ map single cases) (* TODO: case names *) ||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ pelims) ||> (case domintros of NONE => I | SOME thms => - Local_Theory.note ((qualify "domintros", []), thms) #> snd) + Local_Theory.note ((derived_name defname "domintros", []), thms) #> snd) val info = { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps', @@ -204,8 +202,7 @@ lthy |> add_simps I "simps" I simp_attribs tsimps ||>> Local_Theory.note - ((Binding.qualify_name true defname "induct", - [Attrib.internal (K (Rule_Cases.case_names case_names))]), + ((derived_name defname "induct", [Attrib.internal (K (Rule_Cases.case_names case_names))]), tinduct) ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ telims) diff -r f507e6fe1d77 -r d743bb1b6c23 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Sun Apr 17 20:54:17 2016 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Sun Apr 17 22:10:09 2016 +0200 @@ -58,10 +58,6 @@ val profile : bool Unsynchronized.ref val PROFILE : string -> ('a -> 'b) -> 'a -> 'b val mk_acc : typ -> term -> term - val function_name : string -> string - val graph_name : string -> string - val rel_name : string -> string - val dom_name : string -> string val split_def : Proof.context -> (string -> 'a) -> term -> string * (string * typ) list * term list * term list * term val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit @@ -125,11 +121,6 @@ fun mk_acc domT R = Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R -val function_name = suffix "C" -val graph_name = suffix "_graph" -val rel_name = suffix "_rel" -val dom_name = suffix "_dom" - (* analyzing function equations *) diff -r f507e6fe1d77 -r d743bb1b6c23 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Sun Apr 17 20:54:17 2016 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Sun Apr 17 22:10:09 2016 +0200 @@ -492,14 +492,14 @@ let val f_def_binding = Thm.make_def_binding (Config.get lthy function_internals) - (Binding.map_name (suffix "_sumC") defname) + (derived_name_suffix defname "_sumC") val f_def = Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |> Syntax.check_term lthy in - Local_Theory.define - ((Binding.name (function_name fname), mixfix), ((f_def_binding, []), f_def)) lthy + lthy |> Local_Theory.define + ((Binding.name (fname ^ "C") (* FIXME proper binding *), mixfix), ((f_def_binding, []), f_def)) end fun define_recursion_relation (R_binding, R_type) qglrs clauses RCss lthy = @@ -851,7 +851,7 @@ val ((G, GIntro_thms, G_elim, G_induct), lthy) = PROFILE "def_graph" (define_graph - (Binding.map_name graph_name defname, domT --> ranT --> boolT) fvar clauses RCss) lthy + (derived_name_suffix defname "_graph", domT --> ranT --> boolT) fvar clauses RCss) lthy val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function defname (fname, mixfix) domT ranT G default) lthy @@ -861,13 +861,13 @@ val ((R, RIntro_thmss, R_elim), lthy) = PROFILE "def_rel" - (define_recursion_relation (Binding.map_name rel_name defname, domT --> domT --> boolT) + (define_recursion_relation (derived_name_suffix defname "_rel", domT --> domT --> boolT) abstract_qglrs clauses RCss) lthy val dom = mk_acc domT R val (_, lthy) = Local_Theory.abbrev Syntax.mode_default - (((Binding.map_name dom_name defname), NoSyn), dom) lthy + ((name_suffix defname "_dom", NoSyn), dom) lthy val newthy = Proof_Context.theory_of lthy val clauses = map (transfer_clause_ctx newthy) clauses diff -r f507e6fe1d77 -r d743bb1b6c23 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Sun Apr 17 20:54:17 2016 +0200 +++ b/src/HOL/Tools/Function/function_lib.ML Sun Apr 17 22:10:09 2016 +0200 @@ -9,6 +9,10 @@ sig val function_internals: bool Config.T + val derived_name: binding -> string -> binding + val name_suffix: binding -> string -> binding + val derived_name_suffix: binding -> string -> binding + val plural: string -> string -> 'a list -> string val dest_all_all: term -> term list * term @@ -34,6 +38,12 @@ val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false) +fun derived_name binding name = + Binding.reset_pos (Binding.qualify_name true binding name) + +fun name_suffix binding sffx = Binding.map_name (suffix sffx) binding +fun derived_name_suffix binding sffx = Binding.reset_pos (name_suffix binding sffx) + (* "The variable" ^ plural " is" "s are" vs *) fun plural sg pl [x] = sg diff -r f507e6fe1d77 -r d743bb1b6c23 src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Sun Apr 17 20:54:17 2016 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Sun Apr 17 22:10:09 2016 +0200 @@ -17,6 +17,9 @@ structure Partial_Function: PARTIAL_FUNCTION = struct +open Function_Lib + + (*** Context Data ***) datatype setup_data = Setup_Data of @@ -230,8 +233,7 @@ val f_bname = Binding.name_of f_binding; fun note_qualified (name, thms) = - Local_Theory.note ((Binding.qualify_name true (Binding.reset_pos f_binding) name, []), thms) - #> snd + Local_Theory.note ((derived_name f_binding name, []), thms) #> snd val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn); val (head, args) = strip_comb lhs;