Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lambda/Lambda.ML
changeset 6307 fdf236c98914
parent 6141 a6922171b396 
--- 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]
isabelle