--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sun Apr 17 20:54:17 2016 +0200
@@ -1822,13 +1822,13 @@
(plugins, friend, transfer)
end;
-fun add_function name parsed_eq lthy =
+fun add_function binding parsed_eq lthy =
let
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt;
val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
- Function.add_function [(Binding.concealed (Binding.name name), NONE, NoSyn)]
+ Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
[(apfst Binding.concealed Attrib.empty_binding, parsed_eq)]
Function_Common.default_config pat_completeness_auto lthy;
in
@@ -1847,7 +1847,7 @@
mk_Trueprop_eq (betapply (inner_fp_free, arg), betapply (explored_rhs, arg));
val ((inner_fp_name, (pelim, pinduct, psimp)), lthy') =
- add_function inner_fp_name0 inner_fp_eq lthy;
+ add_function (Binding.name inner_fp_name0) inner_fp_eq lthy;
fun mk_triple elim induct simp = ([elim], [induct], [simp]);
@@ -1870,7 +1870,7 @@
else
prepare_termin ();
- val inner_fp_const = (inner_fp_name, fastype_of explored_rhs)
+ val inner_fp_const = (Binding.name_of inner_fp_name, fastype_of explored_rhs)
|>> Proof_Context.read_const {proper = true, strict = false} lthy'
|> (fn (Const (s, _), T) => Const (s, T));
in
--- a/src/HOL/Tools/Function/function.ML Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML Sun Apr 17 20:54:17 2016 +0200
@@ -51,7 +51,7 @@
@{attributes [nitpick_psimp]}
fun note_qualified suffix attrs (fname, thms) =
- Local_Theory.note ((Binding.qualify true fname (Binding.name suffix),
+ Local_Theory.note ((Binding.qualify_name true fname suffix,
map (Attrib.internal o K) attrs), thms)
#> apfst snd
@@ -68,13 +68,9 @@
val saved_simps = maps snd saved_spec_simps
val simps_by_f = sort saved_simps
- fun add_for_f fname simps =
- Local_Theory.note
- ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
- #> snd
- in
- (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
- end
+ fun note fname simps =
+ Local_Theory.note ((mod_binding (Binding.qualify_name true 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 =
let
@@ -83,8 +79,12 @@
val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
- val fnames = map (fst o fst) fixes
- val defname = space_implode "_" fnames
+ val fnames = map (fst o fst) fixes0
+ val f_base_names = map (fst o fst) fixes
+ val defname =
+ (case fixes0 of
+ [((b, _), _)] => b
+ | _ => Binding.name (space_implode "_" f_base_names))
val FunctionConfig {partials, default, ...} = config
val _ =
@@ -103,8 +103,7 @@
val pelims = Function_Elims.mk_partial_elim_rules lthy result
- fun qualify n = Binding.name n
- |> Binding.qualify true defname
+ 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
@@ -118,13 +117,17 @@
[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]))
- ||>> 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)
+ ||>> (apfst snd o
+ Local_Theory.note ((Binding.concealed (qualify "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 ((qualify "domintros", []), thms) #> snd)
- val info = { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
+ val info =
+ { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
pelims=pelims',elims=NONE}
@@ -135,7 +138,7 @@
in
(info,
lthy |> Local_Theory.declaration {syntax = false, pervasive = false}
- (add_function_data o transform_function_data info))
+ (fn phi => add_function_data (transform_function_data phi info)))
end
in
((goal_state, afterqed), lthy')
@@ -197,18 +200,15 @@
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
val telims = map (map remove_domain_condition) pelims
-
- fun qualify n = Binding.name n
- |> Binding.qualify true defname
-
in
lthy
|> add_simps I "simps" I simp_attribs tsimps
||>> Local_Theory.note
- ((qualify "induct",
+ ((Binding.qualify_name true 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)
+ ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1])
+ (fnames ~~ telims)
|-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
@@ -217,7 +217,7 @@
(info',
lthy
|> Local_Theory.declaration {syntax = false, pervasive = false}
- (add_function_data o transform_function_data info')
+ (fn phi => add_function_data (transform_function_data phi info'))
|> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
end)
end
@@ -291,5 +291,4 @@
"prove termination of a recursive function"
(Scan.option Parse.term >> termination_cmd)
-
end
--- a/src/HOL/Tools/Function/function_common.ML Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Sun Apr 17 20:54:17 2016 +0200
@@ -8,11 +8,11 @@
sig
type info =
{is_partial : bool,
- defname : string,
+ defname : binding,
(*contains no logical entities: invariant under morphisms:*)
add_simps : (binding -> binding) -> string -> (binding -> binding) ->
Token.src list -> thm list -> local_theory -> thm list * local_theory,
- fnames : string list,
+ fnames : binding list,
case_names : string list,
fs : term list,
R : term,
@@ -32,11 +32,11 @@
type info =
{is_partial : bool,
- defname : string,
+ defname : binding,
(*contains no logical entities: invariant under morphisms:*)
add_simps : (binding -> binding) -> string -> (binding -> binding) ->
Token.src list -> thm list -> local_theory -> thm list * local_theory,
- fnames : string list,
+ fnames : binding list,
case_names : string list,
fs : term list,
R : term,
@@ -98,7 +98,7 @@
pelims : thm list list,
termination : thm,
domintros : thm list option}
- val transform_function_data : info -> morphism -> info
+ val transform_function_data : morphism -> info -> info
val import_function_data : term -> Proof.context -> info option
val import_last_function : Proof.context -> info option
val default_config : function_config
@@ -300,19 +300,18 @@
termination : thm,
domintros : thm list option}
-fun transform_function_data ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
- simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) phi =
+fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
+ simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) =
let
val term = Morphism.term phi
val thm = Morphism.thm phi
val fact = Morphism.fact phi
- val name = Binding.name_of o Morphism.binding phi o Binding.name
in
{ add_simps = add_simps, case_names = case_names, fnames = fnames,
fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
pinducts = fact pinducts, simps = Option.map fact simps,
inducts = Option.map fact inducts, termination = thm termination,
- defname = name defname, is_partial=is_partial, cases = fact cases,
+ defname = Morphism.binding phi defname, is_partial=is_partial, cases = fact cases,
elims = Option.map (map fact) elims, pelims = map fact pelims }
end
@@ -333,7 +332,7 @@
val inst_morph = lift_morphism ctxt o Thm.instantiate
fun match (trm, data) =
- SOME (transform_function_data data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))))
+ SOME (transform_function_data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))) data)
handle Pattern.MATCH => NONE
in
get_first match (Item_Net.retrieve (get_functions ctxt) t)
--- a/src/HOL/Tools/Function/function_core.ML Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Sun Apr 17 20:54:17 2016 +0200
@@ -8,7 +8,7 @@
sig
val trace: bool Unsynchronized.ref
val prepare_function : Function_Common.function_config
- -> string (* defname *)
+ -> binding (* defname *)
-> ((bstring * typ) * mixfix) list (* defined symbol *)
-> ((bstring * typ) list * term list * term * term) list (* specification *)
-> local_theory
@@ -469,9 +469,9 @@
((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
end
-fun define_graph (G_name, G_type) fvar clauses RCss lthy =
+fun define_graph (G_binding, G_type) fvar clauses RCss lthy =
let
- val G = Free (G_name, G_type)
+ val G = Free (Binding.name_of G_binding, G_type)
fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
let
fun mk_h_assm (rcfix, rcassm, rcarg) =
@@ -486,28 +486,27 @@
end
val G_intros = map2 mk_GIntro clauses RCss
- in
- inductive_def ((Binding.name G_name, G_type), NoSyn) G_intros lthy
- end
+ in inductive_def ((G_binding, G_type), NoSyn) G_intros lthy end
-fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
+fun define_function defname (fname, mixfix) domT ranT G default lthy =
let
+ val f_def_binding =
+ Thm.make_def_binding (Config.get lthy function_internals)
+ (Binding.map_name (suffix "_sumC") defname)
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
- val def_binding =
- if Config.get lthy function_internals then (Binding.name fdefname, [])
- else Attrib.empty_binding
in
Local_Theory.define
- ((Binding.name (function_name fname), mixfix), (def_binding, f_def)) lthy
+ ((Binding.name (function_name fname), mixfix), ((f_def_binding, []), f_def)) lthy
end
-fun define_recursion_relation (R_name, R_type) qglrs clauses RCss lthy =
+fun define_recursion_relation (R_binding, R_type) qglrs clauses RCss lthy =
let
+ val R = Free (Binding.name_of R_binding, R_type)
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
- HOLogic.mk_Trueprop (Free (R_name, R_type) $ rcarg $ lhs)
+ HOLogic.mk_Trueprop (R $ rcarg $ lhs)
|> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev (Logic.all o Free) rcfix
@@ -517,7 +516,7 @@
val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
val ((R, RIntro_thms, R_elim, _), lthy) =
- inductive_def ((Binding.name R_name, R_type), NoSyn) (flat R_intross) lthy
+ inductive_def ((R_binding, R_type), NoSyn) (flat R_intross) lthy
in
((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
end
@@ -851,22 +850,24 @@
val ((G, GIntro_thms, G_elim, G_induct), lthy) =
PROFILE "def_graph"
- (define_graph (graph_name defname, domT --> ranT --> boolT) fvar clauses RCss) lthy
+ (define_graph
+ (Binding.map_name graph_name defname, domT --> ranT --> boolT) fvar clauses RCss) lthy
val ((f, (_, f_defthm)), lthy) =
- PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
+ PROFILE "def_fun" (define_function defname (fname, mixfix) domT ranT G default) lthy
val RCss = map (map (inst_RC lthy fvar f)) RCss
val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees
val ((R, RIntro_thmss, R_elim), lthy) =
PROFILE "def_rel"
- (define_recursion_relation (rel_name defname, domT --> domT --> boolT)
+ (define_recursion_relation (Binding.map_name rel_name defname, domT --> domT --> boolT)
abstract_qglrs clauses RCss) lthy
val dom = mk_acc domT R
val (_, lthy) =
- Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), dom) lthy
+ Local_Theory.abbrev Syntax.mode_default
+ (((Binding.map_name dom_name defname), NoSyn), dom) lthy
val newthy = Proof_Context.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
--- a/src/HOL/Tools/Function/mutual.ML Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Sun Apr 17 20:54:17 2016 +0200
@@ -7,7 +7,7 @@
signature FUNCTION_MUTUAL =
sig
val prepare_function_mutual : Function_Common.function_config
- -> string (* defname *)
+ -> binding (* defname *)
-> ((string * typ) * mixfix) list
-> term list
-> local_theory
@@ -90,7 +90,8 @@
val fsum_type = ST --> RST
- val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
+ val ([fsum_var_name], _) =
+ Variable.add_fixes_binding [Binding.map_name (suffix "_sum") defname] ctxt
val fsum_var = (fsum_var_name, fsum_type)
fun define (fvar as (n, _)) caTs resultT i =