author | nipkow |
Thu, 15 Mar 2001 15:05:51 +0100 | |
changeset 11210 | 33300d16a63a |
parent 11080 | 22855d091249 |
child 11234 | 6902638af59e |
permissions | -rw-r--r-- |
10341 | 1 |
(* ID: $Id$ *) |
10295 | 2 |
(* EXTRACT from HOL/ex/Primes.thy*) |
3 |
||
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
4 |
(*Euclid's algorithm |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
5 |
This material now appears AFTER that of Forward.thy *) |
10295 | 6 |
theory Primes = Main: |
7 |
consts |
|
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
8 |
gcd :: "nat*nat \<Rightarrow> nat" |
10295 | 9 |
|
10986 | 10 |
recdef gcd "measure snd" |
10295 | 11 |
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |
12 |
||
13 |
||
14 |
ML "Pretty.setmargin 64" |
|
15 |
ML "IsarOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*) |
|
16 |
||
17 |
||
18 |
text {* |
|
19 |
\begin{quote} |
|
20 |
@{thm[display]"dvd_def"} |
|
21 |
\rulename{dvd_def} |
|
22 |
\end{quote} |
|
23 |
*}; |
|
24 |
||
25 |
||
26 |
(*** Euclid's Algorithm ***) |
|
27 |
||
28 |
lemma gcd_0 [simp]: "gcd(m,0) = m" |
|
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
29 |
apply (simp); |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
30 |
done |
10295 | 31 |
|
32 |
lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd(m,n) = gcd (n, m mod n)" |
|
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
33 |
apply (simp) |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
34 |
done; |
10295 | 35 |
|
36 |
declare gcd.simps [simp del]; |
|
37 |
||
38 |
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) |
|
39 |
lemma gcd_dvd_both: "(gcd(m,n) dvd m) \<and> (gcd(m,n) dvd n)" |
|
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
40 |
apply (induct_tac m n rule: gcd.induct) |
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
41 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
42 |
apply (case_tac "n=0") |
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
43 |
txt{*subgoals after the case tac |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
44 |
@{subgoals[display,indent=0,margin=65]} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
45 |
*}; |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
46 |
apply (simp_all) |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
47 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
48 |
by (blast dest: dvd_mod_imp_dvd) |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
49 |
|
10295 | 50 |
|
51 |
||
52 |
text {* |
|
53 |
@{thm[display] dvd_mod_imp_dvd} |
|
54 |
\rulename{dvd_mod_imp_dvd} |
|
55 |
||
56 |
@{thm[display] dvd_trans} |
|
57 |
\rulename{dvd_trans} |
|
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
58 |
*} |
10295 | 59 |
|
60 |
lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1] |
|
61 |
lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]; |
|
62 |
||
63 |
||
64 |
text {* |
|
65 |
\begin{quote} |
|
66 |
@{thm[display] gcd_dvd1} |
|
67 |
\rulename{gcd_dvd1} |
|
68 |
||
69 |
@{thm[display] gcd_dvd2} |
|
70 |
\rulename{gcd_dvd2} |
|
71 |
\end{quote} |
|
72 |
*}; |
|
73 |
||
74 |
(*Maximality: for all m,n,k naturals, |
|
75 |
if k divides m and k divides n then k divides gcd(m,n)*) |
|
76 |
lemma gcd_greatest [rule_format]: |
|
10790 | 77 |
"k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)" |
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
78 |
apply (induct_tac m n rule: gcd.induct) |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
79 |
apply (case_tac "n=0") |
10853 | 80 |
txt{*subgoals after the case tac |
81 |
@{subgoals[display,indent=0,margin=65]} |
|
82 |
*}; |
|
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
83 |
apply (simp_all add: dvd_mod) |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
84 |
done |
10295 | 85 |
|
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
86 |
text {* |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
87 |
@{thm[display] dvd_mod} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
88 |
\rulename{dvd_mod} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
89 |
*} |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
90 |
|
10853 | 91 |
(*just checking the claim that case_tac "n" works too*) |
92 |
lemma "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)" |
|
93 |
apply (induct_tac m n rule: gcd.induct) |
|
94 |
apply (case_tac "n") |
|
11080
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
95 |
apply (simp_all add: dvd_mod) |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
96 |
done |
22855d091249
various revisions in response to comments from Tobias
paulson
parents:
10986
diff
changeset
|
97 |
|
10853 | 98 |
|
10295 | 99 |
theorem gcd_greatest_iff [iff]: |
10795 | 100 |
"(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)" |
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
101 |
by (blast intro!: gcd_greatest intro: dvd_trans) |
10295 | 102 |
|
103 |
||
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
104 |
(**** The material below was omitted from the book ****) |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
105 |
|
10295 | 106 |
constdefs |
10300 | 107 |
is_gcd :: "[nat,nat,nat] \<Rightarrow> bool" (*gcd as a relation*) |
10295 | 108 |
"is_gcd p m n == p dvd m \<and> p dvd n \<and> |
109 |
(ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)" |
|
110 |
||
111 |
(*Function gcd yields the Greatest Common Divisor*) |
|
112 |
lemma is_gcd: "is_gcd (gcd(m,n)) m n" |
|
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
113 |
apply (simp add: is_gcd_def gcd_greatest); |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
114 |
done |
10295 | 115 |
|
116 |
(*uniqueness of GCDs*) |
|
117 |
lemma is_gcd_unique: "\<lbrakk> is_gcd m a b; is_gcd n a b \<rbrakk> \<Longrightarrow> m=n" |
|
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
118 |
apply (simp add: is_gcd_def); |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
119 |
apply (blast intro: dvd_anti_sym) |
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
10795
diff
changeset
|
120 |
done |
10295 | 121 |
|
122 |
||
123 |
text {* |
|
124 |
@{thm[display] dvd_anti_sym} |
|
125 |
\rulename{dvd_anti_sym} |
|
126 |
||
127 |
\begin{isabelle} |
|
128 |
proof\ (prove):\ step\ 1\isanewline |
|
129 |
\isanewline |
|
130 |
goal\ (lemma\ is_gcd_unique):\isanewline |
|
131 |
\isasymlbrakk is_gcd\ m\ a\ b;\ is_gcd\ n\ a\ b\isasymrbrakk \ \isasymLongrightarrow \ m\ =\ n\isanewline |
|
132 |
\ 1.\ \isasymlbrakk m\ dvd\ a\ \isasymand \ m\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ m);\isanewline |
|
133 |
\ \ \ \ \ \ \ n\ dvd\ a\ \isasymand \ n\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ n)\isasymrbrakk \isanewline |
|
134 |
\ \ \ \ \isasymLongrightarrow \ m\ =\ n |
|
135 |
\end{isabelle} |
|
136 |
*}; |
|
137 |
||
138 |
lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))" |
|
139 |
apply (rule is_gcd_unique) |
|
140 |
apply (rule is_gcd) |
|
141 |
apply (simp add: is_gcd_def); |
|
142 |
apply (blast intro: dvd_trans); |
|
143 |
done |
|
144 |
||
145 |
text{* |
|
146 |
\begin{isabelle} |
|
147 |
proof\ (prove):\ step\ 3\isanewline |
|
148 |
\isanewline |
|
149 |
goal\ (lemma\ gcd_assoc):\isanewline |
|
150 |
gcd\ (gcd\ (k,\ m),\ n)\ =\ gcd\ (k,\ gcd\ (m,\ n))\isanewline |
|
151 |
\ 1.\ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ k\ \isasymand \isanewline |
|
152 |
\ \ \ \ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ m\ \isasymand \ gcd\ (k,\ gcd\ (m,\ n))\ dvd\ n |
|
153 |
\end{isabelle} |
|
154 |
*} |
|
155 |
||
156 |
||
157 |
lemma gcd_dvd_gcd_mult: "gcd(m,n) dvd gcd(k*m, n)" |
|
158 |
apply (blast intro: dvd_trans); |
|
159 |
done |
|
160 |
||
161 |
(*This is half of the proof (by dvd_anti_sym) of*) |
|
162 |
lemma gcd_mult_cancel: "gcd(k,n) = 1 \<Longrightarrow> gcd(k*m, n) = gcd(m,n)" |
|
163 |
oops |
|
164 |
||
165 |
end |