# HG changeset patch
# User nipkow
# Date 920897393 -3600
# Node ID fdf236c98914cfbcd768f27129c676bf2d4cf702
# Parent  81e7fbf61db26969b1f29a7af6adf4db166bcd92
Suc -> +1

diff -r 81e7fbf61db2 -r fdf236c98914 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Mon Mar 08 13:49:14 1999 +0100
+++ b/src/HOL/Lambda/Eta.ML	Mon Mar 08 13:49:53 1999 +0100
@@ -34,7 +34,7 @@
 Addsimps [free_lift];
 
 Goal "!i k t. free (s[t/k]) i = \
-\              (free s k & free t i | free s (if i<k then i else Suc i))";
+\              (free s k & free t i | free s (if i<k then i else i+1))";
 by (induct_tac "s" 1);
 by (Asm_simp_tac 2);
 by (Blast_tac 2);
@@ -113,7 +113,7 @@
 qed_spec_mp "beta_subst";
 AddIs [beta_subst];
 
-Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
+Goal "!i. t[Var i/i] = t[Var(i)/i+1]";
 by (induct_tac "t" 1);
 by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
 qed_spec_mp "subst_Var_Suc";
diff -r 81e7fbf61db2 -r fdf236c98914 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Mon Mar 08 13:49:14 1999 +0100
+++ b/src/HOL/Lambda/Eta.thy	Mon Mar 08 13:49:53 1999 +0100
@@ -22,7 +22,7 @@
 primrec
   "free (Var j) i = (j=i)"
   "free (s $ t) i = (free s i | free t i)"
-  "free (Abs s) i = free s (Suc i)"
+  "free (Abs s) i = free s (i+1)"
 
 inductive eta
 intrs
diff -r 81e7fbf61db2 -r fdf236c98914 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Mon Mar 08 13:49:14 1999 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Mon Mar 08 13:49:53 1999 +0100
@@ -62,12 +62,12 @@
 Addsimps [subst_eq,subst_gt,subst_lt];
 
 Goal
-  "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
+  "!i k. i < k+1 --> lift (lift t i) (Suc k) = lift (lift t k) i";
 by (induct_tac "t" 1);
 by (Auto_tac);
 qed_spec_mp "lift_lift";
 
-Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
+Goal "!i j s. j < i+1 --> lift (t[s/j]) i = (lift t (i+1)) [lift s i / j]";
 by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
                                 addsplits [nat.split])));
@@ -76,7 +76,7 @@
 Addsimps [lift_subst];
 
 Goal
-  "!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
+  "!i j s. i < j+1 --> lift (t[s/j]) i = (lift t i) [lift s i / j+1]";
 by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift])));
 qed "lift_subst_lt";
@@ -88,7 +88,7 @@
 Addsimps [subst_lift];
 
 
-Goal "!i j u v. i < Suc j --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
+Goal "!i j u v. i < j+1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
 by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
       (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
diff -r 81e7fbf61db2 -r fdf236c98914 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Mon Mar 08 13:49:14 1999 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Mon Mar 08 13:49:53 1999 +0100
@@ -19,26 +19,26 @@
   liftn  :: [nat,dB,nat] => dB
 
 primrec
-  "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
+  "lift (Var i) k = (if i < k then Var i else Var(i+1))"
   "lift (s $ t) k = (lift s k) $ (lift t k)"
-  "lift (Abs s) k = Abs(lift s (Suc k))"
+  "lift (Abs s) k = Abs(lift s (k+1))"
 
 primrec
   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])"
+  subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
 
 primrec
   "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
   "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
-  "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
+  "liftn n (Abs s) k = Abs(liftn n s (k+1))"
 
 primrec
   "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))"
+  "substn (Abs t) s k = Abs (substn t s (k+1))"
 
 consts  beta :: "(dB * dB) set"