# HG changeset patch # User paulson # Date 1460991108 -3600 # Node ID 00f4461fa99f79fd676d737b5ab6f422330d4bfa # Parent 3590590699b1f3a42c5fd17f56a90b011cb6cff4# Parent 15e6ae52e91aef820181c503edbbfbcbfae65934 Merge diff -r 3590590699b1 -r 00f4461fa99f src/HOL/Eisbach/Examples.thy --- a/src/HOL/Eisbach/Examples.thy Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/Eisbach/Examples.thy Mon Apr 18 15:51:48 2016 +0100 @@ -183,7 +183,7 @@ apply prop_solver done -lemma "(\x. P x \ Q x) \ P z \ P y \ Q y" +lemma "(\x. P x \ Q x) \ P z \ P y \ Q y" apply (solves \guess_all, prop_solver\) \ \Try it without solve\ done diff -r 3590590699b1 -r 00f4461fa99f src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Apr 18 15:51:48 2016 +0100 @@ -1187,7 +1187,7 @@ " as unnamed BNF"); val (bnf_b, key) = - if Binding.eq_name (bnf_b, Binding.empty) then + if Binding.is_empty bnf_b then (case T_rhs of Type (C, Ts) => if forall (can dest_TFree) Ts then (Binding.qualified_name C, C) else err T_rhs diff -r 3590590699b1 -r 00f4461fa99f src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/Tools/Function/function.ML Mon Apr 18 15:51:48 2016 +0100 @@ -87,7 +87,7 @@ else () val ((goal_state, cont), lthy') = - Function_Mutual.prepare_function_mutual config defname fixes eqs lthy + Function_Mutual.prepare_function_mutual config defname fixes0 eqs lthy fun afterqed [[proof]] lthy = let diff -r 3590590699b1 -r 00f4461fa99f src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/Tools/Function/function_common.ML Mon Apr 18 15:51:48 2016 +0100 @@ -69,7 +69,7 @@ domintros: bool, partials: bool} type preproc = function_config -> Proof.context -> fixes -> term spec -> - (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) + term list * (thm list -> thm spec) * (thm list -> thm list list) * string list val fname_of : term -> string val mk_case_names : int -> string -> int -> string list val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> @@ -209,7 +209,7 @@ partials: bool} type preproc = function_config -> Proof.context -> fixes -> term spec -> - (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) + term list * (thm list -> thm spec) * (thm list -> thm list list) * string list val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all diff -r 3590590699b1 -r 00f4461fa99f src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Mon Apr 18 15:51:48 2016 +0100 @@ -9,8 +9,8 @@ val trace: bool Unsynchronized.ref val prepare_function : Function_Common.function_config -> binding (* defname *) - -> ((bstring * typ) * mixfix) list (* defined symbol *) - -> ((bstring * typ) list * term list * term * term) list (* specification *) + -> ((binding * typ) * mixfix) list (* defined symbol *) + -> ((string * typ) list * term list * term * term) list (* specification *) -> local_theory -> (term (* f *) * thm (* goalstate *) @@ -499,7 +499,7 @@ |> Syntax.check_term lthy in lthy |> Local_Theory.define - ((Binding.name (fname ^ "C") (* FIXME proper binding *), mixfix), ((f_def_binding, []), f_def)) + ((Binding.map_name (suffix "C") fname, mixfix), ((f_def_binding, []), f_def)) end fun define_recursion_relation (R_binding, R_type) qglrs clauses RCss lthy = @@ -826,15 +826,15 @@ let val FunctionConfig {domintros, default=default_opt, ...} = config - val default_str = the_default "%x. HOL.undefined" default_opt - val fvar = Free (fname, fT) + val default_str = the_default "%x. HOL.undefined" (* FIXME proper term!? *) default_opt + val fvar = (Binding.name_of fname, fT) val domT = domain_type fT val ranT = range_type fT val default = Syntax.parse_term lthy default_str |> Type.constraint fT |> Syntax.check_term lthy - val (globals, ctxt') = fix_globals domT ranT fvar lthy + val (globals, ctxt') = fix_globals domT ranT (Free fvar) lthy val Globals { x, h, ... } = globals @@ -843,7 +843,7 @@ val n = length abstract_qglrs fun build_tree (ClauseContext { ctxt, rhs, ...}) = - Function_Context_Tree.mk_tree (fname, fT) h ctxt rhs + Function_Context_Tree.mk_tree fvar h ctxt rhs val trees = map build_tree clauses val RCss = map find_calls trees @@ -851,13 +851,14 @@ val ((G, GIntro_thms, G_elim, G_induct), lthy) = PROFILE "def_graph" (define_graph - (derived_name_suffix defname "_graph", domT --> ranT --> boolT) fvar clauses RCss) lthy + (derived_name_suffix defname "_graph", domT --> ranT --> boolT) (Free fvar) clauses RCss) + lthy val ((f, (_, f_defthm)), 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 RCss = map (map (inst_RC lthy (Free fvar) f)) RCss + val trees = map (Function_Context_Tree.inst_tree lthy (Free fvar) f) trees val ((R, RIntro_thmss, R_elim), lthy) = PROFILE "def_rel" @@ -867,7 +868,7 @@ val dom = mk_acc domT R val (_, lthy) = Local_Theory.abbrev Syntax.mode_default - ((name_suffix defname "_dom", NoSyn), dom) lthy + ((derived_name_suffix defname "_dom", NoSyn), dom) lthy val newthy = Proof_Context.theory_of lthy val clauses = map (transfer_clause_ctx newthy) clauses @@ -880,7 +881,7 @@ mk_completeness globals clauses abstract_qglrs |> Thm.cterm_of lthy |> Thm.assume val compat = - mk_compat_proof_obligations domT ranT fvar f abstract_qglrs + mk_compat_proof_obligations domT ranT (Free fvar) f abstract_qglrs |> map (Thm.cterm_of lthy #> Thm.assume) val compat_store = store_compat_thms n compat @@ -921,5 +922,4 @@ ((f, goalstate, mk_partial_rules), lthy) end - end diff -r 3590590699b1 -r 00f4461fa99f src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/Tools/Function/function_lib.ML Mon Apr 18 15:51:48 2016 +0100 @@ -10,7 +10,6 @@ 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 @@ -41,8 +40,8 @@ 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) +fun derived_name_suffix binding sffx = + Binding.reset_pos (Binding.map_name (suffix sffx) binding) (* "The variable" ^ plural " is" "s are" vs *) diff -r 3590590699b1 -r 00f4461fa99f src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Mon Apr 18 15:51:48 2016 +0100 @@ -8,7 +8,7 @@ sig val prepare_function_mutual : Function_Common.function_config -> binding (* defname *) - -> ((string * typ) * mixfix) list + -> ((binding * typ) * mixfix) list -> term list -> local_theory -> ((thm (* goalstate *) @@ -27,7 +27,8 @@ datatype mutual_part = MutualPart of {i : int, i' : int, - fvar : string * typ, + fname : binding, + fT : typ, cargTs: typ list, f_def: term, @@ -37,7 +38,8 @@ datatype mutual_info = Mutual of {n : int, n' : int, - fsum_var : string * typ, + fsum_name : binding, + fsum_type: typ, ST: typ, RST: typ, @@ -52,8 +54,8 @@ if n < 5 then fst (chop n ["P","Q","R","S"]) else map (fn i => "P" ^ string_of_int i) (1 upto n) -fun get_part fname = - the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) +fun get_part f = + the o find_first (fn (MutualPart {fname, ...}) => Binding.name_of fname = f) (* FIXME *) fun mk_prod_abs e (t1, t2) = @@ -69,15 +71,13 @@ let val num = length fs val fqgars = map (split_def ctxt (K true)) eqs - val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars - |> AList.lookup (op =) #> the + fun arity_of fname = + the (get_first (fn (f, _, _, args, _) => + if f = Binding.name_of fname then SOME (length args) else NONE) fqgars) fun curried_types (fname, fT) = - let - val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) - in - (caTs, uaTs ---> body_type fT) - end + let val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) + in (caTs, uaTs ---> body_type fT) end val (caTss, resultTs) = split_list (map curried_types fs) val argTs = map (foldr1 HOLogic.mk_prodT) caTss @@ -88,13 +88,12 @@ val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs + val fsum_name = derived_name_suffix defname "_sum" + val ([fsum_var_name], _) = Variable.add_fixes_binding [fsum_name] ctxt val fsum_type = ST --> RST - - 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 = + fun define (fname, fT) caTs resultT i = let val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 @@ -102,9 +101,11 @@ val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) - val rew = (n, fold_rev lambda vars f_exp) + val rew = (Binding.name_of fname, fold_rev lambda vars f_exp) in - (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) + (MutualPart + {i = i, i' = i', fname = fname, fT = fT, cargTs = caTs, + f_def = def, f = NONE, f_defthm = NONE}, rew) end val (parts, rews) = split_list (@{map 4} define fs caTss resultTs (1 upto num)) @@ -121,33 +122,28 @@ val qglrs = map convert_eqs fqgars in - Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, - parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} + Mutual {n = num, n' = n', fsum_name = fsum_name, fsum_type = fsum_type, + ST = ST, RST = RST, parts = parts, fqgars = fqgars, qglrs = qglrs, fsum = NONE} end fun define_projections fixes mutual fsum lthy = let - fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = + fun def ((MutualPart {i=i, i'=i', fname, fT, cargTs, f_def, ...}), (_, mixfix)) lthy = let - val def_binding = - if Config.get lthy function_internals then (Binding.name (Thm.def_name fname), []) - else Attrib.empty_binding + val def_binding = Thm.make_def_binding (Config.get lthy function_internals) fname val ((f, (_, f_defthm)), lthy') = Local_Theory.define - ((Binding.name fname, mixfix), - (def_binding, Term.subst_bound (fsum, f_def))) lthy + ((fname, mixfix), ((def_binding, []), Term.subst_bound (fsum, f_def))) lthy in - (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, - f=SOME f, f_defthm=SOME f_defthm }, - lthy') + (MutualPart {i = i, i' = i', fname = fname, fT = fT, cargTs = cargTs, + f_def = f_def, f = SOME f, f_defthm = SOME f_defthm}, lthy') end - val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual + val Mutual {n, n', fsum_name, fsum_type, ST, RST, parts, fqgars, qglrs, ...} = mutual val (parts', lthy') = fold_map def (parts ~~ fixes) lthy in - (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts', - fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, - lthy') + (Mutual {n = n, n' = n', fsum_name = fsum_name, fsum_type = fsum_type, ST = ST, + RST = RST, parts = parts', fqgars = fqgars, qglrs = qglrs, fsum = SOME fsum}, lthy') end fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = @@ -305,11 +301,11 @@ fun prepare_function_mutual config defname fixes eqss lthy = let - val mutual as Mutual {fsum_var=(n, T), qglrs, ...} = + val mutual as Mutual {fsum_name, fsum_type, qglrs, ...} = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) val ((fsum, goalstate, cont), lthy') = - Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy + Function_Core.prepare_function config defname [((fsum_name, fsum_type), NoSyn)] qglrs lthy val (mutual', lthy'') = define_projections fixes mutual fsum lthy' diff -r 3590590699b1 -r 00f4461fa99f src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/Tools/Function/partial_function.ML Mon Apr 18 15:51:48 2016 +0100 @@ -246,7 +246,7 @@ val tupleT = foldl1 HOLogic.mk_prodT aTs; val fT_uc = tupleT :: bTs ---> body_type fT; val f_uc = Var ((f_bname, 0), fT_uc); - val x_uc = Var (("x", 0), tupleT); + val x_uc = Var (("x", 1), tupleT); val uncurry = lambda head (uncurry_n arity head); val curry = lambda f_uc (curry_n arity f_uc); diff -r 3590590699b1 -r 00f4461fa99f src/HOL/ex/Functions.thy --- a/src/HOL/ex/Functions.thy Mon Apr 18 15:40:55 2016 +0100 +++ b/src/HOL/ex/Functions.thy Mon Apr 18 15:51:48 2016 +0100 @@ -489,7 +489,7 @@ | "f4 _ _ = False" -subsubsection \Polymorphic partial_function\ +subsubsection \Polymorphic partial-function\ partial_function (option) f5 :: "'a list \ 'a option" where