author | haftmann |
Mon, 21 Jan 2008 08:43:32 +0100 | |
changeset 25932 | db0fd0ecdcd4 |
parent 25919 | 8b1c0d434824 |
child 25967 | dd602eb20f3f |
permissions | -rw-r--r-- |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
1 |
(* Title: HOL/Tools/Int.ML |
23575
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 |
25932 | 12 |
val add_code: string -> bool -> bool -> string -> theory -> theory |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
13 |
end; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
14 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
15 |
structure Numeral: NUMERAL = |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
16 |
struct |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
17 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
18 |
(* numeral *) |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
19 |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
20 |
fun mk_cbit 0 = @{cterm "Int.bit.B0"} |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
21 |
| mk_cbit 1 = @{cterm "Int.bit.B1"} |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
22 |
| mk_cbit _ = raise CTERM ("mk_cbit", []); |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
23 |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
24 |
fun mk_cnumeral 0 = @{cterm "Int.Pls"} |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
25 |
| mk_cnumeral ~1 = @{cterm "Int.Min"} |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
26 |
| mk_cnumeral i = |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset
|
27 |
let val (q, r) = Integer.div_mod i 2 in |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
28 |
Thm.capply (Thm.capply @{cterm "Int.Bit"} (mk_cnumeral q)) (mk_cbit r) |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
29 |
end; |
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 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
32 |
(* number *) |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
33 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
34 |
local |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
35 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
36 |
val zero = @{cpat "0"}; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
37 |
val zeroT = Thm.ctyp_of_term zero; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
38 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
39 |
val one = @{cpat "1"}; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
40 |
val oneT = Thm.ctyp_of_term one; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
41 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
42 |
val number_of = @{cpat "number_of"}; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
43 |
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
|
44 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
45 |
fun instT T V = Thm.instantiate_cterm ([(V, T)], []); |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
46 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
47 |
in |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
48 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
49 |
fun mk_cnumber T 0 = instT T zeroT zero |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
50 |
| mk_cnumber T 1 = instT T oneT one |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
51 |
| 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
|
52 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
53 |
end; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
54 |
|
25932 | 55 |
|
56 |
(* code generator *) |
|
57 |
||
58 |
fun add_code number_of negative unbounded target = |
|
59 |
CodeTarget.add_pretty_numeral target unbounded negative number_of |
|
60 |
@{const_name Int.B0} @{const_name Int.B1} |
|
61 |
@{const_name Int.Pls} @{const_name Int.Min} |
|
62 |
@{const_name Int.Bit}; |
|
63 |
||
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
64 |
end; |