equal
deleted
inserted
replaced
367 by Safe_tac; |
367 by Safe_tac; |
368 by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1); |
368 by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1); |
369 qed "diff_Suc_less"; |
369 qed "diff_Suc_less"; |
370 Addsimps [diff_Suc_less]; |
370 Addsimps [diff_Suc_less]; |
371 |
371 |
|
372 Goal "i<n ==> n - Suc i < n - i"; |
|
373 by (exhaust_tac "n" 1); |
|
374 by Safe_tac; |
|
375 by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1); |
|
376 qed "diff_Suc_less_diff"; |
|
377 |
372 Goal "!!n::nat. m - n <= Suc m - n"; |
378 Goal "!!n::nat. m - n <= Suc m - n"; |
373 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
379 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
374 by (ALLGOALS Asm_simp_tac); |
380 by (ALLGOALS Asm_simp_tac); |
375 qed "diff_le_Suc_diff"; |
381 qed "diff_le_Suc_diff"; |
376 |
382 |