1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Sep 18 10:57:30 2008 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Sep 18 12:13:50 2008 +0200
     1.3 @@ -26,6 +26,22 @@
     1.4  val rel_name = suffix "_rel"
     1.5  val dom_name = suffix "_dom"
     1.6  
     1.7 +(* Termination rules *)
     1.8 +
     1.9 +structure TerminationRule = GenericDataFun
    1.10 +(
    1.11 +  type T = thm list
    1.12 +  val empty = []
    1.13 +  val extend = I
    1.14 +  fun merge _ = Thm.merge_thms
    1.15 +);
    1.16 +
    1.17 +val get_termination_rules = TerminationRule.get
    1.18 +val store_termination_rule = TerminationRule.map o cons
    1.19 +val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
    1.20 +
    1.21 +
    1.22 +(* Function definition result data *)
    1.23  
    1.24  datatype fundef_result =
    1.25    FundefResult of
    1.26 @@ -119,27 +135,33 @@
    1.27  
    1.28  val all_fundef_data = NetRules.rules o FundefData.get
    1.29  
    1.30 +fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
    1.31 +    FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
    1.32 +    #> store_termination_rule termination
    1.33 +
    1.34 +
    1.35 +(* Simp rules for termination proofs *)
    1.36 +
    1.37  structure TerminationSimps = NamedThmsFun
    1.38  (
    1.39    val name = "termination_simp" 
    1.40    val description = "Simplification rule for termination proofs"
    1.41  );
    1.42  
    1.43 -structure TerminationRule = GenericDataFun
    1.44 +
    1.45 +(* Default Termination Prover *)
    1.46 +
    1.47 +structure TerminationProver = GenericDataFun
    1.48  (
    1.49 -  type T = thm list
    1.50 -  val empty = []
    1.51 +  type T = (Proof.context -> Method.method)
    1.52 +  val empty = (fn _ => error "Termination prover not configured")
    1.53    val extend = I
    1.54 -  fun merge _ = Thm.merge_thms
    1.55 +  fun merge _ (a,b) = b (* FIXME *)
    1.56  );
    1.57  
    1.58 -val get_termination_rules = TerminationRule.get
    1.59 -val store_termination_rule = TerminationRule.map o cons
    1.60 -val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
    1.61 +val set_termination_prover = TerminationProver.put
    1.62 +val get_termination_prover = TerminationProver.get
    1.63  
    1.64 -fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
    1.65 -    FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
    1.66 -    #> store_termination_rule termination
    1.67  
    1.68  (* Configuration management *)
    1.69  datatype fundef_opt 
    1.70 @@ -170,15 +192,13 @@
    1.71    FundefConfig { sequential=false, default="%x. arbitrary", domintros=false, tailrec=false }
    1.72  
    1.73  
    1.74 -(* Common operations on equations *)
    1.75 -
    1.76 -fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
    1.77 -  | open_all_all t = ([], t)
    1.78 +(* Analyzing function equations *)
    1.79  
    1.80  fun split_def ctxt geq =
    1.81      let
    1.82        fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
    1.83 -      val (qs, imp) = open_all_all geq
    1.84 +      val qs = Term.strip_qnt_vars "all" geq
    1.85 +      val imp = Term.strip_qnt_body "all" geq
    1.86        val (gs, eq) = Logic.strip_horn imp
    1.87  
    1.88        val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)