src/HOL/Nat.thy
 author oheimb Thu Feb 15 16:00:36 2001 +0100 (2001-02-15) changeset 11134 8bc06c4202cd parent 10435 b100e8d2c355 child 11325 a5e0289dd56c permissions -rw-r--r--
added nat as instance of new wellorder axclass
```     1 (*  Title:      HOL/Nat.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow and Lawrence C Paulson
```
```     4
```
```     5 Type "nat" is a linear order, and a datatype; arithmetic operators + -
```
```     6 and * (for div, mod and dvd, see theory Divides).
```
```     7 *)
```
```     8
```
```     9 Nat = NatDef + Inductive +
```
```    10
```
```    11 (* type "nat" is a wellfounded linear order, and a datatype *)
```
```    12
```
```    13 rep_datatype nat
```
```    14   distinct Suc_not_Zero, Zero_not_Suc
```
```    15   inject   Suc_Suc_eq
```
```    16   induct   nat_induct
```
```    17
```
```    18 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
```
```    19 instance nat :: linorder (nat_le_linear)
```
```    20 instance nat :: wellorder (wf_less)
```
```    21
```
```    22 axclass power < term
```
```    23
```
```    24 consts
```
```    25   power :: ['a::power, nat] => 'a            (infixr "^" 80)
```
```    26
```
```    27
```
```    28 (* arithmetic operators + - and * *)
```
```    29
```
```    30 instance
```
```    31   nat :: {plus, minus, times, power}
```
```    32
```
```    33 (* size of a datatype value; overloaded *)
```
```    34 consts size :: 'a => nat
```
```    35
```
```    36 primrec
```
```    37   add_0    "0 + n = n"
```
```    38   add_Suc  "Suc m + n = Suc(m + n)"
```
```    39
```
```    40 primrec
```
```    41   diff_0   "m - 0 = m"
```
```    42   diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
```
```    43
```
```    44 primrec
```
```    45   mult_0   "0 * n = 0"
```
```    46   mult_Suc "Suc m * n = n + (m * n)"
```
```    47
```
```    48 end
```