# HG changeset patch # User krauss # Date 1272469357 -7200 # Node ID a294e4ebe0a3ef7dc3dc9c0d547c0a980fe48252 # Parent e80a95279ef63ff40f3babd28ca131dd3c033750 clarified signature; simpler implementation in terms of function's tactic interface diff -r e80a95279ef6 -r a294e4ebe0a3 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Wed Apr 28 16:13:17 2010 +0200 +++ b/src/HOL/Tools/Function/fun.ML Wed Apr 28 17:42:37 2010 +0200 @@ -7,12 +7,12 @@ signature FUNCTION_FUN = sig - val add_fun : Function_Common.function_config -> - (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> - bool -> local_theory -> Proof.context - val add_fun_cmd : Function_Common.function_config -> - (binding * string option * mixfix) list -> (Attrib.binding * string) list -> - bool -> local_theory -> Proof.context + val add_fun : (binding * typ option * mixfix) list -> + (Attrib.binding * term) list -> Function_Common.function_config -> + local_theory -> Proof.context + val add_fun_cmd : (binding * string option * mixfix) list -> + (Attrib.binding * string) list -> Function_Common.function_config -> + local_theory -> Proof.context val setup : theory -> theory end @@ -56,15 +56,6 @@ () end -val by_pat_completeness_auto = - Proof.global_future_terminal_proof - (Method.Basic Pat_Completeness.pat_completeness, - SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) - -fun termination_by method int = - Function.termination NONE - #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int - fun mk_catchall fixes arity_of = let fun mk_eqn ((fname, fT), _) = @@ -148,24 +139,32 @@ val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, partials=false, tailrec=false } -fun gen_fun add config fixes statements int lthy = - lthy - |> add fixes statements config - |> by_pat_completeness_auto int - |> Local_Theory.restore - |> termination_by (SIMPLE_METHOD o Function_Common.get_termination_prover lthy) int +fun gen_add_fun add fixes statements config lthy = + let + fun pat_completeness_auto ctxt = + Pat_Completeness.pat_completeness_tac ctxt 1 + THEN auto_tac (clasimpset_of ctxt) + fun prove_termination lthy = + Function.prove_termination NONE + (Function_Common.get_termination_prover lthy lthy) lthy + in + lthy + |> add fixes statements config pat_completeness_auto |> snd + |> Local_Theory.restore + |> prove_termination + end -val add_fun = gen_fun Function.function -val add_fun_cmd = gen_fun Function.function_cmd +val add_fun = gen_add_fun Function.add_function +val add_fun_cmd = gen_add_fun Function.add_function_cmd local structure P = OuterParse and K = OuterKeyword in val _ = - OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl + OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl (function_parser fun_config - >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements)); + >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config)); end