equal
deleted
inserted
replaced
11 text {* |
11 text {* |
12 \medskip Contrast this linear Isar script with Markus Wenzel's more |
12 \medskip Contrast this linear Isar script with Markus Wenzel's more |
13 mathematical version. |
13 mathematical version. |
14 *} |
14 *} |
15 |
15 |
16 section {* Preliminaries *} |
16 subsection {* Preliminaries *} |
17 |
17 |
18 lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p\<noteq>0" |
18 lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p\<noteq>0" |
19 by (force simp add: prime_def) |
19 by (force simp add: prime_def) |
20 |
20 |
21 lemma prime_dvd_other_side: "\<lbrakk>n*n = p*(k*k); p \<in> prime\<rbrakk> \<Longrightarrow> p dvd n" |
21 lemma prime_dvd_other_side: "\<lbrakk>n*n = p*(k*k); p \<in> prime\<rbrakk> \<Longrightarrow> p dvd n" |
44 apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) |
44 apply (simp add: nat_mult_eq_cancel_disj prime_nonzero) |
45 apply (blast dest: rearrange reduction) |
45 apply (blast dest: rearrange reduction) |
46 done |
46 done |
47 |
47 |
48 |
48 |
49 section {* The set of rational numbers [Borrowed from Markus Wenzel] *} |
49 subsection {* The set of rational numbers *} |
50 |
50 |
51 constdefs |
51 constdefs |
52 rationals :: "real set" ("\<rat>") |
52 rationals :: "real set" ("\<rat>") |
53 "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
53 "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
54 |
54 |
55 |
55 |
56 section {* Main theorem *} |
56 subsection {* Main theorem *} |
57 |
57 |
58 text {* |
58 text {* |
59 The square root of any prime number (including @{text 2}) is |
59 The square root of any prime number (including @{text 2}) is |
60 irrational. |
60 irrational. |
61 *} |
61 *} |