src/HOL/Tools/res_skolem_function.ML
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 15347 14585bc8fa09
child 16803 014090d1e64b
permissions -rw-r--r--
*** empty log message ***
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 Generation of unique Skolem functions (with types) as Term.term.
     6 *)
     7 
     8 signature RES_SKOLEM_FUNCTION =
     9 sig
    10 
    11 val gen_skolem: Term.term list -> Term.typ  -> Term.term
    12 
    13 end;
    14 
    15 structure ResSkolemFunction: RES_SKOLEM_FUNCTION  =
    16 
    17 struct
    18 
    19 val skolem_prefix = "sk_";
    20 
    21 (* internal reference starting from 0. *)
    22 val skolem_id = ref 0;
    23 
    24 
    25 fun gen_skolem_name () = 
    26     let val new_id = !skolem_id
    27 	val sk_fun = skolem_prefix ^ (string_of_int new_id)
    28     in
    29 	(skolem_id := new_id + 1; sk_fun) (* increment id by 1. *)
    30     end;
    31 
    32 fun sk_type_of_aux [Var(_,tp1)] tp = Type("fun",[tp1,tp])
    33   | sk_type_of_aux (Var(_,tp1)::vars) tp = 
    34     let val tp' = sk_type_of_aux vars tp
    35     in
    36 	Type("fun",[tp1,tp'])
    37     end;
    38 
    39 
    40 fun sk_type_of [] tp = tp
    41   | sk_type_of vars tp = sk_type_of_aux vars tp; 
    42 
    43 
    44 
    45 fun gen_skolem univ_vars tp = 
    46     let val new_sk_name = gen_skolem_name ()
    47 	val new_sk_type = sk_type_of univ_vars tp
    48 	val skolem_term = Const(new_sk_name,new_sk_type)
    49 	fun app [] sf = sf
    50 	  | app (var::vars) sf= app vars (sf $ var)
    51     in
    52 	app univ_vars skolem_term
    53     end;
    54 
    55 
    56 end;