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