equal
deleted
inserted
replaced
219 non-empty and infinite subsets of @{text S} obtained by successively |
219 non-empty and infinite subsets of @{text S} obtained by successively |
220 removing elements of @{text S}. |
220 removing elements of @{text S}. |
221 *} |
221 *} |
222 |
222 |
223 lemma linorder_injI: |
223 lemma linorder_injI: |
224 assumes hyp: "\<forall>x y. x < (y::'a::linorder) \<longrightarrow> f x \<noteq> f y" |
224 assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y" |
225 shows "inj f" |
225 shows "inj f" |
226 proof (rule inj_onI) |
226 proof (rule inj_onI) |
227 fix x y |
227 fix x y |
228 assume f_eq: "f x = f y" |
228 assume f_eq: "f x = f y" |
229 show "x = y" |
229 show "x = y" |
293 ultimately show "pick n \<noteq> pick (n + Suc m)" |
293 ultimately show "pick n \<noteq> pick (n + Suc m)" |
294 by auto |
294 by auto |
295 qed |
295 qed |
296 have inj: "inj pick" |
296 have inj: "inj pick" |
297 proof (rule linorder_injI) |
297 proof (rule linorder_injI) |
298 show "\<forall>i j. i<(j::nat) \<longrightarrow> pick i \<noteq> pick j" |
298 show "!!i j. i<(j::nat) ==> pick i \<noteq> pick j" |
299 proof (clarify) |
299 proof |
300 fix i j |
300 fix i j |
301 assume ij: "i<(j::nat)" |
301 assume ij: "i<(j::nat)" |
302 and eq: "pick i = pick j" |
302 and eq: "pick i = pick j" |
303 from ij obtain k where "j = i + (Suc k)" |
303 from ij obtain k where "j = i + (Suc k)" |
304 by (auto simp add: less_iff_Suc_add) |
304 by (auto simp add: less_iff_Suc_add) |