# HG changeset patch
# User nipkow
# Date 1032932544 -7200
# Node ID ecb6ecd9af130236c55ae4fff5907149557d9ce0
# Parent  f9796358e66f4645844e7241116a3e13ba8cea51
added nat_split

diff -r f9796358e66f -r ecb6ecd9af13 src/HOL/Integ/Int.thy
--- a/src/HOL/Integ/Int.thy	Sat Sep 21 21:10:34 2002 +0200
+++ b/src/HOL/Integ/Int.thy	Wed Sep 25 07:42:24 2002 +0200
@@ -6,17 +6,25 @@
 Type "int" is a linear order
 *)
 
-Int = IntDef + 
+theory Int = IntDef
+files ("int.ML"):
+
+instance int :: order
+proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
 
-instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
-instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_0)
-instance int :: linorder (zle_linear)
+instance int :: plus_ac0
+proof qed (rule zadd_commute zadd_assoc zadd_0)+
+
+instance int :: linorder
+proof qed (rule zle_linear)
 
 constdefs
-  nat  :: int => nat
-  "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
+  nat  :: "int => nat"
+ "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
 
-defs
-  zabs_def  "abs(i::int) == if i < 0 then -i else i"
+defs (overloaded)
+  zabs_def:  "abs(i::int) == if i < 0 then -i else i"
+
+use "int.ML"
 
 end
diff -r f9796358e66f -r ecb6ecd9af13 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Sat Sep 21 21:10:34 2002 +0200
+++ b/src/HOL/Integ/IntArith.thy	Wed Sep 25 07:42:24 2002 +0200
@@ -9,4 +9,20 @@
 use "int_arith2.ML"
 declare zabs_split [arith_split]
 
+lemma split_nat[arith_split]:
+  "P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
+  (is "?P = (?L & ?R)")
+proof (cases "i < 0")
+  case True thus ?thesis by simp
+next
+  case False
+  have "?P = ?L"
+  proof
+    assume ?P thus ?L using False by clarsimp
+  next
+    assume ?L thus ?P using False by simp
+  qed
+  with False show ?thesis by simp
+qed
+
 end