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