1473

1 
(* Title: FOL/ex/nat2.thy

0

2 
ID: $Id$

1473

3 
Author: Tobias Nipkow

352

4 
Copyright 1994 University of Cambridge

0

5 
*)


6 

17245

7 
header {* Theory for examples of simplification and induction on the natural numbers *}

0

8 

17245

9 
theory Nat2


10 
imports FOL


11 
begin


12 


13 
typedecl nat


14 
arities nat :: "term"

0

15 

352

16 
consts

17245

17 
succ :: "nat => nat"


18 
pred :: "nat => nat"


19 
0 :: nat ("0")


20 
add :: "[nat,nat] => nat" (infixr "+" 90)


21 
lt :: "[nat,nat] => o" (infixr "<" 70)


22 
leq :: "[nat,nat] => o" (infixr "<=" 70)

0

23 

17245

24 
axioms


25 
pred_0: "pred(0) = 0"


26 
pred_succ: "pred(succ(m)) = m"

0

27 

17245

28 
plus_0: "0+n = n"


29 
plus_succ: "succ(m)+n = succ(m+n)"

0

30 

17245

31 
nat_distinct1: "~ 0=succ(n)"


32 
nat_distinct2: "~ succ(m)=0"


33 
succ_inject: "succ(m)=succ(n) <> m=n"


34 


35 
leq_0: "0 <= n"


36 
leq_succ_succ: "succ(m)<=succ(n) <> m<=n"


37 
leq_succ_0: "~ succ(m) <= 0"

0

38 

17245

39 
lt_0_succ: "0 < succ(n)"


40 
lt_succ_succ: "succ(m)<succ(n) <> m<n"


41 
lt_0: "~ m < 0"

0

42 

17245

43 
nat_ind: "[ P(0); ALL n. P(n)>P(succ(n)) ] ==> All(P)"

0

44 

17245

45 
ML {* use_legacy_bindings (the_context ()) *}


46 

0

47 
end
