author | oheimb |
Thu, 01 Feb 2001 20:51:48 +0100 | |
changeset 11025 | a70b796d9af8 |
parent 10574 | 8f98f0301d67 |
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 |