equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/numeral.ML |
1 (* Title: HOL/Tools/Int.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Makarius |
3 Author: Makarius |
4 |
4 |
5 Logical operations on numerals (see also HOL/hologic.ML). |
5 Logical operations on numerals (see also HOL/hologic.ML). |
6 *) |
6 *) |
14 structure Numeral: NUMERAL = |
14 structure Numeral: NUMERAL = |
15 struct |
15 struct |
16 |
16 |
17 (* numeral *) |
17 (* numeral *) |
18 |
18 |
19 fun mk_cbit 0 = @{cterm "Numeral.bit.B0"} |
19 fun mk_cbit 0 = @{cterm "Int.bit.B0"} |
20 | mk_cbit 1 = @{cterm "Numeral.bit.B1"} |
20 | mk_cbit 1 = @{cterm "Int.bit.B1"} |
21 | mk_cbit _ = raise CTERM ("mk_cbit", []); |
21 | mk_cbit _ = raise CTERM ("mk_cbit", []); |
22 |
22 |
23 fun mk_cnumeral 0 = @{cterm "Numeral.Pls"} |
23 fun mk_cnumeral 0 = @{cterm "Int.Pls"} |
24 | mk_cnumeral ~1 = @{cterm "Numeral.Min"} |
24 | mk_cnumeral ~1 = @{cterm "Int.Min"} |
25 | mk_cnumeral i = |
25 | mk_cnumeral i = |
26 let val (q, r) = Integer.div_mod i 2 in |
26 let val (q, r) = Integer.div_mod i 2 in |
27 Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q)) (mk_cbit r) |
27 Thm.capply (Thm.capply @{cterm "Int.Bit"} (mk_cnumeral q)) (mk_cbit r) |
28 end; |
28 end; |
29 |
29 |
30 |
30 |
31 (* number *) |
31 (* number *) |
32 |
32 |