File ‹fologic.ML›

(*  Title:      FOL/fologic.ML
    Author:     Lawrence C Paulson

Abstract syntax operations for FOL.
*)

signature FOLOGIC =
sig
  val mk_conj: term * term -> term
  val mk_disj: term * term -> term
  val mk_imp: term * term -> term
  val dest_imp: term -> term * term
  val dest_conj: term -> term list
  val mk_iff: term * term -> term
  val dest_iff: term -> term * term
  val mk_all: string * typ -> term -> term
  val mk_exists: string * typ -> term -> term
  val mk_eq: term * term -> term
  val dest_eq: term -> term * term
end;

structure FOLogic: FOLOGIC =
struct

fun mk_conj (t1, t2) = \<^Const>‹conj for t1 t2›
and mk_disj (t1, t2) = \<^Const>‹disj for t1 t2›
and mk_imp (t1, t2) = \<^Const>‹imp for t1 t2›
and mk_iff (t1, t2) = \<^Const>‹iff for t1 t2›;

val dest_imp = \<^Const_fn>‹imp for A B => ‹(A, B)››;

fun dest_conj \<^Const_>‹conj for t t'› = t :: dest_conj t'
  | dest_conj t = [t];

val dest_iff = \<^Const_fn>‹iff for A B => ‹(A, B)››;

fun mk_eq (t, u) =
  let val T = fastype_of t
  in \<^Const>‹eq T for t u› end;

val dest_eq = \<^Const_fn>‹eq _ for lhs rhs => ‹(lhs, rhs)››;

fun mk_all (x, T) P = \<^Const>‹All T for ‹absfree (x, T) P››;
fun mk_exists (x, T) P = \<^Const>‹Ex T for ‹absfree (x, T) P››;

end;