1.1 --- a/src/HOL/IsaMakefile Tue Jun 23 05:58:00 2009 +0200
1.2 +++ b/src/HOL/IsaMakefile Tue Jun 23 10:22:11 2009 +0200
1.3 @@ -325,7 +325,7 @@
1.4 Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
1.5 Library/Bit.thy Library/Topology_Euclidean_Space.thy \
1.6 Library/Finite_Cartesian_Product.thy \
1.7 - Library/FrechetDeriv.thy \
1.8 + Library/FrechetDeriv.thy Library/Fraction_Field.thy\
1.9 Library/Fundamental_Theorem_Algebra.thy \
1.10 Library/Inner_Product.thy Library/Lattice_Syntax.thy \
1.11 Library/Legacy_GCD.thy \
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Library/Fraction_Field.thy Tue Jun 23 10:22:11 2009 +0200
2.3 @@ -0,0 +1,274 @@
2.4 +(* Title: Fraction_Field.thy
2.5 + Author: Amine Chaieb, University of Cambridge
2.6 +*)
2.7 +
2.8 +header{* A formalization of the fraction field of any integral domain
2.9 + A generalization of Rational.thy from int to any integral domain *}
2.10 +
2.11 +theory Fraction_Field
2.12 +imports Main (* Equiv_Relations Plain *)
2.13 +begin
2.14 +
2.15 +subsection {* General fractions construction *}
2.16 +
2.17 +subsubsection {* Construction of the type of fractions *}
2.18 +
2.19 +definition fractrel :: "(('a::idom * 'a ) * ('a * 'a)) set" where
2.20 + "fractrel == {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
2.21 +
2.22 +lemma fractrel_iff [simp]:
2.23 + "(x, y) \<in> fractrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
2.24 + by (simp add: fractrel_def)
2.25 +
2.26 +lemma refl_fractrel: "refl_on {x. snd x \<noteq> 0} fractrel"
2.27 + by (auto simp add: refl_on_def fractrel_def)
2.28 +
2.29 +lemma sym_fractrel: "sym fractrel"
2.30 + by (simp add: fractrel_def sym_def)
2.31 +
2.32 +lemma trans_fractrel: "trans fractrel"
2.33 +proof (rule transI, unfold split_paired_all)
2.34 + fix a b a' b' a'' b'' :: 'a
2.35 + assume A: "((a, b), (a', b')) \<in> fractrel"
2.36 + assume B: "((a', b'), (a'', b'')) \<in> fractrel"
2.37 + have "b' * (a * b'') = b'' * (a * b')" by (simp add: mult_ac)
2.38 + also from A have "a * b' = a' * b" by auto
2.39 + also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: mult_ac)
2.40 + also from B have "a' * b'' = a'' * b'" by auto
2.41 + also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: mult_ac)
2.42 + finally have "b' * (a * b'') = b' * (a'' * b)" .
2.43 + moreover from B have "b' \<noteq> 0" by auto
2.44 + ultimately have "a * b'' = a'' * b" by simp
2.45 + with A B show "((a, b), (a'', b'')) \<in> fractrel" by auto
2.46 +qed
2.47 +
2.48 +lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel"
2.49 + by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel])
2.50 +
2.51 +lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel]
2.52 +lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel]
2.53 +
2.54 +lemma equiv_fractrel_iff [iff]:
2.55 + assumes "snd x \<noteq> 0" and "snd y \<noteq> 0"
2.56 + shows "fractrel `` {x} = fractrel `` {y} \<longleftrightarrow> (x, y) \<in> fractrel"
2.57 + by (rule eq_equiv_class_iff, rule equiv_fractrel) (auto simp add: assms)
2.58 +
2.59 +typedef 'a fract = "{(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
2.60 +proof
2.61 + have "(0::'a, 1::'a) \<in> {x. snd x \<noteq> 0}" by simp
2.62 + then show "fractrel `` {(0::'a, 1)} \<in> {x. snd x \<noteq> 0} // fractrel" by (rule quotientI)
2.63 +qed
2.64 +
2.65 +lemma fractrel_in_fract [simp]: "snd x \<noteq> 0 \<Longrightarrow> fractrel `` {x} \<in> fract"
2.66 + by (simp add: fract_def quotientI)
2.67 +
2.68 +declare Abs_fract_inject [simp] Abs_fract_inverse [simp]
2.69 +
2.70 +
2.71 +subsubsection {* Representation and basic operations *}
2.72 +
2.73 +definition
2.74 + Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
2.75 + [code del]: "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
2.76 +
2.77 +code_datatype Fract
2.78 +
2.79 +lemma Fract_cases [case_names Fract, cases type: fract]:
2.80 + assumes "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> C"
2.81 + shows C
2.82 + using assms by (cases q) (clarsimp simp add: Fract_def fract_def quotient_def)
2.83 +
2.84 +lemma Fract_induct [case_names Fract, induct type: fract]:
2.85 + assumes "\<And>a b. b \<noteq> 0 \<Longrightarrow> P (Fract a b)"
2.86 + shows "P q"
2.87 + using assms by (cases q) simp
2.88 +
2.89 +lemma eq_fract:
2.90 + 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"
2.91 + and "\<And>a. Fract a 0 = Fract 0 1"
2.92 + and "\<And>a c. Fract 0 a = Fract 0 c"
2.93 + by (simp_all add: Fract_def)
2.94 +
2.95 +instantiation fract :: (idom) "{comm_ring_1, power}"
2.96 +begin
2.97 +
2.98 +definition
2.99 + Zero_fract_def [code, code unfold]: "0 = Fract 0 1"
2.100 +
2.101 +definition
2.102 + One_fract_def [code, code unfold]: "1 = Fract 1 1"
2.103 +
2.104 +definition
2.105 + add_fract_def [code del]:
2.106 + "q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
2.107 + fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
2.108 +
2.109 +lemma add_fract [simp]:
2.110 + assumes "b \<noteq> (0::'a::idom)" and "d \<noteq> 0"
2.111 + shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)"
2.112 +proof -
2.113 + have "(\<lambda>x y. fractrel``{(fst x * snd y + fst y * snd x, snd x * snd y :: 'a)})
2.114 + respects2 fractrel"
2.115 + apply (rule equiv_fractrel [THEN congruent2_commuteI]) apply (auto simp add: algebra_simps)
2.116 + unfolding mult_assoc[symmetric] .
2.117 + with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2)
2.118 +qed
2.119 +
2.120 +definition
2.121 + minus_fract_def [code del]:
2.122 + "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})"
2.123 +
2.124 +lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
2.125 +proof -
2.126 + have "(\<lambda>x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel"
2.127 + by (simp add: congruent_def)
2.128 + then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel)
2.129 +qed
2.130 +
2.131 +lemma minus_fract_cancel [simp]: "Fract (- a) (- b) = Fract a b"
2.132 + by (cases "b = 0") (simp_all add: eq_fract)
2.133 +
2.134 +definition
2.135 + diff_fract_def [code del]: "q - r = q + - (r::'a fract)"
2.136 +
2.137 +lemma diff_fract [simp]:
2.138 + assumes "b \<noteq> 0" and "d \<noteq> 0"
2.139 + shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
2.140 + using assms by (simp add: diff_fract_def diff_minus)
2.141 +
2.142 +definition
2.143 + mult_fract_def [code del]:
2.144 + "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
2.145 + fractrel``{(fst x * fst y, snd x * snd y)})"
2.146 +
2.147 +lemma mult_fract [simp]: "Fract (a::'a::idom) b * Fract c d = Fract (a * c) (b * d)"
2.148 +proof -
2.149 + have "(\<lambda>x y. fractrel `` {(fst x * fst y, snd x * snd y :: 'a)}) respects2 fractrel"
2.150 + apply (rule equiv_fractrel [THEN congruent2_commuteI]) apply (auto simp add: algebra_simps)
2.151 + unfolding mult_assoc[symmetric] .
2.152 + then show ?thesis by (simp add: Fract_def mult_fract_def UN_fractrel2)
2.153 +qed
2.154 +
2.155 +lemma mult_fract_cancel:
2.156 + assumes "c \<noteq> 0"
2.157 + shows "Fract (c * a) (c * b) = Fract a b"
2.158 +proof -
2.159 + from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def)
2.160 + then show ?thesis by (simp add: mult_fract [symmetric])
2.161 +qed
2.162 +
2.163 +instance proof
2.164 + fix q r s :: "'a fract" show "(q * r) * s = q * (r * s)"
2.165 + by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps)
2.166 +next
2.167 + fix q r :: "'a fract" show "q * r = r * q"
2.168 + by (cases q, cases r) (simp add: eq_fract algebra_simps)
2.169 +next
2.170 + fix q :: "'a fract" show "1 * q = q"
2.171 + by (cases q) (simp add: One_fract_def eq_fract)
2.172 +next
2.173 + fix q r s :: "'a fract" show "(q + r) + s = q + (r + s)"
2.174 + by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps)
2.175 +next
2.176 + fix q r :: "'a fract" show "q + r = r + q"
2.177 + by (cases q, cases r) (simp add: eq_fract algebra_simps)
2.178 +next
2.179 + fix q :: "'a fract" show "0 + q = q"
2.180 + by (cases q) (simp add: Zero_fract_def eq_fract)
2.181 +next
2.182 + fix q :: "'a fract" show "- q + q = 0"
2.183 + by (cases q) (simp add: Zero_fract_def eq_fract)
2.184 +next
2.185 + fix q r :: "'a fract" show "q - r = q + - r"
2.186 + by (cases q, cases r) (simp add: eq_fract)
2.187 +next
2.188 + fix q r s :: "'a fract" show "(q + r) * s = q * s + r * s"
2.189 + by (cases q, cases r, cases s) (simp add: eq_fract algebra_simps)
2.190 +next
2.191 + show "(0::'a fract) \<noteq> 1" by (simp add: Zero_fract_def One_fract_def eq_fract)
2.192 +qed
2.193 +
2.194 +end
2.195 +
2.196 +lemma of_nat_fract: "of_nat k = Fract (of_nat k) 1"
2.197 + by (induct k) (simp_all add: Zero_fract_def One_fract_def)
2.198 +
2.199 +lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
2.200 + by (rule of_nat_fract [symmetric])
2.201 +
2.202 +lemma fract_collapse [code post]:
2.203 + "Fract 0 k = 0"
2.204 + "Fract 1 1 = 1"
2.205 + "Fract k 0 = 0"
2.206 + by (cases "k = 0")
2.207 + (simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def)
2.208 +
2.209 +lemma fract_expand [code unfold]:
2.210 + "0 = Fract 0 1"
2.211 + "1 = Fract 1 1"
2.212 + by (simp_all add: fract_collapse)
2.213 +
2.214 +lemma Fract_cases_nonzero [case_names Fract 0]:
2.215 + assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> C"
2.216 + assumes 0: "q = 0 \<Longrightarrow> C"
2.217 + shows C
2.218 +proof (cases "q = 0")
2.219 + case True then show C using 0 by auto
2.220 +next
2.221 + case False
2.222 + then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto
2.223 + moreover with False have "0 \<noteq> Fract a b" by simp
2.224 + with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_fract_def eq_fract)
2.225 + with Fract `q = Fract a b` `b \<noteq> 0` show C by auto
2.226 +qed
2.227 +
2.228 +
2.229 +
2.230 +subsubsection {* The field of rational numbers *}
2.231 +
2.232 +context idom
2.233 +begin
2.234 +subclass ring_no_zero_divisors ..
2.235 +thm mult_eq_0_iff
2.236 +end
2.237 +
2.238 +instantiation fract :: (idom) "{field, division_by_zero}"
2.239 +begin
2.240 +
2.241 +definition
2.242 + inverse_fract_def [code del]:
2.243 + "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.
2.244 + fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
2.245 +
2.246 +
2.247 +lemma inverse_fract [simp]: "inverse (Fract a b) = Fract (b::'a::idom) a"
2.248 +proof -
2.249 + have stupid: "\<And>x. (0::'a) = x \<longleftrightarrow> x = 0" by auto
2.250 + have "(\<lambda>x. fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x :: 'a)}) respects fractrel"
2.251 + by (auto simp add: congruent_def stupid algebra_simps)
2.252 + then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel)
2.253 +qed
2.254 +
2.255 +definition
2.256 + divide_fract_def [code del]: "q / r = q * inverse (r:: 'a fract)"
2.257 +
2.258 +lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
2.259 + by (simp add: divide_fract_def)
2.260 +
2.261 +instance proof
2.262 + show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
2.263 + (simp add: fract_collapse)
2.264 +next
2.265 + fix q :: "'a fract"
2.266 + assume "q \<noteq> 0"
2.267 + then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero)
2.268 + by (simp_all add: mult_fract inverse_fract fract_expand eq_fract mult_commute)
2.269 +next
2.270 + fix q r :: "'a fract"
2.271 + show "q / r = q * inverse r" by (simp add: divide_fract_def)
2.272 +qed
2.273 +
2.274 +end
2.275 +
2.276 +
2.277 +end
2.278 \ No newline at end of file
3.1 --- a/src/HOL/Library/Library.thy Tue Jun 23 05:58:00 2009 +0200
3.2 +++ b/src/HOL/Library/Library.thy Tue Jun 23 10:22:11 2009 +0200
3.3 @@ -25,6 +25,7 @@
3.4 Fin_Fun
3.5 Float
3.6 Formal_Power_Series
3.7 + Fraction_Field
3.8 FrechetDeriv
3.9 FuncSet
3.10 Fundamental_Theorem_Algebra