src/FOL/fologic.ML

Instantiated the one-point-rule quantifier simpprocs for FOL

New file fologic.ML holds abstract syntax operations

Also, miniscoping provided for intuitionistic logic

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

Abstract syntax operations for FOL.
*)

signature FOLOGIC =
sig
  val oT: typ
  val mk_Trueprop: term -> term
  val dest_Trueprop: term -> term
  val conj: term
  val disj: term
  val imp: term
  val eq_const: typ -> term
  val all_const: typ -> term
  val exists_const: typ -> term
  val mk_eq: term * term -> term
  val mk_all: term * term -> term
  val mk_exists: term * term -> term
end;


structure FOLogic: FOLOGIC =
struct

val oT = Type("o",[]);

val Trueprop = Const("Trueprop", oT-->propT);

fun mk_Trueprop P = Trueprop $ P;

fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);

(** Logical constants **)

val conj = Const("op &", [oT,oT]--->oT)
and disj = Const("op |", [oT,oT]--->oT)
and imp = Const("op -->", [oT,oT]--->oT);

fun eq_const T = Const ("op =", [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;

fun all_const T = Const ("All", [T --> oT] ---> oT);
fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));

fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));

end;