src/HOL/Integ/NatBin.thy
author nipkow
Fri May 31 07:53:37 2002 +0200 (2002-05-31)
changeset 13189 81ed5c6de890
parent 13154 f1097ea60ba4
child 13491 ddf6ae639f21
permissions -rw-r--r--
Now arith can deal with div/mod arbitrary nat numerals.
     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 
     7 header {* Binary arithmetic for the natural numbers *}
     8 
     9 theory NatBin = IntPower
    10 files ("nat_bin.ML"):
    11 
    12 text {*
    13   This case is simply reduced to that for the non-negative integers.
    14 *}
    15 
    16 
    17 instance nat :: number ..
    18 
    19 defs (overloaded)
    20   nat_number_of_def: "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
    21 
    22 use "nat_bin.ML"
    23 setup nat_bin_arith_setup
    24 
    25 (* Enable arith to deal with div/mod k where k is a numeral: *)
    26 declare split_div[of _ _ "number_of k", standard, arith_split]
    27 declare split_mod[of _ _ "number_of k", standard, arith_split]
    28 
    29 lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
    30   by (simp add: number_of_Pls nat_number_of_def)
    31 
    32 lemma nat_number_of_Min: "number_of Min = (0::nat)"
    33   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
    34   apply (simp add: neg_nat)
    35   done
    36 
    37 lemma nat_number_of_BIT_True:
    38   "number_of (w BIT True) =
    39     (if neg (number_of w) then 0
    40      else let n = number_of w in Suc (n + n))"
    41   apply (simp only: nat_number_of_def Let_def split: split_if)
    42   apply (intro conjI impI)
    43    apply (simp add: neg_nat neg_number_of_BIT)
    44   apply (rule int_int_eq [THEN iffD1])
    45   apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
    46   apply (simp only: number_of_BIT if_True zadd_assoc)
    47   done
    48 
    49 lemma nat_number_of_BIT_False:
    50     "number_of (w BIT False) = (let n::nat = number_of w in n + n)"
    51   apply (simp only: nat_number_of_def Let_def)
    52   apply (cases "neg (number_of w)")
    53    apply (simp add: neg_nat neg_number_of_BIT)
    54   apply (rule int_int_eq [THEN iffD1])
    55   apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms)
    56   apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc)
    57   done
    58 
    59 lemmas nat_number =
    60   nat_number_of_Pls nat_number_of_Min
    61   nat_number_of_BIT_True nat_number_of_BIT_False
    62 
    63 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
    64   by (simp add: Let_def)
    65 
    66 
    67 subsection {* Configuration of the code generator *}
    68 
    69 ML {*
    70 infix 7 `*;
    71 infix 6 `+;
    72 
    73 val op `* = op * : int * int -> int;
    74 val op `+ = op + : int * int -> int;
    75 val `~ = ~ : int -> int;
    76 *}
    77 
    78 types_code
    79   "int" ("int")
    80 
    81 lemmas [code] = int_0 int_Suc
    82 
    83 lemma [code]: "nat x = (if x <= 0 then 0 else Suc (nat (x - 1)))"
    84   by (simp add: Suc_nat_eq_nat_zadd1)
    85 
    86 consts_code
    87   "0" :: "int"                  ("0")
    88   "1" :: "int"                  ("1")
    89   "uminus" :: "int => int"      ("`~")
    90   "op +" :: "int => int => int" ("(_ `+/ _)")
    91   "op *" :: "int => int => int" ("(_ `*/ _)")
    92   "neg"                         ("(_ < 0)")
    93 
    94 end