equal
deleted
inserted
replaced
1198 qed "length_upt"; |
1198 qed "length_upt"; |
1199 Addsimps [length_upt]; |
1199 Addsimps [length_upt]; |
1200 |
1200 |
1201 Goal "i+k < j --> [i..j(] ! k = i+k"; |
1201 Goal "i+k < j --> [i..j(] ! k = i+k"; |
1202 by (induct_tac "j" 1); |
1202 by (induct_tac "j" 1); |
1203 by (Simp_tac 1); |
1203 by (asm_simp_tac (simpset() addsimps [less_Suc_eq, nth_append] |
1204 by (asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1); |
1204 addsplits [nat_diff_split]) 2); |
1205 by (Clarify_tac 1); |
1205 by (Simp_tac 1); |
1206 by (subgoal_tac "n=i+k" 1); |
|
1207 by (Asm_simp_tac 2); |
|
1208 by (Asm_simp_tac 1); |
|
1209 qed_spec_mp "nth_upt"; |
1206 qed_spec_mp "nth_upt"; |
1210 Addsimps [nth_upt]; |
1207 Addsimps [nth_upt]; |
1211 |
1208 |
1212 Goal "!i. i+m <= n --> take m [i..n(] = [i..i+m(]"; |
1209 Goal "!i. i+m <= n --> take m [i..n(] = [i..i+m(]"; |
1213 by (induct_tac "m" 1); |
1210 by (induct_tac "m" 1); |