author | nipkow |
Fri, 01 Dec 2000 19:53:29 +0100 | |
changeset 10574 | 8f98f0301d67 |
parent 9509 | 0f3ee1f89ca8 |
child 11464 | ddea204de5bc |
permissions | -rw-r--r-- |
7032 | 1 |
(* Title: HOL/NatBin.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Binary arithmetic for the natural numbers |
|
7 |
||
8 |
This case is simply reduced to that for the non-negative integers |
|
9 |
*) |
|
10 |
||
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
9509
diff
changeset
|
11 |
theory NatBin = IntPower |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
9509
diff
changeset
|
12 |
files ("nat_bin.ML"): |
7032 | 13 |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
9509
diff
changeset
|
14 |
instance nat :: number .. |
7032 | 15 |
|
16 |
defs |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
9509
diff
changeset
|
17 |
nat_number_of_def: |
7032 | 18 |
"number_of v == nat (number_of v)" |
19 |
(*::bin=>nat ::bin=>int*) |
|
20 |
||
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
9509
diff
changeset
|
21 |
use "nat_bin.ML" setup nat_bin_arith_setup |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
9509
diff
changeset
|
22 |
|
7032 | 23 |
end |