src/HOL/hologic.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10693 9e4a0e84d0d6
child 11604 14b03d1463d4
permissions -rw-r--r--
improved theory reference in comment
     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 termT: typ
    13   val boolN: string
    14   val boolT: typ
    15   val false_const: term
    16   val true_const: term
    17   val not_const: term
    18   val mk_setT: typ -> typ
    19   val dest_setT: typ -> typ
    20   val mk_Trueprop: term -> term
    21   val dest_Trueprop: term -> term
    22   val conj: term
    23   val disj: term
    24   val imp: term
    25   val Not: term
    26   val mk_conj: term * term -> term
    27   val mk_disj: term * term -> term
    28   val mk_imp: term * term -> term
    29   val dest_imp: term -> term * term
    30   val dest_conj: term -> term list
    31   val eq_const: typ -> term
    32   val all_const: typ -> term
    33   val exists_const: typ -> term
    34   val Collect_const: typ -> term
    35   val mk_eq: term * term -> term
    36   val dest_eq: term -> term * term
    37   val mk_all: string * typ * term -> term
    38   val mk_exists: string * typ * term -> term
    39   val mk_Collect: string * typ * term -> term
    40   val mk_mem: term * term -> term
    41   val dest_mem: term -> term * term
    42   val mk_binop: string -> term * term -> term
    43   val mk_binrel: string -> term * term -> term
    44   val dest_bin: string -> typ -> term -> term * term
    45   val unitT: typ
    46   val is_unitT: typ -> bool
    47   val unit: term
    48   val is_unit: term -> bool
    49   val mk_prodT: typ * typ -> typ
    50   val dest_prodT: typ -> typ * typ
    51   val mk_prod: term * term -> term
    52   val dest_prod: term -> term * term
    53   val mk_fst: term -> term
    54   val mk_snd: term -> term
    55   val prodT_factors: typ -> typ list
    56   val split_const: typ * typ * typ -> term
    57   val mk_tuple: typ -> term list -> term
    58   val natT: typ
    59   val zero: term
    60   val is_zero: term -> bool
    61   val mk_Suc: term -> term
    62   val dest_Suc: term -> term
    63   val mk_nat: int -> term
    64   val dest_nat: term -> int
    65   val intT: typ
    66   val realT: typ
    67   val binT: typ
    68   val pls_const: term
    69   val min_const: term
    70   val bit_const: term
    71   val number_of_const: typ -> term
    72   val int_of: int list -> int
    73   val dest_binum: term -> int
    74   val mk_bin   : int -> term
    75 end;
    76 
    77 
    78 structure HOLogic: HOLOGIC =
    79 struct
    80 
    81 (* basics *)
    82 
    83 val termC: class = "term";
    84 val termS: sort = [termC];
    85 val termT = TypeInfer.anyT termS;
    86 
    87 
    88 (* bool and set *)
    89 
    90 val boolN = "bool";
    91 val boolT = Type (boolN, []);
    92 
    93 val true_const =  Const ("True", boolT);
    94 val false_const = Const ("False", boolT);
    95 val not_const = Const ("Not", boolT --> boolT);
    96 
    97 fun mk_setT T = Type ("set", [T]);
    98 
    99 fun dest_setT (Type ("set", [T])) = T
   100   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
   101 
   102 
   103 (* logic *)
   104 
   105 val Trueprop = Const ("Trueprop", boolT --> propT);
   106 
   107 fun mk_Trueprop P = Trueprop $ P;
   108 
   109 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   110   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
   111 
   112 
   113 val conj = Const ("op &", [boolT, boolT] ---> boolT)
   114 and disj = Const ("op |", [boolT, boolT] ---> boolT)
   115 and imp = Const ("op -->", [boolT, boolT] ---> boolT)
   116 and Not = Const ("Not", boolT --> boolT);
   117 
   118 fun mk_conj (t1, t2) = conj $ t1 $ t2
   119 and mk_disj (t1, t2) = disj $ t1 $ t2
   120 and mk_imp (t1, t2) = imp $ t1 $ t2;
   121 
   122 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   123   | dest_imp  t = raise TERM ("dest_imp", [t]);
   124 
   125 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
   126   | dest_conj t = [t];
   127 
   128 fun eq_const T = Const ("op =", [T, T] ---> boolT);
   129 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
   130 
   131 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
   132   | dest_eq t = raise TERM ("dest_eq", [t])
   133 
   134 fun all_const T = Const ("All", [T --> boolT] ---> boolT);
   135 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
   136 
   137 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
   138 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
   139 
   140 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
   141 fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
   142 
   143 fun mk_mem (x, A) =
   144   let val setT = fastype_of A in
   145     Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
   146   end;
   147 
   148 fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
   149   | dest_mem t = raise TERM ("dest_mem", [t]);
   150 
   151 
   152 (* binary oprations and relations *)
   153 
   154 fun mk_binop c (t, u) =
   155   let val T = fastype_of t in
   156     Const (c, [T, T] ---> T) $ t $ u
   157   end;
   158 
   159 fun mk_binrel c (t, u) =
   160   let val T = fastype_of t in
   161     Const (c, [T, T] ---> boolT) $ t $ u
   162   end;
   163 
   164 fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
   165       if c = c' andalso T = T' then (t, u)
   166       else raise TERM ("dest_bin " ^ c, [tm])
   167   | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
   168 
   169 
   170 (* unit *)
   171 
   172 val unitT = Type ("unit", []);
   173 
   174 fun is_unitT (Type ("unit", [])) = true
   175   | is_unitT _ = false;
   176 
   177 val unit = Const ("()", unitT);
   178 
   179 fun is_unit (Const ("()", _)) = true
   180   | is_unit _ = false;
   181 
   182 
   183 (* prod *)
   184 
   185 fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
   186 
   187 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
   188   | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
   189 
   190 fun mk_prod (t1, t2) =
   191   let val T1 = fastype_of t1 and T2 = fastype_of t2 in
   192     Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2)) $ t1 $ t2
   193   end;
   194 
   195 fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
   196   | dest_prod t = raise TERM ("dest_prod", [t]);
   197 
   198 fun mk_fst p =
   199   let val pT = fastype_of p in
   200     Const ("fst", pT --> fst (dest_prodT pT)) $ p
   201   end;
   202 
   203 fun mk_snd p =
   204   let val pT = fastype_of p in
   205     Const ("snd", pT --> snd (dest_prodT pT)) $ p
   206   end;
   207 
   208 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
   209 fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
   210   | prodT_factors T = [T];
   211 
   212 fun split_const (Ta, Tb, Tc) = 
   213     Const ("split", [[Ta, Tb] ---> Tc, mk_prodT (Ta, Tb)] ---> Tc);
   214 
   215 (*Makes a nested tuple from a list, following the product type structure*)
   216 fun mk_tuple (Type ("*", [T1, T2])) tms = 
   217         mk_prod (mk_tuple T1 tms, 
   218                  mk_tuple T2 (drop (length (prodT_factors T1), tms)))
   219   | mk_tuple T (t::_) = t;
   220 
   221 
   222 
   223 (* proper tuples *)
   224 
   225 local  (*currently unused*)
   226 
   227 fun mk_tupleT Ts = foldr mk_prodT (Ts, unitT);
   228 
   229 fun dest_tupleT (Type ("unit", [])) = []
   230   | dest_tupleT (Type ("*", [T, U])) = T :: dest_tupleT U
   231   | dest_tupleT T = raise TYPE ("dest_tupleT", [T], []);
   232 
   233 fun mk_tuple ts = foldr mk_prod (ts, unit);
   234 
   235 fun dest_tuple (Const ("()", _)) = []
   236   | dest_tuple (Const ("Pair", _) $ t $ u) = t :: dest_tuple u
   237   | dest_tuple t = raise TERM ("dest_tuple", [t]);
   238 
   239 in val _ = unit end;
   240 
   241 
   242 (* nat *)
   243 
   244 val natT = Type ("nat", []);
   245 
   246 val zero = Const ("0", natT);
   247 
   248 fun is_zero (Const ("0", _)) = true
   249   | is_zero _ = false;
   250 
   251 fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   252 
   253 fun dest_Suc (Const ("Suc", _) $ t) = t
   254   | dest_Suc t = raise TERM ("dest_Suc", [t]);
   255 
   256 fun mk_nat 0 = zero
   257   | mk_nat n = mk_Suc (mk_nat (n - 1));
   258 
   259 fun dest_nat (Const ("0", _)) = 0
   260   | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   261   | dest_nat t = raise TERM ("dest_nat", [t]);
   262 
   263 
   264 val intT = Type ("IntDef.int", []);
   265 
   266 val realT = Type("RealDef.real",[]);
   267 
   268 
   269 (* binary numerals *)
   270 
   271 val binT = Type ("Numeral.bin", []);
   272 
   273 val pls_const =  Const ("Numeral.bin.Pls", binT)
   274 and min_const = Const ("Numeral.bin.Min", binT)
   275 and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
   276 
   277 fun number_of_const T = Const ("Numeral.number_of", binT --> T);
   278 
   279 
   280 fun int_of [] = 0
   281   | int_of (b :: bs) = b + 2 * int_of bs;
   282 
   283 fun dest_bit (Const ("False", _)) = 0
   284   | dest_bit (Const ("True", _)) = 1
   285   | dest_bit t = raise TERM("dest_bit", [t]);
   286 
   287 fun bin_of (Const ("Numeral.bin.Pls", _)) = []
   288   | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
   289   | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   290   | bin_of t = raise TERM("bin_of", [t]);
   291 
   292 val dest_binum = int_of o bin_of;
   293 
   294 fun mk_bit 0 = false_const
   295   | mk_bit 1 = true_const
   296   | mk_bit _ = sys_error "mk_bit";
   297 
   298 fun mk_bin n =
   299   let
   300     fun bin_of 0  = []
   301       | bin_of ~1 = [~1]
   302       | bin_of n  = (n mod 2) :: bin_of (n div 2);
   303 
   304     fun term_of []   = pls_const
   305       | term_of [~1] = min_const
   306       | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
   307     in term_of (bin_of n) end;
   308 
   309 end;