equal
deleted
inserted
replaced
108 Addsimps [liftn_0]; |
108 Addsimps [liftn_0]; |
109 |
109 |
110 Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k"; |
110 Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k"; |
111 by (induct_tac "t" 1); |
111 by (induct_tac "t" 1); |
112 by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
112 by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
113 by (blast_tac (claset() addDs [add_lessD1]) 1); |
|
114 qed "liftn_lift"; |
113 qed "liftn_lift"; |
115 Addsimps [liftn_lift]; |
114 Addsimps [liftn_lift]; |
116 |
115 |
117 Goal "!n. substn t s n = t[liftn n s 0 / n]"; |
116 Goal "!n. substn t s n = t[liftn n s 0 / n]"; |
118 by (induct_tac "t" 1); |
117 by (induct_tac "t" 1); |