src/FOL/ex/Nat2.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Nat2.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,39 @@
+(*  Title: 	FOL/ex/nat2.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1991  University of Cambridge
+
+Theory for examples of simplification and induction on the natural numbers
+*)
+
+Nat2 = FOL +
+
+types nat 0
+arities nat :: term
+
+consts succ,pred :: "nat => nat"
+       "0" :: "nat"	("0")
+       "+" :: "[nat,nat] => nat" (infixr 90)
+  "<","<=" :: "[nat,nat] => o"   (infixr 70)
+
+rules
+ pred_0		"pred(0) = 0"
+ pred_succ	"pred(succ(m)) = m"
+
+ plus_0		"0+n = n"
+ plus_succ	"succ(m)+n = succ(m+n)"
+
+ nat_distinct1	"~ 0=succ(n)"
+ nat_distinct2	"~ succ(m)=0"
+ succ_inject	"succ(m)=succ(n) <-> m=n"
+
+ leq_0		"0 <= n"
+ leq_succ_succ	"succ(m)<=succ(n) <-> m<=n"
+ leq_succ_0	"~ succ(m) <= 0"
+
+ lt_0_succ	"0 < succ(n)"
+ lt_succ_succ	"succ(m)<succ(n) <-> m<n"
+ lt_0 "~ m < 0"
+
+ nat_ind	"[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"
+end