src/HOL/Arith.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5183 89f162de39cf
child 8929 4829556a56f8
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Arith.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Arithmetic operators + - and * (for div, mod and dvd, see Divides)
     7 *)
     8 
     9 Arith = Nat +
    10 
    11 instance
    12   nat :: {plus, minus, times, power}
    13 
    14 (* size of a datatype value; overloaded *)
    15 consts size :: 'a => nat
    16 
    17 primrec
    18   add_0    "0 + n = n"
    19   add_Suc  "Suc m + n = Suc(m + n)"
    20 
    21 primrec
    22   diff_0   "m - 0 = m"
    23   diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    24 
    25 primrec
    26   mult_0   "0 * n = 0"
    27   mult_Suc "Suc m * n = n + (m * n)"
    28 
    29 end