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