author | haftmann |
Tue, 15 Jan 2008 16:19:23 +0100 | |
changeset 25919 | 8b1c0d434824 |
parent 24630 | 351a308ab58d |
child 25932 | db0fd0ecdcd4 |
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 |
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 |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
19 |
fun mk_cbit 0 = @{cterm "Int.bit.B0"} |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
20 |
| mk_cbit 1 = @{cterm "Int.bit.B1"} |
23575
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 |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
23 |
fun mk_cnumeral 0 = @{cterm "Int.Pls"} |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
24 |
| mk_cnumeral ~1 = @{cterm "Int.Min"} |
23575
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 |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset
|
27 |
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
|
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; |