equal
deleted
inserted
replaced
38 done |
38 done |
39 |
39 |
40 text{*No longer required as a simprule because of the @{text inverse_fold} |
40 text{*No longer required as a simprule because of the @{text inverse_fold} |
41 simproc*} |
41 simproc*} |
42 lemma Suc_diff_number_of: |
42 lemma Suc_diff_number_of: |
43 "neg (number_of (uminus v)::int) ==> |
43 "Int.Pls < v ==> |
44 Suc m - (number_of v) = m - (number_of (Int.pred v))" |
44 Suc m - (number_of v) = m - (number_of (Int.pred v))" |
45 apply (subst Suc_diff_eq_diff_pred) |
45 apply (subst Suc_diff_eq_diff_pred) |
46 apply simp |
46 apply simp |
47 apply (simp del: nat_numeral_1_eq_1) |
47 apply (simp del: nat_numeral_1_eq_1) |
48 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] |
48 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] |