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 ***
paulson@15347
     1
(*  Author: Jia Meng, Cambridge University Computer Laboratory
paulson@15347
     2
    ID: $Id$
paulson@15347
     3
    Copyright 2004 University of Cambridge
paulson@15347
     4
paulson@15347
     5
Generation of unique Skolem functions (with types) as Term.term.
paulson@15347
     6
*)
paulson@15347
     7
paulson@15347
     8
signature RES_SKOLEM_FUNCTION =
paulson@15347
     9
sig
paulson@15347
    10
paulson@15347
    11
val gen_skolem: Term.term list -> Term.typ  -> Term.term
paulson@15347
    12
paulson@15347
    13
end;
paulson@15347
    14
paulson@15347
    15
structure ResSkolemFunction: RES_SKOLEM_FUNCTION  =
paulson@15347
    16
paulson@15347
    17
struct
paulson@15347
    18
paulson@15347
    19
val skolem_prefix = "sk_";
paulson@15347
    20
paulson@15347
    21
(* internal reference starting from 0. *)
paulson@15347
    22
val skolem_id = ref 0;
paulson@15347
    23
paulson@15347
    24
paulson@15347
    25
fun gen_skolem_name () = 
paulson@15347
    26
    let val new_id = !skolem_id
paulson@15347
    27
	val sk_fun = skolem_prefix ^ (string_of_int new_id)
paulson@15347
    28
    in
paulson@15347
    29
	(skolem_id := new_id + 1; sk_fun) (* increment id by 1. *)
paulson@15347
    30
    end;
paulson@15347
    31
paulson@15347
    32
fun sk_type_of_aux [Var(_,tp1)] tp = Type("fun",[tp1,tp])
paulson@15347
    33
  | sk_type_of_aux (Var(_,tp1)::vars) tp = 
paulson@15347
    34
    let val tp' = sk_type_of_aux vars tp
paulson@15347
    35
    in
paulson@15347
    36
	Type("fun",[tp1,tp'])
paulson@15347
    37
    end;
paulson@15347
    38
paulson@15347
    39
paulson@15347
    40
fun sk_type_of [] tp = tp
paulson@15347
    41
  | sk_type_of vars tp = sk_type_of_aux vars tp; 
paulson@15347
    42
paulson@15347
    43
paulson@15347
    44
paulson@15347
    45
fun gen_skolem univ_vars tp = 
paulson@15347
    46
    let val new_sk_name = gen_skolem_name ()
paulson@15347
    47
	val new_sk_type = sk_type_of univ_vars tp
paulson@15347
    48
	val skolem_term = Const(new_sk_name,new_sk_type)
paulson@15347
    49
	fun app [] sf = sf
paulson@15347
    50
	  | app (var::vars) sf= app vars (sf $ var)
paulson@15347
    51
    in
paulson@15347
    52
	app univ_vars skolem_term
paulson@15347
    53
    end;
paulson@15347
    54
paulson@15347
    55
paulson@15347
    56
end;