# HG changeset patch # User krauss # Date 1292186459 -3600 # Node ID b223fa19af3c17796ca1b1ca4ef0eef967ac9c2e # Parent 866148b762470e4eaeb8fa6824a29845a70038da added signature; more honest header diff -r 866148b76247 -r b223fa19af3c src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Sat Dec 11 21:27:53 2010 -0800 +++ b/src/HOL/Tools/Function/function_lib.ML Sun Dec 12 21:40:59 2010 +0100 @@ -1,11 +1,39 @@ (* Title: HOL/Tools/Function/function_lib.ML Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. -Some fairly general functions that should probably go somewhere else... +Ad-hoc collection of function waiting to be eliminated, generalized, +moved elsewhere or otherwise cleaned up. *) -structure Function_Lib = (* FIXME proper signature *) +signature FUNCTION_LIB = +sig + val plural: string -> string -> 'a list -> string + + val dest_all_all: term -> term list * term + val dest_all_all_ctx: Proof.context -> term -> Proof.context * (string * typ) list * term + + val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list + val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a list -> 'b list -> 'c list -> + 'd list -> 'e list -> 'f list -> 'g list -> 'h list + + val unordered_pairs: 'a list -> ('a * 'a) list + + val replace_frees: (string * term) list -> term -> term + val rename_bound: string -> term -> term + val mk_forall_rename: (string * term) -> term -> term + val forall_intr_rename: (string * cterm) -> thm -> thm + + val frees_in_term: Proof.context -> term -> (string * typ) list + + datatype proof_attempt = Solved of thm | Stuck of thm | Fail + val try_proof: cterm -> tactic -> proof_attempt + + val dest_binop_list: string -> term -> term list + val regroup_conv: string -> string -> thm list -> int list -> conv + val regroup_union_conv: int list -> conv +end + +structure Function_Lib: FUNCTION_LIB = struct (* "The variable" ^ plural " is" "s are" vs *)