author | hoelzl |
Mon, 03 Dec 2012 18:19:08 +0100 | |
changeset 50328 | 25b1e8686ce0 |
parent 50178 | ad52ddd35c3a |
child 51126 | df86080de4cb |
permissions | -rw-r--r-- |
35372 | 1 |
(* Title: HOL/Rat.thy |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
3 |
*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
4 |
|
14691 | 5 |
header {* Rational numbers *} |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
6 |
|
35372 | 7 |
theory Rat |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
8 |
imports GCD Archimedean_Field |
15131 | 9 |
begin |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
10 |
|
27551 | 11 |
subsection {* Rational numbers as quotient *} |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
12 |
|
27551 | 13 |
subsubsection {* Construction of the type of rational numbers *} |
18913 | 14 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20522
diff
changeset
|
15 |
definition |
47906 | 16 |
ratrel :: "(int \<times> int) \<Rightarrow> (int \<times> int) \<Rightarrow> bool" where |
17 |
"ratrel = (\<lambda>x y. snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x)" |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
18 |
|
18913 | 19 |
lemma ratrel_iff [simp]: |
47906 | 20 |
"ratrel x y \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x" |
27551 | 21 |
by (simp add: ratrel_def) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
22 |
|
47906 | 23 |
lemma exists_ratrel_refl: "\<exists>x. ratrel x x" |
24 |
by (auto intro!: one_neq_zero) |
|
18913 | 25 |
|
47906 | 26 |
lemma symp_ratrel: "symp ratrel" |
27 |
by (simp add: ratrel_def symp_def) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
28 |
|
47906 | 29 |
lemma transp_ratrel: "transp ratrel" |
30 |
proof (rule transpI, unfold split_paired_all) |
|
27551 | 31 |
fix a b a' b' a'' b'' :: int |
47906 | 32 |
assume A: "ratrel (a, b) (a', b')" |
33 |
assume B: "ratrel (a', b') (a'', b'')" |
|
27551 | 34 |
have "b' * (a * b'') = b'' * (a * b')" by simp |
35 |
also from A have "a * b' = a' * b" by auto |
|
36 |
also have "b'' * (a' * b) = b * (a' * b'')" by simp |
|
37 |
also from B have "a' * b'' = a'' * b'" by auto |
|
38 |
also have "b * (a'' * b') = b' * (a'' * b)" by simp |
|
39 |
finally have "b' * (a * b'') = b' * (a'' * b)" . |
|
40 |
moreover from B have "b' \<noteq> 0" by auto |
|
41 |
ultimately have "a * b'' = a'' * b" by simp |
|
47906 | 42 |
with A B show "ratrel (a, b) (a'', b'')" by auto |
27551 | 43 |
qed |
44 |
||
47906 | 45 |
lemma part_equivp_ratrel: "part_equivp ratrel" |
46 |
by (rule part_equivpI [OF exists_ratrel_refl symp_ratrel transp_ratrel]) |
|
47 |
||
48 |
quotient_type rat = "int \<times> int" / partial: "ratrel" |
|
49 |
morphisms Rep_Rat Abs_Rat |
|
50 |
by (rule part_equivp_ratrel) |
|
27551 | 51 |
|
47906 | 52 |
declare rat.forall_transfer [transfer_rule del] |
53 |
||
54 |
lemma forall_rat_transfer [transfer_rule]: (* TODO: generate automatically *) |
|
55 |
"(fun_rel (fun_rel cr_rat op =) op =) |
|
56 |
(transfer_bforall (\<lambda>x. snd x \<noteq> 0)) transfer_forall" |
|
57 |
using rat.forall_transfer by simp |
|
27551 | 58 |
|
59 |
||
60 |
subsubsection {* Representation and basic operations *} |
|
61 |
||
47906 | 62 |
lift_definition Fract :: "int \<Rightarrow> int \<Rightarrow> rat" |
63 |
is "\<lambda>a b. if b = 0 then (0, 1) else (a, b)" |
|
64 |
by simp |
|
27551 | 65 |
|
66 |
lemma eq_rat: |
|
67 |
shows "\<And>a b c d. b \<noteq> 0 \<Longrightarrow> d \<noteq> 0 \<Longrightarrow> Fract a b = Fract c d \<longleftrightarrow> a * d = c * b" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
68 |
and "\<And>a. Fract a 0 = Fract 0 1" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
69 |
and "\<And>a c. Fract 0 a = Fract 0 c" |
47906 | 70 |
by (transfer, simp)+ |
27551 | 71 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
72 |
lemma Rat_cases [case_names Fract, cases type: rat]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
73 |
assumes "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
74 |
shows C |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
75 |
proof - |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
76 |
obtain a b :: int where "q = Fract a b" and "b \<noteq> 0" |
47906 | 77 |
by transfer simp |
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
78 |
let ?a = "a div gcd a b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
79 |
let ?b = "b div gcd a b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
80 |
from `b \<noteq> 0` have "?b * gcd a b = b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
81 |
by (simp add: dvd_div_mult_self) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
82 |
with `b \<noteq> 0` have "?b \<noteq> 0" by auto |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
83 |
from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
84 |
by (simp add: eq_rat dvd_div_mult mult_commute [of a]) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
85 |
from `b \<noteq> 0` have coprime: "coprime ?a ?b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
86 |
by (auto intro: div_gcd_coprime_int) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
87 |
show C proof (cases "b > 0") |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
88 |
case True |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
89 |
note assms |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
90 |
moreover note q |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
91 |
moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
92 |
moreover note coprime |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
93 |
ultimately show C . |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
94 |
next |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
95 |
case False |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
96 |
note assms |
47906 | 97 |
moreover have "q = Fract (- ?a) (- ?b)" unfolding q by transfer simp |
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
98 |
moreover from False `b \<noteq> 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
99 |
moreover from coprime have "coprime (- ?a) (- ?b)" by simp |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
100 |
ultimately show C . |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
101 |
qed |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
102 |
qed |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
103 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
104 |
lemma Rat_induct [case_names Fract, induct type: rat]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
105 |
assumes "\<And>a b. b > 0 \<Longrightarrow> coprime a b \<Longrightarrow> P (Fract a b)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
106 |
shows "P q" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
107 |
using assms by (cases q) simp |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
108 |
|
47906 | 109 |
instantiation rat :: field_inverse_zero |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
110 |
begin |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
111 |
|
47906 | 112 |
lift_definition zero_rat :: "rat" is "(0, 1)" |
113 |
by simp |
|
114 |
||
115 |
lift_definition one_rat :: "rat" is "(1, 1)" |
|
116 |
by simp |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
117 |
|
47906 | 118 |
lemma Zero_rat_def: "0 = Fract 0 1" |
119 |
by transfer simp |
|
18913 | 120 |
|
47906 | 121 |
lemma One_rat_def: "1 = Fract 1 1" |
122 |
by transfer simp |
|
123 |
||
124 |
lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" |
|
125 |
is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)" |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset
|
126 |
by (clarsimp, simp add: distrib_right, simp add: mult_ac) |
27551 | 127 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
128 |
lemma add_rat [simp]: |
27551 | 129 |
assumes "b \<noteq> 0" and "d \<noteq> 0" |
130 |
shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
|
47906 | 131 |
using assms by transfer simp |
18913 | 132 |
|
47906 | 133 |
lift_definition uminus_rat :: "rat \<Rightarrow> rat" is "\<lambda>x. (- fst x, snd x)" |
134 |
by simp |
|
27551 | 135 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
136 |
lemma minus_rat [simp]: "- Fract a b = Fract (- a) b" |
47906 | 137 |
by transfer simp |
27551 | 138 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
139 |
lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b" |
27551 | 140 |
by (cases "b = 0") (simp_all add: eq_rat) |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
141 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
142 |
definition |
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
143 |
diff_rat_def: "q - r = q + - (r::rat)" |
18913 | 144 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
145 |
lemma diff_rat [simp]: |
27551 | 146 |
assumes "b \<noteq> 0" and "d \<noteq> 0" |
147 |
shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
148 |
using assms by (simp add: diff_rat_def) |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset
|
149 |
|
47906 | 150 |
lift_definition times_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" |
151 |
is "\<lambda>x y. (fst x * fst y, snd x * snd y)" |
|
152 |
by (simp add: mult_ac) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
153 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
154 |
lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)" |
47906 | 155 |
by transfer simp |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
156 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
157 |
lemma mult_rat_cancel: |
27551 | 158 |
assumes "c \<noteq> 0" |
159 |
shows "Fract (c * a) (c * b) = Fract a b" |
|
47906 | 160 |
using assms by transfer simp |
161 |
||
162 |
lift_definition inverse_rat :: "rat \<Rightarrow> rat" |
|
163 |
is "\<lambda>x. if fst x = 0 then (0, 1) else (snd x, fst x)" |
|
164 |
by (auto simp add: mult_commute) |
|
165 |
||
166 |
lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" |
|
167 |
by transfer simp |
|
168 |
||
169 |
definition |
|
170 |
divide_rat_def: "q / r = q * inverse (r::rat)" |
|
171 |
||
172 |
lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" |
|
173 |
by (simp add: divide_rat_def) |
|
27509 | 174 |
|
175 |
instance proof |
|
47906 | 176 |
fix q r s :: rat |
177 |
show "(q * r) * s = q * (r * s)" |
|
178 |
by transfer simp |
|
179 |
show "q * r = r * q" |
|
180 |
by transfer simp |
|
181 |
show "1 * q = q" |
|
182 |
by transfer simp |
|
183 |
show "(q + r) + s = q + (r + s)" |
|
184 |
by transfer (simp add: algebra_simps) |
|
185 |
show "q + r = r + q" |
|
186 |
by transfer simp |
|
187 |
show "0 + q = q" |
|
188 |
by transfer simp |
|
189 |
show "- q + q = 0" |
|
190 |
by transfer simp |
|
191 |
show "q - r = q + - r" |
|
192 |
by (fact diff_rat_def) |
|
193 |
show "(q + r) * s = q * s + r * s" |
|
194 |
by transfer (simp add: algebra_simps) |
|
195 |
show "(0::rat) \<noteq> 1" |
|
196 |
by transfer simp |
|
197 |
{ assume "q \<noteq> 0" thus "inverse q * q = 1" |
|
198 |
by transfer simp } |
|
199 |
show "q / r = q * inverse r" |
|
200 |
by (fact divide_rat_def) |
|
201 |
show "inverse 0 = (0::rat)" |
|
202 |
by transfer simp |
|
27509 | 203 |
qed |
204 |
||
205 |
end |
|
206 |
||
27551 | 207 |
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
208 |
by (induct k) (simp_all add: Zero_rat_def One_rat_def) |
27551 | 209 |
|
210 |
lemma of_int_rat: "of_int k = Fract k 1" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
211 |
by (cases k rule: int_diff_cases) (simp add: of_nat_rat) |
27551 | 212 |
|
213 |
lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k" |
|
214 |
by (rule of_nat_rat [symmetric]) |
|
215 |
||
216 |
lemma Fract_of_int_eq: "Fract k 1 = of_int k" |
|
217 |
by (rule of_int_rat [symmetric]) |
|
218 |
||
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
219 |
lemma rat_number_collapse: |
27551 | 220 |
"Fract 0 k = 0" |
221 |
"Fract 1 1 = 1" |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
222 |
"Fract (numeral w) 1 = numeral w" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
223 |
"Fract (neg_numeral w) 1 = neg_numeral w" |
27551 | 224 |
"Fract k 0 = 0" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
225 |
using Fract_of_int_eq [of "numeral w"] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
226 |
using Fract_of_int_eq [of "neg_numeral w"] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
227 |
by (simp_all add: Zero_rat_def One_rat_def eq_rat) |
27551 | 228 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
229 |
lemma rat_number_expand: |
27551 | 230 |
"0 = Fract 0 1" |
231 |
"1 = Fract 1 1" |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
232 |
"numeral k = Fract (numeral k) 1" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
233 |
"neg_numeral k = Fract (neg_numeral k) 1" |
27551 | 234 |
by (simp_all add: rat_number_collapse) |
235 |
||
236 |
lemma Rat_cases_nonzero [case_names Fract 0]: |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
237 |
assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C" |
27551 | 238 |
assumes 0: "q = 0 \<Longrightarrow> C" |
239 |
shows C |
|
240 |
proof (cases "q = 0") |
|
241 |
case True then show C using 0 by auto |
|
242 |
next |
|
243 |
case False |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
244 |
then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto |
27551 | 245 |
moreover with False have "0 \<noteq> Fract a b" by simp |
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
246 |
with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
247 |
with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast |
27551 | 248 |
qed |
249 |
||
33805 | 250 |
subsubsection {* Function @{text normalize} *} |
251 |
||
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
252 |
lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
253 |
proof (cases "b = 0") |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
254 |
case True then show ?thesis by (simp add: eq_rat) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
255 |
next |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
256 |
case False |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
257 |
moreover have "b div gcd a b * gcd a b = b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
258 |
by (rule dvd_div_mult_self) simp |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
259 |
ultimately have "b div gcd a b \<noteq> 0" by auto |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
260 |
with False show ?thesis by (simp add: eq_rat dvd_div_mult mult_commute [of a]) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
261 |
qed |
33805 | 262 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
263 |
definition normalize :: "int \<times> int \<Rightarrow> int \<times> int" where |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
264 |
"normalize p = (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a)) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
265 |
else if snd p = 0 then (0, 1) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
266 |
else (let a = - gcd (fst p) (snd p) in (fst p div a, snd p div a)))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
267 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
268 |
lemma normalize_crossproduct: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
269 |
assumes "q \<noteq> 0" "s \<noteq> 0" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
270 |
assumes "normalize (p, q) = normalize (r, s)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
271 |
shows "p * s = r * q" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
272 |
proof - |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
273 |
have aux: "p * gcd r s = sgn (q * s) * r * gcd p q \<Longrightarrow> q * gcd r s = sgn (q * s) * s * gcd p q \<Longrightarrow> p * s = q * r" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
274 |
proof - |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
275 |
assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
276 |
then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
277 |
with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
278 |
qed |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
279 |
from assms show ?thesis |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
280 |
by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux) |
33805 | 281 |
qed |
282 |
||
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
283 |
lemma normalize_eq: "normalize (a, b) = (p, q) \<Longrightarrow> Fract p q = Fract a b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
284 |
by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
285 |
split:split_if_asm) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
286 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
287 |
lemma normalize_denom_pos: "normalize r = (p, q) \<Longrightarrow> q > 0" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
288 |
by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
289 |
split:split_if_asm) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
290 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
291 |
lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
292 |
by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
293 |
split:split_if_asm) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
294 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
295 |
lemma normalize_stable [simp]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
296 |
"q > 0 \<Longrightarrow> coprime p q \<Longrightarrow> normalize (p, q) = (p, q)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
297 |
by (simp add: normalize_def) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
298 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
299 |
lemma normalize_denom_zero [simp]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
300 |
"normalize (p, 0) = (0, 1)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
301 |
by (simp add: normalize_def) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
302 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
303 |
lemma normalize_negative [simp]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
304 |
"q < 0 \<Longrightarrow> normalize (p, q) = normalize (- p, - q)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
305 |
by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
306 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
307 |
text{* |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
308 |
Decompose a fraction into normalized, i.e. coprime numerator and denominator: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
309 |
*} |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
310 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
311 |
definition quotient_of :: "rat \<Rightarrow> int \<times> int" where |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
312 |
"quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) & |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
313 |
snd pair > 0 & coprime (fst pair) (snd pair))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
314 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
315 |
lemma quotient_of_unique: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
316 |
"\<exists>!p. r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
317 |
proof (cases r) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
318 |
case (Fract a b) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
319 |
then have "r = Fract (fst (a, b)) (snd (a, b)) \<and> snd (a, b) > 0 \<and> coprime (fst (a, b)) (snd (a, b))" by auto |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
320 |
then show ?thesis proof (rule ex1I) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
321 |
fix p |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
322 |
obtain c d :: int where p: "p = (c, d)" by (cases p) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
323 |
assume "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
324 |
with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
325 |
have "c = a \<and> d = b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
326 |
proof (cases "a = 0") |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
327 |
case True with Fract Fract' show ?thesis by (simp add: eq_rat) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
328 |
next |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
329 |
case False |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
330 |
with Fract Fract' have *: "c * b = a * d" and "c \<noteq> 0" by (auto simp add: eq_rat) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
331 |
then have "c * b > 0 \<longleftrightarrow> a * d > 0" by auto |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
332 |
with `b > 0` `d > 0` have "a > 0 \<longleftrightarrow> c > 0" by (simp add: zero_less_mult_iff) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
333 |
with `a \<noteq> 0` `c \<noteq> 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
334 |
from `coprime a b` `coprime c d` have "\<bar>a\<bar> * \<bar>d\<bar> = \<bar>c\<bar> * \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> \<bar>d\<bar> = \<bar>b\<bar>" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
335 |
by (simp add: coprime_crossproduct_int) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
336 |
with `b > 0` `d > 0` have "\<bar>a\<bar> * d = \<bar>c\<bar> * b \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> d = b" by simp |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
337 |
then have "a * sgn a * d = c * sgn c * b \<longleftrightarrow> a * sgn a = c * sgn c \<and> d = b" by (simp add: abs_sgn) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
338 |
with sgn * show ?thesis by (auto simp add: sgn_0_0) |
33805 | 339 |
qed |
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
340 |
with p show "p = (a, b)" by simp |
33805 | 341 |
qed |
342 |
qed |
|
343 |
||
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
344 |
lemma quotient_of_Fract [code]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
345 |
"quotient_of (Fract a b) = normalize (a, b)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
346 |
proof - |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
347 |
have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
348 |
by (rule sym) (auto intro: normalize_eq) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
349 |
moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
350 |
by (cases "normalize (a, b)") (rule normalize_denom_pos, simp) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
351 |
moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
352 |
by (rule normalize_coprime) simp |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
353 |
ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
354 |
with quotient_of_unique have |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
355 |
"(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and> coprime (fst p) (snd p)) = normalize (a, b)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
356 |
by (rule the1_equality) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
357 |
then show ?thesis by (simp add: quotient_of_def) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
358 |
qed |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
359 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
360 |
lemma quotient_of_number [simp]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
361 |
"quotient_of 0 = (0, 1)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
362 |
"quotient_of 1 = (1, 1)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
363 |
"quotient_of (numeral k) = (numeral k, 1)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
364 |
"quotient_of (neg_numeral k) = (neg_numeral k, 1)" |
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
365 |
by (simp_all add: rat_number_expand quotient_of_Fract) |
33805 | 366 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
367 |
lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
368 |
by (simp add: quotient_of_Fract normalize_eq) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
369 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
370 |
lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
371 |
by (cases r) (simp add: quotient_of_Fract normalize_denom_pos) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
372 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
373 |
lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
374 |
by (cases r) (simp add: quotient_of_Fract normalize_coprime) |
33805 | 375 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
376 |
lemma quotient_of_inject: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
377 |
assumes "quotient_of a = quotient_of b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
378 |
shows "a = b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
379 |
proof - |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
380 |
obtain p q r s where a: "a = Fract p q" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
381 |
and b: "b = Fract r s" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
382 |
and "q > 0" and "s > 0" by (cases a, cases b) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
383 |
with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
384 |
qed |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
385 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
386 |
lemma quotient_of_inject_eq: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
387 |
"quotient_of a = quotient_of b \<longleftrightarrow> a = b" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
388 |
by (auto simp add: quotient_of_inject) |
33805 | 389 |
|
27551 | 390 |
|
391 |
subsubsection {* Various *} |
|
392 |
||
393 |
lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
394 |
by (simp add: Fract_of_int_eq [symmetric]) |
27551 | 395 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
396 |
lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
397 |
by (simp add: rat_number_expand) |
27551 | 398 |
|
50178 | 399 |
lemma quotient_of_div: |
400 |
assumes r: "quotient_of r = (n,d)" |
|
401 |
shows "r = of_int n / of_int d" |
|
402 |
proof - |
|
403 |
from theI'[OF quotient_of_unique[of r], unfolded r[unfolded quotient_of_def]] |
|
404 |
have "r = Fract n d" by simp |
|
405 |
thus ?thesis using Fract_of_int_quotient by simp |
|
406 |
qed |
|
27551 | 407 |
|
408 |
subsubsection {* The ordered field of rational numbers *} |
|
27509 | 409 |
|
47907 | 410 |
lift_definition positive :: "rat \<Rightarrow> bool" |
411 |
is "\<lambda>x. 0 < fst x * snd x" |
|
412 |
proof (clarsimp) |
|
413 |
fix a b c d :: int |
|
414 |
assume "b \<noteq> 0" and "d \<noteq> 0" and "a * d = c * b" |
|
415 |
hence "a * d * b * d = c * b * b * d" |
|
416 |
by simp |
|
417 |
hence "a * b * d\<twosuperior> = c * d * b\<twosuperior>" |
|
418 |
unfolding power2_eq_square by (simp add: mult_ac) |
|
419 |
hence "0 < a * b * d\<twosuperior> \<longleftrightarrow> 0 < c * d * b\<twosuperior>" |
|
420 |
by simp |
|
421 |
thus "0 < a * b \<longleftrightarrow> 0 < c * d" |
|
422 |
using `b \<noteq> 0` and `d \<noteq> 0` |
|
423 |
by (simp add: zero_less_mult_iff) |
|
424 |
qed |
|
425 |
||
426 |
lemma positive_zero: "\<not> positive 0" |
|
427 |
by transfer simp |
|
428 |
||
429 |
lemma positive_add: |
|
430 |
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)" |
|
431 |
apply transfer |
|
432 |
apply (simp add: zero_less_mult_iff) |
|
433 |
apply (elim disjE, simp_all add: add_pos_pos add_neg_neg |
|
434 |
mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg) |
|
435 |
done |
|
436 |
||
437 |
lemma positive_mult: |
|
438 |
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)" |
|
439 |
by transfer (drule (1) mult_pos_pos, simp add: mult_ac) |
|
440 |
||
441 |
lemma positive_minus: |
|
442 |
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)" |
|
443 |
by transfer (force simp: neq_iff zero_less_mult_iff mult_less_0_iff) |
|
444 |
||
445 |
instantiation rat :: linordered_field_inverse_zero |
|
27509 | 446 |
begin |
447 |
||
47907 | 448 |
definition |
449 |
"x < y \<longleftrightarrow> positive (y - x)" |
|
450 |
||
451 |
definition |
|
452 |
"x \<le> (y::rat) \<longleftrightarrow> x < y \<or> x = y" |
|
453 |
||
454 |
definition |
|
455 |
"abs (a::rat) = (if a < 0 then - a else a)" |
|
456 |
||
457 |
definition |
|
458 |
"sgn (a::rat) = (if a = 0 then 0 else if 0 < a then 1 else - 1)" |
|
47906 | 459 |
|
47907 | 460 |
instance proof |
461 |
fix a b c :: rat |
|
462 |
show "\<bar>a\<bar> = (if a < 0 then - a else a)" |
|
463 |
by (rule abs_rat_def) |
|
464 |
show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" |
|
465 |
unfolding less_eq_rat_def less_rat_def |
|
466 |
by (auto, drule (1) positive_add, simp_all add: positive_zero) |
|
467 |
show "a \<le> a" |
|
468 |
unfolding less_eq_rat_def by simp |
|
469 |
show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c" |
|
470 |
unfolding less_eq_rat_def less_rat_def |
|
471 |
by (auto, drule (1) positive_add, simp add: algebra_simps) |
|
472 |
show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b" |
|
473 |
unfolding less_eq_rat_def less_rat_def |
|
474 |
by (auto, drule (1) positive_add, simp add: positive_zero) |
|
475 |
show "a \<le> b \<Longrightarrow> c + a \<le> c + b" |
|
476 |
unfolding less_eq_rat_def less_rat_def by (auto simp: diff_minus) |
|
477 |
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" |
|
478 |
by (rule sgn_rat_def) |
|
479 |
show "a \<le> b \<or> b \<le> a" |
|
480 |
unfolding less_eq_rat_def less_rat_def |
|
481 |
by (auto dest!: positive_minus) |
|
482 |
show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" |
|
483 |
unfolding less_rat_def |
|
484 |
by (drule (1) positive_mult, simp add: algebra_simps) |
|
47906 | 485 |
qed |
27551 | 486 |
|
47907 | 487 |
end |
488 |
||
489 |
instantiation rat :: distrib_lattice |
|
490 |
begin |
|
491 |
||
492 |
definition |
|
493 |
"(inf :: rat \<Rightarrow> rat \<Rightarrow> rat) = min" |
|
27509 | 494 |
|
495 |
definition |
|
47907 | 496 |
"(sup :: rat \<Rightarrow> rat \<Rightarrow> rat) = max" |
497 |
||
498 |
instance proof |
|
499 |
qed (auto simp add: inf_rat_def sup_rat_def min_max.sup_inf_distrib1) |
|
500 |
||
501 |
end |
|
502 |
||
503 |
lemma positive_rat: "positive (Fract a b) \<longleftrightarrow> 0 < a * b" |
|
504 |
by transfer simp |
|
27509 | 505 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
506 |
lemma less_rat [simp]: |
27551 | 507 |
assumes "b \<noteq> 0" and "d \<noteq> 0" |
508 |
shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)" |
|
47907 | 509 |
using assms unfolding less_rat_def |
510 |
by (simp add: positive_rat algebra_simps) |
|
27509 | 511 |
|
47907 | 512 |
lemma le_rat [simp]: |
513 |
assumes "b \<noteq> 0" and "d \<noteq> 0" |
|
514 |
shows "Fract a b \<le> Fract c d \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)" |
|
515 |
using assms unfolding le_less by (simp add: eq_rat) |
|
27551 | 516 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
517 |
lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>" |
35216 | 518 |
by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff) |
27551 | 519 |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
520 |
lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)" |
27551 | 521 |
unfolding Fract_of_int_eq |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
522 |
by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) |
27551 | 523 |
(auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) |
524 |
||
525 |
lemma Rat_induct_pos [case_names Fract, induct type: rat]: |
|
526 |
assumes step: "\<And>a b. 0 < b \<Longrightarrow> P (Fract a b)" |
|
527 |
shows "P q" |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
528 |
proof (cases q) |
27551 | 529 |
have step': "\<And>a b. b < 0 \<Longrightarrow> P (Fract a b)" |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
530 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
531 |
fix a::int and b::int |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
532 |
assume b: "b < 0" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
533 |
hence "0 < -b" by simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
534 |
hence "P (Fract (-a) (-b))" by (rule step) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
535 |
thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
536 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
537 |
case (Fract a b) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
538 |
thus "P q" by (force simp add: linorder_neq_iff step step') |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
539 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
540 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
541 |
lemma zero_less_Fract_iff: |
30095
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
542 |
"0 < b \<Longrightarrow> 0 < Fract a b \<longleftrightarrow> 0 < a" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
543 |
by (simp add: Zero_rat_def zero_less_mult_iff) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
544 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
545 |
lemma Fract_less_zero_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
546 |
"0 < b \<Longrightarrow> Fract a b < 0 \<longleftrightarrow> a < 0" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
547 |
by (simp add: Zero_rat_def mult_less_0_iff) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
548 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
549 |
lemma zero_le_Fract_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
550 |
"0 < b \<Longrightarrow> 0 \<le> Fract a b \<longleftrightarrow> 0 \<le> a" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
551 |
by (simp add: Zero_rat_def zero_le_mult_iff) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
552 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
553 |
lemma Fract_le_zero_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
554 |
"0 < b \<Longrightarrow> Fract a b \<le> 0 \<longleftrightarrow> a \<le> 0" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
555 |
by (simp add: Zero_rat_def mult_le_0_iff) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
556 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
557 |
lemma one_less_Fract_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
558 |
"0 < b \<Longrightarrow> 1 < Fract a b \<longleftrightarrow> b < a" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
559 |
by (simp add: One_rat_def mult_less_cancel_right_disj) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
560 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
561 |
lemma Fract_less_one_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
562 |
"0 < b \<Longrightarrow> Fract a b < 1 \<longleftrightarrow> a < b" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
563 |
by (simp add: One_rat_def mult_less_cancel_right_disj) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
564 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
565 |
lemma one_le_Fract_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
566 |
"0 < b \<Longrightarrow> 1 \<le> Fract a b \<longleftrightarrow> b \<le> a" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
567 |
by (simp add: One_rat_def mult_le_cancel_right) |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
568 |
|
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
569 |
lemma Fract_le_one_iff: |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
570 |
"0 < b \<Longrightarrow> Fract a b \<le> 1 \<longleftrightarrow> a \<le> b" |
c6e184561159
add lemmas about comparisons of Fract a b with 0 and 1
huffman
parents:
29940
diff
changeset
|
571 |
by (simp add: One_rat_def mult_le_cancel_right) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
572 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
573 |
|
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
574 |
subsubsection {* Rationals are an Archimedean field *} |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
575 |
|
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
576 |
lemma rat_floor_lemma: |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
577 |
shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
578 |
proof - |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
579 |
have "Fract a b = of_int (a div b) + Fract (a mod b) b" |
35293
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset
|
580 |
by (cases "b = 0", simp, simp add: of_int_rat) |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
581 |
moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1" |
35293
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset
|
582 |
unfolding Fract_of_int_quotient |
36409 | 583 |
by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos) |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
584 |
ultimately show ?thesis by simp |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
585 |
qed |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
586 |
|
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
587 |
instance rat :: archimedean_field |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
588 |
proof |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
589 |
fix r :: rat |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
590 |
show "\<exists>z. r \<le> of_int z" |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
591 |
proof (induct r) |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
592 |
case (Fract a b) |
35293
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset
|
593 |
have "Fract a b \<le> of_int (a div b + 1)" |
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset
|
594 |
using rat_floor_lemma [of a b] by simp |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
595 |
then show "\<exists>z. Fract a b \<le> of_int z" .. |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
596 |
qed |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
597 |
qed |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
598 |
|
43732
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
599 |
instantiation rat :: floor_ceiling |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
600 |
begin |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
601 |
|
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
602 |
definition [code del]: |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
603 |
"floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
604 |
|
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
605 |
instance proof |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
606 |
fix x :: rat |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
607 |
show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)" |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
608 |
unfolding floor_rat_def using floor_exists1 by (rule theI') |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
609 |
qed |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
610 |
|
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
611 |
end |
6b2bdc57155b
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents:
42311
diff
changeset
|
612 |
|
35293
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset
|
613 |
lemma floor_Fract: "floor (Fract a b) = a div b" |
06a98796453e
remove unneeded premise from rat_floor_lemma and floor_Fract
huffman
parents:
35216
diff
changeset
|
614 |
using rat_floor_lemma [of a b] |
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
615 |
by (simp add: floor_unique) |
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
616 |
|
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
30095
diff
changeset
|
617 |
|
31100 | 618 |
subsection {* Linear arithmetic setup *} |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
619 |
|
31100 | 620 |
declaration {* |
621 |
K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] |
|
622 |
(* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) |
|
623 |
#> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2] |
|
624 |
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) |
|
625 |
#> Lin_Arith.add_simps [@{thm neg_less_iff_less}, |
|
626 |
@{thm True_implies_equals}, |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset
|
627 |
read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left}, |
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset
|
628 |
read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left}, |
31100 | 629 |
@{thm divide_1}, @{thm divide_zero_left}, |
630 |
@{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
|
631 |
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, |
|
632 |
@{thm of_int_minus}, @{thm of_int_diff}, |
|
633 |
@{thm of_int_of_nat_eq}] |
|
634 |
#> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors |
|
635 |
#> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) |
|
636 |
#> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})) |
|
637 |
*} |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
638 |
|
23342 | 639 |
|
640 |
subsection {* Embedding from Rationals to other Fields *} |
|
641 |
||
24198 | 642 |
class field_char_0 = field + ring_char_0 |
23342 | 643 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33814
diff
changeset
|
644 |
subclass (in linordered_field) field_char_0 .. |
23342 | 645 |
|
27551 | 646 |
context field_char_0 |
647 |
begin |
|
648 |
||
47906 | 649 |
lift_definition of_rat :: "rat \<Rightarrow> 'a" |
650 |
is "\<lambda>x. of_int (fst x) / of_int (snd x)" |
|
23342 | 651 |
apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) |
652 |
apply (simp only: of_int_mult [symmetric]) |
|
653 |
done |
|
654 |
||
47906 | 655 |
end |
656 |
||
27551 | 657 |
lemma of_rat_rat: "b \<noteq> 0 \<Longrightarrow> of_rat (Fract a b) = of_int a / of_int b" |
47906 | 658 |
by transfer simp |
23342 | 659 |
|
660 |
lemma of_rat_0 [simp]: "of_rat 0 = 0" |
|
47906 | 661 |
by transfer simp |
23342 | 662 |
|
663 |
lemma of_rat_1 [simp]: "of_rat 1 = 1" |
|
47906 | 664 |
by transfer simp |
23342 | 665 |
|
666 |
lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b" |
|
47906 | 667 |
by transfer (simp add: add_frac_eq) |
23342 | 668 |
|
23343 | 669 |
lemma of_rat_minus: "of_rat (- a) = - of_rat a" |
47906 | 670 |
by transfer simp |
23343 | 671 |
|
672 |
lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b" |
|
673 |
by (simp only: diff_minus of_rat_add of_rat_minus) |
|
674 |
||
23342 | 675 |
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" |
47906 | 676 |
apply transfer |
23342 | 677 |
apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) |
678 |
done |
|
679 |
||
680 |
lemma nonzero_of_rat_inverse: |
|
681 |
"a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)" |
|
23343 | 682 |
apply (rule inverse_unique [symmetric]) |
683 |
apply (simp add: of_rat_mult [symmetric]) |
|
23342 | 684 |
done |
685 |
||
686 |
lemma of_rat_inverse: |
|
36409 | 687 |
"(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) = |
23342 | 688 |
inverse (of_rat a)" |
689 |
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) |
|
690 |
||
691 |
lemma nonzero_of_rat_divide: |
|
692 |
"b \<noteq> 0 \<Longrightarrow> of_rat (a / b) = of_rat a / of_rat b" |
|
693 |
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) |
|
694 |
||
695 |
lemma of_rat_divide: |
|
36409 | 696 |
"(of_rat (a / b)::'a::{field_char_0, field_inverse_zero}) |
23342 | 697 |
= of_rat a / of_rat b" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
698 |
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) |
23342 | 699 |
|
23343 | 700 |
lemma of_rat_power: |
31017 | 701 |
"(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n" |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30242
diff
changeset
|
702 |
by (induct n) (simp_all add: of_rat_mult) |
23343 | 703 |
|
704 |
lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)" |
|
47906 | 705 |
apply transfer |
23343 | 706 |
apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) |
707 |
apply (simp only: of_int_mult [symmetric] of_int_eq_iff) |
|
708 |
done |
|
709 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
710 |
lemma of_rat_less: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33814
diff
changeset
|
711 |
"(of_rat r :: 'a::linordered_field) < of_rat s \<longleftrightarrow> r < s" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
712 |
proof (induct r, induct s) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
713 |
fix a b c d :: int |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
714 |
assume not_zero: "b > 0" "d > 0" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
715 |
then have "b * d > 0" by (rule mult_pos_pos) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
716 |
have of_int_divide_less_eq: |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
717 |
"(of_int a :: 'a) / of_int b < of_int c / of_int d |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
718 |
\<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
719 |
using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq) |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33814
diff
changeset
|
720 |
show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
721 |
\<longleftrightarrow> Fract a b < Fract c d" |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
722 |
using not_zero `b * d > 0` |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
723 |
by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
724 |
qed |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
725 |
|
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
726 |
lemma of_rat_less_eq: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33814
diff
changeset
|
727 |
"(of_rat r :: 'a::linordered_field) \<le> of_rat s \<longleftrightarrow> r \<le> s" |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
728 |
unfolding le_less by (auto simp add: of_rat_less) |
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
729 |
|
23343 | 730 |
lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] |
731 |
||
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
732 |
lemma of_rat_eq_id [simp]: "of_rat = id" |
23343 | 733 |
proof |
734 |
fix a |
|
735 |
show "of_rat a = id a" |
|
736 |
by (induct a) |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
737 |
(simp add: of_rat_rat Fract_of_int_eq [symmetric]) |
23343 | 738 |
qed |
739 |
||
740 |
text{*Collapse nested embeddings*} |
|
741 |
lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n" |
|
742 |
by (induct n) (simp_all add: of_rat_add) |
|
743 |
||
744 |
lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z" |
|
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
745 |
by (cases z rule: int_diff_cases) (simp add: of_rat_diff) |
23343 | 746 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
747 |
lemma of_rat_numeral_eq [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
748 |
"of_rat (numeral w) = numeral w" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
749 |
using of_rat_of_int_eq [of "numeral w"] by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
750 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
751 |
lemma of_rat_neg_numeral_eq [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
752 |
"of_rat (neg_numeral w) = neg_numeral w" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
753 |
using of_rat_of_int_eq [of "neg_numeral w"] by simp |
23343 | 754 |
|
23879 | 755 |
lemmas zero_rat = Zero_rat_def |
756 |
lemmas one_rat = One_rat_def |
|
757 |
||
24198 | 758 |
abbreviation |
759 |
rat_of_nat :: "nat \<Rightarrow> rat" |
|
760 |
where |
|
761 |
"rat_of_nat \<equiv> of_nat" |
|
762 |
||
763 |
abbreviation |
|
764 |
rat_of_int :: "int \<Rightarrow> rat" |
|
765 |
where |
|
766 |
"rat_of_int \<equiv> of_int" |
|
767 |
||
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
768 |
subsection {* The Set of Rational Numbers *} |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
769 |
|
28001 | 770 |
context field_char_0 |
771 |
begin |
|
772 |
||
773 |
definition |
|
774 |
Rats :: "'a set" where |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
775 |
"Rats = range of_rat" |
28001 | 776 |
|
777 |
notation (xsymbols) |
|
778 |
Rats ("\<rat>") |
|
779 |
||
780 |
end |
|
781 |
||
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
782 |
lemma Rats_of_rat [simp]: "of_rat r \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
783 |
by (simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
784 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
785 |
lemma Rats_of_int [simp]: "of_int z \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
786 |
by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
787 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
788 |
lemma Rats_of_nat [simp]: "of_nat n \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
789 |
by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
790 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
791 |
lemma Rats_number_of [simp]: "numeral w \<in> Rats" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
792 |
by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
793 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
794 |
lemma Rats_neg_number_of [simp]: "neg_numeral w \<in> Rats" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
795 |
by (subst of_rat_neg_numeral_eq [symmetric], rule Rats_of_rat) |
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
796 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
797 |
lemma Rats_0 [simp]: "0 \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
798 |
apply (unfold Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
799 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
800 |
apply (rule of_rat_0 [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
801 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
802 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
803 |
lemma Rats_1 [simp]: "1 \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
804 |
apply (unfold Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
805 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
806 |
apply (rule of_rat_1 [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
807 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
808 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
809 |
lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
810 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
811 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
812 |
apply (rule of_rat_add [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
813 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
814 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
815 |
lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
816 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
817 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
818 |
apply (rule of_rat_minus [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
819 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
820 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
821 |
lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
822 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
823 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
824 |
apply (rule of_rat_diff [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
825 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
826 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
827 |
lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
828 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
829 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
830 |
apply (rule of_rat_mult [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
831 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
832 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
833 |
lemma nonzero_Rats_inverse: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
834 |
fixes a :: "'a::field_char_0" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
835 |
shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
836 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
837 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
838 |
apply (erule nonzero_of_rat_inverse [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
839 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
840 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
841 |
lemma Rats_inverse [simp]: |
36409 | 842 |
fixes a :: "'a::{field_char_0, field_inverse_zero}" |
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
843 |
shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
844 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
845 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
846 |
apply (rule of_rat_inverse [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
847 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
848 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
849 |
lemma nonzero_Rats_divide: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
850 |
fixes a b :: "'a::field_char_0" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
851 |
shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
852 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
853 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
854 |
apply (erule nonzero_of_rat_divide [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
855 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
856 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
857 |
lemma Rats_divide [simp]: |
36409 | 858 |
fixes a b :: "'a::{field_char_0, field_inverse_zero}" |
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
859 |
shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
860 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
861 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
862 |
apply (rule of_rat_divide [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
863 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
864 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
865 |
lemma Rats_power [simp]: |
31017 | 866 |
fixes a :: "'a::field_char_0" |
28010
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
867 |
shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
868 |
apply (auto simp add: Rats_def) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
869 |
apply (rule range_eqI) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
870 |
apply (rule of_rat_power [symmetric]) |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
871 |
done |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
872 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
873 |
lemma Rats_cases [cases set: Rats]: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
874 |
assumes "q \<in> \<rat>" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
875 |
obtains (of_rat) r where "q = of_rat r" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
876 |
proof - |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
877 |
from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def . |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
878 |
then obtain r where "q = of_rat r" .. |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
879 |
then show thesis .. |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
880 |
qed |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
881 |
|
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
882 |
lemma Rats_induct [case_names of_rat, induct set: Rats]: |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
883 |
"q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q" |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
884 |
by (rule Rats_cases) auto |
8312edc51969
add lemmas about Rats similar to those about Reals
huffman
parents:
28001
diff
changeset
|
885 |
|
28001 | 886 |
|
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
887 |
subsection {* Implementation of rational numbers as pairs of integers *} |
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
888 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
889 |
text {* Formal constructor *} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
890 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
891 |
definition Frct :: "int \<times> int \<Rightarrow> rat" where |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
892 |
[simp]: "Frct p = Fract (fst p) (snd p)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
893 |
|
36112
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35726
diff
changeset
|
894 |
lemma [code abstype]: |
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35726
diff
changeset
|
895 |
"Frct (quotient_of q) = q" |
7fa17a225852
user interface for abstract datatypes is an attribute, not a command
haftmann
parents:
35726
diff
changeset
|
896 |
by (cases q) (auto intro: quotient_of_eq) |
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
897 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
898 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
899 |
text {* Numerals *} |
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
900 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
901 |
declare quotient_of_Fract [code abstract] |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
902 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
903 |
definition of_int :: "int \<Rightarrow> rat" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
904 |
where |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
905 |
[code_abbrev]: "of_int = Int.of_int" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
906 |
hide_const (open) of_int |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
907 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
908 |
lemma quotient_of_int [code abstract]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
909 |
"quotient_of (Rat.of_int a) = (a, 1)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
910 |
by (simp add: of_int_def of_int_rat quotient_of_Fract) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
911 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
912 |
lemma [code_unfold]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
913 |
"numeral k = Rat.of_int (numeral k)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
914 |
by (simp add: Rat.of_int_def) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
915 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
916 |
lemma [code_unfold]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
917 |
"neg_numeral k = Rat.of_int (neg_numeral k)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
918 |
by (simp add: Rat.of_int_def) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
919 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
920 |
lemma Frct_code_post [code_post]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
921 |
"Frct (0, a) = 0" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
922 |
"Frct (a, 0) = 0" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
923 |
"Frct (1, 1) = 1" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
924 |
"Frct (numeral k, 1) = numeral k" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
925 |
"Frct (neg_numeral k, 1) = neg_numeral k" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
926 |
"Frct (1, numeral k) = 1 / numeral k" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
927 |
"Frct (1, neg_numeral k) = 1 / neg_numeral k" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
928 |
"Frct (numeral k, numeral l) = numeral k / numeral l" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
929 |
"Frct (numeral k, neg_numeral l) = numeral k / neg_numeral l" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
930 |
"Frct (neg_numeral k, numeral l) = neg_numeral k / numeral l" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
931 |
"Frct (neg_numeral k, neg_numeral l) = neg_numeral k / neg_numeral l" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
932 |
by (simp_all add: Fract_of_int_quotient) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
933 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
934 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
935 |
text {* Operations *} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
936 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
937 |
lemma rat_zero_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
938 |
"quotient_of 0 = (0, 1)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
939 |
by (simp add: Zero_rat_def quotient_of_Fract normalize_def) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
940 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
941 |
lemma rat_one_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
942 |
"quotient_of 1 = (1, 1)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
943 |
by (simp add: One_rat_def quotient_of_Fract normalize_def) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
944 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
945 |
lemma rat_plus_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
946 |
"quotient_of (p + q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
947 |
in normalize (a * d + b * c, c * d))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
948 |
by (cases p, cases q) (simp add: quotient_of_Fract) |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
949 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
950 |
lemma rat_uminus_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
951 |
"quotient_of (- p) = (let (a, b) = quotient_of p in (- a, b))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
952 |
by (cases p) (simp add: quotient_of_Fract) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
953 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
954 |
lemma rat_minus_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
955 |
"quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
956 |
in normalize (a * d - b * c, c * d))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
957 |
by (cases p, cases q) (simp add: quotient_of_Fract) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
958 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
959 |
lemma rat_times_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
960 |
"quotient_of (p * q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
961 |
in normalize (a * b, c * d))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
962 |
by (cases p, cases q) (simp add: quotient_of_Fract) |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
963 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
964 |
lemma rat_inverse_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
965 |
"quotient_of (inverse p) = (let (a, b) = quotient_of p |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
966 |
in if a = 0 then (0, 1) else (sgn a * b, \<bar>a\<bar>))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
967 |
proof (cases p) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
968 |
case (Fract a b) then show ?thesis |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
969 |
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd_int.commute) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
970 |
qed |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
971 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
972 |
lemma rat_divide_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
973 |
"quotient_of (p / q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
974 |
in normalize (a * d, c * b))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
975 |
by (cases p, cases q) (simp add: quotient_of_Fract) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
976 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
977 |
lemma rat_abs_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
978 |
"quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
979 |
by (cases p) (simp add: quotient_of_Fract) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
980 |
|
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
981 |
lemma rat_sgn_code [code abstract]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
982 |
"quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
983 |
proof (cases p) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
984 |
case (Fract a b) then show ?thesis |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
985 |
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract) |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
986 |
qed |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
987 |
|
43733
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset
|
988 |
lemma rat_floor_code [code]: |
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset
|
989 |
"floor p = (let (a, b) = quotient_of p in a div b)" |
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset
|
990 |
by (cases p) (simp add: quotient_of_Fract floor_Fract) |
a6ca7b83612f
adding code equations to execute floor and ceiling on rational and real numbers
bulwahn
parents:
43732
diff
changeset
|
991 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset
|
992 |
instantiation rat :: equal |
26513 | 993 |
begin |
994 |
||
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
995 |
definition [code]: |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset
|
996 |
"HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b" |
26513 | 997 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
998 |
instance proof |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset
|
999 |
qed (simp add: equal_rat_def quotient_of_inject_eq) |
26513 | 1000 |
|
28351 | 1001 |
lemma rat_eq_refl [code nbe]: |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset
|
1002 |
"HOL.equal (r::rat) r \<longleftrightarrow> True" |
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38287
diff
changeset
|
1003 |
by (rule equal_refl) |
28351 | 1004 |
|
26513 | 1005 |
end |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1006 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
1007 |
lemma rat_less_eq_code [code]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
1008 |
"p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)" |
35726 | 1009 |
by (cases p, cases q) (simp add: quotient_of_Fract mult.commute) |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1010 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
1011 |
lemma rat_less_code [code]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
1012 |
"p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)" |
35726 | 1013 |
by (cases p, cases q) (simp add: quotient_of_Fract mult.commute) |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1014 |
|
35369
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
1015 |
lemma [code]: |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
1016 |
"of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)" |
e4a7947e02b8
more general case and induct rules; normalize and quotient_of; abstract code generation
haftmann
parents:
35293
diff
changeset
|
1017 |
by (cases p) (simp add: quotient_of_Fract of_rat_rat) |
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27551
diff
changeset
|
1018 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
1019 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
1020 |
text {* Quickcheck *} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
1021 |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1022 |
definition (in term_syntax) |
32657 | 1023 |
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
1024 |
[code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l" |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1025 |
|
37751 | 1026 |
notation fcomp (infixl "\<circ>>" 60) |
1027 |
notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1028 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1029 |
instantiation rat :: random |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1030 |
begin |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1031 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1032 |
definition |
37751 | 1033 |
"Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair ( |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
1034 |
let j = Code_Numeral.int_of (denom + 1) |
32657 | 1035 |
in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))" |
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1036 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1037 |
instance .. |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1038 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1039 |
end |
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1040 |
|
37751 | 1041 |
no_notation fcomp (infixl "\<circ>>" 60) |
1042 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31100
diff
changeset
|
1043 |
|
41920
d4fb7a418152
moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents:
41792
diff
changeset
|
1044 |
instantiation rat :: exhaustive |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset
|
1045 |
begin |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset
|
1046 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset
|
1047 |
definition |
45818
53a697f5454a
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents:
45694
diff
changeset
|
1048 |
"exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive (%l. Quickcheck_Exhaustive.exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d" |
42311
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1049 |
|
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1050 |
instance .. |
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1051 |
|
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1052 |
end |
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1053 |
|
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1054 |
instantiation rat :: full_exhaustive |
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1055 |
begin |
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1056 |
|
eb32a8474a57
rational and real instances for new compilation scheme for exhaustive quickcheck
bulwahn
parents:
41920
diff
changeset
|
1057 |
definition |
45818
53a697f5454a
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents:
45694
diff
changeset
|
1058 |
"full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k. |
45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset
|
1059 |
f (let j = Code_Numeral.int_of l + 1 |
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset
|
1060 |
in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d" |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset
|
1061 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset
|
1062 |
instance .. |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset
|
1063 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset
|
1064 |
end |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40819
diff
changeset
|
1065 |
|
43889
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1066 |
instantiation rat :: partial_term_of |
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1067 |
begin |
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1068 |
|
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1069 |
instance .. |
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1070 |
|
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1071 |
end |
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1072 |
|
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1073 |
lemma [code]: |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
45818
diff
changeset
|
1074 |
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])" |
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
45818
diff
changeset
|
1075 |
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) == |
45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset
|
1076 |
Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'') |
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset
|
1077 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []], |
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset
|
1078 |
Typerep.Typerep (STR ''Rat.rat'') []])) (Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Product_Type.Pair'') (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))" |
43889
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1079 |
by (rule partial_term_of_anything)+ |
90d24cafb05d
adding code equations for partial_term_of for rational numbers
bulwahn
parents:
43887
diff
changeset
|
1080 |
|
43887 | 1081 |
instantiation rat :: narrowing |
1082 |
begin |
|
1083 |
||
1084 |
definition |
|
45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset
|
1085 |
"narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply |
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45478
diff
changeset
|
1086 |
(Quickcheck_Narrowing.cons (%nom denom. Fract nom denom)) narrowing) narrowing" |
43887 | 1087 |
|
1088 |
instance .. |
|
1089 |
||
1090 |
end |
|
1091 |
||
1092 |
||
45183
2e1ad4a54189
removing old code generator setup for rational numbers; tuned
bulwahn
parents:
43889
diff
changeset
|
1093 |
subsection {* Setup for Nitpick *} |
24533
fe1f93f6a15a
Added code generator setup (taken from Library/Executable_Rat.thy,
berghofe
parents:
24506
diff
changeset
|
1094 |
|
38287 | 1095 |
declaration {* |
1096 |
Nitpick_HOL.register_frac_type @{type_name rat} |
|
33209 | 1097 |
[(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), |
1098 |
(@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), |
|
1099 |
(@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}), |
|
1100 |
(@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}), |
|
1101 |
(@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), |
|
1102 |
(@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}), |
|
37397
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37143
diff
changeset
|
1103 |
(@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}), |
33209 | 1104 |
(@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), |
45478 | 1105 |
(@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})] |
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset
|
1106 |
*} |
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset
|
1107 |
|
41792
ff3cb0c418b7
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
blanchet
parents:
41231
diff
changeset
|
1108 |
lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46758
diff
changeset
|
1109 |
one_rat_inst.one_rat ord_rat_inst.less_rat |
37397
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37143
diff
changeset
|
1110 |
ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat |
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37143
diff
changeset
|
1111 |
uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat |
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
32657
diff
changeset
|
1112 |
|
35343 | 1113 |
subsection{* Float syntax *} |
1114 |
||
1115 |
syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_") |
|
1116 |
||
48891 | 1117 |
ML_file "Tools/float_syntax.ML" |
35343 | 1118 |
setup Float_Syntax.setup |
1119 |
||
1120 |
text{* Test: *} |
|
1121 |
lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)" |
|
1122 |
by simp |
|
1123 |
||
37143 | 1124 |
|
47907 | 1125 |
hide_const (open) normalize positive |
37143 | 1126 |
|
47906 | 1127 |
lemmas [transfer_rule del] = |
1128 |
rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer |
|
1129 |
Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer |
|
1130 |
uminus_rat.transfer times_rat.transfer inverse_rat.transfer |
|
47907 | 1131 |
positive.transfer of_rat.transfer |
47906 | 1132 |
|
1133 |
text {* De-register @{text "rat"} as a quotient type: *} |
|
1134 |
||
47952 | 1135 |
declare Quotient_rat[quot_del] |
47906 | 1136 |
|
29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29667
diff
changeset
|
1137 |
end |