# HG changeset patch # User wenzelm # Date 1434228262 -7200 # Node ID abee0de69a894b18597770826492195f71f42ecc # Parent 310853646597beaad3d552edc6d65377c9c3daf1# Parent 2761a2249c83b7ba54e66356dafddf311715410f merged diff -r 2761a2249c83 -r abee0de69a89 CONTRIBUTORS --- a/CONTRIBUTORS Sat Jun 13 22:42:23 2015 +0200 +++ b/CONTRIBUTORS Sat Jun 13 22:44:22 2015 +0200 @@ -6,6 +6,10 @@ Contributions to this Isabelle version -------------------------------------- +* Summer 2015: Florian Haftmann, TUM + Generic partial division in rings as inverse operation + of multiplication. + Contributions to Isabelle2015 ----------------------------- diff -r 2761a2249c83 -r abee0de69a89 NEWS --- a/NEWS Sat Jun 13 22:42:23 2015 +0200 +++ b/NEWS Sat Jun 13 22:44:22 2015 +0200 @@ -86,13 +86,13 @@ * Nitpick: - Removed "check_potential" and "check_genuine" options. -* Constants Fields.divide (... / ...) and Divides.div (... div ...) +* Former constants Fields.divide (_ / _) and Divides.div (_ div _) are logically unified to Rings.divide in syntactic type class -Rings.divide, with particular infix syntax added as abbreviations -in classes Fields.inverse and Divides.div respectively. INCOMPATIBILITY, -instantiatios must refer to Rings.divide rather than the former -separate constants, and infix syntax is usually not available during -instantiation. +Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) +for field division is added later as abbreviation in class Fields.inverse. +INCOMPATIBILITY, instantiatios must refer to Rings.divide rather +than the former separate constants, hence infix syntax (_ / _) is usually +not available during instantiation. * Library/Multiset: - Renamed multiset inclusion operators: diff -r 2761a2249c83 -r abee0de69a89 src/Doc/Tutorial/Misc/appendix.thy --- a/src/Doc/Tutorial/Misc/appendix.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/Doc/Tutorial/Misc/appendix.thy Sat Jun 13 22:44:22 2015 +0200 @@ -14,8 +14,8 @@ @{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\ @{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\ @{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\ -@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\ -@{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\ +@{term [source] inverse_divide} & @{typeof [show_sorts] "inverse_divide"} & (infixl $/$ 70) \\ +@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $div$ 70) \\ @{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\ @{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\ @{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\ diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Complex.thy Sat Jun 13 22:44:22 2015 +0200 @@ -70,7 +70,7 @@ "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" -definition "divide x (y\complex) = x * inverse y" +definition "x div (y\complex) = x * inverse y" instance by intro_classes diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Divides.thy Sat Jun 13 22:44:22 2015 +0200 @@ -9,19 +9,10 @@ imports Parity begin -subsection {* Syntactic division operations *} +subsection {* Abstract division in commutative semirings. *} class div = dvd + divide + fixes mod :: "'a \ 'a \ 'a" (infixl "mod" 70) -begin - -abbreviation div :: "'a \ 'a \ 'a" (infixl "div" 70) -where - "op div \ divide" - -end - -subsection {* Abstract division in commutative semirings. *} class semiring_div = semidom + div + assumes mod_div_equality: "a div b * b + a mod b = a" @@ -47,7 +38,7 @@ "n \ 0 \ a ^ n = 0 \ a = 0" using power_not_zero [of a n] by (auto simp add: zero_power) -text {* @{const div} and @{const mod} *} +text {* @{const divide} and @{const mod} *} lemma mod_div_equality2: "b * (a div b) + a mod b = a" unfolding mult.commute [of b] @@ -874,7 +865,7 @@ subsection {* Division on @{typ nat} *} text {* - We define @{const div} and @{const mod} on @{typ nat} by means + We define @{const divide} and @{const mod} on @{typ nat} by means of a characteristic relation with two input arguments @{term "m\nat"}, @{term "n\nat"} and two output arguments @{term "q\nat"}(uotient) and @{term "r\nat"}(emainder). @@ -964,21 +955,14 @@ shows "divmod_nat m n = qr" using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat) -instantiation nat :: "Divides.div" +instantiation nat :: semiring_div begin definition divide_nat where - div_nat_def: "divide m n = fst (divmod_nat m n)" + div_nat_def: "m div n = fst (divmod_nat m n)" definition mod_nat where "m mod n = snd (divmod_nat m n)" - -instance .. - -end - -instantiation nat :: semiring_div -begin lemma fst_divmod_nat [simp]: "fst (divmod_nat m n) = m div n" @@ -1024,7 +1008,7 @@ unfolding divmod_nat_rel_def using assms by auto qed -text {* The ''recursion'' equations for @{const div} and @{const mod} *} +text {* The ''recursion'' equations for @{const divide} and @{const mod} *} lemma div_less [simp]: fixes m n :: nat @@ -1082,7 +1066,7 @@ let (q, r) = divmod_nat (m - n) n in (Suc q, r))" by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq) -text {* Simproc for cancelling @{const div} and @{const mod} *} +text {* Simproc for cancelling @{const divide} and @{const mod} *} ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" @@ -1699,19 +1683,15 @@ if 0 < b then negDivAlg a b else apsnd uminus (posDivAlg (-a) (-b)))" -instantiation int :: Divides.div +instantiation int :: ring_div begin definition divide_int where - div_int_def: "divide a b = fst (divmod_int a b)" + div_int_def: "a div b = fst (divmod_int a b)" definition mod_int where "a mod b = snd (divmod_int a b)" -instance .. - -end - lemma fst_divmod_int [simp]: "fst (divmod_int a b) = a div b" by (simp add: div_int_def) @@ -1897,7 +1877,7 @@ lemma mod_int_unique: "divmod_int_rel a b (q, r) \ a mod b = r" by (simp add: divmod_int_rel_div_mod [THEN unique_remainder]) -instance int :: ring_div +instance proof fix a b :: int show "a div b * b + a mod b = a" @@ -1932,6 +1912,8 @@ by (rule div_int_unique, auto simp add: divmod_int_rel_def) qed +end + text{*Basic laws about division and remainder*} lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" @@ -2479,7 +2461,7 @@ split_neg_lemma [of concl: "%x y. P y"]) done -text {* Enable (lin)arith to deal with @{const div} and @{const mod} +text {* Enable (lin)arith to deal with @{const divide} and @{const mod} when these are applied to some constant that is of the form @{term "numeral k"}: *} declare split_zdiv [of _ _ "numeral k", arith_split] for k diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Enum.thy Sat Jun 13 22:44:22 2015 +0200 @@ -817,7 +817,7 @@ definition "x - y = x + (- y :: finite_3)" definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \ a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \ a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \ a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \ a\<^sub>3 | _ \ a\<^sub>1)" definition "inverse = (\x :: finite_3. x)" -definition "divide x y = x * inverse (y :: finite_3)" +definition "x div y = x * inverse (y :: finite_3)" definition "abs = (\x :: finite_3. x)" definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \ a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \ a\<^sub>3 | _ \ a\<^sub>1)" definition "sgn = (\x. case x of a\<^sub>1 \ a\<^sub>1 | _ \ a\<^sub>2)" diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Groups_Big.thy Sat Jun 13 22:44:22 2015 +0200 @@ -1155,7 +1155,7 @@ lemma (in semidom_divide) setprod_diff1: assumes "finite A" and "f a \ 0" - shows "setprod f (A - {a}) = (if a \ A then divide (setprod f A) (f a) else setprod f A)" + shows "setprod f (A - {a}) = (if a \ A then setprod f A div f a else setprod f A)" proof (cases "a \ A") case True then show ?thesis by simp next diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Import/HOL_Light_Maps.thy --- a/src/HOL/Import/HOL_Light_Maps.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Import/HOL_Light_Maps.thy Sat Jun 13 22:44:22 2015 +0200 @@ -198,7 +198,7 @@ by simp import_const_map MOD : mod -import_const_map DIV : div +import_const_map DIV : divide lemma DIVISION_0: "\m n\nat. if n = id 0 then m div n = id 0 \ m mod n = m else m = m div n * n + m mod n \ m mod n < n" diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Library/Bit.thy Sat Jun 13 22:44:22 2015 +0200 @@ -117,7 +117,7 @@ "inverse x = (x :: bit)" definition divide_bit_def [simp]: - "divide x y = (x * y :: bit)" + "x div y = (x * y :: bit)" lemmas field_bit_defs = plus_bit_def times_bit_def minus_bit_def uminus_bit_def diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Library/Extended_Real.thy Sat Jun 13 22:44:22 2015 +0200 @@ -1403,7 +1403,7 @@ by (auto intro: ereal_cases) termination by (relation "{}") simp -definition "divide x y = x * inverse (y :: ereal)" +definition "x div y = x * inverse (y :: ereal)" instance .. diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Library/Fraction_Field.thy Sat Jun 13 22:44:22 2015 +0200 @@ -241,9 +241,9 @@ by (simp add: Fract_def inverse_fract_def UN_fractrel) qed -definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)" +definition divide_fract_def: "q div r = q * inverse (r:: 'a fract)" -lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)" +lemma divide_fract [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)" by (simp add: divide_fract_def) instance @@ -255,7 +255,7 @@ (simp_all add: fract_expand eq_fract mult.commute) next fix q r :: "'a fract" - show "divide q r = q * inverse r" by (simp add: divide_fract_def) + show "q div r = q * inverse r" by (simp add: divide_fract_def) next show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand) (simp add: fract_collapse) diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Library/Function_Division.thy --- a/src/HOL/Library/Function_Division.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Library/Function_Division.thy Sat Jun 13 22:44:22 2015 +0200 @@ -15,7 +15,7 @@ definition "inverse f = inverse \ f" -definition "divide f g = (\x. f x / g x)" +definition "f div g = (\x. f x / g x)" instance .. diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Library/Order_Continuity.thy --- a/src/HOL/Library/Order_Continuity.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Library/Order_Continuity.thy Sat Jun 13 22:44:22 2015 +0200 @@ -91,6 +91,19 @@ qed qed +lemma lfp_transfer: + assumes \: "sup_continuous \" and f: "sup_continuous f" and g: "sup_continuous g" + assumes [simp]: "\ bot = bot" "\x. \ (f x) = g (\ x)" + shows "\ (lfp f) = lfp g" +proof - + have "\ (lfp f) = (SUP i. \ ((f^^i) bot))" + unfolding sup_continuous_lfp[OF f] by (intro f \ sup_continuousD mono_funpow sup_continuous_mono) + moreover have "\ ((f^^i) bot) = (g^^i) bot" for i + by (induction i; simp) + ultimately show ?thesis + unfolding sup_continuous_lfp[OF g] by simp +qed + definition inf_continuous :: "('a::complete_lattice \ 'a::complete_lattice) \ bool" where "inf_continuous F \ (\M::nat \ 'a. antimono M \ F (INF i. M i) = (INF i. F (M i)))" @@ -146,4 +159,17 @@ qed qed +lemma gfp_transfer: + assumes \: "inf_continuous \" and f: "inf_continuous f" and g: "inf_continuous g" + assumes [simp]: "\ top = top" "\x. \ (f x) = g (\ x)" + shows "\ (gfp f) = gfp g" +proof - + have "\ (gfp f) = (INF i. \ ((f^^i) top))" + unfolding inf_continuous_gfp[OF f] by (intro f \ inf_continuousD antimono_funpow inf_continuous_mono) + moreover have "\ ((f^^i) top) = (g^^i) top" for i + by (induction i; simp) + ultimately show ?thesis + unfolding inf_continuous_gfp[OF g] by simp +qed + end diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Library/Polynomial.thy Sat Jun 13 22:44:22 2015 +0200 @@ -1361,13 +1361,13 @@ begin definition divide_poly where - div_poly_def: "divide x y = (THE q. \r. pdivmod_rel x y q r)" + div_poly_def: "x div y = (THE q. \r. pdivmod_rel x y q r)" definition mod_poly where "x mod y = (THE r. \q. pdivmod_rel x y q r)" lemma div_poly_eq: - "pdivmod_rel x y q r \ divide x y = q" + "pdivmod_rel x y q r \ x div y = q" unfolding div_poly_def by (fast elim: pdivmod_rel_unique_div) @@ -1377,7 +1377,7 @@ by (fast elim: pdivmod_rel_unique_mod) lemma pdivmod_rel: - "pdivmod_rel x y (divide x y) (x mod y)" + "pdivmod_rel x y (x div y) (x mod y)" proof - from pdivmod_rel_exists obtain q r where "pdivmod_rel x y q r" by fast @@ -1387,41 +1387,41 @@ instance proof fix x y :: "'a poly" - show "divide x y * y + x mod y = x" + show "x div y * y + x mod y = x" using pdivmod_rel [of x y] by (simp add: pdivmod_rel_def) next fix x :: "'a poly" have "pdivmod_rel x 0 0 x" by (rule pdivmod_rel_by_0) - thus "divide x 0 = 0" + thus "x div 0 = 0" by (rule div_poly_eq) next fix y :: "'a poly" have "pdivmod_rel 0 y 0 0" by (rule pdivmod_rel_0) - thus "divide 0 y = 0" + thus "0 div y = 0" by (rule div_poly_eq) next fix x y z :: "'a poly" assume "y \ 0" - hence "pdivmod_rel (x + z * y) y (z + divide x y) (x mod y)" + hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)" using pdivmod_rel [of x y] by (simp add: pdivmod_rel_def distrib_right) - thus "divide (x + z * y) y = z + divide x y" + thus "(x + z * y) div y = z + x div y" by (rule div_poly_eq) next fix x y z :: "'a poly" assume "x \ 0" - show "divide (x * y) (x * z) = divide y z" + show "(x * y) div (x * z) = y div z" proof (cases "y \ 0 \ z \ 0") have "\x::'a poly. pdivmod_rel x 0 0 x" by (rule pdivmod_rel_by_0) - then have [simp]: "\x::'a poly. divide x 0 = 0" + then have [simp]: "\x::'a poly. x div 0 = 0" by (rule div_poly_eq) have "\x::'a poly. pdivmod_rel 0 x 0 0" by (rule pdivmod_rel_0) - then have [simp]: "\x::'a poly. divide 0 x = 0" + then have [simp]: "\x::'a poly. 0 div x = 0" by (rule div_poly_eq) case False then show ?thesis by auto next @@ -1430,8 +1430,8 @@ have "\q r. pdivmod_rel y z q r \ pdivmod_rel (x * y) (x * z) q (x * r)" by (auto simp add: pdivmod_rel_def algebra_simps) (rule classical, simp add: degree_mult_eq) - moreover from pdivmod_rel have "pdivmod_rel y z (divide y z) (y mod z)" . - ultimately have "pdivmod_rel (x * y) (x * z) (divide y z) (x * (y mod z))" . + moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" . + ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" . then show ?thesis by (simp add: div_poly_eq) qed qed diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Jun 13 22:44:22 2015 +0200 @@ -1,5 +1,5 @@ (* Author: John Harrison - Author: Robert Himmelmann, TU Muenchen (Translation from HOL light) + Author: Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP *) section \Kurzweil-Henstock Gauge Integration in many dimensions.\ @@ -1042,7 +1042,7 @@ next case False note p = division_ofD[OF assms(1)] - have *: "\k\p. \q. q division_of cbox a b \ k \ q" + have div_cbox: "\k\p. \q. q division_of cbox a b \ k \ q" proof case goal1 obtain c d where k: "k = cbox c d" @@ -1056,7 +1056,7 @@ unfolding k by auto qed obtain q where q: "\x. x \ p \ q x division_of cbox a b" "\x. x \ p \ x \ q x" - using bchoice[OF *] by blast + using bchoice[OF div_cbox] by blast { fix x assume x: "x \ p" have "q x division_of \q x" @@ -1075,44 +1075,37 @@ have "d \ p division_of cbox a b" proof - have te: "\s f t. s \ {} \ \i\s. f i \ i = t \ t = \(f ` s) \ \s" by auto - have *: "cbox a b = \((\i. \(q i - {i})) ` p) \ \p" + have cbox_eq: "cbox a b = \((\i. \(q i - {i})) ` p) \ \p" proof (rule te[OF False], clarify) fix i assume i: "i \ p" show "\(q i - {i}) \ i = cbox a b" using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto qed - show "d \ p division_of (cbox a b)" - unfolding * - apply (rule division_disjoint_union[OF d assms(1)]) - apply (rule inter_interior_unions_intervals) - apply (rule p open_interior ballI)+ - apply assumption - proof - fix k + { fix k assume k: "k \ p" - have *: "\u t s. u \ s \ s \ t = {} \ u \ t = {}" + have *: "\u t s. t \ s = {} \ u \ s \ u \ t = {}" by auto - show "interior (\ ((\i. \(q i - {i})) ` p)) \ interior k = {}" - apply (rule *[of _ "interior (\(q k - {k}))"]) - defer - apply (subst Int_commute) - apply (rule inter_interior_unions_intervals) - proof - + have "interior (\i\p. \(q i - {i})) \ interior k = {}" + proof (rule *[OF inter_interior_unions_intervals]) note qk=division_ofD[OF q(1)[OF k]] show "finite (q k - {k})" "open (interior k)" "\t\q k - {k}. \a b. t = cbox a b" using qk by auto show "\t\q k - {k}. interior k \ interior t = {}" using qk(5) using q(2)[OF k] by auto - have *: "\x s. x \ s \ \s \ x" - by auto - show "interior (\ ((\i. \(q i - {i})) ` p)) \ interior (\(q k - {k}))" - apply (rule interior_mono *)+ + show "interior (\i\p. \(q i - {i})) \ interior (\(q k - {k}))" + apply (rule interior_mono)+ using k apply auto done - qed - qed + qed } note [simp] = this + show "d \ p division_of (cbox a b)" + unfolding cbox_eq + apply (rule division_disjoint_union[OF d assms(1)]) + apply (rule inter_interior_unions_intervals) + apply (rule p open_interior ballI)+ + apply simp_all + done qed then show ?thesis by (meson Un_upper2 that) @@ -1144,51 +1137,40 @@ show ?thesis proof (cases "cbox a b \ cbox c d = {}") case True - have *: "\a b. {a, b} = {a} \ {b}" by auto show ?thesis apply (rule that[of "{cbox c d}"]) - unfolding * + apply (subst insert_is_Un) apply (rule division_disjoint_union) - using \cbox c d \ {}\ True assms - using interior_subset + using \cbox c d \ {}\ True assms interior_subset apply auto done next case False obtain u v where uv: "cbox a b \ cbox c d = cbox u v" unfolding inter_interval by auto - have *: "cbox u v \ cbox c d" using uv by auto + have uv_sub: "cbox u v \ cbox c d" using uv by auto obtain p where "p division_of cbox c d" "cbox u v \ p" - by (rule partial_division_extend_1[OF * False[unfolded uv]]) + by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]]) note p = this division_ofD[OF this(1)] - have *: "cbox a b \ cbox c d = cbox a b \ \(p - {cbox u v})" "\x s. insert x s = {x} \ s" + have "interior (cbox a b \ \(p - {cbox u v})) = interior(cbox u v \ \(p - {cbox u v}))" + apply (rule arg_cong[of _ _ interior]) + using p(8) uv by auto + also have "\ = {}" + unfolding interior_inter + apply (rule inter_interior_unions_intervals) + using p(6) p(7)[OF p(2)] p(3) + apply auto + done + finally have [simp]: "interior (cbox a b) \ interior (\(p - {cbox u v})) = {}" by simp + have cbe: "cbox a b \ cbox c d = cbox a b \ \(p - {cbox u v})" using p(8) unfolding uv[symmetric] by auto show ?thesis apply (rule that[of "p - {cbox u v}"]) - unfolding *(1) - apply (subst *(2)) + apply (simp add: cbe) + apply (subst insert_is_Un) apply (rule division_disjoint_union) - apply (rule, rule assms) - apply (rule division_of_subset[of p]) - apply (rule division_of_union_self[OF p(1)]) - defer - unfolding interior_inter[symmetric] - proof - - have *: "\cd p uv ab. p \ cd \ ab \ cd = uv \ ab \ p = uv \ p" by auto - have "interior (cbox a b \ \(p - {cbox u v})) = interior(cbox u v \ \(p - {cbox u v}))" - apply (rule arg_cong[of _ _ interior]) - apply (rule *[OF _ uv]) - using p(8) - apply auto - done - also have "\ = {}" - unfolding interior_inter - apply (rule inter_interior_unions_intervals) - using p(6) p(7)[OF p(2)] p(3) - apply auto - done - finally show "interior (cbox a b \ \(p - {cbox u v})) = {}" . - qed auto + apply (simp_all add: assms division_of_self) + by (metis Diff_subset division_of_subset p(1) p(8)) qed qed @@ -1248,10 +1230,8 @@ from bchoice[OF this] obtain q where "\x\p. insert (cbox a b) (q x) division_of (cbox a b) \ x" .. note q = division_ofD[OF this[rule_format]] let ?D = "\{insert (cbox a b) (q k) | k. k \ p}" - show thesis - apply (rule that[of "?D"]) - apply (rule division_ofI) - proof - + show thesis + proof (rule that[OF division_ofI]) have *: "{insert (cbox a b) (q k) |k. k \ p} = (\k. insert (cbox a b) (q k)) ` p" by auto show "finite ?D" @@ -1842,12 +1822,11 @@ using assms(1,3) by metis then have ab: "\i. i\Basis \ a \ i \ b \ i" by (force simp: mem_box) - { - fix f - have "finite f \ - \s\f. P s \ - \s\f. \a b. s = cbox a b \ - \s\f.\t\f. s \ t \ interior s \ interior t = {} \ P (\f)" + { fix f + have "\finite f; + \s. s\f \ P s; + \s. s\f \ \a b. s = cbox a b; + \s t. s\f \ t\f \ s \ t \ interior s \ interior t = {}\ \ P (\f)" proof (induct f rule: finite_induct) case empty show ?case @@ -1859,9 +1838,9 @@ apply (rule assms(2)[rule_format]) using inter_interior_unions_intervals [of f "interior x"] apply (auto simp: insert) - using insert.prems(3) insert.hyps(2) by fastforce - qed - } note * = this + by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff) + qed + } note UN_cases = this let ?A = "{cbox c d | c d::'a. \i\Basis. (c\i = a\i) \ (d\i = (a\i + b\i) / 2) \ (c\i = (a\i + b\i) / 2) \ (d\i = b\i)}" let ?PP = "\c d. \i\Basis. a\i \ c\i \ c\i \ d\i \ d\i \ b\i \ 2 * (d\i - c\i) \ b\i - a\i" @@ -1873,47 +1852,35 @@ } assume as: "\c d. ?PP c d \ P (cbox c d)" have "P (\ ?A)" - apply (rule *) - apply (rule_tac[2-] ballI) - apply (rule_tac[4] ballI) - apply (rule_tac[4] impI) - proof - + proof (rule UN_cases) let ?B = "(\s. cbox (\i\Basis. (if i \ s then a\i else (a\i + b\i) / 2) *\<^sub>R i::'a) (\i\Basis. (if i \ s then (a\i + b\i) / 2 else b\i) *\<^sub>R i)) ` {s. s \ Basis}" have "?A \ ?B" proof case goal1 - then obtain c d where x: "x = cbox c d" - "\i. i \ Basis \ - c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" by blast - have *: "\a b c d. a = c \ b = d \ cbox a b = cbox c d" - by auto + then obtain c d + where x: "x = cbox c d" + "\i. i \ Basis \ + c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ + c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" by blast show "x \ ?B" - unfolding image_iff + unfolding image_iff x apply (rule_tac x="{i. i\Basis \ c\i = a\i}" in bexI) - unfolding x - apply (rule *) - apply (simp_all only: euclidean_eq_iff[where 'a='a] inner_setsum_left_Basis mem_Collect_eq simp_thms - cong: ball_cong) - apply safe - proof - - fix i :: 'a - assume i: "i \ Basis" - then show "c \ i = (if c \ i = a \ i then a \ i else (a \ i + b \ i) / 2)" - and "d \ i = (if c \ i = a \ i then (a \ i + b \ i) / 2 else b \ i)" - using x(2)[of i] ab[OF i] by (auto simp add:field_simps) - qed + apply (rule arg_cong2 [where f = cbox]) + using x(2) ab + apply (auto simp add: euclidean_eq_iff[where 'a='a]) + by fastforce qed then show "finite ?A" by (rule finite_subset) auto + next fix s assume "s \ ?A" - then obtain c d where s: - "s = cbox c d" - "\i. i \ Basis \ - c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" + then obtain c d + where s: "s = cbox c d" + "\i. i \ Basis \ + c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ + c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" by blast show "P s" unfolding s @@ -2179,28 +2146,18 @@ next assume as: "\ (\p. p tagged_division_of (cbox a b) \ g fine p)" obtain x where x: - "x \ (cbox a b)" - "\e. 0 < e \ - \c d. - x \ cbox c d \ - cbox c d \ ball x e \ - cbox c d \ (cbox a b) \ - \ (\p. p tagged_division_of cbox c d \ g fine p)" - apply (rule interval_bisection[of "\s. \p. p tagged_division_of s \ g fine p",rule_format,OF _ _ as]) - apply (rule_tac x="{}" in exI) - defer - apply (erule conjE exE)+ - proof - - show "{} tagged_division_of {} \ g fine {}" - unfolding fine_def by auto - fix s t p p' - assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'" - "interior s \ interior t = {}" - then show "\p. p tagged_division_of s \ t \ g fine p" - apply (rule_tac x="p \ p'" in exI) - apply (simp add: tagged_division_union fine_union) - done - qed blast + "x \ (cbox a b)" + "\e. 0 < e \ + \c d. + x \ cbox c d \ + cbox c d \ ball x e \ + cbox c d \ (cbox a b) \ + \ (\p. p tagged_division_of cbox c d \ g fine p)" + apply (rule interval_bisection[of "\s. \p. p tagged_division_of s \ g fine p", OF _ _ as]) + apply (simp add: fine_def) + apply (metis tagged_division_union fine_union) + apply (auto simp: ) + done obtain e where e: "e > 0" "ball x e \ g x" using gaugeD[OF assms, of x] unfolding open_contains_ball by auto from x(2)[OF e(1)] @@ -2388,35 +2345,30 @@ from pos_bounded obtain B where B: "0 < B" "\x. norm (h x) \ norm x * B" by blast - have *: "e / B > 0" using goal1(2) B by simp - obtain g where g: "gauge g" - "\p. p tagged_division_of (cbox a b) \ g fine p \ - norm ((\(x, k)\p. content k *\<^sub>R f x) - y) < e / B" - using "*" goal1(1) by auto - show ?case - apply (rule_tac x=g in exI) - apply rule - apply (rule g(1)) - apply rule - apply rule - apply (erule conjE) - proof - - fix p + have "e / B > 0" using goal1(2) B by simp + then obtain g + where g: "gauge g" + "\p. p tagged_division_of (cbox a b) \ g fine p \ + norm ((\(x, k)\p. content k *\<^sub>R f x) - y) < e / B" + using goal1(1) by auto + { fix p assume as: "p tagged_division_of (cbox a b)" "g fine p" - have *: "\x k. h ((\(x, k). content k *\<^sub>R f x) x) = (\(x, k). h (content k *\<^sub>R f x)) x" + have hc: "\x k. h ((\(x, k). content k *\<^sub>R f x) x) = (\(x, k). h (content k *\<^sub>R f x)) x" by auto - have "(\(x, k)\p. content k *\<^sub>R (h \ f) x) = setsum (h \ (\(x, k). content k *\<^sub>R f x)) p" - unfolding o_def unfolding scaleR[symmetric] * by simp + then have "(\(x, k)\p. content k *\<^sub>R (h \ f) x) = setsum (h \ (\(x, k). content k *\<^sub>R f x)) p" + unfolding o_def unfolding scaleR[symmetric] hc by simp also have "\ = h (\(x, k)\p. content k *\<^sub>R f x)" using setsum[of "\(x,k). content k *\<^sub>R f x" p] using as by auto - finally have *: "(\(x, k)\p. content k *\<^sub>R (h \ f) x) = h (\(x, k)\p. content k *\<^sub>R f x)" . - show "norm ((\(x, k)\p. content k *\<^sub>R (h \ f) x) - h y) < e" - unfolding * diff[symmetric] + finally have "(\(x, k)\p. content k *\<^sub>R (h \ f) x) = h (\(x, k)\p. content k *\<^sub>R f x)" . + then have "norm ((\(x, k)\p. content k *\<^sub>R (h \ f) x) - h y) < e" + apply (simp add: diff[symmetric]) apply (rule le_less_trans[OF B(2)]) using g(2)[OF as] B(1) apply (auto simp add: field_simps) done - qed + } + with g show ?case + by (rule_tac x=g in exI) auto qed { presume "\ (\a b. s = cbox a b) \ ?thesis" @@ -2696,27 +2648,23 @@ lemma has_integral_null[dest]: assumes "content(cbox a b) = 0" shows "(f has_integral 0) (cbox a b)" - unfolding has_integral - apply rule - apply rule - apply (rule_tac x="\x. ball x 1" in exI) - apply rule - defer - apply rule - apply rule - apply (erule conjE) -proof - - fix e :: real - assume e: "e > 0" - then show "gauge (\x. ball x 1)" +proof - + have "gauge (\x. ball x 1)" by auto - fix p - assume p: "p tagged_division_of (cbox a b)" - have "norm ((\(x, k)\p. content k *\<^sub>R f x) - 0) = 0" - unfolding norm_eq_zero diff_0_right - using setsum_content_null[OF assms(1) p, of f] . - then show "norm ((\(x, k)\p. content k *\<^sub>R f x) - 0) < e" - using e by auto + moreover + { + fix e :: real + fix p + assume e: "e > 0" + assume p: "p tagged_division_of (cbox a b)" + have "norm ((\(x, k)\p. content k *\<^sub>R f x) - 0) = 0" + unfolding norm_eq_zero diff_0_right + using setsum_content_null[OF assms(1) p, of f] . + then have "norm ((\(x, k)\p. content k *\<^sub>R f x) - 0) < e" + using e by auto + } + ultimately show ?thesis + by (auto simp: has_integral) qed lemma has_integral_null_real[dest]: @@ -3088,83 +3036,80 @@ lemma has_integral_split: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" - assumes "(f has_integral i) (cbox a b \ {x. x\k \ c})" - and "(f has_integral j) (cbox a b \ {x. x\k \ c})" - and k: "k \ Basis" + assumes fi: "(f has_integral i) (cbox a b \ {x. x\k \ c})" + and fj: "(f has_integral j) (cbox a b \ {x. x\k \ c})" + and k: "k \ Basis" shows "(f has_integral (i + j)) (cbox a b)" proof (unfold has_integral, rule, rule) case goal1 then have e: "e/2 > 0" by auto - guess d1 using has_integralD[OF assms(1)[unfolded interval_split[OF k]] e] . - note d1=this[unfolded interval_split[symmetric,OF k]] - guess d2 using has_integralD[OF assms(2)[unfolded interval_split[OF k]] e] . - note d2=this[unfolded interval_split[symmetric,OF k]] + obtain d1 + where d1: "gauge d1" + and d1norm: + "\p. \p tagged_division_of cbox a b \ {x. x \ k \ c}; + d1 fine p\ \ norm ((\(x, k) \ p. content k *\<^sub>R f x) - i) < e / 2" + apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e]) + apply (simp add: interval_split[symmetric] k) + done + obtain d2 + where d2: "gauge d2" + and d2norm: + "\p. \p tagged_division_of cbox a b \ {x. c \ x \ k}; + d2 fine p\ \ norm ((\(x, k) \ p. content k *\<^sub>R f x) - j) < e / 2" + apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e]) + apply (simp add: interval_split[symmetric] k) + done let ?d = "\x. if x\k = c then (d1 x \ d2 x) else ball x (abs(x\k - c)) \ d1 x \ d2 x" - show ?case - apply (rule_tac x="?d" in exI) - apply rule - defer - apply rule - apply rule - apply (elim conjE) - proof - - show "gauge ?d" - using d1(1) d2(1) unfolding gauge_def by auto + have "gauge ?d" + using d1 d2 unfolding gauge_def by auto + then show ?case + proof (rule_tac x="?d" in exI, safe) fix p assume "p tagged_division_of (cbox a b)" "?d fine p" note p = this tagged_division_ofD[OF this(1)] - have lem0: - "\x kk. (x, kk) \ p \ kk \ {x. x\k \ c} \ {} \ x\k \ c" - "\x kk. (x, kk) \ p \ kk \ {x. x\k \ c} \ {} \ x\k \ c" + have xk_le_c: "\x kk. (x, kk) \ p \ kk \ {x. x\k \ c} \ {} \ x\k \ c" proof - fix x kk - assume as: "(x, kk) \ p" - { - assume *: "kk \ {x. x\k \ c} \ {}" - show "x\k \ c" - proof (rule ccontr) - assume **: "\ ?thesis" - from this[unfolded not_le] - have "kk \ ball x \x \ k - c\" - using p(2)[unfolded fine_def, rule_format,OF as,unfolded split_conv] by auto - with * have "\y. y \ ball x \x \ k - c\ \ {x. x \ k \ c}" - by blast - then guess y .. - then have "\x \ k - y \ k\ < \x \ k - c\" "y\k \ c" - apply - - apply (rule le_less_trans) - using Basis_le_norm[OF k, of "x - y"] - apply (auto simp add: dist_norm inner_diff_left) - done - then show False - using **[unfolded not_le] by (auto simp add: field_simps) - qed - next - assume *: "kk \ {x. x\k \ c} \ {}" - show "x\k \ c" - proof (rule ccontr) - assume **: "\ ?thesis" - from this[unfolded not_le] have "kk \ ball x \x \ k - c\" - using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto - with * have "\y. y \ ball x \x \ k - c\ \ {x. x \ k \ c}" - by blast - then guess y .. - then have "\x \ k - y \ k\ < \x \ k - c\" "y\k \ c" - apply - - apply (rule le_less_trans) - using Basis_le_norm[OF k, of "x - y"] - apply (auto simp add: dist_norm inner_diff_left) - done - then show False - using **[unfolded not_le] by (auto simp add: field_simps) - qed - } + assume as: "(x, kk) \ p" and kk: "kk \ {x. x\k \ c} \ {}" + show "x\k \ c" + proof (rule ccontr) + assume **: "\ ?thesis" + from this[unfolded not_le] + have "kk \ ball x \x \ k - c\" + using p(2)[unfolded fine_def, rule_format,OF as] by auto + with kk obtain y where y: "y \ ball x \x \ k - c\" "y\k \ c" + by blast + then have "\x \ k - y \ k\ < \x \ k - c\" + using Basis_le_norm[OF k, of "x - y"] + by (auto simp add: dist_norm inner_diff_left intro: le_less_trans) + with y show False + using ** by (auto simp add: field_simps) + qed + qed + have xk_ge_c: "\x kk. (x, kk) \ p \ kk \ {x. x\k \ c} \ {} \ x\k \ c" + proof - + fix x kk + assume as: "(x, kk) \ p" and kk: "kk \ {x. x\k \ c} \ {}" + show "x\k \ c" + proof (rule ccontr) + assume **: "\ ?thesis" + from this[unfolded not_le] have "kk \ ball x \x \ k - c\" + using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto + with kk obtain y where y: "y \ ball x \x \ k - c\" "y\k \ c" + by blast + then have "\x \ k - y \ k\ < \x \ k - c\" + using Basis_le_norm[OF k, of "x - y"] + by (auto simp add: dist_norm inner_diff_left intro: le_less_trans) + with y show False + using ** by (auto simp add: field_simps) + qed qed have lem1: "\f P Q. (\x k. (x, k) \ {(x, f k) | x k. P x k} \ Q x k) \ - (\x k. P x k \ Q x (f k))" by auto - have lem2: "\f s P f. finite s \ finite {(x,f k) | x k. (x,k) \ s \ P x k}" + (\x k. P x k \ Q x (f k))" + by auto + have fin_finite: "\f s P f. finite s \ finite {(x,f k) | x k. (x,k) \ s \ P x k}" proof - case goal1 then have "finite ((\(x, k). (x, f k)) ` s)" @@ -3172,50 +3117,38 @@ then show ?case by (rule rev_finite_subset) auto qed - have lem3: "\g :: 'a set \ 'a set. finite p \ - setsum (\(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \ p \ g k \ {}} = - setsum (\(x, k). content k *\<^sub>R f x) ((\(x, k). (x, g k)) ` p)" - apply (rule setsum.mono_neutral_left) - prefer 3 - proof - fix g :: "'a set \ 'a set" + { fix g :: "'a set \ 'a set" fix i :: "'a \ 'a set" assume "i \ (\(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \ p \ g k \ {}}" then obtain x k where xk: - "i = (x, g k)" - "(x, k) \ p" - "(x, g k) \ {(x, g k) |x k. (x, k) \ p \ g k \ {}}" - by auto + "i = (x, g k)" "(x, k) \ p" + "(x, g k) \ {(x, g k) |x k. (x, k) \ p \ g k \ {}}" + by auto have "content (g k) = 0" using xk using content_empty by auto - then show "(\(x, k). content k *\<^sub>R f x) i = 0" + then have "(\(x, k). content k *\<^sub>R f x) i = 0" unfolding xk split_conv by auto - qed auto - have lem4: "\g. (\(x,l). content (g l) *\<^sub>R f x) = (\(x,l). content l *\<^sub>R f x) \ (\(x,l). (x,g l))" - by auto - + } note [simp] = this + have lem3: "\g :: 'a set \ 'a set. finite p \ + setsum (\(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \ p \ g k \ {}} = + setsum (\(x, k). content k *\<^sub>R f x) ((\(x, k). (x, g k)) ` p)" + by (rule setsum.mono_neutral_left) auto let ?M1 = "{(x, kk \ {x. x\k \ c}) |x kk. (x, kk) \ p \ kk \ {x. x\k \ c} \ {}}" + have d1_fine: "d1 fine ?M1" + by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm) have "norm ((\(x, k)\?M1. content k *\<^sub>R f x) - i) < e/2" - apply (rule d1(2),rule tagged_division_ofI) - apply (rule lem2 p(3))+ - prefer 6 - apply (rule fineI) - proof - + proof (rule d1norm [OF tagged_division_ofI d1_fine]) + show "finite ?M1" + by (rule fin_finite p(3))+ show "\{k. \x. (x, k) \ ?M1} = cbox a b \ {x. x\k \ c}" unfolding p(8)[symmetric] by auto fix x l assume xl: "(x, l) \ ?M1" then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this - have "l' \ d1 x'" - apply (rule order_trans[OF fineD[OF p(2) xl'(3)]]) - apply auto - done - then show "l \ d1 x" - unfolding xl' by auto show "x \ l" "l \ cbox a b \ {x. x \ k \ c}" unfolding xl' using p(4-6)[OF xl'(3)] using xl'(4) - using lem0(1)[OF xl'(3-4)] by auto + using xk_le_c[OF xl'(3-4)] by auto show "\a b. l = cbox a b" unfolding xl' using p(6)[OF xl'(3)] @@ -3240,28 +3173,20 @@ qed moreover let ?M2 = "{(x,kk \ {x. x\k \ c}) |x kk. (x,kk) \ p \ kk \ {x. x\k \ c} \ {}}" + have d2_fine: "d2 fine ?M2" + by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm) have "norm ((\(x, k)\?M2. content k *\<^sub>R f x) - j) < e/2" - apply (rule d2(2),rule tagged_division_ofI) - apply (rule lem2 p(3))+ - prefer 6 - apply (rule fineI) - proof - + proof (rule d2norm [OF tagged_division_ofI d2_fine]) + show "finite ?M2" + by (rule fin_finite p(3))+ show "\{k. \x. (x, k) \ ?M2} = cbox a b \ {x. x\k \ c}" unfolding p(8)[symmetric] by auto fix x l assume xl: "(x, l) \ ?M2" then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this - have "l' \ d2 x'" - apply (rule order_trans[OF fineD[OF p(2) xl'(3)]]) - apply auto - done - then show "l \ d2 x" - unfolding xl' by auto show "x \ l" "l \ cbox a b \ {x. x \ k \ c}" unfolding xl' - using p(4-6)[OF xl'(3)] - using xl'(4) - using lem0(2)[OF xl'(3-4)] + using p(4-6)[OF xl'(3)] xl'(4) xk_ge_c[OF xl'(3-4)] by auto show "\a b. l = cbox a b" unfolding xl' @@ -3289,46 +3214,24 @@ have "norm (((\(x, k)\?M1. content k *\<^sub>R f x) - i) + ((\(x, k)\?M2. content k *\<^sub>R f x) - j)) < e/2 + e/2" using norm_add_less by blast also { - have *: "\x y. x = (0::real) \ x *\<^sub>R (y::'b) = 0" + have eq0: "\x y. x = (0::real) \ x *\<^sub>R (y::'b) = 0" using scaleR_zero_left by auto + have cont_eq: "\g. (\(x,l). content l *\<^sub>R f x) \ (\(x,l). (x,g l)) = (\(x,l). content (g l) *\<^sub>R f x)" + by auto have "((\(x, k)\?M1. content k *\<^sub>R f x) - i) + ((\(x, k)\?M2. content k *\<^sub>R f x) - j) = (\(x, k)\?M1. content k *\<^sub>R f x) + (\(x, k)\?M2. content k *\<^sub>R f x) - (i + j)" by auto also have "\ = (\(x, ka)\p. content (ka \ {x. x \ k \ c}) *\<^sub>R f x) + (\(x, ka)\p. content (ka \ {x. c \ x \ k}) *\<^sub>R f x) - (i + j)" unfolding lem3[OF p(3)] - apply (subst setsum.reindex_nontrivial[OF p(3)]) - defer - apply (subst setsum.reindex_nontrivial[OF p(3)]) - defer - unfolding lem4[symmetric] - apply (rule refl) - unfolding split_paired_all split_conv - apply (rule_tac[!] *) - proof - - case goal1 - then show ?case - apply - - apply (rule tagged_division_split_left_inj [OF p(1), of a b aa ba]) - using k - apply auto - done - next - case goal2 - then show ?case - apply - - apply (rule tagged_division_split_right_inj[OF p(1), of a b aa ba]) - using k - apply auto - done - qed + by (subst setsum.reindex_nontrivial[OF p(3)], auto intro!: k eq0 tagged_division_split_left_inj[OF p(1)] tagged_division_split_right_inj[OF p(1)] + simp: cont_eq)+ also note setsum.distrib[symmetric] - also have *: "\x. x \ p \ - (\(x,ka). content (ka \ {x. x \ k \ c}) *\<^sub>R f x) x + - (\(x,ka). content (ka \ {x. c \ x \ k}) *\<^sub>R f x) x = - (\(x,ka). content ka *\<^sub>R f x) x" - unfolding split_paired_all split_conv - proof - + also have "\x. x \ p \ + (\(x,ka). content (ka \ {x. x \ k \ c}) *\<^sub>R f x) x + + (\(x,ka). content (ka \ {x. c \ x \ k}) *\<^sub>R f x) x = + (\(x,ka). content ka *\<^sub>R f x) x" + proof clarify fix a b assume "(a, b) \ p" from p(6)[OF this] guess u v by (elim exE) note uv=this @@ -3391,32 +3294,17 @@ norm ((setsum (\(x,k). content k *\<^sub>R f x) p1 + setsum (\(x,k). content k *\<^sub>R f x) p2) - i) < e" proof - guess d using has_integralD[OF assms(1-2)] . note d=this - show ?thesis - apply (rule that[of d]) - apply (rule d) - apply rule - apply rule - apply rule - apply (elim conjE) - proof - - fix p1 p2 + { fix p1 p2 assume "p1 tagged_division_of (cbox a b) \ {x. x \ k \ c}" "d fine p1" note p1=tagged_division_ofD[OF this(1)] this assume "p2 tagged_division_of (cbox a b) \ {x. c \ x \ k}" "d fine p2" note p2=tagged_division_ofD[OF this(1)] this note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this - have "norm ((\(x, k)\p1. content k *\<^sub>R f x) + (\(x, k)\p2. content k *\<^sub>R f x) - i) = - norm ((\(x, k)\p1 \ p2. content k *\<^sub>R f x) - i)" - apply (subst setsum.union_inter_neutral) - apply (rule p1 p2)+ - apply rule - unfolding split_paired_all split_conv - proof - - fix a b + { fix a b assume ab: "(a, b) \ p1 \ p2" have "(a, b) \ p1" using ab by auto - from p1(4)[OF this] guess u v by (elim exE) note uv = this + with p1 obtain u v where uv: "b = cbox u v" by auto have "b \ {x. x\k = c}" using ab p1(3)[of a b] p2(3)[of a b] by fastforce moreover @@ -3447,17 +3335,19 @@ qed ultimately have "content b = 0" unfolding uv content_eq_0_interior - apply - - apply (drule interior_mono) - apply auto - done - then show "content b *\<^sub>R f a = 0" + using interior_mono by blast + then have "content b *\<^sub>R f a = 0" by auto - qed auto + } + then have "norm ((\(x, k)\p1. content k *\<^sub>R f x) + (\(x, k)\p2. content k *\<^sub>R f x) - i) = + norm ((\(x, k)\p1 \ p2. content k *\<^sub>R f x) - i)" + by (subst setsum.union_inter_neutral) (auto simp: p1 p2) also have "\ < e" by (rule k d(2) p12 fine_union p1 p2)+ - finally show "norm ((\(x, k)\p1. content k *\<^sub>R f x) + (\(x, k)\p2. content k *\<^sub>R f x) - i) < e" . - qed + finally have "norm ((\(x, k)\p1. content k *\<^sub>R f x) + (\(x, k)\p2. content k *\<^sub>R f x) - i) < e" . + } + then show ?thesis + by (auto intro: that[of d] d elim: ) qed lemma integrable_split[intro]: @@ -3483,46 +3373,32 @@ p2 tagged_division_of (cbox a b) \ A \ d fine p2 \ norm ((\(x, k)\p1. content k *\<^sub>R f x) - (\(x, k)\p2. content k *\<^sub>R f x)) < e)" show "?P {x. x \ k \ c}" - apply (rule_tac x=d in exI) - apply rule - apply (rule d) - apply rule - apply rule - apply rule - proof - + proof (rule_tac x=d in exI, clarsimp simp add: d) fix p1 p2 - assume as: "p1 tagged_division_of (cbox a b) \ {x. x \ k \ c} \ d fine p1 \ - p2 tagged_division_of (cbox a b) \ {x. x \ k \ c} \ d fine p2" + assume as: "p1 tagged_division_of (cbox a b) \ {x. x \ k \ c}" "d fine p1" + "p2 tagged_division_of (cbox a b) \ {x. x \ k \ c}" "d fine p2" show "norm ((\(x, k)\p1. content k *\<^sub>R f x) - (\(x, k)\p2. content k *\<^sub>R f x)) < e" - proof - - guess p using fine_division_exists[OF d(1), of a' b] . note p=this - show ?thesis - using norm_triangle_half_l[OF d(2)[of p1 p] d(2)[of p2 p]] - using as unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric] - using p using assms + proof (rule fine_division_exists[OF d(1), of a' b] ) + fix p + assume "p tagged_division_of cbox a' b" "d fine p" + then show ?thesis + using as norm_triangle_half_l[OF d(2)[of p1 p] d(2)[of p2 p]] + unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric] by (auto simp add: algebra_simps) qed qed show "?P {x. x \ k \ c}" - apply (rule_tac x=d in exI) - apply rule - apply (rule d) - apply rule - apply rule - apply rule - proof - + proof (rule_tac x=d in exI, clarsimp simp add: d) fix p1 p2 - assume as: "p1 tagged_division_of (cbox a b) \ {x. x \ k \ c} \ d fine p1 \ - p2 tagged_division_of (cbox a b) \ {x. x \ k \ c} \ d fine p2" + assume as: "p1 tagged_division_of (cbox a b) \ {x. x \ k \ c}" "d fine p1" + "p2 tagged_division_of (cbox a b) \ {x. x \ k \ c}" "d fine p2" show "norm ((\(x, k)\p1. content k *\<^sub>R f x) - (\(x, k)\p2. content k *\<^sub>R f x)) < e" - proof - - guess p using fine_division_exists[OF d(1), of a b'] . note p=this - show ?thesis - using norm_triangle_half_l[OF d(2)[of p p1] d(2)[of p p2]] - using as + proof (rule fine_division_exists[OF d(1), of a b'] ) + fix p + assume "p tagged_division_of cbox a b'" "d fine p" + then show ?thesis + using as norm_triangle_half_l[OF d(2)[of p p1] d(2)[of p p2]] unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric] - using p - using assms by (auto simp add: algebra_simps) qed qed @@ -3547,9 +3423,6 @@ opp (f (cbox a b \ {x. x\k \ c})) (f (cbox a b \ {x. x\k \ c}))" using assms unfolding operative_def by auto -lemma operative_trivial: "operative opp f \ content (cbox a b) = 0 \ f (cbox a b) = neutral opp" - unfolding operative_def by auto - lemma property_empty_interval: "\a b. content (cbox a b) = 0 \ P (cbox a b) \ P {}" using content_empty unfolding empty_as_interval by auto @@ -3559,12 +3432,6 @@ subsection \Using additivity of lifted function to encode definedness.\ -lemma forall_option: "(\x. P x) \ P None \ (\x. P (Some x))" - by (metis option.nchotomy) - -lemma exists_option: "(\x. P x) \ P None \ (\x. P (Some x))" - by (metis option.nchotomy) - fun lifted where "lifted (opp :: 'a \ 'a \ 'b) (Some x) (Some y) = Some (opp x y)" | "lifted opp None _ = (None::'b option)" @@ -3587,50 +3454,36 @@ lemma monoidal_ac: assumes "monoidal opp" - shows "opp (neutral opp) a = a" - and "opp a (neutral opp) = a" + shows [simp]: "opp (neutral opp) a = a" + and [simp]: "opp a (neutral opp) = a" and "opp a b = opp b a" and "opp (opp a b) c = opp a (opp b c)" and "opp a (opp b c) = opp b (opp a c)" using assms unfolding monoidal_def by metis+ -lemma monoidal_simps[simp]: - assumes "monoidal opp" - shows "opp (neutral opp) a = a" - and "opp a (neutral opp) = a" - using monoidal_ac[OF assms] by auto - -lemma neutral_lifted[cong]: +lemma neutral_lifted [cong]: assumes "monoidal opp" shows "neutral (lifted opp) = Some (neutral opp)" - apply (subst neutral_def) - apply (rule some_equality) - apply rule - apply (induct_tac y) - prefer 3 -proof - - fix x - assume "\y. lifted opp x y = y \ lifted opp y x = y" - then show "x = Some (neutral opp)" - apply (induct x) - defer - apply rule +proof - + { fix x + assume "\y. lifted opp x y = y \ lifted opp y x = y" + then have "Some (neutral opp) = x" + apply (induct x) + apply force + by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) } + note [simp] = this + show ?thesis apply (subst neutral_def) - apply (subst eq_commute) - apply(rule some_equality) - apply rule - apply (erule_tac x="Some y" in allE) - defer - apply (rename_tac x) - apply (erule_tac x="Some x" in allE) - apply auto - done -qed (auto simp add:monoidal_ac[OF assms]) + apply (intro some_equality allI) + apply (induct_tac y) + apply (auto simp add:monoidal_ac[OF assms]) + done +qed lemma monoidal_lifted[intro]: assumes "monoidal opp" shows "monoidal (lifted opp)" - unfolding monoidal_def forall_option neutral_lifted[OF assms] + unfolding monoidal_def split_option_all neutral_lifted[OF assms] using monoidal_ac[OF assms] by auto @@ -3672,76 +3525,42 @@ assumes "monoidal opp" and "finite s" shows "iterate opp (insert x s) f = - (if x \ s then iterate opp s f else opp (f x) (iterate opp s f))" + (if x \ s then iterate opp s f else opp (f x) (iterate opp s f))" proof (cases "x \ s") case True - then have *: "insert x s = s" - by auto - show ?thesis unfolding iterate_def if_P[OF True] * by auto + then show ?thesis by (auto simp: insert_absorb iterate_def) next case False - note x = this note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]] show ?thesis proof (cases "f x = neutral opp") case True - show ?thesis - unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True] - unfolding True monoidal_simps[OF assms(1)] - by auto + then show ?thesis + using assms `x \ s` + by (auto simp: iterate_def support_clauses) next case False - show ?thesis - unfolding iterate_def fold'_def if_not_P[OF x] support_clauses if_not_P[OF False] + with `x \ s` \finite s\ support_subset show ?thesis + apply (simp add: iterate_def fold'_def support_clauses) apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def]) - using \finite s\ - unfolding support_def - using False x - apply auto + apply (force simp add: )+ done qed qed lemma iterate_some: - assumes "monoidal opp" - and "finite s" - shows "iterate (lifted opp) s (\x. Some(f x)) = Some (iterate opp s f)" - using assms(2) -proof (induct s) - case empty - then show ?case - using assms by auto -next - case (insert x F) - show ?case - apply (subst iterate_insert) - prefer 3 - apply (subst if_not_P) - defer - unfolding insert(3) lifted.simps - apply rule - using assms insert - apply auto - done -qed + "\monoidal opp; finite s\ \ iterate (lifted opp) s (\x. Some(f x)) = Some (iterate opp s f)" + by (erule finite_induct) (auto simp: monoidal_lifted) subsection \Two key instances of additivity.\ lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)" unfolding neutral_def - apply (rule some_equality) - defer - apply (erule_tac x=0 in allE) - apply auto - done + by (force elim: allE [where x=0]) lemma operative_content[intro]: "operative (op +) content" - unfolding operative_def neutral_add - apply safe - unfolding content_split[symmetric] - apply rule - done + by (force simp add: operative_def content_split[symmetric]) lemma monoidal_monoid[intro]: "monoidal ((op +)::('a::comm_monoid_add) \ 'a \ 'a)" unfolding monoidal_def neutral_add @@ -3750,35 +3569,20 @@ lemma operative_integral: fixes f :: "'a::euclidean_space \ 'b::banach" shows "operative (lifted(op +)) (\i. if f integrable_on i then Some(integral i f) else None)" - unfolding operative_def - unfolding neutral_lifted[OF monoidal_monoid] neutral_add - apply rule - apply rule - apply rule - apply rule - defer - apply (rule allI ballI)+ -proof - + unfolding operative_def neutral_lifted[OF monoidal_monoid] neutral_add +proof safe fix a b c fix k :: 'a assume k: "k \ Basis" show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = - lifted op + (if f integrable_on cbox a b \ {x. x \ k \ c} then Some (integral (cbox a b \ {x. x \ k \ c}) f) else None) - (if f integrable_on cbox a b \ {x. c \ x \ k} then Some (integral (cbox a b \ {x. c \ x \ k}) f) else None)" + lifted op + (if f integrable_on cbox a b \ {x. x \ k \ c} then Some (integral (cbox a b \ {x. x \ k \ c}) f) else None) + (if f integrable_on cbox a b \ {x. c \ x \ k} then Some (integral (cbox a b \ {x. c \ x \ k}) f) else None)" proof (cases "f integrable_on cbox a b") case True - show ?thesis - unfolding if_P[OF True] - using k - apply - - unfolding if_P[OF integrable_split(1)[OF True]] - unfolding if_P[OF integrable_split(2)[OF True]] - unfolding lifted.simps option.inject - apply (rule integral_unique) - apply (rule has_integral_split[OF _ _ k]) - apply (rule_tac[!] integrable_integral integrable_split)+ - using True k - apply auto + with k show ?thesis + apply (simp add: integrable_split) + apply (rule integral_unique [OF has_integral_split[OF _ _ k]]) + apply (auto intro: integrable_integral) done next case False @@ -3786,12 +3590,10 @@ proof (rule ccontr) assume "\ ?thesis" then have "f integrable_on cbox a b" - apply - unfolding integrable_on_def apply (rule_tac x="integral (cbox a b \ {x. x \ k \ c}) f + integral (cbox a b \ {x. x \ k \ c}) f" in exI) apply (rule has_integral_split[OF _ _ k]) - apply (rule_tac[!] integrable_integral) - apply auto + apply (auto intro: integrable_integral) done then show False using False by auto @@ -3801,11 +3603,10 @@ qed next fix a b :: 'a - assume as: "content (cbox a b) = 0" + assume "content (cbox a b) = 0" then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0" - unfolding if_P[OF integrable_on_null[OF as]] - using has_integral_null_eq[OF as] - by auto + using has_integral_null_eq + by (auto simp: integrable_on_null) qed @@ -3845,15 +3646,14 @@ "\i\Basis. (\i\Basis. (if i = k then max (a \ k) c else a \ i) *\<^sub>R i) \ i \ b\i" "min (b \ k) c = c" "max (a \ k) c = c" using assms using less_imp_le by auto - show ?t1 + show ?t1 (*FIXME a horrible mess*) unfolding division_points_def interval_split[OF k, of a b] unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)] unfolding * - unfolding subset_eq - apply rule + apply (rule subsetI) unfolding mem_Collect_eq split_beta apply (erule bexE conjE)+ - apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms) + apply (simp add: ) apply (erule exE conjE)+ proof fix i l x @@ -3912,84 +3712,58 @@ lemma division_points_psubset: fixes a :: "'a::euclidean_space" assumes "d division_of (cbox a b)" - and "\i\Basis. a\i < b\i" "a\k < c" "c < b\k" - and "l \ d" - and "interval_lowerbound l\k = c \ interval_upperbound l\k = c" - and k: "k \ Basis" + and "\i\Basis. a\i < b\i" "a\k < c" "c < b\k" + and "l \ d" + and "interval_lowerbound l\k = c \ interval_upperbound l\k = c" + and k: "k \ Basis" shows "division_points (cbox a b \ {x. x\k \ c}) {l \ {x. x\k \ c} | l. l\d \ l \ {x. x\k \ c} \ {}} \ - division_points (cbox a b) d" (is "?D1 \ ?D") + division_points (cbox a b) d" (is "?D1 \ ?D") and "division_points (cbox a b \ {x. x\k \ c}) {l \ {x. x\k \ c} | l. l\d \ l \ {x. x\k \ c} \ {}} \ - division_points (cbox a b) d" (is "?D2 \ ?D") + division_points (cbox a b) d" (is "?D2 \ ?D") proof - have ab: "\i\Basis. a\i \ b\i" using assms(2) by (auto intro!:less_imp_le) guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this have uv: "\i\Basis. u\i \ v\i" "\i\Basis. a\i \ u\i \ v\i \ b\i" using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty - unfolding subset_eq - apply - - defer - apply (erule_tac x=u in ballE) - apply (erule_tac x=v in ballE) - unfolding mem_box + using subset_box(1) apply auto + apply blast+ done have *: "interval_upperbound (cbox a b \ {x. x \ k \ interval_upperbound l \ k}) \ k = interval_upperbound l \ k" - "interval_upperbound (cbox a b \ {x. x \ k \ interval_lowerbound l \ k}) \ k = interval_lowerbound l \ k" - unfolding interval_split[OF k] - apply (subst interval_bounds) - prefer 3 - apply (subst interval_bounds) - unfolding l interval_bounds[OF uv(1)] - using uv[rule_format,of k] ab k - apply auto - done + "interval_upperbound (cbox a b \ {x. x \ k \ interval_lowerbound l \ k}) \ k = interval_lowerbound l \ k" + unfolding l interval_split[OF k] interval_bounds[OF uv(1)] + using uv[rule_format, of k] ab k + by auto have "\x. x \ ?D - ?D1" - using assms(2-) + using assms(3-) + unfolding division_points_def interval_bounds[OF ab] apply - apply (erule disjE) - apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI) - defer - apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI) - unfolding division_points_def - unfolding interval_bounds[OF ab] - apply (auto simp add:*) - done - then show "?D1 \ ?D" - apply - - apply rule - apply (rule division_points_subset[OF assms(1-4)]) - using k - apply auto - done - + apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI, force simp add: *) + apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI, force simp add: *) + done + moreover have "?D1 \ ?D" + by (auto simp add: assms division_points_subset) + ultimately show "?D1 \ ?D" + by blast have *: "interval_lowerbound (cbox a b \ {x. x \ k \ interval_lowerbound l \ k}) \ k = interval_lowerbound l \ k" "interval_lowerbound (cbox a b \ {x. x \ k \ interval_upperbound l \ k}) \ k = interval_upperbound l \ k" - unfolding interval_split[OF k] - apply (subst interval_bounds) - prefer 3 - apply (subst interval_bounds) - unfolding l interval_bounds[OF uv(1)] - using uv[rule_format,of k] ab k - apply auto - done + unfolding l interval_split[OF k] interval_bounds[OF uv(1)] + using uv[rule_format, of k] ab k + by auto have "\x. x \ ?D - ?D2" - using assms(2-) + using assms(3-) + unfolding division_points_def interval_bounds[OF ab] apply - apply (erule disjE) - apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI) - defer - apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI) - unfolding division_points_def - unfolding interval_bounds[OF ab] - apply (auto simp add:*) - done - then show "?D2 \ ?D" - apply - - apply rule - apply (rule division_points_subset[OF assms(1-4) k]) - apply auto - done + apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI, force simp add: *) + apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI, force simp add: *) + done + moreover have "?D2 \ ?D" + by (auto simp add: assms division_points_subset) + ultimately show "?D2 \ ?D" + by blast qed @@ -4003,57 +3777,30 @@ lemma iterate_expand_cases: "iterate opp s f = (if finite(support opp f s) then iterate opp (support opp f s) f else neutral opp)" - apply cases - apply (subst if_P, assumption) - unfolding iterate_def support_support fold'_def - apply auto - done + by (simp add: iterate_def fold'_def) lemma iterate_image: assumes "monoidal opp" - and "inj_on f s" - shows "iterate opp (f ` s) g = iterate opp s (g \ f)" + and "inj_on f s" + shows "iterate opp (f ` s) g = iterate opp s (g \ f)" proof - have *: "\s. finite s \ \x\s. \y\s. f x = f y \ x = y \ iterate opp (f ` s) g = iterate opp s (g \ f)" proof - case goal1 then show ?case - proof (induct s) - case empty - then show ?case - using assms(1) by auto - next - case (insert x s) - show ?case - unfolding iterate_insert[OF assms(1) insert(1)] - unfolding if_not_P[OF insert(2)] - apply (subst insert(3)[symmetric]) - unfolding image_insert - defer - apply (subst iterate_insert[OF assms(1)]) - apply (rule finite_imageI insert)+ - apply (subst if_not_P) - unfolding image_iff o_def - using insert(2,4) - apply auto - done - qed + apply (induct s) + using assms(1) by auto qed show ?thesis apply (cases "finite (support opp g (f ` s))") - apply (subst (1) iterate_support[symmetric],subst (2) iterate_support[symmetric]) + prefer 2 + apply (metis finite_imageI iterate_expand_cases support_clauses(7)) + apply (subst (1) iterate_support[symmetric], subst (2) iterate_support[symmetric]) unfolding support_clauses apply (rule *) - apply (rule finite_imageD,assumption) - unfolding inj_on_def[symmetric] - apply (rule subset_inj_on[OF assms(2) support_subset])+ - apply (subst iterate_expand_cases) - unfolding support_clauses - apply (simp only: if_False) - apply (subst iterate_expand_cases) - apply (subst if_not_P) - apply auto + apply (meson assms(2) finite_imageD subset_inj_on support_subset) + apply (meson assms(2) inj_on_contraD rev_subsetD support_subset) done qed @@ -4069,51 +3816,32 @@ by auto have **: "support opp (g \ f) {x \ s. f x \ a} = support opp (g \ f) s" unfolding support_def using assms(3) by auto + have inj: "inj_on f (support opp (g \ f) {x \ s. f x \ a})" + apply (simp add: inj_on_def) + apply (metis (mono_tags, lifting) assms(4) comp_def mem_Collect_eq support_def) + done show ?thesis - unfolding * apply (subst iterate_support[symmetric]) - unfolding support_clauses - apply (subst iterate_image[OF assms(1)]) - defer - apply (subst(2) iterate_support[symmetric]) - apply (subst **) - unfolding inj_on_def - using assms(3,4) - unfolding support_def - apply auto + apply (simp add: * support_clauses iterate_image[OF assms(1) inj]) + apply (simp add: iterate_def **) done qed lemma iterate_eq_neutral: assumes "monoidal opp" - and "\x \ s. f x = neutral opp" - shows "iterate opp s f = neutral opp" -proof - - have *: "support opp f s = {}" + and "\x \ s. f x = neutral opp" + shows "iterate opp s f = neutral opp" +proof - + have [simp]: "support opp f s = {}" unfolding support_def using assms(2) by auto show ?thesis - apply (subst iterate_support[symmetric]) - unfolding * - using assms(1) - apply auto - done + by (subst iterate_support[symmetric]) simp qed lemma iterate_op: - assumes "monoidal opp" - and "finite s" - shows "iterate opp s (\x. opp (f x) (g x)) = opp (iterate opp s f) (iterate opp s g)" - using assms(2) -proof (induct s) - case empty - then show ?case - unfolding iterate_insert[OF assms(1)] using assms(1) by auto -next - case (insert x F) - show ?case - unfolding iterate_insert[OF assms(1) insert(1)] if_not_P[OF insert(2)] insert(3) - by (simp add: monoidal_ac[OF assms(1)]) -qed + "\monoidal opp; finite s\ + \ iterate opp s (\x. opp (f x) (g x)) = opp (iterate opp s f) (iterate opp s g)" +by (erule finite_induct) (auto simp: monoidal_ac(4) monoidal_ac(5)) lemma iterate_eq: assumes "monoidal opp" @@ -4126,36 +3854,21 @@ proof (cases "finite (support opp f s)") case False then show ?thesis - apply (subst iterate_expand_cases) - apply (subst(2) iterate_expand_cases) - unfolding * - apply auto - done + by (simp add: "*" iterate_expand_cases) next + case True def su \ "support opp f s" - case True note support_subset[of opp f s] + have fsu: "finite su" + using True by (simp add: su_def) + moreover + { assume "finite su" "su \ s" + then have "iterate opp su f = iterate opp su g" + by (induct su) (auto simp: assms) + } + ultimately have "iterate opp (support opp f s) f = iterate opp (support opp g s) g" + by (simp add: "*" su_def support_subset) then show ?thesis - apply - - apply (subst iterate_support[symmetric]) - apply (subst(2) iterate_support[symmetric]) - unfolding * - using True - unfolding su_def[symmetric] - proof (induct su) - case empty - show ?case by auto - next - case (insert x s) - show ?case - unfolding iterate_insert[OF assms(1) insert(1)] - unfolding if_not_P[OF insert(2)] - apply (subst insert(3)) - defer - apply (subst assms(2)[of x]) - using insert - apply auto - done - qed + by simp qed qed diff -r 2761a2249c83 -r abee0de69a89 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/NSA/StarDef.thy Sat Jun 13 22:44:22 2015 +0200 @@ -577,7 +577,7 @@ lemma Standard_mult: "\x \ Standard; y \ Standard\ \ x * y \ Standard" by (simp add: star_mult_def) -lemma Standard_divide: "\x \ Standard; y \ Standard\ \ divide x y \ Standard" +lemma Standard_divide: "\x \ Standard; y \ Standard\ \ x / y \ Standard" by (simp add: star_divide_def) lemma Standard_inverse: "x \ Standard \ inverse x \ Standard" @@ -855,9 +855,9 @@ instance star :: (semidom) semidom .. instance star :: (semidom_divide) semidom_divide proof - show "\b a :: 'a star. b \ 0 \ divide (a * b) b = a" + show "\b a :: 'a star. b \ 0 \ (a * b) div b = a" by transfer simp - show "\a :: 'a star. divide a 0 = 0" + show "\a :: 'a star. a div 0 = 0" by transfer simp qed instance star :: (semiring_div) semiring_div diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Nat.thy Sat Jun 13 22:44:22 2015 +0200 @@ -1881,12 +1881,12 @@ intro: order_trans[OF _ funpow_mono]) lemma mono_funpow: - fixes Q :: "('i \ 'a::{lattice, order_bot}) \ ('i \ 'a)" + fixes Q :: "'a::{lattice, order_bot} \ 'a" shows "mono Q \ mono (\i. (Q ^^ i) \)" by (auto intro!: funpow_decreasing simp: mono_def) lemma antimono_funpow: - fixes Q :: "('i \ 'a::{lattice, order_top}) \ ('i \ 'a)" + fixes Q :: "'a::{lattice, order_top} \ 'a" shows "mono Q \ antimono (\i. (Q ^^ i) \)" by (auto intro!: funpow_increasing simp: antimono_def) diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sat Jun 13 22:44:22 2015 +0200 @@ -6,206 +6,292 @@ imports Complex_Main begin -context semiring_div +context semidom_divide +begin + +lemma mult_cancel_right [simp]: + "a * c = b * c \ c = 0 \ a = b" +proof (cases "c = 0") + case True then show ?thesis by simp +next + case False + { assume "a * c = b * c" + then have "a * c div c = b * c div c" + by simp + with False have "a = b" + by simp + } then show ?thesis by auto +qed + +lemma mult_cancel_left [simp]: + "c * a = c * b \ c = 0 \ a = b" + using mult_cancel_right [of a c b] by (simp add: ac_simps) + +end + +context semidom_divide begin + +lemma div_self [simp]: + assumes "a \ 0" + shows "a div a = 1" + using assms nonzero_mult_divide_cancel_left [of a 1] by simp + +lemma dvd_div_mult_self [simp]: + "a dvd b \ b div a * a = b" + by (cases "a = 0") (auto elim: dvdE simp add: ac_simps) + +lemma dvd_mult_div_cancel [simp]: + "a dvd b \ a * (b div a) = b" + using dvd_div_mult_self [of a b] by (simp add: ac_simps) + +lemma div_mult_swap: + assumes "c dvd b" + shows "a * (b div c) = (a * b) div c" +proof (cases "c = 0") + case True then show ?thesis by simp +next + case False from assms obtain d where "b = c * d" .. + moreover from False have "a * divide (d * c) c = ((a * d) * c) div c" + by simp + ultimately show ?thesis by (simp add: ac_simps) +qed + +lemma dvd_div_mult: + assumes "c dvd b" + shows "b div c * a = (b * a) div c" + using assms div_mult_swap [of c b a] by (simp add: ac_simps) + + +text \Units: invertible elements in a ring\ abbreviation is_unit :: "'a \ bool" where - "is_unit x \ x dvd 1" + "is_unit a \ a dvd 1" + +lemma not_is_unit_0 [simp]: + "\ is_unit 0" + by simp + +lemma unit_imp_dvd [dest]: + "is_unit b \ b dvd a" + by (rule dvd_trans [of _ 1]) simp_all + +lemma unit_dvdE: + assumes "is_unit a" + obtains c where "a \ 0" and "b = a * c" +proof - + from assms have "a dvd b" by auto + then obtain c where "b = a * c" .. + moreover from assms have "a \ 0" by auto + ultimately show thesis using that by blast +qed + +lemma dvd_unit_imp_unit: + "a dvd b \ is_unit b \ is_unit a" + by (rule dvd_trans) -definition associated :: "'a \ 'a \ bool" -where - "associated x y \ x dvd y \ y dvd x" +lemma unit_div_1_unit [simp, intro]: + assumes "is_unit a" + shows "is_unit (1 div a)" +proof - + from assms have "1 = 1 div a * a" by simp + then show "is_unit (1 div a)" by (rule dvdI) +qed -definition ring_inv :: "'a \ 'a" -where - "ring_inv x = 1 div x" +lemma is_unitE [elim?]: + assumes "is_unit a" + obtains b where "a \ 0" and "b \ 0" + and "is_unit b" and "1 div a = b" and "1 div b = a" + and "a * b = 1" and "c div a = c * b" +proof (rule that) + def b \ "1 div a" + then show "1 div a = b" by simp + from b_def `is_unit a` show "is_unit b" by simp + from `is_unit a` and `is_unit b` show "a \ 0" and "b \ 0" by auto + from b_def `is_unit a` show "a * b = 1" by simp + then have "1 = a * b" .. + with b_def `b \ 0` show "1 div b = a" by simp + from `is_unit a` have "a dvd c" .. + then obtain d where "c = a * d" .. + with `a \ 0` `a * b = 1` show "c div a = c * b" + by (simp add: mult.assoc mult.left_commute [of a]) +qed lemma unit_prod [intro]: - "is_unit x \ is_unit y \ is_unit (x * y)" - by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono) - -lemma unit_ring_inv: - "is_unit y \ x div y = x * ring_inv y" - by (simp add: div_mult_swap ring_inv_def) - -lemma unit_ring_inv_ring_inv [simp]: - "is_unit x \ ring_inv (ring_inv x) = x" - unfolding ring_inv_def - by (metis div_mult_mult1_if div_mult_self1_is_id dvd_mult_div_cancel mult_1_right) + "is_unit a \ is_unit b \ is_unit (a * b)" + by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) + +lemma unit_div [intro]: + "is_unit a \ is_unit b \ is_unit (a div b)" + by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod) -lemma inv_imp_eq_ring_inv: - "a * b = 1 \ ring_inv a = b" - by (metis dvd_mult_div_cancel dvd_mult_right mult_1_right mult.left_commute one_dvd ring_inv_def) - -lemma ring_inv_is_inv1 [simp]: - "is_unit a \ a * ring_inv a = 1" - unfolding ring_inv_def by simp - -lemma ring_inv_is_inv2 [simp]: - "is_unit a \ ring_inv a * a = 1" - by (simp add: ac_simps) - -lemma unit_ring_inv_unit [simp, intro]: - assumes "is_unit x" - shows "is_unit (ring_inv x)" -proof - - from assms have "1 = ring_inv x * x" by simp - then show "is_unit (ring_inv x)" by (rule dvdI) +lemma mult_unit_dvd_iff: + assumes "is_unit b" + shows "a * b dvd c \ a dvd c" +proof + assume "a * b dvd c" + with assms show "a dvd c" + by (simp add: dvd_mult_left) +next + assume "a dvd c" + then obtain k where "c = a * k" .. + with assms have "c = (a * b) * (1 div b * k)" + by (simp add: mult_ac) + then show "a * b dvd c" by (rule dvdI) qed -lemma mult_unit_dvd_iff: - "is_unit y \ x * y dvd z \ x dvd z" +lemma dvd_mult_unit_iff: + assumes "is_unit b" + shows "a dvd c * b \ a dvd c" proof - assume "is_unit y" "x * y dvd z" - then show "x dvd z" by (simp add: dvd_mult_left) + assume "a dvd c * b" + with assms have "c * b dvd c * (b * (1 div b))" + by (subst mult_assoc [symmetric]) simp + also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp + finally have "c * b dvd c" by simp + with `a dvd c * b` show "a dvd c" by (rule dvd_trans) next - assume "is_unit y" "x dvd z" - then obtain k where "z = x * k" unfolding dvd_def by blast - with `is_unit y` have "z = (x * y) * (ring_inv y * k)" - by (simp add: mult_ac) - then show "x * y dvd z" by (rule dvdI) + assume "a dvd c" + then show "a dvd c * b" by simp qed lemma div_unit_dvd_iff: - "is_unit y \ x div y dvd z \ x dvd z" - by (subst unit_ring_inv) (assumption, simp add: mult_unit_dvd_iff) - -lemma dvd_mult_unit_iff: - "is_unit y \ x dvd z * y \ x dvd z" -proof - assume "is_unit y" and "x dvd z * y" - have "z * y dvd z * (y * ring_inv y)" by (subst mult_assoc [symmetric]) simp - also from `is_unit y` have "y * ring_inv y = 1" by simp - finally have "z * y dvd z" by simp - with `x dvd z * y` show "x dvd z" by (rule dvd_trans) -next - assume "x dvd z" - then show "x dvd z * y" by simp -qed + "is_unit b \ a div b dvd c \ a dvd c" + by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff) lemma dvd_div_unit_iff: - "is_unit y \ x dvd z div y \ x dvd z" - by (subst unit_ring_inv) (assumption, simp add: dvd_mult_unit_iff) + "is_unit b \ a dvd c div b \ a dvd c" + by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff) + +lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff + dvd_mult_unit_iff dvd_div_unit_iff -- \FIXME consider fact collection\ -lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff dvd_div_unit_iff +lemma unit_mult_div_div [simp]: + "is_unit a \ b * (1 div a) = b div a" + by (erule is_unitE [of _ b]) simp -lemma unit_div [intro]: - "is_unit x \ is_unit y \ is_unit (x div y)" - by (subst unit_ring_inv) (assumption, rule unit_prod, simp_all) +lemma unit_div_mult_self [simp]: + "is_unit a \ b div a * a = b" + by (rule dvd_div_mult_self) auto + +lemma unit_div_1_div_1 [simp]: + "is_unit a \ 1 div (1 div a) = a" + by (erule is_unitE) simp lemma unit_div_mult_swap: - "is_unit z \ x * (y div z) = x * y div z" - by (simp only: unit_ring_inv [of _ y] unit_ring_inv [of _ "x*y"] ac_simps) + "is_unit c \ a * (b div c) = (a * b) div c" + by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c]) lemma unit_div_commute: - "is_unit y \ x div y * z = x * z div y" - by (simp only: unit_ring_inv [of _ x] unit_ring_inv [of _ "x*z"] ac_simps) + "is_unit b \ (a div b) * c = (a * c) div b" + using unit_div_mult_swap [of b c a] by (simp add: ac_simps) + +lemma unit_eq_div1: + "is_unit b \ a div b = c \ a = c * b" + by (auto elim: is_unitE) -lemma unit_imp_dvd [dest]: - "is_unit y \ y dvd x" - by (rule dvd_trans [of _ 1]) simp_all +lemma unit_eq_div2: + "is_unit b \ a = c div b \ a * b = c" + using unit_eq_div1 [of b c a] by auto + +lemma unit_mult_left_cancel: + assumes "is_unit a" + shows "a * b = a * c \ b = c" (is "?P \ ?Q") + using assms mult_cancel_left [of a b c] by auto -lemma dvd_unit_imp_unit: - "is_unit y \ x dvd y \ is_unit x" - by (rule dvd_trans) +lemma unit_mult_right_cancel: + "is_unit a \ b * a = c * a \ b = c" + using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps) -lemma ring_inv_0 [simp]: - "ring_inv 0 = 0" - unfolding ring_inv_def by simp +lemma unit_div_cancel: + assumes "is_unit a" + shows "b div a = c div a \ b = c" +proof - + from assms have "is_unit (1 div a)" by simp + then have "b * (1 div a) = c * (1 div a) \ b = c" + by (rule unit_mult_right_cancel) + with assms show ?thesis by simp +qed + + +text \Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \ -lemma unit_ring_inv'1: - assumes "is_unit y" - shows "x div (y * z) = x * ring_inv y div z" -proof - - from assms have "x div (y * z) = x * (ring_inv y * y) div (y * z)" - by simp - also have "... = y * (x * ring_inv y) div (y * z)" - by (simp only: mult_ac) - also have "... = x * ring_inv y div z" - by (cases "y = 0", simp, rule div_mult_mult1) - finally show ?thesis . +definition associated :: "'a \ 'a \ bool" +where + "associated a b \ a dvd b \ b dvd a" + +lemma associatedI: + "a dvd b \ b dvd a \ associated a b" + by (simp add: associated_def) + +lemma associatedD1: + "associated a b \ a dvd b" + by (simp add: associated_def) + +lemma associatedD2: + "associated a b \ b dvd a" + by (simp add: associated_def) + +lemma associated_refl [simp]: + "associated a a" + by (auto intro: associatedI) + +lemma associated_sym: + "associated b a \ associated a b" + by (auto intro: associatedI dest: associatedD1 associatedD2) + +lemma associated_trans: + "associated a b \ associated b c \ associated a c" + by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2) + +lemma equivp_associated: + "equivp associated" +proof (rule equivpI) + show "reflp associated" + by (rule reflpI) simp + show "symp associated" + by (rule sympI) (simp add: associated_sym) + show "transp associated" + by (rule transpI) (fact associated_trans) qed -lemma associated_comm: - "associated x y \ associated y x" - by (simp add: associated_def) - lemma associated_0 [simp]: "associated 0 b \ b = 0" "associated a 0 \ a = 0" - unfolding associated_def by simp_all + by (auto dest: associatedD1 associatedD2) lemma associated_unit: - "is_unit x \ associated x y \ is_unit y" - unfolding associated_def using dvd_unit_imp_unit by auto - -lemma is_unit_1 [simp]: - "is_unit 1" - by simp + "associated a b \ is_unit a \ is_unit b" + using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2) -lemma not_is_unit_0 [simp]: - "\ is_unit 0" - by auto - -lemma unit_mult_left_cancel: - assumes "is_unit x" - shows "(x * y) = (x * z) \ y = z" -proof - - from assms have "x \ 0" by auto - then show ?thesis by (metis div_mult_self1_is_id) +lemma is_unit_associatedI: + assumes "is_unit c" and "a = c * b" + shows "associated a b" +proof (rule associatedI) + from `a = c * b` show "b dvd a" by auto + from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE) + moreover from `a = c * b` have "d * a = d * (c * b)" by simp + ultimately have "b = a * d" by (simp add: ac_simps) + then show "a dvd b" .. qed -lemma unit_mult_right_cancel: - "is_unit x \ (y * x) = (z * x) \ y = z" - by (simp add: ac_simps unit_mult_left_cancel) - -lemma unit_div_cancel: - "is_unit x \ (y div x) = (z div x) \ y = z" - apply (subst unit_ring_inv[of _ y], assumption) - apply (subst unit_ring_inv[of _ z], assumption) - apply (rule unit_mult_right_cancel, erule unit_ring_inv_unit) - done - -lemma unit_eq_div1: - "is_unit y \ x div y = z \ x = z * y" - apply (subst unit_ring_inv, assumption) - apply (subst unit_mult_right_cancel[symmetric], assumption) - apply (subst mult_assoc, subst ring_inv_is_inv2, assumption, simp) - done - -lemma unit_eq_div2: - "is_unit y \ x = z div y \ x * y = z" - by (subst (1 2) eq_commute, simp add: unit_eq_div1, subst eq_commute, rule refl) - -lemma associated_iff_div_unit: - "associated x y \ (\z. is_unit z \ x = z * y)" -proof - assume "associated x y" - show "\z. is_unit z \ x = z * y" - proof (cases "x = 0") - assume "x = 0" - then show "\z. is_unit z \ x = z * y" using `associated x y` - by (intro exI[of _ 1], simp add: associated_def) - next - assume [simp]: "x \ 0" - hence [simp]: "x dvd y" "y dvd x" using `associated x y` - unfolding associated_def by simp_all - hence "1 = x div y * (y div x)" - by (simp add: div_mult_swap) - hence "is_unit (x div y)" .. - moreover have "x = (x div y) * y" by simp - ultimately show ?thesis by blast - qed +lemma associated_is_unitE: + assumes "associated a b" + obtains c where "is_unit c" and "a = c * b" +proof (cases "b = 0") + case True with assms have "is_unit 1" and "a = 1 * b" by simp_all + with that show thesis . next - assume "\z. is_unit z \ x = z * y" - then obtain z where "is_unit z" and "x = z * y" by blast - hence "y = x * ring_inv z" by (simp add: algebra_simps) - hence "x dvd y" by simp - moreover from `x = z * y` have "y dvd x" by simp - ultimately show "associated x y" unfolding associated_def by simp + case False + from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2) + then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE) + then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps) + with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp + then have "is_unit c" by auto + with `a = c * b` that show thesis by blast qed - + lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff dvd_div_unit_iff unit_div_mult_swap unit_div_commute unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel @@ -213,27 +299,11 @@ end -context ring_div -begin - -lemma is_unit_neg [simp]: - "is_unit (- x) \ is_unit x" - by simp - -lemma is_unit_neg_1 [simp]: - "is_unit (-1)" - by simp - -end - -lemma is_unit_nat [simp]: - "is_unit (x::nat) \ x = 1" - by simp - lemma is_unit_int: - "is_unit (x::int) \ x = 1 \ x = -1" + "is_unit (k::int) \ k = 1 \ k = - 1" by auto + text {* A Euclidean semiring is a semiring upon which the Euclidean algorithm can be implemented. It must provide: @@ -241,100 +311,103 @@ \item division with remainder \item a size function such that @{term "size (a mod b) < size b"} for any @{term "b \ 0"} - \item a normalisation factor such that two associated numbers are equal iff - they are the same when divided by their normalisation factors. + \item a normalization factor such that two associated numbers are equal iff + they are the same when divd by their normalization factors. \end{itemize} The existence of these functions makes it possible to derive gcd and lcm functions for any Euclidean semiring. *} class euclidean_semiring = semiring_div + fixes euclidean_size :: "'a \ nat" - fixes normalisation_factor :: "'a \ 'a" + fixes normalization_factor :: "'a \ 'a" assumes mod_size_less [simp]: "b \ 0 \ euclidean_size (a mod b) < euclidean_size b" assumes size_mult_mono: "b \ 0 \ euclidean_size (a * b) \ euclidean_size a" - assumes normalisation_factor_is_unit [intro,simp]: - "a \ 0 \ is_unit (normalisation_factor a)" - assumes normalisation_factor_mult: "normalisation_factor (a * b) = - normalisation_factor a * normalisation_factor b" - assumes normalisation_factor_unit: "is_unit x \ normalisation_factor x = x" - assumes normalisation_factor_0 [simp]: "normalisation_factor 0 = 0" + assumes normalization_factor_is_unit [intro,simp]: + "a \ 0 \ is_unit (normalization_factor a)" + assumes normalization_factor_mult: "normalization_factor (a * b) = + normalization_factor a * normalization_factor b" + assumes normalization_factor_unit: "is_unit a \ normalization_factor a = a" + assumes normalization_factor_0 [simp]: "normalization_factor 0 = 0" begin -lemma normalisation_factor_dvd [simp]: - "a \ 0 \ normalisation_factor a dvd b" +lemma normalization_factor_dvd [simp]: + "a \ 0 \ normalization_factor a dvd b" by (rule unit_imp_dvd, simp) -lemma normalisation_factor_1 [simp]: - "normalisation_factor 1 = 1" - by (simp add: normalisation_factor_unit) +lemma normalization_factor_1 [simp]: + "normalization_factor 1 = 1" + by (simp add: normalization_factor_unit) -lemma normalisation_factor_0_iff [simp]: - "normalisation_factor x = 0 \ x = 0" +lemma normalization_factor_0_iff [simp]: + "normalization_factor a = 0 \ a = 0" proof - assume "normalisation_factor x = 0" - hence "\ is_unit (normalisation_factor x)" - by (metis not_is_unit_0) - then show "x = 0" by force -next - assume "x = 0" - then show "normalisation_factor x = 0" by simp + assume "normalization_factor a = 0" + hence "\ is_unit (normalization_factor a)" + by simp + then show "a = 0" by auto +qed simp + +lemma normalization_factor_pow: + "normalization_factor (a ^ n) = normalization_factor a ^ n" + by (induct n) (simp_all add: normalization_factor_mult power_Suc2) + +lemma normalization_correct [simp]: + "normalization_factor (a div normalization_factor a) = (if a = 0 then 0 else 1)" +proof (cases "a = 0", simp) + assume "a \ 0" + let ?nf = "normalization_factor" + from normalization_factor_is_unit[OF `a \ 0`] have "?nf a \ 0" + by auto + have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)" + by (simp add: normalization_factor_mult) + also have "a div ?nf a * ?nf a = a" using `a \ 0` + by simp + also have "?nf (?nf a) = ?nf a" using `a \ 0` + normalization_factor_is_unit normalization_factor_unit by simp + finally have "normalization_factor (a div normalization_factor a) = 1" + using `?nf a \ 0` by (metis div_mult_self2_is_id div_self) + with `a \ 0` show ?thesis by simp qed -lemma normalisation_factor_pow: - "normalisation_factor (x ^ n) = normalisation_factor x ^ n" - by (induct n) (simp_all add: normalisation_factor_mult power_Suc2) +lemma normalization_0_iff [simp]: + "a div normalization_factor a = 0 \ a = 0" + by (cases "a = 0", simp, subst unit_eq_div1, blast, simp) -lemma normalisation_correct [simp]: - "normalisation_factor (x div normalisation_factor x) = (if x = 0 then 0 else 1)" -proof (cases "x = 0", simp) - assume "x \ 0" - let ?nf = "normalisation_factor" - from normalisation_factor_is_unit[OF `x \ 0`] have "?nf x \ 0" - by (metis not_is_unit_0) - have "?nf (x div ?nf x) * ?nf (?nf x) = ?nf (x div ?nf x * ?nf x)" - by (simp add: normalisation_factor_mult) - also have "x div ?nf x * ?nf x = x" using `x \ 0` - by simp - also have "?nf (?nf x) = ?nf x" using `x \ 0` - normalisation_factor_is_unit normalisation_factor_unit by simp - finally show ?thesis using `x \ 0` and `?nf x \ 0` - by (metis div_mult_self2_is_id div_self) -qed - -lemma normalisation_0_iff [simp]: - "x div normalisation_factor x = 0 \ x = 0" - by (cases "x = 0", simp, subst unit_eq_div1, blast, simp) +lemma mult_div_normalization [simp]: + "b * (1 div normalization_factor a) = b div normalization_factor a" + by (cases "a = 0") simp_all lemma associated_iff_normed_eq: - "associated a b \ a div normalisation_factor a = b div normalisation_factor b" -proof (cases "b = 0", simp, cases "a = 0", metis associated_0(1) normalisation_0_iff, rule iffI) - let ?nf = normalisation_factor + "associated a b \ a div normalization_factor a = b div normalization_factor b" +proof (cases "b = 0", simp, cases "a = 0", metis associated_0(1) normalization_0_iff, rule iffI) + let ?nf = normalization_factor assume "a \ 0" "b \ 0" "a div ?nf a = b div ?nf b" hence "a = b * (?nf a div ?nf b)" apply (subst (asm) unit_eq_div1, blast, subst (asm) unit_div_commute, blast) apply (subst div_mult_swap, simp, simp) done - with `a \ 0` `b \ 0` have "\z. is_unit z \ a = z * b" + with `a \ 0` `b \ 0` have "\c. is_unit c \ a = c * b" by (intro exI[of _ "?nf a div ?nf b"], force simp: mult_ac) - with associated_iff_div_unit show "associated a b" by simp + then obtain c where "is_unit c" and "a = c * b" by blast + then show "associated a b" by (rule is_unit_associatedI) next - let ?nf = normalisation_factor + let ?nf = normalization_factor assume "a \ 0" "b \ 0" "associated a b" - with associated_iff_div_unit obtain z where "is_unit z" and "a = z * b" by blast + then obtain c where "is_unit c" and "a = c * b" by (blast elim: associated_is_unitE) then show "a div ?nf a = b div ?nf b" - apply (simp only: `a = z * b` normalisation_factor_mult normalisation_factor_unit) + apply (simp only: `a = c * b` normalization_factor_mult normalization_factor_unit) apply (rule div_mult_mult1, force) done qed lemma normed_associated_imp_eq: - "associated a b \ normalisation_factor a \ {0, 1} \ normalisation_factor b \ {0, 1} \ a = b" + "associated a b \ normalization_factor a \ {0, 1} \ normalization_factor b \ {0, 1} \ a = b" by (simp add: associated_iff_normed_eq, elim disjE, simp_all) -lemmas normalisation_factor_dvd_iff [simp] = - unit_dvd_iff [OF normalisation_factor_is_unit] +lemmas normalization_factor_dvd_iff [simp] = + unit_dvd_iff [OF normalization_factor_is_unit] lemma euclidean_division: fixes a :: 'a and b :: 'a @@ -364,7 +437,7 @@ function gcd_eucl :: "'a \ 'a \ 'a" where - "gcd_eucl a b = (if b = 0 then a div normalisation_factor a else gcd_eucl b (a mod b))" + "gcd_eucl a b = (if b = 0 then a div normalization_factor a else gcd_eucl b (a mod b))" by (pat_completeness, simp) termination by (relation "measure (euclidean_size \ snd)", simp_all) @@ -378,17 +451,17 @@ definition lcm_eucl :: "'a \ 'a \ 'a" where - "lcm_eucl a b = a * b div (gcd_eucl a b * normalisation_factor (a * b))" + "lcm_eucl a b = a * b div (gcd_eucl a b * normalization_factor (a * b))" (* Somewhat complicated definition of Lcm that has the advantage of working for infinite sets as well *) definition Lcm_eucl :: "'a set \ 'a" where - "Lcm_eucl A = (if \l. l \ 0 \ (\x\A. x dvd l) then - let l = SOME l. l \ 0 \ (\x\A. x dvd l) \ euclidean_size l = - (LEAST n. \l. l \ 0 \ (\x\A. x dvd l) \ euclidean_size l = n) - in l div normalisation_factor l + "Lcm_eucl A = (if \l. l \ 0 \ (\a\A. a dvd l) then + let l = SOME l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = + (LEAST n. \l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n) + in l div normalization_factor l else 0)" definition Gcd_eucl :: "'a set \ 'a" @@ -403,37 +476,37 @@ begin lemma gcd_red: - "gcd x y = gcd y (x mod y)" + "gcd a b = gcd b (a mod b)" by (metis gcd_eucl.simps mod_0 mod_by_0 gcd_gcd_eucl) lemma gcd_non_0: - "y \ 0 \ gcd x y = gcd y (x mod y)" + "b \ 0 \ gcd a b = gcd b (a mod b)" by (rule gcd_red) lemma gcd_0_left: - "gcd 0 x = x div normalisation_factor x" + "gcd 0 a = a div normalization_factor a" by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, subst gcd_eucl.simps, simp add: Let_def) lemma gcd_0: - "gcd x 0 = x div normalisation_factor x" + "gcd a 0 = a div normalization_factor a" by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, simp add: Let_def) -lemma gcd_dvd1 [iff]: "gcd x y dvd x" - and gcd_dvd2 [iff]: "gcd x y dvd y" -proof (induct x y rule: gcd_eucl.induct) - fix x y :: 'a - assume IH1: "y \ 0 \ gcd y (x mod y) dvd y" - assume IH2: "y \ 0 \ gcd y (x mod y) dvd (x mod y)" +lemma gcd_dvd1 [iff]: "gcd a b dvd a" + and gcd_dvd2 [iff]: "gcd a b dvd b" +proof (induct a b rule: gcd_eucl.induct) + fix a b :: 'a + assume IH1: "b \ 0 \ gcd b (a mod b) dvd b" + assume IH2: "b \ 0 \ gcd b (a mod b) dvd (a mod b)" - have "gcd x y dvd x \ gcd x y dvd y" - proof (cases "y = 0") + have "gcd a b dvd a \ gcd a b dvd b" + proof (cases "b = 0") case True - then show ?thesis by (cases "x = 0", simp_all add: gcd_0) + then show ?thesis by (cases "a = 0", simp_all add: gcd_0) next case False with IH1 and IH2 show ?thesis by (simp add: gcd_non_0 dvd_mod_iff) qed - then show "gcd x y dvd x" "gcd x y dvd y" by simp_all + then show "gcd a b dvd a" "gcd a b dvd b" by simp_all qed lemma dvd_gcd_D1: "k dvd gcd m n \ k dvd m" @@ -443,147 +516,147 @@ by (rule dvd_trans, assumption, rule gcd_dvd2) lemma gcd_greatest: - fixes k x y :: 'a - shows "k dvd x \ k dvd y \ k dvd gcd x y" -proof (induct x y rule: gcd_eucl.induct) - case (1 x y) + fixes k a b :: 'a + shows "k dvd a \ k dvd b \ k dvd gcd a b" +proof (induct a b rule: gcd_eucl.induct) + case (1 a b) show ?case - proof (cases "y = 0") - assume "y = 0" - with 1 show ?thesis by (cases "x = 0", simp_all add: gcd_0) + proof (cases "b = 0") + assume "b = 0" + with 1 show ?thesis by (cases "a = 0", simp_all add: gcd_0) next - assume "y \ 0" + assume "b \ 0" with 1 show ?thesis by (simp add: gcd_non_0 dvd_mod_iff) qed qed lemma dvd_gcd_iff: - "k dvd gcd x y \ k dvd x \ k dvd y" + "k dvd gcd a b \ k dvd a \ k dvd b" by (blast intro!: gcd_greatest intro: dvd_trans) lemmas gcd_greatest_iff = dvd_gcd_iff lemma gcd_zero [simp]: - "gcd x y = 0 \ x = 0 \ y = 0" + "gcd a b = 0 \ a = 0 \ b = 0" by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+ -lemma normalisation_factor_gcd [simp]: - "normalisation_factor (gcd x y) = (if x = 0 \ y = 0 then 0 else 1)" (is "?f x y = ?g x y") -proof (induct x y rule: gcd_eucl.induct) - fix x y :: 'a - assume IH: "y \ 0 \ ?f y (x mod y) = ?g y (x mod y)" - then show "?f x y = ?g x y" by (cases "y = 0", auto simp: gcd_non_0 gcd_0) +lemma normalization_factor_gcd [simp]: + "normalization_factor (gcd a b) = (if a = 0 \ b = 0 then 0 else 1)" (is "?f a b = ?g a b") +proof (induct a b rule: gcd_eucl.induct) + fix a b :: 'a + assume IH: "b \ 0 \ ?f b (a mod b) = ?g b (a mod b)" + then show "?f a b = ?g a b" by (cases "b = 0", auto simp: gcd_non_0 gcd_0) qed lemma gcdI: - "k dvd x \ k dvd y \ (\l. l dvd x \ l dvd y \ l dvd k) - \ normalisation_factor k = (if k = 0 then 0 else 1) \ k = gcd x y" + "k dvd a \ k dvd b \ (\l. l dvd a \ l dvd b \ l dvd k) + \ normalization_factor k = (if k = 0 then 0 else 1) \ k = gcd a b" by (intro normed_associated_imp_eq) (auto simp: associated_def intro: gcd_greatest) sublocale gcd!: abel_semigroup gcd proof - fix x y z - show "gcd (gcd x y) z = gcd x (gcd y z)" + fix a b c + show "gcd (gcd a b) c = gcd a (gcd b c)" proof (rule gcdI) - have "gcd (gcd x y) z dvd gcd x y" "gcd x y dvd x" by simp_all - then show "gcd (gcd x y) z dvd x" by (rule dvd_trans) - have "gcd (gcd x y) z dvd gcd x y" "gcd x y dvd y" by simp_all - hence "gcd (gcd x y) z dvd y" by (rule dvd_trans) - moreover have "gcd (gcd x y) z dvd z" by simp - ultimately show "gcd (gcd x y) z dvd gcd y z" + have "gcd (gcd a b) c dvd gcd a b" "gcd a b dvd a" by simp_all + then show "gcd (gcd a b) c dvd a" by (rule dvd_trans) + have "gcd (gcd a b) c dvd gcd a b" "gcd a b dvd b" by simp_all + hence "gcd (gcd a b) c dvd b" by (rule dvd_trans) + moreover have "gcd (gcd a b) c dvd c" by simp + ultimately show "gcd (gcd a b) c dvd gcd b c" by (rule gcd_greatest) - show "normalisation_factor (gcd (gcd x y) z) = (if gcd (gcd x y) z = 0 then 0 else 1)" + show "normalization_factor (gcd (gcd a b) c) = (if gcd (gcd a b) c = 0 then 0 else 1)" by auto - fix l assume "l dvd x" and "l dvd gcd y z" + fix l assume "l dvd a" and "l dvd gcd b c" with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2] - have "l dvd y" and "l dvd z" by blast+ - with `l dvd x` show "l dvd gcd (gcd x y) z" + have "l dvd b" and "l dvd c" by blast+ + with `l dvd a` show "l dvd gcd (gcd a b) c" by (intro gcd_greatest) qed next - fix x y - show "gcd x y = gcd y x" + fix a b + show "gcd a b = gcd b a" by (rule gcdI) (simp_all add: gcd_greatest) qed lemma gcd_unique: "d dvd a \ d dvd b \ - normalisation_factor d = (if d = 0 then 0 else 1) \ + normalization_factor d = (if d = 0 then 0 else 1) \ (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" by (rule, auto intro: gcdI simp: gcd_greatest) lemma gcd_dvd_prod: "gcd a b dvd k * b" using mult_dvd_mono [of 1] by auto -lemma gcd_1_left [simp]: "gcd 1 x = 1" +lemma gcd_1_left [simp]: "gcd 1 a = 1" by (rule sym, rule gcdI, simp_all) -lemma gcd_1 [simp]: "gcd x 1 = 1" +lemma gcd_1 [simp]: "gcd a 1 = 1" by (rule sym, rule gcdI, simp_all) lemma gcd_proj2_if_dvd: - "y dvd x \ gcd x y = y div normalisation_factor y" - by (cases "y = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0 gcd_0) + "b dvd a \ gcd a b = b div normalization_factor b" + by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0 gcd_0) lemma gcd_proj1_if_dvd: - "x dvd y \ gcd x y = x div normalisation_factor x" + "a dvd b \ gcd a b = a div normalization_factor a" by (subst gcd.commute, simp add: gcd_proj2_if_dvd) -lemma gcd_proj1_iff: "gcd m n = m div normalisation_factor m \ m dvd n" +lemma gcd_proj1_iff: "gcd m n = m div normalization_factor m \ m dvd n" proof - assume A: "gcd m n = m div normalisation_factor m" + assume A: "gcd m n = m div normalization_factor m" show "m dvd n" proof (cases "m = 0") assume [simp]: "m \ 0" - from A have B: "m = gcd m n * normalisation_factor m" + from A have B: "m = gcd m n * normalization_factor m" by (simp add: unit_eq_div2) show ?thesis by (subst B, simp add: mult_unit_dvd_iff) qed (insert A, simp) next assume "m dvd n" - then show "gcd m n = m div normalisation_factor m" by (rule gcd_proj1_if_dvd) + then show "gcd m n = m div normalization_factor m" by (rule gcd_proj1_if_dvd) qed -lemma gcd_proj2_iff: "gcd m n = n div normalisation_factor n \ n dvd m" +lemma gcd_proj2_iff: "gcd m n = n div normalization_factor n \ n dvd m" by (subst gcd.commute, simp add: gcd_proj1_iff) lemma gcd_mod1 [simp]: - "gcd (x mod y) y = gcd x y" + "gcd (a mod b) b = gcd a b" by (rule gcdI, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) lemma gcd_mod2 [simp]: - "gcd x (y mod x) = gcd x y" + "gcd a (b mod a) = gcd a b" by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) -lemma normalisation_factor_dvd' [simp]: - "normalisation_factor x dvd x" - by (cases "x = 0", simp_all) +lemma normalization_factor_dvd' [simp]: + "normalization_factor a dvd a" + by (cases "a = 0", simp_all) lemma gcd_mult_distrib': - "k div normalisation_factor k * gcd x y = gcd (k*x) (k*y)" -proof (induct x y rule: gcd_eucl.induct) - case (1 x y) + "k div normalization_factor k * gcd a b = gcd (k*a) (k*b)" +proof (induct a b rule: gcd_eucl.induct) + case (1 a b) show ?case - proof (cases "y = 0") + proof (cases "b = 0") case True - then show ?thesis by (simp add: normalisation_factor_mult gcd_0 algebra_simps div_mult_div_if_dvd) + then show ?thesis by (simp add: normalization_factor_mult gcd_0 algebra_simps div_mult_div_if_dvd) next case False - hence "k div normalisation_factor k * gcd x y = gcd (k * y) (k * (x mod y))" + hence "k div normalization_factor k * gcd a b = gcd (k * b) (k * (a mod b))" using 1 by (subst gcd_red, simp) - also have "... = gcd (k * x) (k * y)" + also have "... = gcd (k * a) (k * b)" by (simp add: mult_mod_right gcd.commute) finally show ?thesis . qed qed lemma gcd_mult_distrib: - "k * gcd x y = gcd (k*x) (k*y) * normalisation_factor k" + "k * gcd a b = gcd (k*a) (k*b) * normalization_factor k" proof- - let ?nf = "normalisation_factor" + let ?nf = "normalization_factor" from gcd_mult_distrib' - have "gcd (k*x) (k*y) = k div ?nf k * gcd x y" .. - also have "... = k * gcd x y div ?nf k" - by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalisation_factor_dvd) + have "gcd (k*a) (k*b) = k div ?nf k * gcd a b" .. + also have "... = k * gcd a b div ?nf k" + by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalization_factor_dvd) finally show ?thesis by simp qed @@ -618,27 +691,27 @@ shows "euclidean_size (gcd a b) < euclidean_size b" using assms by (subst gcd.commute, rule euclidean_size_gcd_less1) -lemma gcd_mult_unit1: "is_unit a \ gcd (x*a) y = gcd x y" +lemma gcd_mult_unit1: "is_unit a \ gcd (b * a) c = gcd b c" apply (rule gcdI) apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps) apply (rule gcd_dvd2) apply (rule gcd_greatest, simp add: unit_simps, assumption) - apply (subst normalisation_factor_gcd, simp add: gcd_0) + apply (subst normalization_factor_gcd, simp add: gcd_0) done -lemma gcd_mult_unit2: "is_unit a \ gcd x (y*a) = gcd x y" +lemma gcd_mult_unit2: "is_unit a \ gcd b (c * a) = gcd b c" by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute) -lemma gcd_div_unit1: "is_unit a \ gcd (x div a) y = gcd x y" - by (simp add: unit_ring_inv gcd_mult_unit1) +lemma gcd_div_unit1: "is_unit a \ gcd (b div a) c = gcd b c" + by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1) -lemma gcd_div_unit2: "is_unit a \ gcd x (y div a) = gcd x y" - by (simp add: unit_ring_inv gcd_mult_unit2) +lemma gcd_div_unit2: "is_unit a \ gcd b (c div a) = gcd b c" + by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2) -lemma gcd_idem: "gcd x x = x div normalisation_factor x" - by (cases "x = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all) +lemma gcd_idem: "gcd a a = a div normalization_factor a" + by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all) -lemma gcd_right_idem: "gcd (gcd p q) q = gcd p q" +lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b" apply (rule gcdI) apply (simp add: ac_simps) apply (rule gcd_dvd2) @@ -646,7 +719,7 @@ apply simp done -lemma gcd_left_idem: "gcd p (gcd p q) = gcd p q" +lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b" apply (rule gcdI) apply simp apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2) @@ -664,17 +737,17 @@ qed lemma coprime_dvd_mult: - assumes "gcd k n = 1" and "k dvd m * n" - shows "k dvd m" + assumes "gcd c b = 1" and "c dvd a * b" + shows "c dvd a" proof - - let ?nf = "normalisation_factor" - from assms gcd_mult_distrib [of m k n] - have A: "m = gcd (m * k) (m * n) * ?nf m" by simp - from `k dvd m * n` show ?thesis by (subst A, simp_all add: gcd_greatest) + let ?nf = "normalization_factor" + from assms gcd_mult_distrib [of a c b] + have A: "a = gcd (a * c) (a * b) * ?nf a" by simp + from `c dvd a * b` show ?thesis by (subst A, simp_all add: gcd_greatest) qed lemma coprime_dvd_mult_iff: - "gcd k n = 1 \ (k dvd m * n) = (k dvd m)" + "gcd c b = 1 \ (c dvd a * b) = (c dvd a)" by (rule, rule coprime_dvd_mult, simp_all) lemma gcd_dvd_antisym: @@ -685,7 +758,7 @@ with A show "gcd a b dvd c" by (rule dvd_trans) have "gcd c d dvd d" by simp with A show "gcd a b dvd d" by (rule dvd_trans) - show "normalisation_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)" + show "normalization_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)" by simp fix l assume "l dvd c" and "l dvd d" hence "l dvd gcd c d" by (rule gcd_greatest) @@ -737,7 +810,7 @@ lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n" by (subst gcd.commute, subst gcd_red, simp) -lemma coprimeI: "(\l. \l dvd x; l dvd y\ \ l dvd 1) \ gcd x y = 1" +lemma coprimeI: "(\l. \l dvd a; l dvd b\ \ l dvd 1) \ gcd a b = 1" by (rule sym, rule gcdI, simp_all) lemma coprime: "gcd a b = 1 \ (\d. d dvd a \ d dvd b \ is_unit d)" @@ -796,10 +869,10 @@ using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast lemma gcd_coprime: - assumes z: "gcd a b \ 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" + assumes c: "gcd a b \ 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" shows "gcd a' b' = 1" proof - - from z have "a \ 0 \ b \ 0" by simp + from c have "a \ 0 \ b \ 0" by simp with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" . also from assms have "a div gcd a b = a'" by (metis div_mult_self2_is_id)+ also from assms have "b div gcd a b = b'" by (metis div_mult_self2_is_id)+ @@ -846,8 +919,8 @@ using div_gcd_coprime by (subst sym, auto simp: div_gcd_coprime) hence "(gcd a b) ^ n = (gcd a b) ^ n * ..." by simp also note gcd_mult_distrib - also have "normalisation_factor ((gcd a b)^n) = 1" - by (simp add: normalisation_factor_pow A) + also have "normalization_factor ((gcd a b)^n) = 1" + by (simp add: normalization_factor_pow A) also have "(gcd a b)^n * (a div gcd a b)^n = a^n" by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) also have "(gcd a b)^n * (b div gcd a b)^n = b^n" @@ -856,8 +929,8 @@ qed lemma coprime_common_divisor: - "gcd a b = 1 \ x dvd a \ x dvd b \ is_unit x" - apply (subgoal_tac "x dvd gcd a b") + "gcd a b = 1 \ a dvd a \ a dvd b \ is_unit a" + apply (subgoal_tac "a dvd gcd a b") apply simp apply (erule (1) gcd_greatest) done @@ -887,7 +960,7 @@ then show ?thesis by blast qed -lemma pow_divides_pow: +lemma pow_divs_pow: assumes ab: "a ^ n dvd b ^ n" and n: "n \ 0" shows "a dvd b" proof (cases "gcd a b = 0") @@ -914,11 +987,11 @@ with ab'(1,2) show ?thesis by simp qed -lemma pow_divides_eq [simp]: +lemma pow_divs_eq [simp]: "n \ 0 \ a ^ n dvd b ^ n \ a dvd b" - by (auto intro: pow_divides_pow dvd_power_same) + by (auto intro: pow_divs_pow dvd_power_same) -lemma divides_mult: +lemma divs_mult: assumes mr: "m dvd r" and nr: "n dvd r" and mn: "gcd m n = 1" shows "m * n dvd r" proof - @@ -935,7 +1008,7 @@ by (subst add_commute, simp) lemma setprod_coprime [rule_format]: - "(\i\A. gcd (f i) x = 1) \ gcd (\i\A. f i) x = 1" + "(\i\A. gcd (f i) a = 1) \ gcd (\i\A. f i) a = 1" apply (cases "finite A") apply (induct set: finite) apply (auto simp add: gcd_mult_cancel) @@ -955,49 +1028,49 @@ qed lemma invertible_coprime: - assumes "x * y mod m = 1" - shows "coprime x m" + assumes "a * b mod m = 1" + shows "coprime a m" proof - - from assms have "coprime m (x * y mod m)" + from assms have "coprime m (a * b mod m)" by simp - then have "coprime m (x * y)" + then have "coprime m (a * b)" by simp - then have "coprime m x" + then have "coprime m a" by (rule coprime_lmult) then show ?thesis by (simp add: ac_simps) qed lemma lcm_gcd: - "lcm a b = a * b div (gcd a b * normalisation_factor (a*b))" + "lcm a b = a * b div (gcd a b * normalization_factor (a*b))" by (simp only: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def) lemma lcm_gcd_prod: - "lcm a b * gcd a b = a * b div normalisation_factor (a*b)" + "lcm a b * gcd a b = a * b div normalization_factor (a*b)" proof (cases "a * b = 0") - let ?nf = normalisation_factor + let ?nf = normalization_factor assume "a * b \ 0" hence "gcd a b \ 0" by simp from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))" by (simp add: mult_ac) - also from `a * b \ 0` have "... = a * b div ?nf (a*b)" - by (simp_all add: unit_ring_inv'1 unit_ring_inv) + also from `a * b \ 0` have "... = a * b div ?nf (a*b)" + by (simp add: div_mult_swap mult.commute) finally show ?thesis . qed (auto simp add: lcm_gcd) lemma lcm_dvd1 [iff]: - "x dvd lcm x y" -proof (cases "x*y = 0") - assume "x * y \ 0" - hence "gcd x y \ 0" by simp - let ?c = "ring_inv (normalisation_factor (x*y))" - from `x * y \ 0` have [simp]: "is_unit (normalisation_factor (x*y))" by simp - from lcm_gcd_prod[of x y] have "lcm x y * gcd x y = x * ?c * y" - by (simp add: mult_ac unit_ring_inv) - hence "lcm x y * gcd x y div gcd x y = x * ?c * y div gcd x y" by simp - with `gcd x y \ 0` have "lcm x y = x * ?c * y div gcd x y" + "a dvd lcm a b" +proof (cases "a*b = 0") + assume "a * b \ 0" + hence "gcd a b \ 0" by simp + let ?c = "1 div normalization_factor (a * b)" + from `a * b \ 0` have [simp]: "is_unit (normalization_factor (a * b))" by simp + from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b" + by (simp add: div_mult_swap unit_div_commute) + hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp + with `gcd a b \ 0` have "lcm a b = a * ?c * b div gcd a b" by (subst (asm) div_mult_self2_is_id, simp_all) - also have "... = x * (?c * y div gcd x y)" + also have "... = a * (?c * b div gcd a b)" by (metis div_mult_swap gcd_dvd2 mult_assoc) finally show ?thesis by (rule dvdI) qed (auto simp add: lcm_gcd) @@ -1005,7 +1078,7 @@ lemma lcm_least: "\a dvd k; b dvd k\ \ lcm a b dvd k" proof (cases "k = 0") - let ?nf = normalisation_factor + let ?nf = normalization_factor assume "k \ 0" hence "is_unit (?nf k)" by simp hence "?nf k \ 0" by (metis not_is_unit_0) @@ -1047,7 +1120,7 @@ lemma lcm_zero: "lcm a b = 0 \ a = 0 \ b = 0" proof - - let ?nf = normalisation_factor + let ?nf = normalization_factor { assume "a \ 0" "b \ 0" hence "a * b div ?nf (a * b) \ 0" by (simp add: no_zero_divisors) @@ -1064,67 +1137,67 @@ lemma gcd_lcm: assumes "lcm a b \ 0" - shows "gcd a b = a * b div (lcm a b * normalisation_factor (a * b))" + shows "gcd a b = a * b div (lcm a b * normalization_factor (a * b))" proof- from assms have "gcd a b \ 0" by (simp add: lcm_zero) - let ?c = "normalisation_factor (a*b)" + let ?c = "normalization_factor (a * b)" from `lcm a b \ 0` have "?c \ 0" by (intro notI, simp add: lcm_zero no_zero_divisors) hence "is_unit ?c" by simp from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b" by (subst (2) div_mult_self2_is_id[OF `lcm a b \ 0`, symmetric], simp add: mult_ac) - also from `is_unit ?c` have "... = a * b div (?c * lcm a b)" - by (simp only: unit_ring_inv'1 unit_ring_inv) - finally show ?thesis by (simp only: ac_simps) + also from `is_unit ?c` have "... = a * b div (lcm a b * ?c)" + by (metis `?c \ 0` div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd') + finally show ?thesis . qed -lemma normalisation_factor_lcm [simp]: - "normalisation_factor (lcm a b) = (if a = 0 \ b = 0 then 0 else 1)" +lemma normalization_factor_lcm [simp]: + "normalization_factor (lcm a b) = (if a = 0 \ b = 0 then 0 else 1)" proof (cases "a = 0 \ b = 0") case True then show ?thesis by (auto simp add: lcm_gcd) next case False - let ?nf = normalisation_factor + let ?nf = normalization_factor from lcm_gcd_prod[of a b] have "?nf (lcm a b) * ?nf (gcd a b) = ?nf (a*b) div ?nf (a*b)" - by (metis div_by_0 div_self normalisation_correct normalisation_factor_0 normalisation_factor_mult) + by (metis div_by_0 div_self normalization_correct normalization_factor_0 normalization_factor_mult) also have "... = (if a*b = 0 then 0 else 1)" by simp finally show ?thesis using False by simp qed -lemma lcm_dvd2 [iff]: "y dvd lcm x y" - using lcm_dvd1 [of y x] by (simp add: lcm_gcd ac_simps) +lemma lcm_dvd2 [iff]: "b dvd lcm a b" + using lcm_dvd1 [of b a] by (simp add: lcm_gcd ac_simps) lemma lcmI: - "\x dvd k; y dvd k; \l. x dvd l \ y dvd l \ k dvd l; - normalisation_factor k = (if k = 0 then 0 else 1)\ \ k = lcm x y" + "\a dvd k; b dvd k; \l. a dvd l \ b dvd l \ k dvd l; + normalization_factor k = (if k = 0 then 0 else 1)\ \ k = lcm a b" by (intro normed_associated_imp_eq) (auto simp: associated_def intro: lcm_least) sublocale lcm!: abel_semigroup lcm proof - fix x y z - show "lcm (lcm x y) z = lcm x (lcm y z)" + fix a b c + show "lcm (lcm a b) c = lcm a (lcm b c)" proof (rule lcmI) - have "x dvd lcm x y" and "lcm x y dvd lcm (lcm x y) z" by simp_all - then show "x dvd lcm (lcm x y) z" by (rule dvd_trans) + have "a dvd lcm a b" and "lcm a b dvd lcm (lcm a b) c" by simp_all + then show "a dvd lcm (lcm a b) c" by (rule dvd_trans) - have "y dvd lcm x y" and "lcm x y dvd lcm (lcm x y) z" by simp_all - hence "y dvd lcm (lcm x y) z" by (rule dvd_trans) - moreover have "z dvd lcm (lcm x y) z" by simp - ultimately show "lcm y z dvd lcm (lcm x y) z" by (rule lcm_least) + have "b dvd lcm a b" and "lcm a b dvd lcm (lcm a b) c" by simp_all + hence "b dvd lcm (lcm a b) c" by (rule dvd_trans) + moreover have "c dvd lcm (lcm a b) c" by simp + ultimately show "lcm b c dvd lcm (lcm a b) c" by (rule lcm_least) - fix l assume "x dvd l" and "lcm y z dvd l" - have "y dvd lcm y z" by simp - from this and `lcm y z dvd l` have "y dvd l" by (rule dvd_trans) - have "z dvd lcm y z" by simp - from this and `lcm y z dvd l` have "z dvd l" by (rule dvd_trans) - from `x dvd l` and `y dvd l` have "lcm x y dvd l" by (rule lcm_least) - from this and `z dvd l` show "lcm (lcm x y) z dvd l" by (rule lcm_least) + fix l assume "a dvd l" and "lcm b c dvd l" + have "b dvd lcm b c" by simp + from this and `lcm b c dvd l` have "b dvd l" by (rule dvd_trans) + have "c dvd lcm b c" by simp + from this and `lcm b c dvd l` have "c dvd l" by (rule dvd_trans) + from `a dvd l` and `b dvd l` have "lcm a b dvd l" by (rule lcm_least) + from this and `c dvd l` show "lcm (lcm a b) c dvd l" by (rule lcm_least) qed (simp add: lcm_zero) next - fix x y - show "lcm x y = lcm y x" + fix a b + show "lcm a b = lcm b a" by (simp add: lcm_gcd ac_simps) qed @@ -1149,24 +1222,24 @@ assume "is_unit a \ is_unit b" hence "a dvd 1" and "b dvd 1" by simp_all hence "is_unit (lcm a b)" by (rule lcm_least) - hence "lcm a b = normalisation_factor (lcm a b)" - by (subst normalisation_factor_unit, simp_all) + hence "lcm a b = normalization_factor (lcm a b)" + by (subst normalization_factor_unit, simp_all) also have "\ = 1" using `is_unit a \ is_unit b` by auto finally show "lcm a b = 1" . qed lemma lcm_0_left [simp]: - "lcm 0 x = 0" + "lcm 0 a = 0" by (rule sym, rule lcmI, simp_all) lemma lcm_0 [simp]: - "lcm x 0 = 0" + "lcm a 0 = 0" by (rule sym, rule lcmI, simp_all) lemma lcm_unique: "a dvd d \ b dvd d \ - normalisation_factor d = (if d = 0 then 0 else 1) \ + normalization_factor d = (if d = 0 then 0 else 1) \ (\e. a dvd e \ b dvd e \ d dvd e) \ d = lcm a b" by (rule, auto intro: lcmI simp: lcm_least lcm_zero) @@ -1179,43 +1252,43 @@ by (metis lcm_dvd2 dvd_trans) lemma lcm_1_left [simp]: - "lcm 1 x = x div normalisation_factor x" - by (cases "x = 0") (simp, rule sym, rule lcmI, simp_all) + "lcm 1 a = a div normalization_factor a" + by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all) lemma lcm_1_right [simp]: - "lcm x 1 = x div normalisation_factor x" - by (simp add: ac_simps) + "lcm a 1 = a div normalization_factor a" + using lcm_1_left [of a] by (simp add: ac_simps) lemma lcm_coprime: - "gcd a b = 1 \ lcm a b = a * b div normalisation_factor (a*b)" + "gcd a b = 1 \ lcm a b = a * b div normalization_factor (a*b)" by (subst lcm_gcd) simp lemma lcm_proj1_if_dvd: - "y dvd x \ lcm x y = x div normalisation_factor x" - by (cases "x = 0") (simp, rule sym, rule lcmI, simp_all) + "b dvd a \ lcm a b = a div normalization_factor a" + by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all) lemma lcm_proj2_if_dvd: - "x dvd y \ lcm x y = y div normalisation_factor y" - using lcm_proj1_if_dvd [of x y] by (simp add: ac_simps) + "a dvd b \ lcm a b = b div normalization_factor b" + using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps) lemma lcm_proj1_iff: - "lcm m n = m div normalisation_factor m \ n dvd m" + "lcm m n = m div normalization_factor m \ n dvd m" proof - assume A: "lcm m n = m div normalisation_factor m" + assume A: "lcm m n = m div normalization_factor m" show "n dvd m" proof (cases "m = 0") assume [simp]: "m \ 0" - from A have B: "m = lcm m n * normalisation_factor m" + from A have B: "m = lcm m n * normalization_factor m" by (simp add: unit_eq_div2) show ?thesis by (subst B, simp) qed simp next assume "n dvd m" - then show "lcm m n = m div normalisation_factor m" by (rule lcm_proj1_if_dvd) + then show "lcm m n = m div normalization_factor m" by (rule lcm_proj1_if_dvd) qed lemma lcm_proj2_iff: - "lcm m n = n div normalisation_factor n \ m dvd n" + "lcm m n = n div normalization_factor n \ m dvd n" using lcm_proj1_iff [of n m] by (simp add: ac_simps) lemma euclidean_size_lcm_le1: @@ -1252,28 +1325,28 @@ using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps) lemma lcm_mult_unit1: - "is_unit a \ lcm (x*a) y = lcm x y" + "is_unit a \ lcm (b * a) c = lcm b c" apply (rule lcmI) - apply (rule dvd_trans[of _ "x*a"], simp, rule lcm_dvd1) + apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1) apply (rule lcm_dvd2) apply (rule lcm_least, simp add: unit_simps, assumption) - apply (subst normalisation_factor_lcm, simp add: lcm_zero) + apply (subst normalization_factor_lcm, simp add: lcm_zero) done lemma lcm_mult_unit2: - "is_unit a \ lcm x (y*a) = lcm x y" - using lcm_mult_unit1 [of a y x] by (simp add: ac_simps) + "is_unit a \ lcm b (c * a) = lcm b c" + using lcm_mult_unit1 [of a c b] by (simp add: ac_simps) lemma lcm_div_unit1: - "is_unit a \ lcm (x div a) y = lcm x y" - by (simp add: unit_ring_inv lcm_mult_unit1) + "is_unit a \ lcm (b div a) c = lcm b c" + by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) lemma lcm_div_unit2: - "is_unit a \ lcm x (y div a) = lcm x y" - by (simp add: unit_ring_inv lcm_mult_unit2) + "is_unit a \ lcm b (c div a) = lcm b c" + by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2) lemma lcm_left_idem: - "lcm p (lcm p q) = lcm p q" + "lcm a (lcm a b) = lcm a b" apply (rule lcmI) apply simp apply (subst lcm.assoc [symmetric], rule lcm_dvd2) @@ -1283,7 +1356,7 @@ done lemma lcm_right_idem: - "lcm (lcm p q) q = lcm p q" + "lcm (lcm a b) b = lcm a b" apply (rule lcmI) apply (subst lcm.assoc, rule lcm_dvd1) apply (rule lcm_dvd2) @@ -1300,35 +1373,35 @@ by (intro ext, simp add: lcm_left_idem) qed -lemma dvd_Lcm [simp]: "x \ A \ x dvd Lcm A" - and Lcm_dvd [simp]: "(\x\A. x dvd l') \ Lcm A dvd l'" - and normalisation_factor_Lcm [simp]: - "normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" +lemma dvd_Lcm [simp]: "a \ A \ a dvd Lcm A" + and Lcm_dvd [simp]: "(\a\A. a dvd l') \ Lcm A dvd l'" + and normalization_factor_Lcm [simp]: + "normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" proof - - have "(\x\A. x dvd Lcm A) \ (\l'. (\x\A. x dvd l') \ Lcm A dvd l') \ - normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis) - proof (cases "\l. l \ 0 \ (\x\A. x dvd l)") + have "(\a\A. a dvd Lcm A) \ (\l'. (\a\A. a dvd l') \ Lcm A dvd l') \ + normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis) + proof (cases "\l. l \ 0 \ (\a\A. a dvd l)") case False hence "Lcm A = 0" by (auto simp: Lcm_Lcm_eucl Lcm_eucl_def) with False show ?thesis by auto next case True - then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \ 0 \ (\x\A. x dvd l\<^sub>0)" by blast - def n \ "LEAST n. \l. l \ 0 \ (\x\A. x dvd l) \ euclidean_size l = n" - def l \ "SOME l. l \ 0 \ (\x\A. x dvd l) \ euclidean_size l = n" - have "\l. l \ 0 \ (\x\A. x dvd l) \ euclidean_size l = n" + then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \ 0 \ (\a\A. a dvd l\<^sub>0)" by blast + def n \ "LEAST n. \l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" + def l \ "SOME l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" + have "\l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" apply (subst n_def) apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) apply (rule exI[of _ l\<^sub>0]) apply (simp add: l\<^sub>0_props) done - from someI_ex[OF this] have "l \ 0" and "\x\A. x dvd l" and "euclidean_size l = n" + from someI_ex[OF this] have "l \ 0" and "\a\A. a dvd l" and "euclidean_size l = n" unfolding l_def by simp_all { - fix l' assume "\x\A. x dvd l'" - with `\x\A. x dvd l` have "\x\A. x dvd gcd l l'" by (auto intro: gcd_greatest) + fix l' assume "\a\A. a dvd l'" + with `\a\A. a dvd l` have "\a\A. a dvd gcd l l'" by (auto intro: gcd_greatest) moreover from `l \ 0` have "gcd l l' \ 0" by simp - ultimately have "\b. b \ 0 \ (\x\A. x dvd b) \ euclidean_size b = euclidean_size (gcd l l')" + ultimately have "\b. b \ 0 \ (\a\A. a dvd b) \ euclidean_size b = euclidean_size (gcd l l')" by (intro exI[of _ "gcd l l'"], auto) hence "euclidean_size (gcd l l') \ n" by (subst n_def) (rule Least_le) moreover have "euclidean_size (gcd l l') \ n" @@ -1348,26 +1421,26 @@ hence "l dvd l'" by (blast dest: dvd_gcd_D2) } - with `(\x\A. x dvd l)` and normalisation_factor_is_unit[OF `l \ 0`] and `l \ 0` - have "(\x\A. x dvd l div normalisation_factor l) \ - (\l'. (\x\A. x dvd l') \ l div normalisation_factor l dvd l') \ - normalisation_factor (l div normalisation_factor l) = - (if l div normalisation_factor l = 0 then 0 else 1)" + with `(\a\A. a dvd l)` and normalization_factor_is_unit[OF `l \ 0`] and `l \ 0` + have "(\a\A. a dvd l div normalization_factor l) \ + (\l'. (\a\A. a dvd l') \ l div normalization_factor l dvd l') \ + normalization_factor (l div normalization_factor l) = + (if l div normalization_factor l = 0 then 0 else 1)" by (auto simp: unit_simps) - also from True have "l div normalisation_factor l = Lcm A" + also from True have "l div normalization_factor l = Lcm A" by (simp add: Lcm_Lcm_eucl Lcm_eucl_def Let_def n_def l_def) finally show ?thesis . qed note A = this - {fix x assume "x \ A" then show "x dvd Lcm A" using A by blast} - {fix l' assume "\x\A. x dvd l'" then show "Lcm A dvd l'" using A by blast} - from A show "normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast + {fix a assume "a \ A" then show "a dvd Lcm A" using A by blast} + {fix l' assume "\a\A. a dvd l'" then show "Lcm A dvd l'" using A by blast} + from A show "normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast qed lemma LcmI: - "(\x. x\A \ x dvd l) \ (\l'. (\x\A. x dvd l') \ l dvd l') \ - normalisation_factor l = (if l = 0 then 0 else 1) \ l = Lcm A" + "(\a. a\A \ a dvd l) \ (\l'. (\a\A. a dvd l') \ l dvd l') \ + normalization_factor l = (if l = 0 then 0 else 1) \ l = Lcm A" by (intro normed_associated_imp_eq) (auto intro: Lcm_dvd dvd_Lcm simp: associated_def) @@ -1387,19 +1460,19 @@ done lemma Lcm_1_iff: - "Lcm A = 1 \ (\x\A. is_unit x)" + "Lcm A = 1 \ (\a\A. is_unit a)" proof assume "Lcm A = 1" - then show "\x\A. is_unit x" by auto + then show "\a\A. is_unit a" by auto qed (rule LcmI [symmetric], auto) lemma Lcm_no_units: - "Lcm A = Lcm (A - {x. is_unit x})" + "Lcm A = Lcm (A - {a. is_unit a})" proof - - have "(A - {x. is_unit x}) \ {x\A. is_unit x} = A" by blast - hence "Lcm A = lcm (Lcm (A - {x. is_unit x})) (Lcm {x\A. is_unit x})" + have "(A - {a. is_unit a}) \ {a\A. is_unit a} = A" by blast + hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\A. is_unit a})" by (simp add: Lcm_Un[symmetric]) - also have "Lcm {x\A. is_unit x} = 1" by (simp add: Lcm_1_iff) + also have "Lcm {a\A. is_unit a} = 1" by (simp add: Lcm_1_iff) finally show ?thesis by simp qed @@ -1412,24 +1485,24 @@ by (drule dvd_Lcm) simp lemma Lcm0_iff': - "Lcm A = 0 \ \(\l. l \ 0 \ (\x\A. x dvd l))" + "Lcm A = 0 \ \(\l. l \ 0 \ (\a\A. a dvd l))" proof assume "Lcm A = 0" - show "\(\l. l \ 0 \ (\x\A. x dvd l))" + show "\(\l. l \ 0 \ (\a\A. a dvd l))" proof - assume ex: "\l. l \ 0 \ (\x\A. x dvd l)" - then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \ 0 \ (\x\A. x dvd l\<^sub>0)" by blast - def n \ "LEAST n. \l. l \ 0 \ (\x\A. x dvd l) \ euclidean_size l = n" - def l \ "SOME l. l \ 0 \ (\x\A. x dvd l) \ euclidean_size l = n" - have "\l. l \ 0 \ (\x\A. x dvd l) \ euclidean_size l = n" + assume ex: "\l. l \ 0 \ (\a\A. a dvd l)" + then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \ 0 \ (\a\A. a dvd l\<^sub>0)" by blast + def n \ "LEAST n. \l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" + def l \ "SOME l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" + have "\l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" apply (subst n_def) apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) apply (rule exI[of _ l\<^sub>0]) apply (simp add: l\<^sub>0_props) done from someI_ex[OF this] have "l \ 0" unfolding l_def by simp_all - hence "l div normalisation_factor l \ 0" by simp - also from ex have "l div normalisation_factor l = Lcm A" + hence "l div normalization_factor l \ 0" by simp + also from ex have "l div normalization_factor l = Lcm A" by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def) finally show False using `Lcm A = 0` by contradiction qed @@ -1449,18 +1522,18 @@ apply (rule no_zero_divisors) apply blast+ done - moreover from `finite A` have "\x\A. x dvd \A" by blast - ultimately have "\l. l \ 0 \ (\x\A. x dvd l)" by blast + moreover from `finite A` have "\a\A. a dvd \A" by blast + ultimately have "\l. l \ 0 \ (\a\A. a dvd l)" by blast with Lcm0_iff' have "Lcm A \ 0" by simp } ultimately show "Lcm A = 0 \ 0 \ A" by blast qed lemma Lcm_no_multiple: - "(\m. m \ 0 \ (\x\A. \x dvd m)) \ Lcm A = 0" + "(\m. m \ 0 \ (\a\A. \a dvd m)) \ Lcm A = 0" proof - - assume "\m. m \ 0 \ (\x\A. \x dvd m)" - hence "\(\l. l \ 0 \ (\x\A. x dvd l))" by blast + assume "\m. m \ 0 \ (\a\A. \a dvd m)" + hence "\(\l. l \ 0 \ (\a\A. a dvd l))" by blast then show "Lcm A = 0" by (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False) qed @@ -1468,7 +1541,7 @@ "Lcm (insert a A) = lcm a (Lcm A)" proof (rule lcmI) fix l assume "a dvd l" and "Lcm A dvd l" - hence "\x\A. x dvd l" by (blast intro: dvd_trans dvd_Lcm) + hence "\a\A. a dvd l" by (blast intro: dvd_trans dvd_Lcm) with `a dvd l` show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd) qed (auto intro: Lcm_dvd dvd_Lcm) @@ -1478,12 +1551,12 @@ by (induct rule: finite.induct[OF `finite A`]) (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm]) -lemma Lcm_set [code, code_unfold]: +lemma Lcm_set [code_unfold]: "Lcm (set xs) = fold lcm xs 1" using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite by (simp add: ac_simps) lemma Lcm_singleton [simp]: - "Lcm {a} = a div normalisation_factor a" + "Lcm {a} = a div normalization_factor a" by simp lemma Lcm_2 [simp]: @@ -1494,52 +1567,52 @@ lemma Lcm_coprime: assumes "finite A" and "A \ {}" assumes "\a b. a \ A \ b \ A \ a \ b \ gcd a b = 1" - shows "Lcm A = \A div normalisation_factor (\A)" + shows "Lcm A = \A div normalization_factor (\A)" using assms proof (induct rule: finite_ne_induct) case (insert a A) have "Lcm (insert a A) = lcm a (Lcm A)" by simp - also from insert have "Lcm A = \A div normalisation_factor (\A)" by blast + also from insert have "Lcm A = \A div normalization_factor (\A)" by blast also have "lcm a \ = lcm a (\A)" by (cases "\A = 0") (simp_all add: lcm_div_unit2) also from insert have "gcd a (\A) = 1" by (subst gcd.commute, intro setprod_coprime) auto - with insert have "lcm a (\A) = \(insert a A) div normalisation_factor (\(insert a A))" + with insert have "lcm a (\A) = \(insert a A) div normalization_factor (\(insert a A))" by (simp add: lcm_coprime) finally show ?case . qed simp lemma Lcm_coprime': "card A \ 0 \ (\a b. a \ A \ b \ A \ a \ b \ gcd a b = 1) - \ Lcm A = \A div normalisation_factor (\A)" + \ Lcm A = \A div normalization_factor (\A)" by (rule Lcm_coprime) (simp_all add: card_eq_0_iff) lemma Gcd_Lcm: - "Gcd A = Lcm {d. \x\A. d dvd x}" + "Gcd A = Lcm {d. \a\A. d dvd a}" by (simp add: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def) -lemma Gcd_dvd [simp]: "x \ A \ Gcd A dvd x" - and dvd_Gcd [simp]: "(\x\A. g' dvd x) \ g' dvd Gcd A" - and normalisation_factor_Gcd [simp]: - "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" +lemma Gcd_dvd [simp]: "a \ A \ Gcd A dvd a" + and dvd_Gcd [simp]: "(\a\A. g' dvd a) \ g' dvd Gcd A" + and normalization_factor_Gcd [simp]: + "normalization_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" proof - - fix x assume "x \ A" - hence "Lcm {d. \x\A. d dvd x} dvd x" by (intro Lcm_dvd) blast - then show "Gcd A dvd x" by (simp add: Gcd_Lcm) + fix a assume "a \ A" + hence "Lcm {d. \a\A. d dvd a} dvd a" by (intro Lcm_dvd) blast + then show "Gcd A dvd a" by (simp add: Gcd_Lcm) next - fix g' assume "\x\A. g' dvd x" - hence "g' dvd Lcm {d. \x\A. d dvd x}" by (intro dvd_Lcm) blast + fix g' assume "\a\A. g' dvd a" + hence "g' dvd Lcm {d. \a\A. d dvd a}" by (intro dvd_Lcm) blast then show "g' dvd Gcd A" by (simp add: Gcd_Lcm) next - show "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" + show "normalization_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" by (simp add: Gcd_Lcm) qed lemma GcdI: - "(\x. x\A \ l dvd x) \ (\l'. (\x\A. l' dvd x) \ l' dvd l) \ - normalisation_factor l = (if l = 0 then 0 else 1) \ l = Gcd A" + "(\a. a\A \ l dvd a) \ (\l'. (\a\A. l' dvd a) \ l' dvd l) \ + normalization_factor l = (if l = 0 then 0 else 1) \ l = Gcd A" by (intro normed_associated_imp_eq) (auto intro: Gcd_dvd dvd_Gcd simp: associated_def) lemma Lcm_Gcd: - "Lcm A = Gcd {m. \x\A. x dvd m}" + "Lcm A = Gcd {m. \a\A. a dvd m}" by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_dvd) lemma Gcd_0_iff: @@ -1561,7 +1634,7 @@ "Gcd (insert a A) = gcd a (Gcd A)" proof (rule gcdI) fix l assume "l dvd a" and "l dvd Gcd A" - hence "\x\A. l dvd x" by (blast intro: dvd_trans Gcd_dvd) + hence "\a\A. l dvd a" by (blast intro: dvd_trans Gcd_dvd) with `l dvd a` show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd) qed auto @@ -1571,16 +1644,19 @@ by (induct rule: finite.induct[OF `finite A`]) (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd]) -lemma Gcd_set [code, code_unfold]: +lemma Gcd_set [code_unfold]: "Gcd (set xs) = fold gcd xs 0" using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps) -lemma Gcd_singleton [simp]: "Gcd {a} = a div normalisation_factor a" +lemma Gcd_singleton [simp]: "Gcd {a} = a div normalization_factor a" by (simp add: gcd_0) lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b" by (simp only: Gcd_insert Gcd_empty gcd_0) (cases "b = 0", simp, rule gcd_div_unit2, simp) +subclass semiring_gcd + by unfold_locales (simp_all add: gcd_greatest_iff) + end text {* @@ -1595,20 +1671,22 @@ subclass euclidean_ring .. +subclass ring_gcd .. + lemma gcd_neg1 [simp]: - "gcd (-x) y = gcd x y" + "gcd (-a) b = gcd a b" by (rule sym, rule gcdI, simp_all add: gcd_greatest) lemma gcd_neg2 [simp]: - "gcd x (-y) = gcd x y" + "gcd a (-b) = gcd a b" by (rule sym, rule gcdI, simp_all add: gcd_greatest) lemma gcd_neg_numeral_1 [simp]: - "gcd (- numeral n) x = gcd (numeral n) x" + "gcd (- numeral n) a = gcd (numeral n) a" by (fact gcd_neg1) lemma gcd_neg_numeral_2 [simp]: - "gcd x (- numeral n) = gcd x (numeral n)" + "gcd a (- numeral n) = gcd a (numeral n)" by (fact gcd_neg2) lemma gcd_diff1: "gcd (m - n) n = gcd m n" @@ -1625,22 +1703,22 @@ finally show ?thesis . qed -lemma lcm_neg1 [simp]: "lcm (-x) y = lcm x y" +lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b" by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero) -lemma lcm_neg2 [simp]: "lcm x (-y) = lcm x y" +lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b" by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero) -lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) x = lcm (numeral n) x" +lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a" by (fact lcm_neg1) -lemma lcm_neg_numeral_2 [simp]: "lcm x (- numeral n) = lcm x (numeral n)" +lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)" by (fact lcm_neg2) function euclid_ext :: "'a \ 'a \ 'a \ 'a \ 'a" where "euclid_ext a b = (if b = 0 then - let x = ring_inv (normalisation_factor a) in (x, 0, a * x) + let c = 1 div normalization_factor a in (c, 0, a * c) else case euclid_ext b (a mod b) of (s,t,c) \ (t, s - t * (a div b), c))" @@ -1650,13 +1728,13 @@ declare euclid_ext.simps [simp del] lemma euclid_ext_0: - "euclid_ext a 0 = (ring_inv (normalisation_factor a), 0, a * ring_inv (normalisation_factor a))" - by (subst euclid_ext.simps, simp add: Let_def) + "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)" + by (subst euclid_ext.simps) (simp add: Let_def) lemma euclid_ext_non_0: "b \ 0 \ euclid_ext a b = (case euclid_ext b (a mod b) of (s,t,c) \ (t, s - t * (a div b), c))" - by (subst euclid_ext.simps, simp) + by (subst euclid_ext.simps) simp definition euclid_ext' :: "'a \ 'a \ 'a \ 'a" where @@ -1669,8 +1747,8 @@ then show ?case proof (cases "b = 0") case True - then show ?thesis by (cases "a = 0") - (simp_all add: euclid_ext_0 unit_div mult_ac unit_simps gcd_0) + then show ?thesis by + (simp add: euclid_ext_0 unit_div mult_ac unit_simps gcd_0) next case False with 1 show ?thesis by (simp add: euclid_ext_non_0 ac_simps split: prod.split prod.split_asm) @@ -1682,21 +1760,21 @@ by (insert euclid_ext_gcd[of a b], drule (1) subst, simp) lemma euclid_ext_correct: - "case euclid_ext x y of (s,t,c) \ s*x + t*y = c" -proof (induct x y rule: euclid_ext.induct) - case (1 x y) + "case euclid_ext a b of (s,t,c) \ s*a + t*b = c" +proof (induct a b rule: euclid_ext.induct) + case (1 a b) show ?case - proof (cases "y = 0") + proof (cases "b = 0") case True then show ?thesis by (simp add: euclid_ext_0 mult_ac) next case False - obtain s t c where stc: "euclid_ext y (x mod y) = (s,t,c)" - by (cases "euclid_ext y (x mod y)", blast) - from 1 have "c = s * y + t * (x mod y)" by (simp add: stc False) - also have "... = t*((x div y)*y + x mod y) + (s - t * (x div y))*y" + obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)" + by (cases "euclid_ext b (a mod b)", blast) + from 1 have "c = s * b + t * (a mod b)" by (simp add: stc False) + also have "... = t*((a div b)*b + a mod b) + (s - t * (a div b))*b" by (simp add: algebra_simps) - also have "(x div y)*y + x mod y = x" using mod_div_equality . + also have "(a div b)*b + a mod b = a" using mod_div_equality . finally show ?thesis by (subst euclid_ext.simps, simp add: False stc) qed @@ -1711,15 +1789,15 @@ show ?thesis unfolding euclid_ext'_def by simp qed -lemma bezout: "\s t. s * x + t * y = gcd x y" +lemma bezout: "\s t. s * a + t * b = gcd a b" using euclid_ext'_correct by blast -lemma euclid_ext'_0 [simp]: "euclid_ext' x 0 = (ring_inv (normalisation_factor x), 0)" +lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (1 div normalization_factor a, 0)" by (simp add: bezw_def euclid_ext'_def euclid_ext_0) -lemma euclid_ext'_non_0: "y \ 0 \ euclid_ext' x y = (snd (euclid_ext' y (x mod y)), - fst (euclid_ext' y (x mod y)) - snd (euclid_ext' y (x mod y)) * (x div y))" - by (cases "euclid_ext y (x mod y)") +lemma euclid_ext'_non_0: "b \ 0 \ euclid_ext' a b = (snd (euclid_ext' b (a mod b)), + fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))" + by (cases "euclid_ext b (a mod b)") (simp add: euclid_ext'_def euclid_ext_non_0) end @@ -1731,7 +1809,7 @@ "euclidean_size_nat = (id :: nat \ nat)" definition [simp]: - "normalisation_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)" + "normalization_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)" instance proof qed simp_all @@ -1745,7 +1823,7 @@ "euclidean_size_int = (nat \ abs :: int \ nat)" definition [simp]: - "normalisation_factor_int = (sgn :: int \ int)" + "normalization_factor_int = (sgn :: int \ int)" instance proof case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib) @@ -1760,4 +1838,3 @@ end end - diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Rat.thy Sat Jun 13 22:44:22 2015 +0200 @@ -162,9 +162,9 @@ by transfer simp definition - divide_rat_def: "divide q r = q * inverse (r::rat)" + divide_rat_def: "q div r = q * inverse (r::rat)" -lemma divide_rat [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)" +lemma divide_rat [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)" by (simp add: divide_rat_def) instance proof @@ -191,7 +191,7 @@ by transfer simp { assume "q \ 0" thus "inverse q * q = 1" by transfer simp } - show "divide q r = q * inverse r" + show "q div r = q * inverse r" by (fact divide_rat_def) show "inverse 0 = (0::rat)" by transfer simp diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Real.thy --- a/src/HOL/Real.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Real.thy Sat Jun 13 22:44:22 2015 +0200 @@ -438,7 +438,7 @@ "x - y = (x::real) + - y" definition - "divide x y = (x::real) * inverse y" + "x div y = (x::real) * inverse y" lemma add_Real: assumes X: "cauchy X" and Y: "cauchy Y" @@ -501,7 +501,7 @@ apply (rule_tac x=k in exI, clarify) apply (drule_tac x=n in spec, simp) done - show "divide a b = a * inverse b" + show "a div b = a * inverse b" by (rule divide_real_def) show "inverse (0::real) = 0" by transfer (simp add: realrel_def) diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Rings.thy Sat Jun 13 22:44:22 2015 +0200 @@ -559,7 +559,7 @@ *} class divide = - fixes divide :: "'a \ 'a \ 'a" + fixes divide :: "'a \ 'a \ 'a" (infixl "div" 70) setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \ 'a \ 'a"}) *} @@ -567,8 +567,8 @@ begin lemma [field_simps]: - shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \ a * (b + c) = a * b + a * c" - and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \ (a + b) * c = a * c + b * c" + shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \ a * (b + c) = a * b + a * c" + and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \ (a + b) * c = a * c + b * c" by (rule distrib_left distrib_right)+ end @@ -577,8 +577,8 @@ begin lemma [field_simps]: - shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \ (a - b) * c = a * c - b * c" - and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \ a * (b - c) = a * b - a * c" + shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \ (a - b) * c = a * c - b * c" + and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \ a * (b - c) = a * b - a * c" by (rule left_diff_distrib right_diff_distrib)+ end @@ -586,12 +586,12 @@ setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \ 'a \ 'a"}) *} class semidom_divide = semidom + divide + - assumes nonzero_mult_divide_cancel_right [simp]: "b \ 0 \ divide (a * b) b = a" - assumes divide_zero [simp]: "divide a 0 = 0" + assumes nonzero_mult_divide_cancel_right [simp]: "b \ 0 \ (a * b) div b = a" + assumes divide_zero [simp]: "a div 0 = 0" begin lemma nonzero_mult_divide_cancel_left [simp]: - "a \ 0 \ divide (a * b) a = b" + "a \ 0 \ (a * b) div a = b" using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps) end diff -r 2761a2249c83 -r abee0de69a89 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/Word/Word.thy Sat Jun 13 22:44:22 2015 +0200 @@ -307,7 +307,7 @@ by (metis bintr_ariths(4)) definition - word_div_def: "divide a b = word_of_int (uint a div uint b)" + word_div_def: "a div b = word_of_int (uint a div uint b)" definition word_mod_def: "a mod b = word_of_int (uint a mod uint b)" diff -r 2761a2249c83 -r abee0de69a89 src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/ex/Arith_Examples.thy Sat Jun 13 22:44:22 2015 +0200 @@ -31,7 +31,7 @@ subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, @{term minus}, @{term nat}, @{term Divides.mod}, - @{term Divides.div} *} + @{term divide} *} lemma "(i::nat) <= max i j" by linarith diff -r 2761a2249c83 -r abee0de69a89 src/HOL/ex/Dedekind_Real.thy --- a/src/HOL/ex/Dedekind_Real.thy Sat Jun 13 22:42:23 2015 +0200 +++ b/src/HOL/ex/Dedekind_Real.thy Sat Jun 13 22:44:22 2015 +0200 @@ -102,7 +102,7 @@ preal_inverse_def: "inverse R == Abs_preal (inverse_set (Rep_preal R))" -definition "divide R S = R * inverse (S\preal)" +definition "R div S = R * inverse (S\preal)" definition preal_one_def: @@ -1222,7 +1222,7 @@ real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)" definition - real_divide_def: "divide R (S::real) = R * inverse S" + real_divide_def: "R div (S::real) = R * inverse S" definition real_le_def: "z \ (w::real) \