src/FOL/fologic.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4466 305390f23734
child 6140 af32e2c3f77a
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      FOL/fologic.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4 
     5 Abstract syntax operations for FOL.
     6 *)
     7 
     8 signature FOLOGIC =
     9 sig
    10   val oT: typ
    11   val mk_Trueprop: term -> term
    12   val dest_Trueprop: term -> term
    13   val dest_imp	       : term -> term*term
    14   val conj: term
    15   val disj: term
    16   val imp: term
    17   val eq_const: typ -> term
    18   val all_const: typ -> term
    19   val exists_const: typ -> term
    20   val mk_eq: term * term -> term
    21   val mk_all: term * term -> term
    22   val mk_exists: term * term -> term
    23 end;
    24 
    25 
    26 structure FOLogic: FOLOGIC =
    27 struct
    28 
    29 val oT = Type("o",[]);
    30 
    31 val Trueprop = Const("Trueprop", oT-->propT);
    32 
    33 fun mk_Trueprop P = Trueprop $ P;
    34 
    35 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    36   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    37 
    38 (** Logical constants **)
    39 
    40 val conj = Const("op &", [oT,oT]--->oT)
    41 and disj = Const("op |", [oT,oT]--->oT)
    42 and imp = Const("op -->", [oT,oT]--->oT);
    43 
    44 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
    45   | dest_imp  t = raise TERM ("dest_imp", [t]);
    46 
    47 fun eq_const T = Const ("op =", [T, T] ---> oT);
    48 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    49 
    50 fun all_const T = Const ("All", [T --> oT] ---> oT);
    51 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
    52 
    53 fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
    54 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
    55 
    56 end;