extensions for Susanto
authorpaulson
Mon Oct 02 17:31:14 2006 +0200 (2006-10-02)
changeset 20824aca7d38283bf
parent 20823 5480ec4b542d
child 20825 4b48fd429b18
extensions for Susanto
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Oct 02 17:30:56 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Mon Oct 02 17:31:14 2006 +0200
     1.3 @@ -11,9 +11,14 @@
     1.4    sig
     1.5    exception CLAUSE of string * term
     1.6    type clause and arityClause and classrelClause
     1.7 -  type fol_type
     1.8 -  type typ_var
     1.9 -  type type_literal
    1.10 +  datatype fol_type = AtomV of string
    1.11 +                    | AtomF of string
    1.12 +                    | Comp of string * fol_type list;
    1.13 +  datatype fol_term = UVar of string * fol_type
    1.14 +                    | Fun of string * fol_type list * fol_term list;
    1.15 +  datatype predicate = Predicate of string * fol_type list * fol_term list;
    1.16 +  type typ_var and type_literal and literal
    1.17 +  val literals_of_term: Term.term -> literal list * (typ_var * Term.sort) list
    1.18    val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    1.19    val arity_clause_thy: theory -> arityClause list 
    1.20    val ascii_of : string -> string
    1.21 @@ -28,6 +33,7 @@
    1.22    val gen_tptp_cls : int * string * string * string -> string
    1.23    val gen_tptp_type_cls : int * string * string * string * int -> string
    1.24    val get_axiomName : clause ->  string
    1.25 +  val get_literals : clause -> literal list
    1.26    val init : theory -> unit
    1.27    val isMeta : string -> bool
    1.28    val isTaut : clause -> bool
    1.29 @@ -212,8 +218,6 @@
    1.30  
    1.31  (**** Isabelle FOL clauses ****)
    1.32  
    1.33 -type pred_name = string;
    1.34 -
    1.35  datatype typ_var = FOLTVar of indexname | FOLTFree of string;
    1.36  
    1.37  (*FIXME: give the constructors more sensible names*)
    1.38 @@ -236,7 +240,7 @@
    1.39  
    1.40  datatype fol_term = UVar of string * fol_type
    1.41                    | Fun of string * fol_type list * fol_term list;
    1.42 -datatype predicate = Predicate of pred_name * fol_type list * fol_term list;
    1.43 +datatype predicate = Predicate of string * fol_type list * fol_term list;
    1.44  
    1.45  datatype literal = Literal of polarity * predicate;
    1.46  
    1.47 @@ -255,6 +259,8 @@
    1.48  
    1.49  fun get_axiomName (Clause cls) = #axiom_name cls;
    1.50  
    1.51 +fun get_literals (Clause cls) = #literals cls;
    1.52 +
    1.53  exception CLAUSE of string * term;
    1.54  
    1.55  fun isFalse (Literal (pol, Predicate(pname,_,[]))) =