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