equal
deleted
inserted
replaced
914 |
914 |
915 lemma Rats_induct [case_names of_rat, induct set: Rats]: |
915 lemma Rats_induct [case_names of_rat, induct set: Rats]: |
916 "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q" |
916 "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q" |
917 by (rule Rats_cases) auto |
917 by (rule Rats_cases) auto |
918 |
918 |
|
919 lemma Rats_infinite: "\<not> finite \<rat>" |
|
920 by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def) |
919 |
921 |
920 subsection {* Implementation of rational numbers as pairs of integers *} |
922 subsection {* Implementation of rational numbers as pairs of integers *} |
921 |
923 |
922 text {* Formal constructor *} |
924 text {* Formal constructor *} |
923 |
925 |