--- 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
-----------------------------
--- 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:
--- 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"} \\
--- 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\<Colon>complex) = x * inverse y"
+definition "x div (y\<Colon>complex) = x * inverse y"
instance
by intro_classes
--- 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 \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
-begin
-
-abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
-where
- "op div \<equiv> 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 \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> 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\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
@{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>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) \<Longrightarrow> 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
--- 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) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
definition "inverse = (\<lambda>x :: finite_3. x)"
-definition "divide x y = x * inverse (y :: finite_3)"
+definition "x div y = x * inverse (y :: finite_3)"
definition "abs = (\<lambda>x :: finite_3. x)"
definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
--- 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 \<noteq> 0"
- shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
+ shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)"
proof (cases "a \<notin> A")
case True then show ?thesis by simp
next
--- 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:
"\<forall>m n\<Colon>nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> m mod n < n"
--- 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
--- 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 ..
--- 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)
--- 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 \<circ> f"
-definition "divide f g = (\<lambda>x. f x / g x)"
+definition "f div g = (\<lambda>x. f x / g x)"
instance ..
--- 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 \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g"
+ assumes [simp]: "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
+ shows "\<alpha> (lfp f) = lfp g"
+proof -
+ have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
+ unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono)
+ moreover have "\<alpha> ((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 \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
"inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
@@ -146,4 +159,17 @@
qed
qed
+lemma gfp_transfer:
+ assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
+ assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
+ shows "\<alpha> (gfp f) = gfp g"
+proof -
+ have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
+ unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
+ moreover have "\<alpha> ((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
--- 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. \<exists>r. pdivmod_rel x y q r)"
+ div_poly_def: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
definition mod_poly where
"x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
lemma div_poly_eq:
- "pdivmod_rel x y q r \<Longrightarrow> divide x y = q"
+ "pdivmod_rel x y q r \<Longrightarrow> 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 \<noteq> 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 \<noteq> 0"
- show "divide (x * y) (x * z) = divide y z"
+ show "(x * y) div (x * z) = y div z"
proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
by (rule pdivmod_rel_by_0)
- then have [simp]: "\<And>x::'a poly. divide x 0 = 0"
+ then have [simp]: "\<And>x::'a poly. x div 0 = 0"
by (rule div_poly_eq)
have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
by (rule pdivmod_rel_0)
- then have [simp]: "\<And>x::'a poly. divide 0 x = 0"
+ then have [simp]: "\<And>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 "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> 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
--- 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 \<open>Kurzweil-Henstock Gauge Integration in many dimensions.\<close>
@@ -1042,7 +1042,7 @@
next
case False
note p = division_ofD[OF assms(1)]
- have *: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
+ have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> 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: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
- using bchoice[OF *] by blast
+ using bchoice[OF div_cbox] by blast
{ fix x
assume x: "x \<in> p"
have "q x division_of \<Union>q x"
@@ -1075,44 +1075,37 @@
have "d \<union> p division_of cbox a b"
proof -
have te: "\<And>s f t. s \<noteq> {} \<Longrightarrow> \<forall>i\<in>s. f i \<union> i = t \<Longrightarrow> t = \<Inter>(f ` s) \<union> \<Union>s" by auto
- have *: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
+ have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
proof (rule te[OF False], clarify)
fix i
assume i: "i \<in> p"
show "\<Union>(q i - {i}) \<union> i = cbox a b"
using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
qed
- show "d \<union> 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 \<in> p"
- have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}"
+ have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}"
by auto
- show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<inter> interior k = {}"
- apply (rule *[of _ "interior (\<Union>(q k - {k}))"])
- defer
- apply (subst Int_commute)
- apply (rule inter_interior_unions_intervals)
- proof -
+ have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> 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)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = cbox a b"
using qk by auto
show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
using qk(5) using q(2)[OF k] by auto
- have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x"
- by auto
- show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<subseteq> interior (\<Union>(q k - {k}))"
- apply (rule interior_mono *)+
+ show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q k - {k}))"
+ apply (rule interior_mono)+
using k
apply auto
done
- qed
- qed
+ qed } note [simp] = this
+ show "d \<union> 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 \<inter> cbox c d = {}")
case True
- have *: "\<And>a b. {a, b} = {a} \<union> {b}" by auto
show ?thesis
apply (rule that[of "{cbox c d}"])
- unfolding *
+ apply (subst insert_is_Un)
apply (rule division_disjoint_union)
- using \<open>cbox c d \<noteq> {}\<close> True assms
- using interior_subset
+ using \<open>cbox c d \<noteq> {}\<close> True assms interior_subset
apply auto
done
next
case False
obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
unfolding inter_interval by auto
- have *: "cbox u v \<subseteq> cbox c d" using uv by auto
+ have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
obtain p where "p division_of cbox c d" "cbox u v \<in> 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 \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})" "\<And>x s. insert x s = {x} \<union> s"
+ have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
+ apply (rule arg_cong[of _ _ interior])
+ using p(8) uv by auto
+ also have "\<dots> = {}"
+ 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) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
+ have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(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 *: "\<And>cd p uv ab. p \<subseteq> cd \<Longrightarrow> ab \<inter> cd = uv \<Longrightarrow> ab \<inter> p = uv \<inter> p" by auto
- have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
- apply (rule arg_cong[of _ _ interior])
- apply (rule *[OF _ uv])
- using p(8)
- apply auto
- done
- also have "\<dots> = {}"
- 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 \<inter> \<Union>(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 "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
note q = division_ofD[OF this[rule_format]]
let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> 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 \<in> p} = (\<lambda>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: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
by (force simp: mem_box)
- {
- fix f
- have "finite f \<Longrightarrow>
- \<forall>s\<in>f. P s \<Longrightarrow>
- \<forall>s\<in>f. \<exists>a b. s = cbox a b \<Longrightarrow>
- \<forall>s\<in>f.\<forall>t\<in>f. s \<noteq> t \<longrightarrow> interior s \<inter> interior t = {} \<Longrightarrow> P (\<Union>f)"
+ { fix f
+ have "\<lbrakk>finite f;
+ \<And>s. s\<in>f \<Longrightarrow> P s;
+ \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
+ \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>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. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
(c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
@@ -1873,47 +1852,35 @@
}
assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
have "P (\<Union> ?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 = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
(\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
have "?A \<subseteq> ?B"
proof
case goal1
- then obtain c d where x: "x = cbox c d"
- "\<And>i. i \<in> Basis \<Longrightarrow>
- c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
- c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
- have *: "\<And>a b c d. a = c \<Longrightarrow> b = d \<Longrightarrow> cbox a b = cbox c d"
- by auto
+ then obtain c d
+ where x: "x = cbox c d"
+ "\<And>i. i \<in> Basis \<Longrightarrow>
+ c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
+ c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
show "x \<in> ?B"
- unfolding image_iff
+ unfolding image_iff x
apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>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 \<in> Basis"
- then show "c \<bullet> i = (if c \<bullet> i = a \<bullet> i then a \<bullet> i else (a \<bullet> i + b \<bullet> i) / 2)"
- and "d \<bullet> i = (if c \<bullet> i = a \<bullet> i then (a \<bullet> i + b \<bullet> i) / 2 else b \<bullet> 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 \<in> ?A"
- then obtain c d where s:
- "s = cbox c d"
- "\<And>i. i \<in> Basis \<Longrightarrow>
- c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
- c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
+ then obtain c d
+ where s: "s = cbox c d"
+ "\<And>i. i \<in> Basis \<Longrightarrow>
+ c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
+ c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
by blast
show "P s"
unfolding s
@@ -2179,28 +2146,18 @@
next
assume as: "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
obtain x where x:
- "x \<in> (cbox a b)"
- "\<And>e. 0 < e \<Longrightarrow>
- \<exists>c d.
- x \<in> cbox c d \<and>
- cbox c d \<subseteq> ball x e \<and>
- cbox c d \<subseteq> (cbox a b) \<and>
- \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
- apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p",rule_format,OF _ _ as])
- apply (rule_tac x="{}" in exI)
- defer
- apply (erule conjE exE)+
- proof -
- show "{} tagged_division_of {} \<and> 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 \<inter> interior t = {}"
- then show "\<exists>p. p tagged_division_of s \<union> t \<and> g fine p"
- apply (rule_tac x="p \<union> p'" in exI)
- apply (simp add: tagged_division_union fine_union)
- done
- qed blast
+ "x \<in> (cbox a b)"
+ "\<And>e. 0 < e \<Longrightarrow>
+ \<exists>c d.
+ x \<in> cbox c d \<and>
+ cbox c d \<subseteq> ball x e \<and>
+ cbox c d \<subseteq> (cbox a b) \<and>
+ \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
+ apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> 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 \<subseteq> 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" "\<And>x. norm (h x) \<le> norm x * B"
by blast
- have *: "e / B > 0" using goal1(2) B by simp
- obtain g where g: "gauge g"
- "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
- norm ((\<Sum>(x, k)\<in>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"
+ "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
+ norm ((\<Sum>(x, k)\<in>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 *: "\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x"
+ have hc: "\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x"
by auto
- have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = setsum (h \<circ> (\<lambda>(x, k). content k *\<^sub>R f x)) p"
- unfolding o_def unfolding scaleR[symmetric] * by simp
+ then have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = setsum (h \<circ> (\<lambda>(x, k). content k *\<^sub>R f x)) p"
+ unfolding o_def unfolding scaleR[symmetric] hc by simp
also have "\<dots> = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
using setsum[of "\<lambda>(x,k). content k *\<^sub>R f x" p] using as by auto
- finally have *: "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" .
- show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) - h y) < e"
- unfolding * diff[symmetric]
+ finally have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" .
+ then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> 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 "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?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="\<lambda>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 (\<lambda>x. ball x 1)"
+proof -
+ have "gauge (\<lambda>x. ball x 1)"
by auto
- fix p
- assume p: "p tagged_division_of (cbox a b)"
- have "norm ((\<Sum>(x, k)\<in>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 ((\<Sum>(x, k)\<in>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 ((\<Sum>(x, k)\<in>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 ((\<Sum>(x, k)\<in>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 \<Rightarrow> 'b::real_normed_vector"
- assumes "(f has_integral i) (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
- and "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
- and k: "k \<in> Basis"
+ assumes fi: "(f has_integral i) (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
+ and fj: "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+ and k: "k \<in> 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:
+ "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c};
+ d1 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> 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:
+ "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k};
+ d2 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> 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 = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x (abs(x\<bullet>k - c)) \<inter> d1 x \<inter> 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:
- "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<le> c"
- "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<ge> c"
+ have xk_le_c: "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<le> c"
proof -
fix x kk
- assume as: "(x, kk) \<in> p"
- {
- assume *: "kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}"
- show "x\<bullet>k \<le> c"
- proof (rule ccontr)
- assume **: "\<not> ?thesis"
- from this[unfolded not_le]
- have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
- using p(2)[unfolded fine_def, rule_format,OF as,unfolded split_conv] by auto
- with * have "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<le> c}"
- by blast
- then guess y ..
- then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> 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 \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}"
- show "x\<bullet>k \<ge> c"
- proof (rule ccontr)
- assume **: "\<not> ?thesis"
- from this[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
- using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
- with * have "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<ge> c}"
- by blast
- then guess y ..
- then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> 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) \<in> p" and kk: "kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}"
+ show "x\<bullet>k \<le> c"
+ proof (rule ccontr)
+ assume **: "\<not> ?thesis"
+ from this[unfolded not_le]
+ have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
+ using p(2)[unfolded fine_def, rule_format,OF as] by auto
+ with kk obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c"
+ by blast
+ then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
+ 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: "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<ge> c"
+ proof -
+ fix x kk
+ assume as: "(x, kk) \<in> p" and kk: "kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}"
+ show "x\<bullet>k \<ge> c"
+ proof (rule ccontr)
+ assume **: "\<not> ?thesis"
+ from this[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
+ using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
+ with kk obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c"
+ by blast
+ then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
+ 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: "\<And>f P Q. (\<forall>x k. (x, k) \<in> {(x, f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow>
- (\<forall>x k. P x k \<longrightarrow> Q x (f k))" by auto
- have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
+ (\<forall>x k. P x k \<longrightarrow> Q x (f k))"
+ by auto
+ have fin_finite: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
proof -
case goal1
then have "finite ((\<lambda>(x, k). (x, f k)) ` s)"
@@ -3172,50 +3117,38 @@
then show ?case
by (rule rev_finite_subset) auto
qed
- have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
- setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
- setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
- apply (rule setsum.mono_neutral_left)
- prefer 3
- proof
- fix g :: "'a set \<Rightarrow> 'a set"
+ { fix g :: "'a set \<Rightarrow> 'a set"
fix i :: "'a \<times> 'a set"
assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
then obtain x k where xk:
- "i = (x, g k)"
- "(x, k) \<in> p"
- "(x, g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
- by auto
+ "i = (x, g k)" "(x, k) \<in> p"
+ "(x, g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
+ by auto
have "content (g k) = 0"
using xk using content_empty by auto
- then show "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0"
+ then have "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0"
unfolding xk split_conv by auto
- qed auto
- have lem4: "\<And>g. (\<lambda>(x,l). content (g l) *\<^sub>R f x) = (\<lambda>(x,l). content l *\<^sub>R f x) \<circ> (\<lambda>(x,l). (x,g l))"
- by auto
-
+ } note [simp] = this
+ have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
+ setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
+ setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
+ by (rule setsum.mono_neutral_left) auto
let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
+ have d1_fine: "d1 fine ?M1"
+ by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm)
have "norm ((\<Sum>(x, k)\<in>?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 "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = cbox a b \<inter> {x. x\<bullet>k \<le> c}"
unfolding p(8)[symmetric] by auto
fix x l
assume xl: "(x, l) \<in> ?M1"
then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
- have "l' \<subseteq> d1 x'"
- apply (rule order_trans[OF fineD[OF p(2) xl'(3)]])
- apply auto
- done
- then show "l \<subseteq> d1 x"
- unfolding xl' by auto
show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<le> 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 "\<exists>a b. l = cbox a b"
unfolding xl'
using p(6)[OF xl'(3)]
@@ -3240,28 +3173,20 @@
qed
moreover
let ?M2 = "{(x,kk \<inter> {x. x\<bullet>k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
+ have d2_fine: "d2 fine ?M2"
+ by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm)
have "norm ((\<Sum>(x, k)\<in>?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 "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = cbox a b \<inter> {x. x\<bullet>k \<ge> c}"
unfolding p(8)[symmetric] by auto
fix x l
assume xl: "(x, l) \<in> ?M2"
then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
- have "l' \<subseteq> d2 x'"
- apply (rule order_trans[OF fineD[OF p(2) xl'(3)]])
- apply auto
- done
- then show "l \<subseteq> d2 x"
- unfolding xl' by auto
show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<ge> 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 "\<exists>a b. l = cbox a b"
unfolding xl'
@@ -3289,46 +3214,24 @@
have "norm (((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)) < e/2 + e/2"
using norm_add_less by blast
also {
- have *: "\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0"
+ have eq0: "\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0"
using scaleR_zero_left by auto
+ have cont_eq: "\<And>g. (\<lambda>(x,l). content l *\<^sub>R f x) \<circ> (\<lambda>(x,l). (x,g l)) = (\<lambda>(x,l). content (g l) *\<^sub>R f x)"
+ by auto
have "((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) =
(\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)"
by auto
also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) +
(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> 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 *: "\<And>x. x \<in> p \<Longrightarrow>
- (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x +
- (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x =
- (\<lambda>(x,ka). content ka *\<^sub>R f x) x"
- unfolding split_paired_all split_conv
- proof -
+ also have "\<And>x. x \<in> p \<Longrightarrow>
+ (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x +
+ (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x =
+ (\<lambda>(x,ka). content ka *\<^sub>R f x) x"
+ proof clarify
fix a b
assume "(a, b) \<in> p"
from p(6)[OF this] guess u v by (elim exE) note uv=this
@@ -3391,32 +3294,17 @@
norm ((setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + setsum (\<lambda>(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) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1"
note p1=tagged_division_ofD[OF this(1)] this
assume "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> 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 ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) =
- norm ((\<Sum>(x, k)\<in>p1 \<union> 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) \<in> p1 \<inter> p2"
have "(a, b) \<in> 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 \<subseteq> {x. x\<bullet>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 ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) =
+ norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
+ by (subst setsum.union_inter_neutral) (auto simp: p1 p2)
also have "\<dots> < e"
by (rule k d(2) p12 fine_union p1 p2)+
- finally show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" .
- qed
+ finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>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) \<inter> A \<and> d fine p2 \<longrightarrow>
norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e)"
show "?P {x. x \<bullet> k \<le> 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) \<inter> {x. x \<bullet> k \<le> c} \<and> d fine p1 \<and>
- p2 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c} \<and> d fine p2"
+ assume as: "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1"
+ "p2 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p2"
show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>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 \<bullet> k \<ge> 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) \<inter> {x. x \<bullet> k \<ge> c} \<and> d fine p1 \<and>
- p2 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<ge> c} \<and> d fine p2"
+ assume as: "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<ge> c}" "d fine p1"
+ "p2 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<ge> c}" "d fine p2"
show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>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 \<inter> {x. x\<bullet>k \<le> c})) (f (cbox a b \<inter> {x. x\<bullet>k \<ge> c}))"
using assms unfolding operative_def by auto
-lemma operative_trivial: "operative opp f \<Longrightarrow> content (cbox a b) = 0 \<Longrightarrow> f (cbox a b) = neutral opp"
- unfolding operative_def by auto
-
lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
using content_empty unfolding empty_as_interval by auto
@@ -3559,12 +3432,6 @@
subsection \<open>Using additivity of lifted function to encode definedness.\<close>
-lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
- by (metis option.nchotomy)
-
-lemma exists_option: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
- by (metis option.nchotomy)
-
fun lifted where
"lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> '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 "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
- then show "x = Some (neutral opp)"
- apply (induct x)
- defer
- apply rule
+proof -
+ { fix x
+ assume "\<forall>y. lifted opp x y = y \<and> 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 \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
+ (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
proof (cases "x \<in> 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 \<notin> 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 \<notin> s` \<open>finite s\<close> 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 \<open>finite s\<close>
- 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 (\<lambda>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
+ "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
+ by (erule finite_induct) (auto simp: monoidal_lifted)
subsection \<open>Two key instances of additivity.\<close>
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) \<Rightarrow> 'a \<Rightarrow> 'a)"
unfolding monoidal_def neutral_add
@@ -3750,35 +3569,20 @@
lemma operative_integral:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
shows "operative (lifted(op +)) (\<lambda>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 \<in> 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 \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
- (if f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k} then Some (integral (cbox a b \<inter> {x. c \<le> x \<bullet> k}) f) else None)"
+ lifted op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
+ (if f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k} then Some (integral (cbox a b \<inter> {x. c \<le> x \<bullet> 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 "\<not> ?thesis"
then have "f integrable_on cbox a b"
- apply -
unfolding integrable_on_def
apply (rule_tac x="integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f + integral (cbox a b \<inter> {x. x \<bullet> k \<ge> 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 @@
"\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i \<le> b\<bullet>i"
"min (b \<bullet> k) c = c" "max (a \<bullet> 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 "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "a\<bullet>k < c" "c < b\<bullet>k"
- and "l \<in> d"
- and "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
- and k: "k \<in> Basis"
+ and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "a\<bullet>k < c" "c < b\<bullet>k"
+ and "l \<in> d"
+ and "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
+ and k: "k \<in> Basis"
shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subset>
- division_points (cbox a b) d" (is "?D1 \<subset> ?D")
+ division_points (cbox a b) d" (is "?D1 \<subset> ?D")
and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} \<subset>
- division_points (cbox a b) d" (is "?D2 \<subset> ?D")
+ division_points (cbox a b) d" (is "?D2 \<subset> ?D")
proof -
have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>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: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>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 \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
- "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> 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 \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
+ unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
+ using uv[rule_format, of k] ab k
+ by auto
have "\<exists>x. x \<in> ?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)\<bullet>k)" in exI)
- defer
- apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI)
- unfolding division_points_def
- unfolding interval_bounds[OF ab]
- apply (auto simp add:*)
- done
- then show "?D1 \<subset> ?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)\<bullet>k)" in exI, force simp add: *)
+ apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
+ done
+ moreover have "?D1 \<subseteq> ?D"
+ by (auto simp add: assms division_points_subset)
+ ultimately show "?D1 \<subset> ?D"
+ by blast
have *: "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
"interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> 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 "\<exists>x. x \<in> ?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)\<bullet>k)" in exI)
- defer
- apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI)
- unfolding division_points_def
- unfolding interval_bounds[OF ab]
- apply (auto simp add:*)
- done
- then show "?D2 \<subset> ?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)\<bullet>k)" in exI, force simp add: *)
+ apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
+ done
+ moreover have "?D2 \<subseteq> ?D"
+ by (auto simp add: assms division_points_subset)
+ ultimately show "?D2 \<subset> ?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 \<circ> f)"
+ and "inj_on f s"
+ shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
proof -
have *: "\<And>s. finite s \<Longrightarrow> \<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<longrightarrow> x = y \<Longrightarrow>
iterate opp (f ` s) g = iterate opp s (g \<circ> 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 \<circ> f) {x \<in> s. f x \<noteq> a} = support opp (g \<circ> f) s"
unfolding support_def using assms(3) by auto
+ have inj: "inj_on f (support opp (g \<circ> f) {x \<in> s. f x \<noteq> 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 "\<forall>x \<in> s. f x = neutral opp"
- shows "iterate opp s f = neutral opp"
-proof -
- have *: "support opp f s = {}"
+ and "\<forall>x \<in> 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 (\<lambda>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
+ "\<lbrakk>monoidal opp; finite s\<rbrakk>
+ \<Longrightarrow> iterate opp s (\<lambda>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 \<equiv> "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 \<subseteq> 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
--- 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: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x * y \<in> Standard"
by (simp add: star_mult_def)
-lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> divide x y \<in> Standard"
+lemma Standard_divide: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x / y \<in> Standard"
by (simp add: star_divide_def)
lemma Standard_inverse: "x \<in> Standard \<Longrightarrow> inverse x \<in> Standard"
@@ -855,9 +855,9 @@
instance star :: (semidom) semidom ..
instance star :: (semidom_divide) semidom_divide
proof
- show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+ show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
by transfer simp
- show "\<And>a :: 'a star. divide a 0 = 0"
+ show "\<And>a :: 'a star. a div 0 = 0"
by transfer simp
qed
instance star :: (semiring_div) semiring_div
--- 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 \<Rightarrow> 'a::{lattice, order_bot}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+ fixes Q :: "'a::{lattice, order_bot} \<Rightarrow> 'a"
shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
by (auto intro!: funpow_decreasing simp: mono_def)
lemma antimono_funpow:
- fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_top}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+ fixes Q :: "'a::{lattice, order_top} \<Rightarrow> 'a"
shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
by (auto intro!: funpow_increasing simp: antimono_def)
--- 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 \<longleftrightarrow> c = 0 \<or> 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 \<longleftrightarrow> c = 0 \<or> 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 \<noteq> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<open>Units: invertible elements in a ring\<close>
abbreviation is_unit :: "'a \<Rightarrow> bool"
where
- "is_unit x \<equiv> x dvd 1"
+ "is_unit a \<equiv> a dvd 1"
+
+lemma not_is_unit_0 [simp]:
+ "\<not> is_unit 0"
+ by simp
+
+lemma unit_imp_dvd [dest]:
+ "is_unit b \<Longrightarrow> b dvd a"
+ by (rule dvd_trans [of _ 1]) simp_all
+
+lemma unit_dvdE:
+ assumes "is_unit a"
+ obtains c where "a \<noteq> 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 \<noteq> 0" by auto
+ ultimately show thesis using that by blast
+qed
+
+lemma dvd_unit_imp_unit:
+ "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
+ by (rule dvd_trans)
-definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
- "associated x y \<longleftrightarrow> x dvd y \<and> 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 \<Rightarrow> 'a"
-where
- "ring_inv x = 1 div x"
+lemma is_unitE [elim?]:
+ assumes "is_unit a"
+ obtains b where "a \<noteq> 0" and "b \<noteq> 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 \<equiv> "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 \<noteq> 0" and "b \<noteq> 0" by auto
+ from b_def `is_unit a` show "a * b = 1" by simp
+ then have "1 = a * b" ..
+ with b_def `b \<noteq> 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 \<noteq> 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 \<Longrightarrow> is_unit y \<Longrightarrow> is_unit (x * y)"
- by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono)
-
-lemma unit_ring_inv:
- "is_unit y \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
+ by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
+
+lemma unit_div [intro]:
+ "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> a * ring_inv a = 1"
- unfolding ring_inv_def by simp
-
-lemma ring_inv_is_inv2 [simp]:
- "is_unit a \<Longrightarrow> 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 \<longleftrightarrow> 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 \<Longrightarrow> x * y dvd z \<longleftrightarrow> x dvd z"
+lemma dvd_mult_unit_iff:
+ assumes "is_unit b"
+ shows "a dvd c * b \<longleftrightarrow> 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 \<Longrightarrow> x div y dvd z \<longleftrightarrow> x dvd z"
- by (subst unit_ring_inv) (assumption, simp add: mult_unit_dvd_iff)
-
-lemma dvd_mult_unit_iff:
- "is_unit y \<Longrightarrow> x dvd z * y \<longleftrightarrow> 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 \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
+ by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
lemma dvd_div_unit_iff:
- "is_unit y \<Longrightarrow> x dvd z div y \<longleftrightarrow> x dvd z"
- by (subst unit_ring_inv) (assumption, simp add: dvd_mult_unit_iff)
+ "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> 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 -- \<open>FIXME consider fact collection\<close>
-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 \<Longrightarrow> b * (1 div a) = b div a"
+ by (erule is_unitE [of _ b]) simp
-lemma unit_div [intro]:
- "is_unit x \<Longrightarrow> is_unit y \<Longrightarrow> 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 \<Longrightarrow> b div a * a = b"
+ by (rule dvd_div_mult_self) auto
+
+lemma unit_div_1_div_1 [simp]:
+ "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
+ by (erule is_unitE) simp
lemma unit_div_mult_swap:
- "is_unit z \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> (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 \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
+ by (auto elim: is_unitE)
-lemma unit_imp_dvd [dest]:
- "is_unit y \<Longrightarrow> y dvd x"
- by (rule dvd_trans [of _ 1]) simp_all
+lemma unit_eq_div2:
+ "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> 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 \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
+ using assms mult_cancel_left [of a b c] by auto
-lemma dvd_unit_imp_unit:
- "is_unit y \<Longrightarrow> x dvd y \<Longrightarrow> is_unit x"
- by (rule dvd_trans)
+lemma unit_mult_right_cancel:
+ "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> 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 \<longleftrightarrow> b = c"
+proof -
+ from assms have "is_unit (1 div a)" by simp
+ then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
+ by (rule unit_mult_right_cancel)
+ with assms show ?thesis by simp
+qed
+
+
+text \<open>Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \<close>
-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 \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
+
+lemma associatedI:
+ "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
+ by (simp add: associated_def)
+
+lemma associatedD1:
+ "associated a b \<Longrightarrow> a dvd b"
+ by (simp add: associated_def)
+
+lemma associatedD2:
+ "associated a b \<Longrightarrow> 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 \<longleftrightarrow> associated a b"
+ by (auto intro: associatedI dest: associatedD1 associatedD2)
+
+lemma associated_trans:
+ "associated a b \<Longrightarrow> associated b c \<Longrightarrow> 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 \<Longrightarrow> associated y x"
- by (simp add: associated_def)
-
lemma associated_0 [simp]:
"associated 0 b \<longleftrightarrow> b = 0"
"associated a 0 \<longleftrightarrow> a = 0"
- unfolding associated_def by simp_all
+ by (auto dest: associatedD1 associatedD2)
lemma associated_unit:
- "is_unit x \<Longrightarrow> associated x y \<Longrightarrow> 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 \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
+ using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
-lemma not_is_unit_0 [simp]:
- "\<not> is_unit 0"
- by auto
-
-lemma unit_mult_left_cancel:
- assumes "is_unit x"
- shows "(x * y) = (x * z) \<longleftrightarrow> y = z"
-proof -
- from assms have "x \<noteq> 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 \<Longrightarrow> (y * x) = (z * x) \<longleftrightarrow> y = z"
- by (simp add: ac_simps unit_mult_left_cancel)
-
-lemma unit_div_cancel:
- "is_unit x \<Longrightarrow> (y div x) = (z div x) \<longleftrightarrow> 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 \<Longrightarrow> x div y = z \<longleftrightarrow> 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 \<Longrightarrow> x = z div y \<longleftrightarrow> 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 \<longleftrightarrow> (\<exists>z. is_unit z \<and> x = z * y)"
-proof
- assume "associated x y"
- show "\<exists>z. is_unit z \<and> x = z * y"
- proof (cases "x = 0")
- assume "x = 0"
- then show "\<exists>z. is_unit z \<and> x = z * y" using `associated x y`
- by (intro exI[of _ 1], simp add: associated_def)
- next
- assume [simp]: "x \<noteq> 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 "\<exists>z. is_unit z \<and> 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) \<Longrightarrow> 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) \<longleftrightarrow> x = 1"
- by simp
-
lemma is_unit_int:
- "is_unit (x::int) \<longleftrightarrow> x = 1 \<or> x = -1"
+ "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> 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 \<noteq> 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 \<Rightarrow> nat"
- fixes normalisation_factor :: "'a \<Rightarrow> 'a"
+ fixes normalization_factor :: "'a \<Rightarrow> 'a"
assumes mod_size_less [simp]:
"b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
assumes size_mult_mono:
"b \<noteq> 0 \<Longrightarrow> euclidean_size (a * b) \<ge> euclidean_size a"
- assumes normalisation_factor_is_unit [intro,simp]:
- "a \<noteq> 0 \<Longrightarrow> 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 \<Longrightarrow> normalisation_factor x = x"
- assumes normalisation_factor_0 [simp]: "normalisation_factor 0 = 0"
+ assumes normalization_factor_is_unit [intro,simp]:
+ "a \<noteq> 0 \<Longrightarrow> 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 \<Longrightarrow> normalization_factor a = a"
+ assumes normalization_factor_0 [simp]: "normalization_factor 0 = 0"
begin
-lemma normalisation_factor_dvd [simp]:
- "a \<noteq> 0 \<Longrightarrow> normalisation_factor a dvd b"
+lemma normalization_factor_dvd [simp]:
+ "a \<noteq> 0 \<Longrightarrow> 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 \<longleftrightarrow> x = 0"
+lemma normalization_factor_0_iff [simp]:
+ "normalization_factor a = 0 \<longleftrightarrow> a = 0"
proof
- assume "normalisation_factor x = 0"
- hence "\<not> 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 "\<not> 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 \<noteq> 0"
+ let ?nf = "normalization_factor"
+ from normalization_factor_is_unit[OF `a \<noteq> 0`] have "?nf a \<noteq> 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 \<noteq> 0`
+ by simp
+ also have "?nf (?nf a) = ?nf a" using `a \<noteq> 0`
+ normalization_factor_is_unit normalization_factor_unit by simp
+ finally have "normalization_factor (a div normalization_factor a) = 1"
+ using `?nf a \<noteq> 0` by (metis div_mult_self2_is_id div_self)
+ with `a \<noteq> 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 \<longleftrightarrow> 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 \<noteq> 0"
- let ?nf = "normalisation_factor"
- from normalisation_factor_is_unit[OF `x \<noteq> 0`] have "?nf x \<noteq> 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 \<noteq> 0`
- by simp
- also have "?nf (?nf x) = ?nf x" using `x \<noteq> 0`
- normalisation_factor_is_unit normalisation_factor_unit by simp
- finally show ?thesis using `x \<noteq> 0` and `?nf x \<noteq> 0`
- by (metis div_mult_self2_is_id div_self)
-qed
-
-lemma normalisation_0_iff [simp]:
- "x div normalisation_factor x = 0 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<noteq> 0" "b \<noteq> 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 \<noteq> 0` `b \<noteq> 0` have "\<exists>z. is_unit z \<and> a = z * b"
+ with `a \<noteq> 0` `b \<noteq> 0` have "\<exists>c. is_unit c \<and> 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 \<noteq> 0" "b \<noteq> 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 \<Longrightarrow> normalisation_factor a \<in> {0, 1} \<Longrightarrow> normalisation_factor b \<in> {0, 1} \<Longrightarrow> a = b"
+ "associated a b \<Longrightarrow> normalization_factor a \<in> {0, 1} \<Longrightarrow> normalization_factor b \<in> {0, 1} \<Longrightarrow> 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 \<Rightarrow> 'a \<Rightarrow> '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 \<circ> snd)", simp_all)
@@ -378,17 +451,17 @@
definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> 'a"
where
- "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) then
- let l = SOME l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l =
- (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n)
- in l div normalisation_factor l
+ "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
+ let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
+ (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)
+ in l div normalization_factor l
else 0)"
definition Gcd_eucl :: "'a set \<Rightarrow> '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 \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
+ "b \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0 \<Longrightarrow> gcd y (x mod y) dvd y"
- assume IH2: "y \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0 \<Longrightarrow> gcd b (a mod b) dvd b"
+ assume IH2: "b \<noteq> 0 \<Longrightarrow> gcd b (a mod b) dvd (a mod b)"
- have "gcd x y dvd x \<and> gcd x y dvd y"
- proof (cases "y = 0")
+ have "gcd a b dvd a \<and> 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 \<Longrightarrow> 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 \<Longrightarrow> k dvd y \<Longrightarrow> 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 \<Longrightarrow> k dvd b \<Longrightarrow> 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 \<noteq> 0"
+ assume "b \<noteq> 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 \<longleftrightarrow> k dvd x \<and> k dvd y"
+ "k dvd gcd a b \<longleftrightarrow> k dvd a \<and> 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 \<longleftrightarrow> x = 0 \<and> y = 0"
+ "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> 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 \<and> 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 \<noteq> 0 \<Longrightarrow> ?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 \<and> 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 \<noteq> 0 \<Longrightarrow> ?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 \<Longrightarrow> k dvd y \<Longrightarrow> (\<And>l. l dvd x \<Longrightarrow> l dvd y \<Longrightarrow> l dvd k)
- \<Longrightarrow> normalisation_factor k = (if k = 0 then 0 else 1) \<Longrightarrow> k = gcd x y"
+ "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> (\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd k)
+ \<Longrightarrow> normalization_factor k = (if k = 0 then 0 else 1) \<Longrightarrow> 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 \<and> d dvd b \<and>
- normalisation_factor d = (if d = 0 then 0 else 1) \<and>
+ normalization_factor d = (if d = 0 then 0 else 1) \<and>
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> gcd x y = x div normalisation_factor x"
+ "a dvd b \<Longrightarrow> 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 \<longleftrightarrow> m dvd n"
+lemma gcd_proj1_iff: "gcd m n = m div normalization_factor m \<longleftrightarrow> 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 \<noteq> 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 \<longleftrightarrow> n dvd m"
+lemma gcd_proj2_iff: "gcd m n = n div normalization_factor n \<longleftrightarrow> 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 \<Longrightarrow> gcd (x*a) y = gcd x y"
+lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> 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 \<Longrightarrow> gcd x (y*a) = gcd x y"
+lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> 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 \<Longrightarrow> gcd (x div a) y = gcd x y"
- by (simp add: unit_ring_inv gcd_mult_unit1)
+lemma gcd_div_unit1: "is_unit a \<Longrightarrow> 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 \<Longrightarrow> gcd x (y div a) = gcd x y"
- by (simp add: unit_ring_inv gcd_mult_unit2)
+lemma gcd_div_unit2: "is_unit a \<Longrightarrow> 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 \<Longrightarrow> (k dvd m * n) = (k dvd m)"
+ "gcd c b = 1 \<Longrightarrow> (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: "(\<And>l. \<lbrakk>l dvd x; l dvd y\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd x y = 1"
+lemma coprimeI: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
by (rule sym, rule gcdI, simp_all)
lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> 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 \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
+ assumes c: "gcd a b \<noteq> 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 \<noteq> 0 \<or> b \<noteq> 0" by simp
+ from c have "a \<noteq> 0 \<or> b \<noteq> 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 \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> is_unit x"
- apply (subgoal_tac "x dvd gcd a b")
+ "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> 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 \<noteq> 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 \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> 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]:
- "(\<forall>i\<in>A. gcd (f i) x = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) x = 1"
+ "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>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 \<noteq> 0"
hence "gcd a b \<noteq> 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 \<noteq> 0` have "... = a * b div ?nf (a*b)"
- by (simp_all add: unit_ring_inv'1 unit_ring_inv)
+ also from `a * b \<noteq> 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 \<noteq> 0"
- hence "gcd x y \<noteq> 0" by simp
- let ?c = "ring_inv (normalisation_factor (x*y))"
- from `x * y \<noteq> 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 \<noteq> 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 \<noteq> 0"
+ hence "gcd a b \<noteq> 0" by simp
+ let ?c = "1 div normalization_factor (a * b)"
+ from `a * b \<noteq> 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 \<noteq> 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:
"\<lbrakk>a dvd k; b dvd k\<rbrakk> \<Longrightarrow> lcm a b dvd k"
proof (cases "k = 0")
- let ?nf = normalisation_factor
+ let ?nf = normalization_factor
assume "k \<noteq> 0"
hence "is_unit (?nf k)" by simp
hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
@@ -1047,7 +1120,7 @@
lemma lcm_zero:
"lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
proof -
- let ?nf = normalisation_factor
+ let ?nf = normalization_factor
{
assume "a \<noteq> 0" "b \<noteq> 0"
hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
@@ -1064,67 +1137,67 @@
lemma gcd_lcm:
assumes "lcm a b \<noteq> 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 \<noteq> 0" by (simp add: lcm_zero)
- let ?c = "normalisation_factor (a*b)"
+ let ?c = "normalization_factor (a * b)"
from `lcm a b \<noteq> 0` have "?c \<noteq> 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 \<noteq> 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 \<noteq> 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 \<or> b = 0 then 0 else 1)"
+lemma normalization_factor_lcm [simp]:
+ "normalization_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
proof (cases "a = 0 \<or> 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:
- "\<lbrakk>x dvd k; y dvd k; \<And>l. x dvd l \<Longrightarrow> y dvd l \<Longrightarrow> k dvd l;
- normalisation_factor k = (if k = 0 then 0 else 1)\<rbrakk> \<Longrightarrow> k = lcm x y"
+ "\<lbrakk>a dvd k; b dvd k; \<And>l. a dvd l \<Longrightarrow> b dvd l \<Longrightarrow> k dvd l;
+ normalization_factor k = (if k = 0 then 0 else 1)\<rbrakk> \<Longrightarrow> 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 \<and> 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 "\<dots> = 1" using `is_unit a \<and> 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 \<and> b dvd d \<and>
- normalisation_factor d = (if d = 0 then 0 else 1) \<and>
+ normalization_factor d = (if d = 0 then 0 else 1) \<and>
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> 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 \<Longrightarrow> lcm a b = a * b div normalisation_factor (a*b)"
+ "gcd a b = 1 \<Longrightarrow> lcm a b = a * b div normalization_factor (a*b)"
by (subst lcm_gcd) simp
lemma lcm_proj1_if_dvd:
- "y dvd x \<Longrightarrow> lcm x y = x div normalisation_factor x"
- by (cases "x = 0") (simp, rule sym, rule lcmI, simp_all)
+ "b dvd a \<Longrightarrow> 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 \<Longrightarrow> lcm x y = y div normalisation_factor y"
- using lcm_proj1_if_dvd [of x y] by (simp add: ac_simps)
+ "a dvd b \<Longrightarrow> 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 \<longleftrightarrow> n dvd m"
+ "lcm m n = m div normalization_factor m \<longleftrightarrow> 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 \<noteq> 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 \<longleftrightarrow> m dvd n"
+ "lcm m n = n div normalization_factor n \<longleftrightarrow> 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 \<Longrightarrow> lcm (x*a) y = lcm x y"
+ "is_unit a \<Longrightarrow> 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 \<Longrightarrow> lcm x (y*a) = lcm x y"
- using lcm_mult_unit1 [of a y x] by (simp add: ac_simps)
+ "is_unit a \<Longrightarrow> 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 \<Longrightarrow> lcm (x div a) y = lcm x y"
- by (simp add: unit_ring_inv lcm_mult_unit1)
+ "is_unit a \<Longrightarrow> 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 \<Longrightarrow> lcm x (y div a) = lcm x y"
- by (simp add: unit_ring_inv lcm_mult_unit2)
+ "is_unit a \<Longrightarrow> 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 \<in> A \<Longrightarrow> x dvd Lcm A"
- and Lcm_dvd [simp]: "(\<forall>x\<in>A. x dvd l') \<Longrightarrow> 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 \<in> A \<Longrightarrow> a dvd Lcm A"
+ and Lcm_dvd [simp]: "(\<forall>a\<in>A. a dvd l') \<Longrightarrow> Lcm A dvd l'"
+ and normalization_factor_Lcm [simp]:
+ "normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
proof -
- have "(\<forall>x\<in>A. x dvd Lcm A) \<and> (\<forall>l'. (\<forall>x\<in>A. x dvd l') \<longrightarrow> Lcm A dvd l') \<and>
- normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
- proof (cases "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l)")
+ have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm A dvd l') \<and>
+ normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
+ proof (cases "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>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 \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l\<^sub>0)" by blast
- def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
- def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
- have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
+ then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
+ def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
+ def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
+ have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> 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 \<noteq> 0" and "\<forall>x\<in>A. x dvd l" and "euclidean_size l = n"
+ from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n"
unfolding l_def by simp_all
{
- fix l' assume "\<forall>x\<in>A. x dvd l'"
- with `\<forall>x\<in>A. x dvd l` have "\<forall>x\<in>A. x dvd gcd l l'" by (auto intro: gcd_greatest)
+ fix l' assume "\<forall>a\<in>A. a dvd l'"
+ with `\<forall>a\<in>A. a dvd l` have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
moreover from `l \<noteq> 0` have "gcd l l' \<noteq> 0" by simp
- ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
+ ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
by (intro exI[of _ "gcd l l'"], auto)
hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
moreover have "euclidean_size (gcd l l') \<le> n"
@@ -1348,26 +1421,26 @@
hence "l dvd l'" by (blast dest: dvd_gcd_D2)
}
- with `(\<forall>x\<in>A. x dvd l)` and normalisation_factor_is_unit[OF `l \<noteq> 0`] and `l \<noteq> 0`
- have "(\<forall>x\<in>A. x dvd l div normalisation_factor l) \<and>
- (\<forall>l'. (\<forall>x\<in>A. x dvd l') \<longrightarrow> l div normalisation_factor l dvd l') \<and>
- normalisation_factor (l div normalisation_factor l) =
- (if l div normalisation_factor l = 0 then 0 else 1)"
+ with `(\<forall>a\<in>A. a dvd l)` and normalization_factor_is_unit[OF `l \<noteq> 0`] and `l \<noteq> 0`
+ have "(\<forall>a\<in>A. a dvd l div normalization_factor l) \<and>
+ (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> l div normalization_factor l dvd l') \<and>
+ 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 \<in> A" then show "x dvd Lcm A" using A by blast}
- {fix l' assume "\<forall>x\<in>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 \<in> A" then show "a dvd Lcm A" using A by blast}
+ {fix l' assume "\<forall>a\<in>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:
- "(\<And>x. x\<in>A \<Longrightarrow> x dvd l) \<Longrightarrow> (\<And>l'. (\<forall>x\<in>A. x dvd l') \<Longrightarrow> l dvd l') \<Longrightarrow>
- normalisation_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Lcm A"
+ "(\<And>a. a\<in>A \<Longrightarrow> a dvd l) \<Longrightarrow> (\<And>l'. (\<forall>a\<in>A. a dvd l') \<Longrightarrow> l dvd l') \<Longrightarrow>
+ normalization_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> 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 \<longleftrightarrow> (\<forall>x\<in>A. is_unit x)"
+ "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
proof
assume "Lcm A = 1"
- then show "\<forall>x\<in>A. is_unit x" by auto
+ then show "\<forall>a\<in>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}) \<union> {x\<in>A. is_unit x} = A" by blast
- hence "Lcm A = lcm (Lcm (A - {x. is_unit x})) (Lcm {x\<in>A. is_unit x})"
+ have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast
+ hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
by (simp add: Lcm_Un[symmetric])
- also have "Lcm {x\<in>A. is_unit x} = 1" by (simp add: Lcm_1_iff)
+ also have "Lcm {a\<in>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 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l))"
+ "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
proof
assume "Lcm A = 0"
- show "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l))"
+ show "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
proof
- assume ex: "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l)"
- then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l\<^sub>0)" by blast
- def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
- def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
- have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l) \<and> euclidean_size l = n"
+ assume ex: "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)"
+ then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
+ def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
+ def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
+ have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> 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 \<noteq> 0" unfolding l_def by simp_all
- hence "l div normalisation_factor l \<noteq> 0" by simp
- also from ex have "l div normalisation_factor l = Lcm A"
+ hence "l div normalization_factor l \<noteq> 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 "\<forall>x\<in>A. x dvd \<Prod>A" by blast
- ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l)" by blast
+ moreover from `finite A` have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
+ ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
}
ultimately show "Lcm A = 0 \<longleftrightarrow> 0 \<in> A" by blast
qed
lemma Lcm_no_multiple:
- "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>x\<in>A. \<not>x dvd m)) \<Longrightarrow> Lcm A = 0"
+ "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
proof -
- assume "\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>x\<in>A. \<not>x dvd m)"
- hence "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l))" by blast
+ assume "\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)"
+ hence "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>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 "\<forall>x\<in>A. x dvd l" by (blast intro: dvd_trans dvd_Lcm)
+ hence "\<forall>a\<in>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 \<noteq> {}"
assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
- shows "Lcm A = \<Prod>A div normalisation_factor (\<Prod>A)"
+ shows "Lcm A = \<Prod>A div normalization_factor (\<Prod>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 = \<Prod>A div normalisation_factor (\<Prod>A)" by blast
+ also from insert have "Lcm A = \<Prod>A div normalization_factor (\<Prod>A)" by blast
also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
- with insert have "lcm a (\<Prod>A) = \<Prod>(insert a A) div normalisation_factor (\<Prod>(insert a A))"
+ with insert have "lcm a (\<Prod>A) = \<Prod>(insert a A) div normalization_factor (\<Prod>(insert a A))"
by (simp add: lcm_coprime)
finally show ?case .
qed simp
lemma Lcm_coprime':
"card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1)
- \<Longrightarrow> Lcm A = \<Prod>A div normalisation_factor (\<Prod>A)"
+ \<Longrightarrow> Lcm A = \<Prod>A div normalization_factor (\<Prod>A)"
by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
lemma Gcd_Lcm:
- "Gcd A = Lcm {d. \<forall>x\<in>A. d dvd x}"
+ "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}"
by (simp add: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def)
-lemma Gcd_dvd [simp]: "x \<in> A \<Longrightarrow> Gcd A dvd x"
- and dvd_Gcd [simp]: "(\<forall>x\<in>A. g' dvd x) \<Longrightarrow> 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 \<in> A \<Longrightarrow> Gcd A dvd a"
+ and dvd_Gcd [simp]: "(\<forall>a\<in>A. g' dvd a) \<Longrightarrow> 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 \<in> A"
- hence "Lcm {d. \<forall>x\<in>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 \<in> A"
+ hence "Lcm {d. \<forall>a\<in>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 "\<forall>x\<in>A. g' dvd x"
- hence "g' dvd Lcm {d. \<forall>x\<in>A. d dvd x}" by (intro dvd_Lcm) blast
+ fix g' assume "\<forall>a\<in>A. g' dvd a"
+ hence "g' dvd Lcm {d. \<forall>a\<in>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:
- "(\<And>x. x\<in>A \<Longrightarrow> l dvd x) \<Longrightarrow> (\<And>l'. (\<forall>x\<in>A. l' dvd x) \<Longrightarrow> l' dvd l) \<Longrightarrow>
- normalisation_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Gcd A"
+ "(\<And>a. a\<in>A \<Longrightarrow> l dvd a) \<Longrightarrow> (\<And>l'. (\<forall>a\<in>A. l' dvd a) \<Longrightarrow> l' dvd l) \<Longrightarrow>
+ normalization_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> 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. \<forall>x\<in>A. x dvd m}"
+ "Lcm A = Gcd {m. \<forall>a\<in>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 "\<forall>x\<in>A. l dvd x" by (blast intro: dvd_trans Gcd_dvd)
+ hence "\<forall>a\<in>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 \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> '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) \<Rightarrow> (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 \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
(s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
- by (subst euclid_ext.simps, simp)
+ by (subst euclid_ext.simps) simp
definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> '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) \<Rightarrow> 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) \<Rightarrow> 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: "\<exists>s t. s * x + t * y = gcd x y"
+lemma bezout: "\<exists>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 \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0 \<Longrightarrow> 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 \<Rightarrow> 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 \<circ> abs :: int \<Rightarrow> nat)"
definition [simp]:
- "normalisation_factor_int = (sgn :: int \<Rightarrow> int)"
+ "normalization_factor_int = (sgn :: int \<Rightarrow> int)"
instance proof
case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib)
@@ -1760,4 +1838,3 @@
end
end
-
--- 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 \<noteq> 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
--- 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)
--- 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 \<Rightarrow> 'a \<Rightarrow> 'a"
+ fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
@@ -567,8 +567,8 @@
begin
lemma [field_simps]:
- shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
- and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
+ shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+ and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (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 \<Longrightarrow> (a - b) * c = a * c - b * c"
- and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
+ shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+ and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> 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 \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
class semidom_divide = semidom + divide +
- assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
- assumes divide_zero [simp]: "divide a 0 = 0"
+ assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
+ assumes divide_zero [simp]: "a div 0 = 0"
begin
lemma nonzero_mult_divide_cancel_left [simp]:
- "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
+ "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
end
--- 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)"
--- 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
--- 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\<Colon>preal)"
+definition "R div S = R * inverse (S\<Colon>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 \<le> (w::real) \<longleftrightarrow>