src/HOL/Tools/numeral.ML
author wenzelm
Tue, 18 Sep 2007 16:08:00 +0200
changeset 24630 351a308ab58d
parent 23575 543803006b3f
child 25919 8b1c0d434824
permissions -rw-r--r--
simplified type int (eliminated IntInf.int, integer);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/numeral.ML
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     4
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     5
Logical operations on numerals (see also HOL/hologic.ML).
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     6
*)
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     7
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     8
signature NUMERAL =
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     9
sig
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
    10
  val mk_cnumeral: int -> cterm
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
    11
  val mk_cnumber: ctyp -> int -> cterm
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    12
end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    13
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    14
structure Numeral: NUMERAL =
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    15
struct
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    16
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    17
(* numeral *)
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    18
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    19
fun mk_cbit 0 = @{cterm "Numeral.bit.B0"}
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    20
  | mk_cbit 1 = @{cterm "Numeral.bit.B1"}
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    21
  | mk_cbit _ = raise CTERM ("mk_cbit", []);
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    22
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    23
fun mk_cnumeral 0 = @{cterm "Numeral.Pls"}
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    24
  | mk_cnumeral ~1 = @{cterm "Numeral.Min"}
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    25
  | mk_cnumeral i =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
    26
      let val (q, r) = Integer.div_mod i 2 in
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
    27
        Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q)) (mk_cbit r)
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    28
      end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    29
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    30
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    31
(* number *)
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    32
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    33
local
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    34
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    35
val zero = @{cpat "0"};
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    36
val zeroT = Thm.ctyp_of_term zero;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    37
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    38
val one = @{cpat "1"};
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    39
val oneT = Thm.ctyp_of_term one;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    40
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    41
val number_of = @{cpat "number_of"};
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    42
val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    43
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    44
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    45
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    46
in
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    47
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    48
fun mk_cnumber T 0 = instT T zeroT zero
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    49
  | mk_cnumber T 1 = instT T oneT one
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    50
  | mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i);
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    51
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    52
end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    53
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    54
end;