src/HOL/hologic.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2510 e3d0ac75c723
child 3794 d543bb9ab896
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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   val mk_binop: string -> term * term -> term
    31   val mk_binrel: string -> term * term -> term
    32   val dest_bin: string -> typ -> term -> term * term
    33   val natT: typ
    34   val zero: term
    35   val is_zero: term -> bool
    36   val mk_Suc: term -> term
    37   val dest_Suc: term -> term
    38   val mk_nat: int -> term
    39 end;
    40 
    41 
    42 structure HOLogic: HOLOGIC =
    43 struct
    44 
    45 (* basics *)
    46 
    47 val termC: class = "term";
    48 val termS: sort = [termC];
    49 
    50 val termTVar = TVar (("'a", 0), termS);
    51 
    52 
    53 (* bool and set *)
    54 
    55 val boolT = Type ("bool", []);
    56 
    57 fun mk_setT T = Type ("set", [T]);
    58 
    59 fun dest_setT (Type ("set", [T])) = T
    60   | dest_setT T = raise_type "dest_setT: set type expected" [T] [];
    61 
    62 
    63 val Trueprop = Const ("Trueprop", boolT --> propT);
    64 
    65 fun mk_Trueprop P = Trueprop $ P;
    66 
    67 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    68   | dest_Trueprop t = raise_term "dest_Trueprop" [t];
    69 
    70 
    71 val conj = Const ("op &", [boolT, boolT] ---> boolT)
    72 and disj = Const ("op |", [boolT, boolT] ---> boolT)
    73 and imp = Const ("op -->", [boolT, boolT] ---> boolT);
    74 
    75 fun eq_const T = Const ("op =", [T, T] ---> boolT);
    76 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    77 
    78 fun all_const T = Const ("All", [T --> boolT] ---> boolT);
    79 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
    80 
    81 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
    82 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
    83 
    84 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
    85 fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
    86 
    87 fun mk_mem (x, A) =
    88   let val setT = fastype_of A in
    89     Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
    90   end;
    91 
    92 
    93 (* binary oprations and relations *)
    94 
    95 fun mk_binop c (t, u) =
    96   let val T = fastype_of t in
    97     Const (c, [T, T] ---> T) $ t $ u
    98   end;
    99 
   100 fun mk_binrel c (t, u) =
   101   let val T = fastype_of t in
   102     Const (c, [T, T] ---> boolT) $ t $ u
   103   end;
   104 
   105 fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
   106       if c = c' andalso T = T' then (t, u)
   107       else raise_term ("dest_bin " ^ c) [tm]
   108   | dest_bin c _ tm = raise_term ("dest_bin " ^ c) [tm];
   109 
   110 
   111 (* nat *)
   112 
   113 val natT = Type ("nat", []);
   114 
   115 val zero = Const ("0", natT);
   116 fun is_zero t = t = zero;
   117 
   118 fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   119 
   120 fun dest_Suc (Const ("Suc", _) $ t) = t
   121   | dest_Suc t = raise_term "dest_Suc" [t];
   122 
   123 fun mk_nat 0 = zero
   124   | mk_nat n = mk_Suc (mk_nat (n - 1));
   125 
   126 
   127 end;