Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ROOT Sprache: SML

Original von: Isabelle^©

(*  Title:      FOL/fologic.ML
    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 not: term
  val conj: term
  val disj: term
  val imp: term
  val iff: term
  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 all_const: typ -> term
  val mk_all: term * term -> term
  val exists_const: typ -> term
  val mk_exists: term * term -> term
  val eq_const: typ -> term
  val mk_eq: term * term -> term
  val dest_eq: term -> term * term
  val mk_binop: string -> term * term -> term
  val mk_binrel: string -> term * term -> term
  val dest_bin: string -> typ -> term -> term * term
end;

structure FOLogic: FOLOGIC =
struct

val oT = Type(\<^type_name>\<open>o\<close>,[]);

val Trueprop = Const(\<^const_name>\<open>Trueprop\<close>, oT-->propT);

fun mk_Trueprop P = Trueprop $ P;

fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P
  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);

(* Logical constants *)

val not = Const (\<^const_name>\<open>Not\<close>, oT --> oT);
val conj = Const(\<^const_name>\<open>conj\<close>, [oT,oT]--->oT);
val disj = Const(\<^const_name>\<open>disj\<close>, [oT,oT]--->oT);
val imp = Const(\<^const_name>\<open>imp\<close>, [oT,oT]--->oT)
val iff = Const(\<^const_name>\<open>iff\<close>, [oT,oT]--->oT);

fun mk_conj (t1, t2) = conj $ t1 $ t2
and mk_disj (t1, t2) = disj $ t1 $ t2
and mk_imp (t1, t2) = imp $ t1 $ t2
and mk_iff (t1, t2) = iff $ t1 $ t2;

fun dest_imp (Const(\<^const_name>\<open>imp\<close>,_) $ A $ B) = (A, B)
  | dest_imp  t = raise TERM ("dest_imp", [t]);

fun dest_conj (Const (\<^const_name>\<open>conj\<close>, _) $ t $ t') = t :: dest_conj t'
  | dest_conj t = [t];

fun dest_iff (Const(\<^const_name>\<open>iff\<close>,_) $ A $ B) = (A, B)
  | dest_iff  t = raise TERM ("dest_iff", [t]);

fun eq_const T = Const (\<^const_name>\<open>eq\<close>, [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;

fun dest_eq (Const (\<^const_name>\<open>eq\<close>, _) $ lhs $ rhs) = (lhs, rhs)
  | dest_eq t = raise TERM ("dest_eq", [t])

fun all_const T = Const (\<^const_name>\<open>All\<close>, [T --> oT] ---> oT);
fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;

fun exists_const T = Const (\<^const_name>\<open>Ex\<close>, [T --> oT] ---> oT);
fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;

(* binary oprations and relations *)

fun mk_binop c (t, u) =
  let val T = fastype_of t in
    Const (c, [T, T] ---> T) $ t $ u
  end;

fun mk_binrel c (t, u) =
  let val T = fastype_of t in
    Const (c, [T, T] ---> oT) $ t $ u
  end;

fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
      if c = c' andalso T = T' then (t, u)
      else raise TERM ("dest_bin " ^ c, [tm])
  | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);

end;

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.