13957
|
1 |
(* Title: HOL/Hyperreal/ex/Sqrt_Script.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2001 University of Cambridge
|
|
5 |
*)
|
|
6 |
|
|
7 |
header {* Square roots of primes are irrational (script version) *}
|
|
8 |
|
|
9 |
theory Sqrt_Script = Primes + Hyperreal:
|
|
10 |
|
|
11 |
text {*
|
|
12 |
\medskip Contrast this linear Isabelle/Isar script with Markus
|
|
13 |
Wenzel's more mathematical version.
|
|
14 |
*}
|
|
15 |
|
|
16 |
subsection {* Preliminaries *}
|
|
17 |
|
|
18 |
lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p \<noteq> 0"
|
|
19 |
by (force simp add: prime_def)
|
|
20 |
|
|
21 |
lemma prime_dvd_other_side:
|
|
22 |
"n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
|
|
23 |
apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
|
|
24 |
apply (rule_tac j = "k * k" in dvd_mult_left, simp)
|
|
25 |
done
|
|
26 |
|
|
27 |
lemma reduction: "p \<in> prime \<Longrightarrow>
|
|
28 |
0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
|
|
29 |
apply (rule ccontr)
|
|
30 |
apply (simp add: linorder_not_less)
|
|
31 |
apply (erule disjE)
|
|
32 |
apply (frule mult_le_mono, assumption)
|
|
33 |
apply auto
|
|
34 |
apply (force simp add: prime_def)
|
|
35 |
done
|
|
36 |
|
|
37 |
lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"
|
|
38 |
by (simp add: mult_ac)
|
|
39 |
|
|
40 |
lemma prime_not_square:
|
|
41 |
"p \<in> prime \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
|
|
42 |
apply (induct m rule: nat_less_induct)
|
|
43 |
apply clarify
|
|
44 |
apply (frule prime_dvd_other_side, assumption)
|
|
45 |
apply (erule dvdE)
|
|
46 |
apply (simp add: nat_mult_eq_cancel_disj prime_nonzero)
|
|
47 |
apply (blast dest: rearrange reduction)
|
|
48 |
done
|
|
49 |
|
|
50 |
|
|
51 |
subsection {* The set of rational numbers *}
|
|
52 |
|
|
53 |
constdefs
|
|
54 |
rationals :: "real set" ("\<rat>")
|
|
55 |
"\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
|
|
56 |
|
|
57 |
|
|
58 |
subsection {* Main theorem *}
|
|
59 |
|
|
60 |
text {*
|
|
61 |
The square root of any prime number (including @{text 2}) is
|
|
62 |
irrational.
|
|
63 |
*}
|
|
64 |
|
|
65 |
theorem prime_sqrt_irrational:
|
|
66 |
"p \<in> prime \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
|
|
67 |
apply (simp add: rationals_def real_abs_def)
|
|
68 |
apply clarify
|
|
69 |
apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
|
|
70 |
apply (simp del: real_of_nat_mult
|
|
71 |
add: real_divide_eq_eq prime_not_square
|
|
72 |
real_of_nat_mult [symmetric])
|
|
73 |
done
|
|
74 |
|
|
75 |
lemmas two_sqrt_irrational =
|
|
76 |
prime_sqrt_irrational [OF two_is_prime]
|
|
77 |
|
|
78 |
end
|