clarified signature; simpler implementation in terms of function's tactic interface
authorkrauss
Wed Apr 28 17:42:37 2010 +0200 (2010-04-28)
changeset 36523a294e4ebe0a3
parent 36522 e80a95279ef6
child 36524 3909002beca5
clarified signature; simpler implementation in terms of function's tactic interface
src/HOL/Tools/Function/fun.ML
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Apr 28 16:13:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Wed Apr 28 17:42:37 2010 +0200
     1.3 @@ -7,12 +7,12 @@
     1.4  
     1.5  signature FUNCTION_FUN =
     1.6  sig
     1.7 -  val add_fun : Function_Common.function_config ->
     1.8 -    (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
     1.9 -    bool -> local_theory -> Proof.context
    1.10 -  val add_fun_cmd : Function_Common.function_config ->
    1.11 -    (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
    1.12 -    bool -> local_theory -> Proof.context
    1.13 +  val add_fun : (binding * typ option * mixfix) list ->
    1.14 +    (Attrib.binding * term) list -> Function_Common.function_config ->
    1.15 +    local_theory -> Proof.context
    1.16 +  val add_fun_cmd : (binding * string option * mixfix) list ->
    1.17 +    (Attrib.binding * string) list -> Function_Common.function_config ->
    1.18 +    local_theory -> Proof.context
    1.19  
    1.20    val setup : theory -> theory
    1.21  end
    1.22 @@ -56,15 +56,6 @@
    1.23      ()
    1.24    end
    1.25  
    1.26 -val by_pat_completeness_auto =
    1.27 -  Proof.global_future_terminal_proof
    1.28 -    (Method.Basic Pat_Completeness.pat_completeness,
    1.29 -     SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
    1.30 -
    1.31 -fun termination_by method int =
    1.32 -  Function.termination NONE
    1.33 -  #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
    1.34 -
    1.35  fun mk_catchall fixes arity_of =
    1.36    let
    1.37      fun mk_eqn ((fname, fT), _) =
    1.38 @@ -148,24 +139,32 @@
    1.39  val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
    1.40    domintros=false, partials=false, tailrec=false }
    1.41  
    1.42 -fun gen_fun add config fixes statements int lthy =
    1.43 -  lthy
    1.44 -  |> add fixes statements config
    1.45 -  |> by_pat_completeness_auto int
    1.46 -  |> Local_Theory.restore
    1.47 -  |> termination_by (SIMPLE_METHOD o Function_Common.get_termination_prover lthy) int
    1.48 +fun gen_add_fun add fixes statements config lthy =
    1.49 +  let
    1.50 +    fun pat_completeness_auto ctxt =
    1.51 +      Pat_Completeness.pat_completeness_tac ctxt 1
    1.52 +      THEN auto_tac (clasimpset_of ctxt)
    1.53 +    fun prove_termination lthy =
    1.54 +      Function.prove_termination NONE
    1.55 +        (Function_Common.get_termination_prover lthy lthy) lthy
    1.56 +  in
    1.57 +    lthy
    1.58 +    |> add fixes statements config pat_completeness_auto |> snd
    1.59 +    |> Local_Theory.restore
    1.60 +    |> prove_termination
    1.61 +  end
    1.62  
    1.63 -val add_fun = gen_fun Function.function
    1.64 -val add_fun_cmd = gen_fun Function.function_cmd
    1.65 +val add_fun = gen_add_fun Function.add_function
    1.66 +val add_fun_cmd = gen_add_fun Function.add_function_cmd
    1.67  
    1.68  
    1.69  
    1.70  local structure P = OuterParse and K = OuterKeyword in
    1.71  
    1.72  val _ =
    1.73 -  OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
    1.74 +  OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
    1.75    (function_parser fun_config
    1.76 -     >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
    1.77 +     >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config));
    1.78  
    1.79  end
    1.80