src/HOL/Tools/hologic.ML
changeset 28952 15a4b2cf8c34
parent 27325 70e4eb732fa9
child 30304 d8e4cd2ac2a1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/hologic.ML	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,568 @@
     1.4 +(*  Title:      HOL/hologic.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson and Markus Wenzel
     1.7 +
     1.8 +Abstract syntax operations for HOL.
     1.9 +*)
    1.10 +
    1.11 +signature HOLOGIC =
    1.12 +sig
    1.13 +  val typeS: sort
    1.14 +  val typeT: typ
    1.15 +  val boolN: string
    1.16 +  val boolT: typ
    1.17 +  val true_const: term
    1.18 +  val false_const: term
    1.19 +  val mk_setT: typ -> typ
    1.20 +  val dest_setT: typ -> typ
    1.21 +  val Trueprop: term
    1.22 +  val mk_Trueprop: term -> term
    1.23 +  val dest_Trueprop: term -> term
    1.24 +  val conj_intr: thm -> thm -> thm
    1.25 +  val conj_elim: thm -> thm * thm
    1.26 +  val conj_elims: thm -> thm list
    1.27 +  val conj: term
    1.28 +  val disj: term
    1.29 +  val imp: term
    1.30 +  val Not: term
    1.31 +  val mk_conj: term * term -> term
    1.32 +  val mk_disj: term * term -> term
    1.33 +  val mk_imp: term * term -> term
    1.34 +  val mk_not: term -> term
    1.35 +  val dest_conj: term -> term list
    1.36 +  val dest_disj: term -> term list
    1.37 +  val disjuncts: term -> term list
    1.38 +  val dest_imp: term -> term * term
    1.39 +  val dest_not: term -> term
    1.40 +  val eq_const: typ -> term
    1.41 +  val mk_eq: term * term -> term
    1.42 +  val dest_eq: term -> term * term
    1.43 +  val all_const: typ -> term
    1.44 +  val mk_all: string * typ * term -> term
    1.45 +  val list_all: (string * typ) list * term -> term
    1.46 +  val exists_const: typ -> term
    1.47 +  val mk_exists: string * typ * term -> term
    1.48 +  val choice_const: typ -> term
    1.49 +  val Collect_const: typ -> term
    1.50 +  val mk_Collect: string * typ * term -> term
    1.51 +  val class_eq: string
    1.52 +  val mk_mem: term * term -> term
    1.53 +  val dest_mem: term -> term * term
    1.54 +  val mk_UNIV: typ -> term
    1.55 +  val mk_binop: string -> term * term -> term
    1.56 +  val mk_binrel: string -> term * term -> term
    1.57 +  val dest_bin: string -> typ -> term -> term * term
    1.58 +  val unitT: typ
    1.59 +  val is_unitT: typ -> bool
    1.60 +  val unit: term
    1.61 +  val is_unit: term -> bool
    1.62 +  val mk_prodT: typ * typ -> typ
    1.63 +  val dest_prodT: typ -> typ * typ
    1.64 +  val pair_const: typ -> typ -> term
    1.65 +  val mk_prod: term * term -> term
    1.66 +  val dest_prod: term -> term * term
    1.67 +  val mk_fst: term -> term
    1.68 +  val mk_snd: term -> term
    1.69 +  val split_const: typ * typ * typ -> term
    1.70 +  val mk_split: term -> term
    1.71 +  val prodT_factors: typ -> typ list
    1.72 +  val mk_tuple: typ -> term list -> term
    1.73 +  val dest_tuple: term -> term list
    1.74 +  val ap_split: typ -> typ -> term -> term
    1.75 +  val prod_factors: term -> int list list
    1.76 +  val dest_tuple': int list list -> term -> term list
    1.77 +  val prodT_factors': int list list -> typ -> typ list
    1.78 +  val ap_split': int list list -> typ -> typ -> term -> term
    1.79 +  val mk_tuple': int list list -> typ -> term list -> term
    1.80 +  val mk_tupleT: int list list -> typ list -> typ
    1.81 +  val strip_split: term -> term * typ list * int list list
    1.82 +  val natT: typ
    1.83 +  val zero: term
    1.84 +  val is_zero: term -> bool
    1.85 +  val mk_Suc: term -> term
    1.86 +  val dest_Suc: term -> term
    1.87 +  val Suc_zero: term
    1.88 +  val mk_nat: int -> term
    1.89 +  val dest_nat: term -> int
    1.90 +  val class_size: string
    1.91 +  val size_const: typ -> term
    1.92 +  val indexT: typ
    1.93 +  val intT: typ
    1.94 +  val pls_const: term
    1.95 +  val min_const: term
    1.96 +  val bit0_const: term
    1.97 +  val bit1_const: term
    1.98 +  val mk_bit: int -> term
    1.99 +  val dest_bit: term -> int
   1.100 +  val mk_numeral: int -> term
   1.101 +  val dest_numeral: term -> int
   1.102 +  val number_of_const: typ -> term
   1.103 +  val add_numerals: term -> (term * typ) list -> (term * typ) list
   1.104 +  val mk_number: typ -> int -> term
   1.105 +  val dest_number: term -> typ * int
   1.106 +  val realT: typ
   1.107 +  val nibbleT: typ
   1.108 +  val mk_nibble: int -> term
   1.109 +  val dest_nibble: term -> int
   1.110 +  val charT: typ
   1.111 +  val mk_char: int -> term
   1.112 +  val dest_char: term -> int
   1.113 +  val listT: typ -> typ
   1.114 +  val nil_const: typ -> term
   1.115 +  val cons_const: typ -> term
   1.116 +  val mk_list: typ -> term list -> term
   1.117 +  val dest_list: term -> term list
   1.118 +  val stringT: typ
   1.119 +  val mk_string: string -> term
   1.120 +  val dest_string: term -> string
   1.121 +end;
   1.122 +
   1.123 +structure HOLogic: HOLOGIC =
   1.124 +struct
   1.125 +
   1.126 +(* HOL syntax *)
   1.127 +
   1.128 +val typeS: sort = ["HOL.type"];
   1.129 +val typeT = TypeInfer.anyT typeS;
   1.130 +
   1.131 +
   1.132 +(* bool and set *)
   1.133 +
   1.134 +val boolN = "bool";
   1.135 +val boolT = Type (boolN, []);
   1.136 +
   1.137 +val true_const =  Const ("True", boolT);
   1.138 +val false_const = Const ("False", boolT);
   1.139 +
   1.140 +fun mk_setT T = T --> boolT;
   1.141 +
   1.142 +fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
   1.143 +  | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
   1.144 +
   1.145 +
   1.146 +(* logic *)
   1.147 +
   1.148 +val Trueprop = Const ("Trueprop", boolT --> propT);
   1.149 +
   1.150 +fun mk_Trueprop P = Trueprop $ P;
   1.151 +
   1.152 +fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   1.153 +  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
   1.154 +
   1.155 +fun conj_intr thP thQ =
   1.156 +  let
   1.157 +    val (P, Q) = pairself (ObjectLogic.dest_judgment o Thm.cprop_of) (thP, thQ)
   1.158 +      handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
   1.159 +    val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   1.160 +  in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
   1.161 +
   1.162 +fun conj_elim thPQ =
   1.163 +  let
   1.164 +    val (P, Q) = Thm.dest_binop (ObjectLogic.dest_judgment (Thm.cprop_of thPQ))
   1.165 +      handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
   1.166 +    val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   1.167 +    val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
   1.168 +    val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
   1.169 +  in (thP, thQ) end;
   1.170 +
   1.171 +fun conj_elims th =
   1.172 +  let val (th1, th2) = conj_elim th
   1.173 +  in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
   1.174 +
   1.175 +val conj = @{term "op &"}
   1.176 +and disj = @{term "op |"}
   1.177 +and imp = @{term "op -->"}
   1.178 +and Not = @{term "Not"};
   1.179 +
   1.180 +fun mk_conj (t1, t2) = conj $ t1 $ t2
   1.181 +and mk_disj (t1, t2) = disj $ t1 $ t2
   1.182 +and mk_imp (t1, t2) = imp $ t1 $ t2
   1.183 +and mk_not t = Not $ t;
   1.184 +
   1.185 +fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
   1.186 +  | dest_conj t = [t];
   1.187 +
   1.188 +fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
   1.189 +  | dest_disj t = [t];
   1.190 +
   1.191 +(*Like dest_disj, but flattens disjunctions however nested*)
   1.192 +fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
   1.193 +  | disjuncts_aux t disjs = t::disjs;
   1.194 +
   1.195 +fun disjuncts t = disjuncts_aux t [];
   1.196 +
   1.197 +fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   1.198 +  | dest_imp  t = raise TERM ("dest_imp", [t]);
   1.199 +
   1.200 +fun dest_not (Const ("Not", _) $ t) = t
   1.201 +  | dest_not t = raise TERM ("dest_not", [t]);
   1.202 +
   1.203 +fun eq_const T = Const ("op =", [T, T] ---> boolT);
   1.204 +fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
   1.205 +
   1.206 +fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
   1.207 +  | dest_eq t = raise TERM ("dest_eq", [t])
   1.208 +
   1.209 +fun all_const T = Const ("All", [T --> boolT] ---> boolT);
   1.210 +fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
   1.211 +fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
   1.212 +
   1.213 +fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
   1.214 +fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
   1.215 +
   1.216 +fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
   1.217 +
   1.218 +fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
   1.219 +fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
   1.220 +
   1.221 +val class_eq = "HOL.eq";
   1.222 +
   1.223 +fun mk_mem (x, A) =
   1.224 +  let val setT = fastype_of A in
   1.225 +    Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
   1.226 +  end;
   1.227 +
   1.228 +fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
   1.229 +  | dest_mem t = raise TERM ("dest_mem", [t]);
   1.230 +
   1.231 +fun mk_UNIV T = Const ("UNIV", mk_setT T);
   1.232 +
   1.233 +
   1.234 +(* binary operations and relations *)
   1.235 +
   1.236 +fun mk_binop c (t, u) =
   1.237 +  let val T = fastype_of t in
   1.238 +    Const (c, [T, T] ---> T) $ t $ u
   1.239 +  end;
   1.240 +
   1.241 +fun mk_binrel c (t, u) =
   1.242 +  let val T = fastype_of t in
   1.243 +    Const (c, [T, T] ---> boolT) $ t $ u
   1.244 +  end;
   1.245 +
   1.246 +(*destruct the application of a binary operator. The dummyT case is a crude
   1.247 +  way of handling polymorphic operators.*)
   1.248 +fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
   1.249 +      if c = c' andalso (T=T' orelse T=dummyT) then (t, u)
   1.250 +      else raise TERM ("dest_bin " ^ c, [tm])
   1.251 +  | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
   1.252 +
   1.253 +
   1.254 +(* unit *)
   1.255 +
   1.256 +val unitT = Type ("Product_Type.unit", []);
   1.257 +
   1.258 +fun is_unitT (Type ("Product_Type.unit", [])) = true
   1.259 +  | is_unitT _ = false;
   1.260 +
   1.261 +val unit = Const ("Product_Type.Unity", unitT);
   1.262 +
   1.263 +fun is_unit (Const ("Product_Type.Unity", _)) = true
   1.264 +  | is_unit _ = false;
   1.265 +
   1.266 +
   1.267 +(* prod *)
   1.268 +
   1.269 +fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
   1.270 +
   1.271 +fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
   1.272 +  | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
   1.273 +
   1.274 +fun pair_const T1 T2 = Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2));
   1.275 +
   1.276 +fun mk_prod (t1, t2) =
   1.277 +  let val T1 = fastype_of t1 and T2 = fastype_of t2 in
   1.278 +    pair_const T1 T2 $ t1 $ t2
   1.279 +  end;
   1.280 +
   1.281 +fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
   1.282 +  | dest_prod t = raise TERM ("dest_prod", [t]);
   1.283 +
   1.284 +fun mk_fst p =
   1.285 +  let val pT = fastype_of p in
   1.286 +    Const ("fst", pT --> fst (dest_prodT pT)) $ p
   1.287 +  end;
   1.288 +
   1.289 +fun mk_snd p =
   1.290 +  let val pT = fastype_of p in
   1.291 +    Const ("snd", pT --> snd (dest_prodT pT)) $ p
   1.292 +  end;
   1.293 +
   1.294 +fun split_const (A, B, C) =
   1.295 +  Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C);
   1.296 +
   1.297 +fun mk_split t =
   1.298 +  (case Term.fastype_of t of
   1.299 +    T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
   1.300 +      Const ("split", T --> mk_prodT (A, B) --> C) $ t
   1.301 +  | _ => raise TERM ("mk_split: bad body type", [t]));
   1.302 +
   1.303 +(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
   1.304 +fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
   1.305 +  | prodT_factors T = [T];
   1.306 +
   1.307 +(*Makes a nested tuple from a list, following the product type structure*)
   1.308 +fun mk_tuple (Type ("*", [T1, T2])) tms =
   1.309 +        mk_prod (mk_tuple T1 tms,
   1.310 +                 mk_tuple T2 (Library.drop (length (prodT_factors T1), tms)))
   1.311 +  | mk_tuple T (t::_) = t;
   1.312 +
   1.313 +fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u
   1.314 +  | dest_tuple t = [t];
   1.315 +
   1.316 +(*In ap_split S T u, term u expects separate arguments for the factors of S,
   1.317 +  with result type T.  The call creates a new term expecting one argument
   1.318 +  of type S.*)
   1.319 +fun ap_split T T3 u =
   1.320 +  let
   1.321 +    fun ap (T :: Ts) =
   1.322 +          (case T of
   1.323 +             Type ("*", [T1, T2]) =>
   1.324 +               split_const (T1, T2, Ts ---> T3) $ ap (T1 :: T2 :: Ts)
   1.325 +           | _ => Abs ("x", T, ap Ts))
   1.326 +      | ap [] =
   1.327 +          let val k = length (prodT_factors T)
   1.328 +          in list_comb (incr_boundvars k u, map Bound (k - 1 downto 0)) end
   1.329 +  in ap [T] end;
   1.330 +
   1.331 +
   1.332 +(* operations on tuples with specific arities *)
   1.333 +(*
   1.334 +  an "arity" of a tuple is a list of lists of integers
   1.335 +  ("factors"), denoting paths to subterms that are pairs
   1.336 +*)
   1.337 +
   1.338 +fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
   1.339 +
   1.340 +fun prod_factors t =
   1.341 +  let
   1.342 +    fun factors p (Const ("Pair", _) $ t $ u) =
   1.343 +          p :: factors (1::p) t @ factors (2::p) u
   1.344 +      | factors p _ = []
   1.345 +  in factors [] t end;
   1.346 +
   1.347 +fun dest_tuple' ps =
   1.348 +  let
   1.349 +    fun dest p t = if p mem ps then (case t of
   1.350 +        Const ("Pair", _) $ t $ u =>
   1.351 +          dest (1::p) t @ dest (2::p) u
   1.352 +      | _ => prod_err "dest_tuple'") else [t]
   1.353 +  in dest [] end;
   1.354 +
   1.355 +fun prodT_factors' ps =
   1.356 +  let
   1.357 +    fun factors p T = if p mem ps then (case T of
   1.358 +        Type ("*", [T1, T2]) =>
   1.359 +          factors (1::p) T1 @ factors (2::p) T2
   1.360 +      | _ => prod_err "prodT_factors'") else [T]
   1.361 +  in factors [] end;
   1.362 +
   1.363 +(*In ap_split' ps S T u, term u expects separate arguments for the factors of S,
   1.364 +  with result type T.  The call creates a new term expecting one argument
   1.365 +  of type S.*)
   1.366 +fun ap_split' ps T T3 u =
   1.367 +  let
   1.368 +    fun ap ((p, T) :: pTs) =
   1.369 +          if p mem ps then (case T of
   1.370 +              Type ("*", [T1, T2]) =>
   1.371 +                split_const (T1, T2, map snd pTs ---> T3) $
   1.372 +                  ap ((1::p, T1) :: (2::p, T2) :: pTs)
   1.373 +            | _ => prod_err "ap_split'")
   1.374 +          else Abs ("x", T, ap pTs)
   1.375 +      | ap [] =
   1.376 +          let val k = length ps
   1.377 +          in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   1.378 +  in ap [([], T)] end;
   1.379 +
   1.380 +fun mk_tuple' ps =
   1.381 +  let
   1.382 +    fun mk p T ts =
   1.383 +      if p mem ps then (case T of
   1.384 +          Type ("*", [T1, T2]) =>
   1.385 +            let
   1.386 +              val (t, ts') = mk (1::p) T1 ts;
   1.387 +              val (u, ts'') = mk (2::p) T2 ts'
   1.388 +            in (pair_const T1 T2 $ t $ u, ts'') end
   1.389 +        | _ => prod_err "mk_tuple'")
   1.390 +      else (hd ts, tl ts)
   1.391 +  in fst oo mk [] end;
   1.392 +
   1.393 +fun mk_tupleT ps =
   1.394 +  let
   1.395 +    fun mk p Ts =
   1.396 +      if p mem ps then
   1.397 +        let
   1.398 +          val (T, Ts') = mk (1::p) Ts;
   1.399 +          val (U, Ts'') = mk (2::p) Ts'
   1.400 +        in (mk_prodT (T, U), Ts'') end
   1.401 +      else (hd Ts, tl Ts)
   1.402 +  in fst o mk [] end;
   1.403 +
   1.404 +fun strip_split t =
   1.405 +  let
   1.406 +    fun strip [] qs Ts t = (t, Ts, qs)
   1.407 +      | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
   1.408 +          strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   1.409 +      | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   1.410 +      | strip (p :: ps) qs Ts t = strip ps qs
   1.411 +          (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
   1.412 +          (incr_boundvars 1 t $ Bound 0)
   1.413 +  in strip [[]] [] [] t end;
   1.414 +
   1.415 +
   1.416 +(* nat *)
   1.417 +
   1.418 +val natT = Type ("nat", []);
   1.419 +
   1.420 +val zero = Const ("HOL.zero_class.zero", natT);
   1.421 +
   1.422 +fun is_zero (Const ("HOL.zero_class.zero", _)) = true
   1.423 +  | is_zero _ = false;
   1.424 +
   1.425 +fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   1.426 +
   1.427 +fun dest_Suc (Const ("Suc", _) $ t) = t
   1.428 +  | dest_Suc t = raise TERM ("dest_Suc", [t]);
   1.429 +
   1.430 +val Suc_zero = mk_Suc zero;
   1.431 +
   1.432 +fun mk_nat n =
   1.433 +  let
   1.434 +    fun mk 0 = zero
   1.435 +      | mk n = mk_Suc (mk (n - 1));
   1.436 +  in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
   1.437 +
   1.438 +fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
   1.439 +  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   1.440 +  | dest_nat t = raise TERM ("dest_nat", [t]);
   1.441 +
   1.442 +val class_size = "Nat.size";
   1.443 +
   1.444 +fun size_const T = Const ("Nat.size_class.size", T --> natT);
   1.445 +
   1.446 +
   1.447 +(* index *)
   1.448 +
   1.449 +val indexT = Type ("Code_Index.index", []);
   1.450 +
   1.451 +
   1.452 +(* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
   1.453 +
   1.454 +val intT = Type ("Int.int", []);
   1.455 +
   1.456 +val pls_const = Const ("Int.Pls", intT)
   1.457 +and min_const = Const ("Int.Min", intT)
   1.458 +and bit0_const = Const ("Int.Bit0", intT --> intT)
   1.459 +and bit1_const = Const ("Int.Bit1", intT --> intT);
   1.460 +
   1.461 +fun mk_bit 0 = bit0_const
   1.462 +  | mk_bit 1 = bit1_const
   1.463 +  | mk_bit _ = raise TERM ("mk_bit", []);
   1.464 +
   1.465 +fun dest_bit (Const ("Int.Bit0", _)) = 0
   1.466 +  | dest_bit (Const ("Int.Bit1", _)) = 1
   1.467 +  | dest_bit t = raise TERM ("dest_bit", [t]);
   1.468 +
   1.469 +fun mk_numeral 0 = pls_const
   1.470 +  | mk_numeral ~1 = min_const
   1.471 +  | mk_numeral i =
   1.472 +      let val (q, r) = Integer.div_mod i 2;
   1.473 +      in mk_bit r $ mk_numeral q end;
   1.474 +
   1.475 +fun dest_numeral (Const ("Int.Pls", _)) = 0
   1.476 +  | dest_numeral (Const ("Int.Min", _)) = ~1
   1.477 +  | dest_numeral (Const ("Int.Bit0", _) $ bs) = 2 * dest_numeral bs
   1.478 +  | dest_numeral (Const ("Int.Bit1", _) $ bs) = 2 * dest_numeral bs + 1
   1.479 +  | dest_numeral t = raise TERM ("dest_numeral", [t]);
   1.480 +
   1.481 +fun number_of_const T = Const ("Int.number_class.number_of", intT --> T);
   1.482 +
   1.483 +fun add_numerals (Const ("Int.number_class.number_of", Type (_, [_, T])) $ t) = cons (t, T)
   1.484 +  | add_numerals (t $ u) = add_numerals t #> add_numerals u
   1.485 +  | add_numerals (Abs (_, _, t)) = add_numerals t
   1.486 +  | add_numerals _ = I;
   1.487 +
   1.488 +fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
   1.489 +  | mk_number T 1 = Const ("HOL.one_class.one", T)
   1.490 +  | mk_number T i = number_of_const T $ mk_numeral i;
   1.491 +
   1.492 +fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
   1.493 +  | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
   1.494 +  | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) =
   1.495 +      (T, dest_numeral t)
   1.496 +  | dest_number t = raise TERM ("dest_number", [t]);
   1.497 +
   1.498 +
   1.499 +(* real *)
   1.500 +
   1.501 +val realT = Type ("RealDef.real", []);
   1.502 +
   1.503 +
   1.504 +(* nibble *)
   1.505 +
   1.506 +val nibbleT = Type ("List.nibble", []);
   1.507 +
   1.508 +fun mk_nibble n =
   1.509 +  let val s =
   1.510 +    if 0 <= n andalso n <= 9 then chr (n + ord "0")
   1.511 +    else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10)
   1.512 +    else raise TERM ("mk_nibble", [])
   1.513 +  in Const ("List.nibble.Nibble" ^ s, nibbleT) end;
   1.514 +
   1.515 +fun dest_nibble t =
   1.516 +  let fun err () = raise TERM ("dest_nibble", [t]) in
   1.517 +    (case try (unprefix "List.nibble.Nibble" o fst o Term.dest_Const) t of
   1.518 +      NONE => err ()
   1.519 +    | SOME c =>
   1.520 +        if size c <> 1 then err ()
   1.521 +        else if "0" <= c andalso c <= "9" then ord c - ord "0"
   1.522 +        else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
   1.523 +        else err ())
   1.524 +  end;
   1.525 +
   1.526 +
   1.527 +(* char *)
   1.528 +
   1.529 +val charT = Type ("List.char", []);
   1.530 +
   1.531 +fun mk_char n =
   1.532 +  if 0 <= n andalso n <= 255 then
   1.533 +    Const ("List.char.Char", nibbleT --> nibbleT --> charT) $
   1.534 +      mk_nibble (n div 16) $ mk_nibble (n mod 16)
   1.535 +  else raise TERM ("mk_char", []);
   1.536 +
   1.537 +fun dest_char (Const ("List.char.Char", _) $ t $ u) =
   1.538 +      dest_nibble t * 16 + dest_nibble u
   1.539 +  | dest_char t = raise TERM ("dest_char", [t]);
   1.540 +
   1.541 +
   1.542 +(* list *)
   1.543 +
   1.544 +fun listT T = Type ("List.list", [T]);
   1.545 +
   1.546 +fun nil_const T = Const ("List.list.Nil", listT T);
   1.547 +
   1.548 +fun cons_const T =
   1.549 +  let val lT = listT T
   1.550 +  in Const ("List.list.Cons", T --> lT --> lT) end;
   1.551 +
   1.552 +fun mk_list T ts =
   1.553 +  let
   1.554 +    val lT = listT T;
   1.555 +    val Nil = Const ("List.list.Nil", lT);
   1.556 +    fun Cons t u = Const ("List.list.Cons", T --> lT --> lT) $ t $ u;
   1.557 +  in fold_rev Cons ts Nil end;
   1.558 +
   1.559 +fun dest_list (Const ("List.list.Nil", _)) = []
   1.560 +  | dest_list (Const ("List.list.Cons", _) $ t $ u) = t :: dest_list u
   1.561 +  | dest_list t = raise TERM ("dest_list", [t]);
   1.562 +
   1.563 +
   1.564 +(* string *)
   1.565 +
   1.566 +val stringT = Type ("List.string", []);
   1.567 +
   1.568 +val mk_string = mk_list charT o map (mk_char o ord) o explode;
   1.569 +val dest_string = implode o map (chr o dest_char) o dest_list;
   1.570 +
   1.571 +end;