# HG changeset patch
# User nipkow
# Date 845455037 -7200
# Node ID c5f004bfcbabf893f57dbe830c8180303e45980f
# Parent  2bfc0675c92ff842f31d4049af9813f2a2a407a7
Defined pred using nat_case rather than nat_rec.
Added expand_nat_case

diff -r 2bfc0675c92f -r c5f004bfcbab src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Oct 15 16:40:04 1996 +0200
+++ b/src/HOL/Arith.ML	Wed Oct 16 10:37:17 1996 +0200
@@ -11,11 +11,16 @@
 
 (*** Basic rewrite rules for the arithmetic operators ***)
 
-val [pred_0, pred_Suc] = nat_recs pred_def;
+goalw Arith.thy [pred_def] "pred 0 = 0";
+by(Simp_tac 1);
+qed "pred_0";
+
+goalw Arith.thy [pred_def] "pred(Suc n) = n";
+by(Simp_tac 1);
+qed "pred_Suc";
+
 val [add_0,add_Suc] = nat_recs add_def; 
 val [mult_0,mult_Suc] = nat_recs mult_def;
-store_thm("pred_0",pred_0);
-store_thm("pred_Suc",pred_Suc);
 store_thm("add_0",add_0);
 store_thm("add_Suc",add_Suc);
 store_thm("mult_0",mult_0);
diff -r 2bfc0675c92f -r c5f004bfcbab src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Tue Oct 15 16:40:04 1996 +0200
+++ b/src/HOL/Arith.thy	Wed Oct 16 10:37:17 1996 +0200
@@ -16,7 +16,7 @@
   div, mod  :: [nat, nat] => nat  (infixl 70)
 
 defs
-  pred_def  "pred(m) == nat_rec 0 (%n r.n) m"
+  pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
   add_def   "m+n == nat_rec n (%u v. Suc(v)) m"
   diff_def  "m-n == nat_rec m (%u v. pred(v)) n"
   mult_def  "m*n == nat_rec 0 (%u v. n + v) m"
diff -r 2bfc0675c92f -r c5f004bfcbab src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue Oct 15 16:40:04 1996 +0200
+++ b/src/HOL/Nat.ML	Wed Oct 16 10:37:17 1996 +0200
@@ -425,6 +425,10 @@
   "m=n ==> nat_rec a f m = nat_rec a f n"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
+qed_goal "expand_nat_case" Nat.thy
+  "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))"
+  (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
+
 val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)";
 by (resolve_tac prems 1);
 qed "leI";