# HG changeset patch
# User nipkow
# Date 881235877 -3600
# Node ID 40e5c97e988d575d81593316a91e0564b66b4d19
# Parent  6f2986464280b66be6857ef5f02f8cc7891e5878
pred n -> n-1

diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Arith.ML	Thu Dec 04 12:44:37 1997 +0100
@@ -9,56 +9,38 @@
 
 (*** Basic rewrite rules for the arithmetic operators ***)
 
-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";
-
-Addsimps [pred_0,pred_Suc];
-
-(** pred **)
-
-val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
-by (res_inst_tac [("n","n")] natE 1);
-by (cut_facts_tac prems 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "Suc_pred";
-Addsimps [Suc_pred];
-
-goal Arith.thy "pred(n) <= (n::nat)";
-by (res_inst_tac [("n","n")] natE 1);
-by (ALLGOALS Asm_simp_tac);
-qed "pred_le";
-AddIffs [pred_le];
-
-goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
-by (simp_tac (simpset() addsplits [expand_nat_case]) 1);
-qed_spec_mp "pred_le_mono";
-
-goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
-by (exhaust_tac "n" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "pred_less";
-Addsimps [pred_less];
 
 (** Difference **)
 
-qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
+qed_goal "diff_0_eq_0" Arith.thy
     "0 - n = 0"
  (fn _ => [induct_tac "n" 1,  ALLGOALS Asm_simp_tac]);
 
 (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
   Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
-qed_goalw "diff_Suc_Suc" Arith.thy [pred_def]
+qed_goal "diff_Suc_Suc" Arith.thy
     "Suc(m) - Suc(n) = m - n"
  (fn _ =>
   [Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
 
 Addsimps [diff_0_eq_0, diff_Suc_Suc];
 
+(* Could be (and is, below) generalized in various ways;
+   However, none of the generalizations are currently in the simpset,
+   and I dread to think what happens if I put them in *)
+goal Arith.thy "!!n. 0 < n ==> Suc(n-1) = n";
+by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
+qed "Suc_pred";
+Addsimps [Suc_pred];
+
+(* Generalize? *)
+goal Arith.thy "!!n. 0<n ==> n-1 < n";
+by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
+qed "pred_less";
+Addsimps [pred_less];
+
+Delsimps [diff_Suc];
+
 
 (**** Inductive properties of the operators ****)
 
@@ -120,17 +102,25 @@
 by (induct_tac "m" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "add_is_0";
-Addsimps [add_is_0];
+AddIffs [add_is_0];
 
-goal Arith.thy "(pred (m+n) = 0) = (m=0 & pred n = 0 | pred m = 0 & n=0)";
-by (induct_tac "m" 1);
+goal Arith.thy "(0<m+n) = (0<m | 0<n)";
+by(simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
+qed "add_gr_0";
+AddIffs [add_gr_0];
+
+(* FIXME: really needed?? *)
+goal Arith.thy "((m+n)-1 = 0) = (m=0 & n-1 = 0 | m-1 = 0 & n=0)";
+by (exhaust_tac "m" 1);
 by (ALLGOALS (fast_tac (claset() addss (simpset()))));
 qed "pred_add_is_0";
 Addsimps [pred_add_is_0];
 
+(* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
 goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
+by (exhaust_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
+                                      addsplits [expand_nat_case])));
 qed "add_pred";
 Addsimps [add_pred];
 
@@ -336,9 +326,6 @@
 
 (*** Difference ***)
 
-qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n"
- (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
-Addsimps [pred_Suc_diff];
 
 qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
  (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
@@ -359,7 +346,6 @@
 qed "le_add_diff_inverse2";
 
 Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
-Delsimps  [diff_Suc];
 
 
 (*** More results about difference ***)
@@ -387,6 +373,14 @@
 by (ALLGOALS Asm_simp_tac);
 qed "diff_diff_left";
 
+(* This is a trivial consequence of diff_diff_left;
+   could be got rid of if diff_diff_left were in the simpset...
+*)
+goal Arith.thy "(Suc m - n)-1 = m - n";
+by(simp_tac (simpset() addsimps [diff_diff_left]) 1);
+qed "pred_Suc_diff";
+Addsimps [pred_Suc_diff];
+
 (*This and the next few suggested by Florian Kammueller*)
 goal Arith.thy "!!i::nat. i-j-k = i-k-j";
 by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
@@ -654,7 +648,7 @@
 by (atac 1);
 by (etac le_trans 1);
 by (res_inst_tac [("m1","n")] (pred_Suc_diff RS subst) 1);
-by (rtac pred_le 1);
+by (simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
 qed_spec_mp "diff_le_mono";
 
 goal Arith.thy "!!n::nat. m<=n ==> (l-n) <= (l-m)";
diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Arith.thy	Thu Dec 04 12:44:37 1997 +0100
@@ -11,13 +11,8 @@
 instance
   nat :: {plus, minus, times, power}
 
-consts
-  pred      :: nat => nat
-  (* size of a datatype value; overloaded *)
-  size      :: 'a => nat
-
-defs
-  pred_def  "pred(m) == case m of 0 => 0 | Suc n => n"
+(* size of a datatype value; overloaded *)
+consts size :: 'a => nat
 
 primrec "op +" nat 
   add_0    "0 + n = n"
@@ -25,7 +20,10 @@
 
 primrec "op -" nat 
   diff_0   "m - 0 = m"
-  diff_Suc "m - Suc n = pred(m - n)"
+  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+
+syntax pred :: nat => nat
+translations "pred m" => "m - 1"
 
 primrec "op *"  nat 
   mult_0   "0 * n = 0"
diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Lambda/Eta.ML	Thu Dec 04 12:44:37 1997 +0100
@@ -33,11 +33,11 @@
 Addsimps [subst_not_free RS eqTrueI];
 
 goal Eta.thy "!i k. free (lift t k) i = \
-\                   (i < k & free t i | k < i & free t (pred i))";
+\                   (i < k & free t i | k < i & free t (i-1))";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
 by (Blast_tac 2);
-by (simp_tac (simpset() addsimps [pred_def] addsplits [expand_nat_case]) 1);
+by (simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
 qed "free_lift";
@@ -49,7 +49,7 @@
 by (Asm_simp_tac 2);
 by (Blast_tac 2);
 by (asm_full_simp_tac (addsplit (simpset())) 2);
-by (simp_tac (simpset() addsimps [pred_def,subst_Var]
+by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
                       addsplits [expand_if,expand_nat_case]) 1);
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
 by (ALLGOALS trans_tac);
@@ -173,7 +173,7 @@
    by (etac nat_neqE 1);
     by (res_inst_tac [("x","Var nat")] exI 1);
     by (Asm_simp_tac 1);
-   by (res_inst_tac [("x","Var(pred nat)")] exI 1);
+   by (res_inst_tac [("x","Var(nat-1)")] exI 1);
    by (Asm_simp_tac 1);
   by (rtac notE 1);
    by (assume_tac 2);
diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Thu Dec 04 12:44:37 1997 +0100
@@ -52,7 +52,7 @@
 by (asm_full_simp_tac(addsplit(simpset())) 1);
 qed "subst_eq";
 
-goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)";
+goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(j-1)";
 by (asm_full_simp_tac(addsplit(simpset())) 1);
 qed "subst_gt";
 
@@ -75,7 +75,7 @@
 goal Lambda.thy "!i j s. j < Suc i --> \
 \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
 by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [pred_def,subst_Var,lift_lift]
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
                                 addsplits [expand_if,expand_nat_case]
                                 addSolver cut_trans_tac)));
 by (safe_tac HOL_cs);
@@ -105,7 +105,7 @@
 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
-      (simpset() addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
+      (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
                 addsplits [expand_if,expand_nat_case]
                 addSolver cut_trans_tac)));
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Thu Dec 04 12:44:37 1997 +0100
@@ -24,7 +24,7 @@
   "lift (Abs s) k = Abs(lift s (Suc k))"
 
 primrec subst dB
-  subst_Var "(Var i)[s/k] = (if k < i then Var(pred i)
+  subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
                             else if i = k then s else Var i)"
   subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]"
   subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
@@ -35,7 +35,7 @@
   "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
 
 primrec substn dB
-  "substn (Var i) s k = (if k < i then Var(pred i)
+  "substn (Var i) s k = (if k < i then Var(i-1)
                          else if i = k then liftn k s 0 else Var i)"
   "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
   "substn (Abs t) s k = Abs (substn t s (Suc k))"