src/FOL/fologic.ML
changeset 6140 af32e2c3f77a
parent 4466 305390f23734
child 7692 89bbce6f5c17
equal deleted inserted replaced
6139:26abad27b03c 6140:af32e2c3f77a
     5 Abstract syntax operations for FOL.
     5 Abstract syntax operations for FOL.
     6 *)
     6 *)
     7 
     7 
     8 signature FOLOGIC =
     8 signature FOLOGIC =
     9 sig
     9 sig
    10   val oT: typ
    10   val oT		: typ
    11   val mk_Trueprop: term -> term
    11   val mk_Trueprop	: term -> term
    12   val dest_Trueprop: term -> term
    12   val dest_Trueprop	: term -> term
    13   val dest_imp	       : term -> term*term
    13   val conj		: term
    14   val conj: term
    14   val disj		: term
    15   val disj: term
    15   val imp		: term
    16   val imp: term
    16   val dest_imp	       	: term -> term*term
    17   val eq_const: typ -> term
    17   val all_const		: typ -> term
    18   val all_const: typ -> term
    18   val mk_all		: term * term -> term
    19   val exists_const: typ -> term
    19   val exists_const	: typ -> term
    20   val mk_eq: term * term -> term
    20   val mk_exists		: term * term -> term
    21   val mk_all: term * term -> term
    21   val eq_const		: typ -> term
    22   val mk_exists: term * term -> term
    22   val mk_eq		: term * term -> term
       
    23   val dest_eq 		: term -> term*term
    23 end;
    24 end;
    24 
    25 
    25 
    26 
    26 structure FOLogic: FOLOGIC =
    27 structure FOLogic: FOLOGIC =
    27 struct
    28 struct
    45   | dest_imp  t = raise TERM ("dest_imp", [t]);
    46   | dest_imp  t = raise TERM ("dest_imp", [t]);
    46 
    47 
    47 fun eq_const T = Const ("op =", [T, T] ---> oT);
    48 fun eq_const T = Const ("op =", [T, T] ---> oT);
    48 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    49 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    49 
    50 
       
    51 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
       
    52   | dest_eq t = raise TERM ("dest_eq", [t])
       
    53 
    50 fun all_const T = Const ("All", [T --> oT] ---> oT);
    54 fun all_const T = Const ("All", [T --> oT] ---> oT);
    51 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
    55 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
    52 
    56 
    53 fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
    57 fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
    54 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
    58 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));