equal
deleted
inserted
replaced
904 |
904 |
905 Goal "i+k < j --> [i..j(] ! k = i+k"; |
905 Goal "i+k < j --> [i..j(] ! k = i+k"; |
906 by(induct_tac "j" 1); |
906 by(induct_tac "j" 1); |
907 by(Simp_tac 1); |
907 by(Simp_tac 1); |
908 by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1); |
908 by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1); |
909 br conjI 1; |
|
910 by(Clarify_tac 1); |
|
911 bd add_lessD1 1; |
|
912 by(Simp_tac 1); |
|
913 by(Clarify_tac 1); |
|
914 br conjI 1; |
|
915 by(Clarify_tac 1); |
|
916 by(subgoal_tac "n=i+k" 1); |
|
917 by(Asm_full_simp_tac 1); |
|
918 by(Simp_tac 1); |
|
919 by(Clarify_tac 1); |
909 by(Clarify_tac 1); |
920 by(subgoal_tac "n=i+k" 1); |
910 by(subgoal_tac "n=i+k" 1); |
921 by(Asm_full_simp_tac 1); |
911 by(Asm_simp_tac 2); |
922 by(Simp_tac 1); |
912 by(Asm_simp_tac 1); |
923 qed_spec_mp "nth_upt"; |
913 qed_spec_mp "nth_upt"; |
924 Addsimps [nth_upt]; |
914 Addsimps [nth_upt]; |
925 |
915 |
926 |
916 |
927 (** nodups & remdups **) |
917 (** nodups & remdups **) |