src/HOL/Tools/res_skolem_function.ML

more fine tuniung

(*  Author: Jia Meng, Cambridge University Computer Laboratory
    ID: $Id$
    Copyright 2004 University of Cambridge

Generation of unique Skolem functions (with types) as Term.term.
*)

signature RES_SKOLEM_FUNCTION =
sig

val gen_skolem: Term.term list -> Term.typ  -> Term.term

end;

structure ResSkolemFunction: RES_SKOLEM_FUNCTION  =

struct

val skolem_prefix = "sk_";

(* internal reference starting from 0. *)
val skolem_id = ref 0;


fun gen_skolem_name () = 
    let val new_id = !skolem_id
	val sk_fun = skolem_prefix ^ (string_of_int new_id)
    in
	(skolem_id := new_id + 1; sk_fun) (* increment id by 1. *)
    end;

fun sk_type_of_aux [Var(_,tp1)] tp = Type("fun",[tp1,tp])
  | sk_type_of_aux (Var(_,tp1)::vars) tp = 
    let val tp' = sk_type_of_aux vars tp
    in
	Type("fun",[tp1,tp'])
    end;


fun sk_type_of [] tp = tp
  | sk_type_of vars tp = sk_type_of_aux vars tp; 



fun gen_skolem univ_vars tp = 
    let val new_sk_name = gen_skolem_name ()
	val new_sk_type = sk_type_of univ_vars tp
	val skolem_term = Const(new_sk_name,new_sk_type)
	fun app [] sf = sf
	  | app (var::vars) sf= app vars (sf $ var)
    in
	app univ_vars skolem_term
    end;


end;