Suc -> +1
authornipkow
Mon Mar 08 13:49:53 1999 +0100 (1999-03-08)
changeset 6307fdf236c98914
parent 6306 81e7fbf61db2
child 6308 76f3865a2b1d
Suc -> +1
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/Lambda.thy
     1.1 --- a/src/HOL/Lambda/Eta.ML	Mon Mar 08 13:49:14 1999 +0100
     1.2 +++ b/src/HOL/Lambda/Eta.ML	Mon Mar 08 13:49:53 1999 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  Addsimps [free_lift];
     1.5  
     1.6  Goal "!i k t. free (s[t/k]) i = \
     1.7 -\              (free s k & free t i | free s (if i<k then i else Suc i))";
     1.8 +\              (free s k & free t i | free s (if i<k then i else i+1))";
     1.9  by (induct_tac "s" 1);
    1.10  by (Asm_simp_tac 2);
    1.11  by (Blast_tac 2);
    1.12 @@ -113,7 +113,7 @@
    1.13  qed_spec_mp "beta_subst";
    1.14  AddIs [beta_subst];
    1.15  
    1.16 -Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
    1.17 +Goal "!i. t[Var i/i] = t[Var(i)/i+1]";
    1.18  by (induct_tac "t" 1);
    1.19  by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
    1.20  qed_spec_mp "subst_Var_Suc";
     2.1 --- a/src/HOL/Lambda/Eta.thy	Mon Mar 08 13:49:14 1999 +0100
     2.2 +++ b/src/HOL/Lambda/Eta.thy	Mon Mar 08 13:49:53 1999 +0100
     2.3 @@ -22,7 +22,7 @@
     2.4  primrec
     2.5    "free (Var j) i = (j=i)"
     2.6    "free (s $ t) i = (free s i | free t i)"
     2.7 -  "free (Abs s) i = free s (Suc i)"
     2.8 +  "free (Abs s) i = free s (i+1)"
     2.9  
    2.10  inductive eta
    2.11  intrs
     3.1 --- a/src/HOL/Lambda/Lambda.ML	Mon Mar 08 13:49:14 1999 +0100
     3.2 +++ b/src/HOL/Lambda/Lambda.ML	Mon Mar 08 13:49:53 1999 +0100
     3.3 @@ -62,12 +62,12 @@
     3.4  Addsimps [subst_eq,subst_gt,subst_lt];
     3.5  
     3.6  Goal
     3.7 -  "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
     3.8 +  "!i k. i < k+1 --> lift (lift t i) (Suc k) = lift (lift t k) i";
     3.9  by (induct_tac "t" 1);
    3.10  by (Auto_tac);
    3.11  qed_spec_mp "lift_lift";
    3.12  
    3.13 -Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
    3.14 +Goal "!i j s. j < i+1 --> lift (t[s/j]) i = (lift t (i+1)) [lift s i / j]";
    3.15  by (induct_tac "t" 1);
    3.16  by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
    3.17                                  addsplits [nat.split])));
    3.18 @@ -76,7 +76,7 @@
    3.19  Addsimps [lift_subst];
    3.20  
    3.21  Goal
    3.22 -  "!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
    3.23 +  "!i j s. i < j+1 --> lift (t[s/j]) i = (lift t i) [lift s i / j+1]";
    3.24  by (induct_tac "t" 1);
    3.25  by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift])));
    3.26  qed "lift_subst_lt";
    3.27 @@ -88,7 +88,7 @@
    3.28  Addsimps [subst_lift];
    3.29  
    3.30  
    3.31 -Goal "!i j u v. i < Suc j --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
    3.32 +Goal "!i j u v. i < j+1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
    3.33  by (induct_tac "t" 1);
    3.34  by (ALLGOALS(asm_simp_tac
    3.35        (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Mon Mar 08 13:49:14 1999 +0100
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Mon Mar 08 13:49:53 1999 +0100
     4.3 @@ -19,26 +19,26 @@
     4.4    liftn  :: [nat,dB,nat] => dB
     4.5  
     4.6  primrec
     4.7 -  "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
     4.8 +  "lift (Var i) k = (if i < k then Var i else Var(i+1))"
     4.9    "lift (s $ t) k = (lift s k) $ (lift t k)"
    4.10 -  "lift (Abs s) k = Abs(lift s (Suc k))"
    4.11 +  "lift (Abs s) k = Abs(lift s (k+1))"
    4.12  
    4.13  primrec
    4.14    subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
    4.15                              else if i = k then s else Var i)"
    4.16    subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
    4.17 -  subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
    4.18 +  subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
    4.19  
    4.20  primrec
    4.21    "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
    4.22    "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
    4.23 -  "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
    4.24 +  "liftn n (Abs s) k = Abs(liftn n s (k+1))"
    4.25  
    4.26  primrec
    4.27    "substn (Var i) s k = (if k < i then Var(i-1)
    4.28                           else if i = k then liftn k s 0 else Var i)"
    4.29    "substn (t $ u) s k = (substn t s k) $ (substn u s k)"
    4.30 -  "substn (Abs t) s k = Abs (substn t s (Suc k))"
    4.31 +  "substn (Abs t) s k = Abs (substn t s (k+1))"
    4.32  
    4.33  consts  beta :: "(dB * dB) set"
    4.34