equal
deleted
inserted
replaced
48 "numbers_of_marks n (replicate m True) = {n..<n+m}" |
48 "numbers_of_marks n (replicate m True) = {n..<n+m}" |
49 by (auto simp add: numbers_of_marks_def enumerate_replicate_eq image_def) |
49 by (auto simp add: numbers_of_marks_def enumerate_replicate_eq image_def) |
50 |
50 |
51 lemma in_numbers_of_marks_eq: |
51 lemma in_numbers_of_marks_eq: |
52 "m \<in> numbers_of_marks n bs \<longleftrightarrow> m \<in> {n..<n + length bs} \<and> bs ! (m - n)" |
52 "m \<in> numbers_of_marks n bs \<longleftrightarrow> m \<in> {n..<n + length bs} \<and> bs ! (m - n)" |
53 by (simp add: numbers_of_marks_def in_set_enumerate_eq image_iff add_commute) |
53 by (simp add: numbers_of_marks_def in_set_enumerate_eq image_iff add.commute) |
54 |
54 |
55 lemma sorted_list_of_set_numbers_of_marks: |
55 lemma sorted_list_of_set_numbers_of_marks: |
56 "sorted_list_of_set (numbers_of_marks n bs) = map fst (filter snd (enumerate n bs))" |
56 "sorted_list_of_set (numbers_of_marks n bs) = map fst (filter snd (enumerate n bs))" |
57 by (auto simp add: numbers_of_marks_def distinct_map |
57 by (auto simp add: numbers_of_marks_def distinct_map |
58 intro!: sorted_filter distinct_filter inj_onI sorted_distinct_set_unique) |
58 intro!: sorted_filter distinct_filter inj_onI sorted_distinct_set_unique) |
139 by simp |
139 by simp |
140 then have "u + (w - u mod w) = w + u div w * w" |
140 then have "u + (w - u mod w) = w + u div w * w" |
141 by (simp add: div_mod_equality' [symmetric]) |
141 by (simp add: div_mod_equality' [symmetric]) |
142 } |
142 } |
143 then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)" |
143 then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)" |
144 by (simp add: add_assoc add_left_commute [of m] add_left_commute [of v] |
144 by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v] |
145 dvd_plus_eq_left dvd_plus_eq_right) |
145 dvd_plus_eq_left dvd_plus_eq_right) |
146 moreover from q have "Suc q = m + w + r" by (simp add: w_def) |
146 moreover from q have "Suc q = m + w + r" by (simp add: w_def) |
147 moreover from q have "Suc (Suc q) = v + w + r" by (simp add: v_def w_def) |
147 moreover from q have "Suc (Suc q) = v + w + r" by (simp add: v_def w_def) |
148 ultimately have "w dvd Suc (Suc (q + (w - v mod w))) \<longleftrightarrow> w dvd Suc (q + (w - m mod w))" |
148 ultimately have "w dvd Suc (Suc (q + (w - v mod w))) \<longleftrightarrow> w dvd Suc (q + (w - m mod w))" |
149 by (simp only: add_Suc [symmetric]) |
149 by (simp only: add_Suc [symmetric]) |