src/HOL/Integ/NatBin.thy
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--
Linear arithmetic now copes with mixed nat/int formulae.
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