src/FOL/fologic.ML
author wenzelm
Sat Aug 29 12:01:25 2009 +0200 (2009-08-29)
changeset 32449 696d64ed85da
parent 31974 e81979a703a4
child 38500 d5477ee35820
permissions -rw-r--r--
eliminated hard tabs;
paulson@4349
     1
(*  Title:      FOL/fologic.ML
paulson@4349
     2
    Author:     Lawrence C Paulson
paulson@4349
     3
paulson@4349
     4
Abstract syntax operations for FOL.
paulson@4349
     5
*)
paulson@4349
     6
paulson@4349
     7
signature FOLOGIC =
paulson@4349
     8
sig
wenzelm@32449
     9
  val oT: typ
wenzelm@32449
    10
  val mk_Trueprop: term -> term
wenzelm@32449
    11
  val dest_Trueprop: term -> term
wenzelm@32449
    12
  val not: term
wenzelm@32449
    13
  val conj: term
wenzelm@32449
    14
  val disj: term
wenzelm@32449
    15
  val imp: term
wenzelm@32449
    16
  val iff: term
wenzelm@32449
    17
  val mk_conj: term * term -> term
wenzelm@32449
    18
  val mk_disj: term * term -> term
wenzelm@32449
    19
  val mk_imp: term * term -> term
wenzelm@32449
    20
  val dest_imp: term -> term * term
wenzelm@32449
    21
  val dest_conj: term -> term list
wenzelm@32449
    22
  val mk_iff: term * term -> term
wenzelm@32449
    23
  val dest_iff: term -> term * term
wenzelm@32449
    24
  val all_const: typ -> term
wenzelm@32449
    25
  val mk_all: term * term -> term
wenzelm@32449
    26
  val exists_const: typ -> term
wenzelm@32449
    27
  val mk_exists: term * term -> term
wenzelm@32449
    28
  val eq_const: typ -> term
wenzelm@32449
    29
  val mk_eq: term * term -> term
wenzelm@32449
    30
  val dest_eq: term -> term * term
paulson@9543
    31
  val mk_binop: string -> term * term -> term
paulson@9543
    32
  val mk_binrel: string -> term * term -> term
paulson@9543
    33
  val dest_bin: string -> typ -> term -> term * term
paulson@4349
    34
end;
paulson@4349
    35
paulson@4349
    36
paulson@4349
    37
structure FOLogic: FOLOGIC =
paulson@4349
    38
struct
paulson@4349
    39
paulson@4349
    40
val oT = Type("o",[]);
paulson@4349
    41
paulson@4349
    42
val Trueprop = Const("Trueprop", oT-->propT);
paulson@4349
    43
paulson@4349
    44
fun mk_Trueprop P = Trueprop $ P;
paulson@4349
    45
paulson@4349
    46
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
paulson@4349
    47
  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
paulson@4349
    48
wenzelm@32449
    49
wenzelm@32449
    50
(* Logical constants *)
paulson@4349
    51
wenzelm@9850
    52
val not = Const ("Not", oT --> oT);
wenzelm@9850
    53
val conj = Const("op &", [oT,oT]--->oT);
wenzelm@9850
    54
val disj = Const("op |", [oT,oT]--->oT);
wenzelm@9850
    55
val imp = Const("op -->", [oT,oT]--->oT)
wenzelm@9850
    56
val iff = Const("op <->", [oT,oT]--->oT);
paulson@4349
    57
wenzelm@7692
    58
fun mk_conj (t1, t2) = conj $ t1 $ t2
wenzelm@7692
    59
and mk_disj (t1, t2) = disj $ t1 $ t2
paulson@9543
    60
and mk_imp (t1, t2) = imp $ t1 $ t2
paulson@9543
    61
and mk_iff (t1, t2) = iff $ t1 $ t2;
wenzelm@7692
    62
paulson@4466
    63
fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
paulson@4466
    64
  | dest_imp  t = raise TERM ("dest_imp", [t]);
paulson@4466
    65
wenzelm@11668
    66
fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
wenzelm@11668
    67
  | dest_conj t = [t];
wenzelm@11668
    68
paulson@9543
    69
fun dest_iff (Const("op <->",_) $ A $ B) = (A, B)
paulson@9543
    70
  | dest_iff  t = raise TERM ("dest_iff", [t]);
paulson@9543
    71
paulson@4349
    72
fun eq_const T = Const ("op =", [T, T] ---> oT);
paulson@4349
    73
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
paulson@4349
    74
paulson@6140
    75
fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
paulson@6140
    76
  | dest_eq t = raise TERM ("dest_eq", [t])
paulson@6140
    77
paulson@4349
    78
fun all_const T = Const ("All", [T --> oT] ---> oT);
paulson@4349
    79
fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
paulson@4349
    80
paulson@4349
    81
fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
paulson@4349
    82
fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
paulson@4349
    83
wenzelm@32449
    84
paulson@9543
    85
(* binary oprations and relations *)
paulson@9543
    86
paulson@9543
    87
fun mk_binop c (t, u) =
paulson@9543
    88
  let val T = fastype_of t in
paulson@9543
    89
    Const (c, [T, T] ---> T) $ t $ u
paulson@9543
    90
  end;
paulson@9543
    91
paulson@9543
    92
fun mk_binrel c (t, u) =
paulson@9543
    93
  let val T = fastype_of t in
paulson@9543
    94
    Const (c, [T, T] ---> oT) $ t $ u
paulson@9543
    95
  end;
paulson@9543
    96
paulson@9543
    97
fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
paulson@9543
    98
      if c = c' andalso T = T' then (t, u)
paulson@9543
    99
      else raise TERM ("dest_bin " ^ c, [tm])
paulson@9543
   100
  | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
paulson@9543
   101
paulson@4349
   102
end;