src/HOL/hologic.ML
author clasohm
Fri, 03 Mar 1995 12:02:25 +0100
changeset 923 ff1574a81019
child 2510 e3d0ac75c723
permissions -rw-r--r--
new version of HOL with curried function application
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/hologic.ML
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson and Markus Wenzel
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
Abstract syntax operations for HOL.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
signature HOLOGIC =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
sig
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
  val termC: class
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
  val termS: sort
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
  val termTVar: typ
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
  val boolT: typ
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
  val mk_setT: typ -> typ
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
  val dest_setT: typ -> typ
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
  val mk_Trueprop: term -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
  val dest_Trueprop: term -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
  val conj: term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
  val disj: term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
  val imp: term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
  val eq_const: typ -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
  val all_const: typ -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
  val exists_const: typ -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
  val Collect_const: typ -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
  val mk_eq: term * term -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
  val mk_all: string * typ * term -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
  val mk_exists: string * typ * term -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
  val mk_Collect: string * typ * term -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
  val mk_mem: term * term -> term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    32
structure HOLogic: HOLOGIC =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    33
struct
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
(* classes *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    36
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
val termC: class = "term";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
val termS: sort = [termC];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
(* types *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
val termTVar = TVar (("'a", 0), termS);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
val boolT = Type ("bool", []);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
fun mk_setT T = Type ("set", [T]);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
fun dest_setT (Type ("set", [T])) = T
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    50
  | dest_setT T = raise_type "dest_setT: set type expected" [T] [];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
(* terms *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    54
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
val Trueprop = Const ("Trueprop", boolT --> propT);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
fun mk_Trueprop P = Trueprop $ P;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
  | dest_Trueprop t = raise_term "dest_Trueprop" [t];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    62
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    63
val conj = Const ("op &", [boolT, boolT] ---> boolT)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
and disj = Const ("op |", [boolT, boolT] ---> boolT)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
and imp = Const ("op -->", [boolT, boolT] ---> boolT);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    67
fun eq_const T = Const ("op =", [T, T] ---> boolT);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    69
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    70
fun all_const T = Const ("All", [T --> boolT] ---> boolT);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
fun mk_mem (x, A) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
  let val setT = fastype_of A in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
    Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86