author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10435  b100e8d2c355 
child 11134  8bc06c4202cd 
permissions  rwrr 
923  1 
(* Title: HOL/Nat.thy 
2 
ID: $Id$ 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

3 
Author: Tobias Nipkow and Lawrence C Paulson 
923  4 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

5 
Type "nat" is a linear order, and a datatype; arithmetic operators +  
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

6 
and * (for div, mod and dvd, see theory Divides). 
923  7 
*) 
8 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
4640
diff
changeset

9 
Nat = NatDef + Inductive + 
923  10 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

11 
(* type "nat" is a linear order, and a datatype *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

12 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
4640
diff
changeset

13 
rep_datatype nat 
5714  14 
distinct Suc_not_Zero, Zero_not_Suc 
15 
inject Suc_Suc_eq 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
4640
diff
changeset

16 
induct nat_induct 
4104  17 

2608  18 
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le) 
4640  19 
instance nat :: linorder (nat_le_linear) 
1660  20 

10435  21 
axclass power < term 
22 

3370
5c5fdce3a4e4
Overloading of "^" requires new type class "power", with types "nat" and
paulson
parents:
2608
diff
changeset

23 
consts 
10435  24 
power :: ['a::power, nat] => 'a (infixr "^" 80) 
3370
5c5fdce3a4e4
Overloading of "^" requires new type class "power", with types "nat" and
paulson
parents:
2608
diff
changeset

25 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

26 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

27 
(* arithmetic operators +  and * *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

28 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

29 
instance 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

30 
nat :: {plus, minus, times, power} 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

31 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

32 
(* size of a datatype value; overloaded *) 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

33 
consts size :: 'a => nat 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

34 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

35 
primrec 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

36 
add_0 "0 + n = n" 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

37 
add_Suc "Suc m + n = Suc(m + n)" 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

38 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

39 
primrec 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

40 
diff_0 "m  0 = m" 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

41 
diff_Suc "m  Suc n = (case m  n of 0 => 0  Suc k => k)" 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

42 

62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

43 
primrec 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

44 
mult_0 "0 * n = 0" 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

45 
mult_Suc "Suc m * n = n + (m * n)" 
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

46 

923  47 
end 