equal
deleted
inserted
replaced
336 addSDs [Suc_inject] |
336 addSDs [Suc_inject] |
337 addEs [less_trans, lessE]) 1); |
337 addEs [less_trans, lessE]) 1); |
338 qed "Suc_mono"; |
338 qed "Suc_mono"; |
339 |
339 |
340 |
340 |
|
341 (* |
341 goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)"; |
342 goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)"; |
342 |
343 |
343 |
344 |
344 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)"; |
345 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)"; |
345 by(stac less_Suc_eq 1); |
346 by(stac less_Suc_eq 1); |
346 by(rtac |
347 by(rtac |
347 |
348 *) |
348 |
349 |
349 (* |
|
350 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)"; |
350 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)"; |
351 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]); |
351 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]); |
352 qed "Suc_less_eq"; |
352 qed "Suc_less_eq"; |
353 Addsimps [Suc_less_eq]; |
353 Addsimps [Suc_less_eq]; |
354 *) |
|
355 |
354 |
356 goal Nat.thy "~(Suc(n) < n)"; |
355 goal Nat.thy "~(Suc(n) < n)"; |
357 by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1); |
356 by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1); |
358 qed "not_Suc_n_less_n"; |
357 qed "not_Suc_n_less_n"; |
359 Addsimps [not_Suc_n_less_n]; |
358 Addsimps [not_Suc_n_less_n]; |