src/HOL/hologic.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5207 dd4f51adfff3
child 6031 d9fa148383e2
permissions -rw-r--r--
tidying
     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 dest_imp: term -> term * term
    22   val eq_const: typ -> term
    23   val all_const: typ -> term
    24   val exists_const: typ -> term
    25   val Collect_const: typ -> term
    26   val mk_eq: term * term -> term
    27   val mk_all: string * typ * term -> term
    28   val mk_exists: string * typ * term -> term
    29   val mk_Collect: string * typ * term -> term
    30   val mk_mem: term * term -> term
    31   val mk_binop: string -> term * term -> term
    32   val mk_binrel: string -> term * term -> term
    33   val dest_bin: string -> typ -> term -> term * term
    34   val unitT: typ
    35   val unit: term
    36   val is_unit: term -> bool
    37   val mk_prodT: typ * typ -> typ
    38   val dest_prodT: typ -> typ * typ
    39   val mk_prod: term * term -> term
    40   val dest_prod: term -> term * term
    41   val mk_fst: term -> term
    42   val mk_snd: term -> term
    43   val prodT_factors: typ -> typ list
    44   val split_const: typ * typ * typ -> term
    45   val mk_tuple: typ -> term list -> term
    46   val natT: typ
    47   val zero: term
    48   val is_zero: term -> bool
    49   val mk_Suc: term -> term
    50   val dest_Suc: term -> term
    51   val mk_nat: int -> term
    52   val dest_nat: term -> int
    53 end;
    54 
    55 
    56 structure HOLogic: HOLOGIC =
    57 struct
    58 
    59 (* basics *)
    60 
    61 val termC: class = "term";
    62 val termS: sort = [termC];
    63 
    64 val termTVar = TVar (("'a", 0), termS);
    65 
    66 
    67 (* bool and set *)
    68 
    69 val boolT = Type ("bool", []);
    70 
    71 fun mk_setT T = Type ("set", [T]);
    72 
    73 fun dest_setT (Type ("set", [T])) = T
    74   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
    75 
    76 
    77 val Trueprop = Const ("Trueprop", boolT --> propT);
    78 
    79 fun mk_Trueprop P = Trueprop $ P;
    80 
    81 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    82   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    83 
    84 
    85 val conj = Const ("op &", [boolT, boolT] ---> boolT)
    86 and disj = Const ("op |", [boolT, boolT] ---> boolT)
    87 and imp = Const ("op -->", [boolT, boolT] ---> boolT);
    88 
    89 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
    90   | dest_imp  t = raise TERM ("dest_imp", [t]);
    91 
    92 fun eq_const T = Const ("op =", [T, T] ---> boolT);
    93 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    94 
    95 fun all_const T = Const ("All", [T --> boolT] ---> boolT);
    96 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
    97 
    98 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
    99 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
   100 
   101 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
   102 fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
   103 
   104 fun mk_mem (x, A) =
   105   let val setT = fastype_of A in
   106     Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
   107   end;
   108 
   109 
   110 (* binary oprations and relations *)
   111 
   112 fun mk_binop c (t, u) =
   113   let val T = fastype_of t in
   114     Const (c, [T, T] ---> T) $ t $ u
   115   end;
   116 
   117 fun mk_binrel c (t, u) =
   118   let val T = fastype_of t in
   119     Const (c, [T, T] ---> boolT) $ t $ u
   120   end;
   121 
   122 fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
   123       if c = c' andalso T = T' then (t, u)
   124       else raise TERM ("dest_bin " ^ c, [tm])
   125   | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
   126 
   127 
   128 (* unit *)
   129 
   130 val unitT = Type ("unit", []);
   131 
   132 val unit = Const ("()", unitT);
   133 
   134 fun is_unit (Const ("()", _)) = true
   135   | is_unit _ = false;
   136 
   137 
   138 (* prod *)
   139 
   140 fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
   141 
   142 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
   143   | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
   144 
   145 fun mk_prod (t1, t2) =
   146   let val T1 = fastype_of t1 and T2 = fastype_of t2 in
   147     Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2)) $ t1 $ t2
   148   end;
   149 
   150 fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
   151   | dest_prod t = raise TERM ("dest_prod", [t]);
   152 
   153 fun mk_fst p =
   154   let val pT = fastype_of p in
   155     Const ("fst", pT --> fst (dest_prodT pT)) $ p
   156   end;
   157 
   158 fun mk_snd p =
   159   let val pT = fastype_of p in
   160     Const ("snd", pT --> snd (dest_prodT pT)) $ p
   161   end;
   162 
   163 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
   164 fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
   165   | prodT_factors T = [T];
   166 
   167 fun split_const (Ta, Tb, Tc) = 
   168     Const ("split", [[Ta, Tb] ---> Tc, mk_prodT (Ta, Tb)] ---> Tc);
   169 
   170 (*Makes a nested tuple from a list, following the product type structure*)
   171 fun mk_tuple (Type ("*", [T1, T2])) tms = 
   172         mk_prod (mk_tuple T1 tms, 
   173                  mk_tuple T2 (drop (length (prodT_factors T1), tms)))
   174   | mk_tuple T (t::_) = t;
   175 
   176 
   177 
   178 (* nat *)
   179 
   180 val natT = Type ("nat", []);
   181 
   182 val zero = Const ("0", natT);
   183 
   184 fun is_zero (Const ("0", _)) = true
   185   | is_zero _ = false;
   186 
   187 fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   188 
   189 fun dest_Suc (Const ("Suc", _) $ t) = t
   190   | dest_Suc t = raise TERM ("dest_Suc", [t]);
   191 
   192 fun mk_nat 0 = zero
   193   | mk_nat n = mk_Suc (mk_nat (n - 1));
   194 
   195 fun dest_nat (Const ("0", _)) = 0
   196   | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   197   | dest_nat t = raise TERM ("dest_nat", [t]);
   198 
   199 
   200 end;