--- a/NEWS Sun Feb 22 10:22:30 2009 +0100
+++ b/NEWS Sun Feb 22 10:22:46 2009 +0100
@@ -367,6 +367,49 @@
mult_div ~> div_mult_self2_is_id
mult_mod ~> mod_mult_self2_is_0
+* HOL/IntDiv: removed most (all?) lemmas that are instances of class-based
+generalizations (from Divides and Ring_and_Field).
+INCOMPATIBILITY. Rename old lemmas as follows:
+
+dvd_diff -> nat_dvd_diff
+dvd_zminus_iff -> dvd_minus_iff
+nat_mod_add_left_eq -> mod_add_left_eq
+nat_mod_add_right_eq -> mod_add_right_eq
+nat_mod_div_trivial -> mod_div_trivial
+nat_mod_mod_trivial -> mod_mod_trivial
+zdiv_zadd_self1 -> div_add_self1
+zdiv_zadd_self2 -> div_add_self2
+zdiv_zmult_self2 -> div_mult_self1_is_id
+zdvd_triv_left -> dvd_triv_left
+zdvd_triv_right -> dvd_triv_right
+zdvd_zmult_cancel_disj -> dvd_mult_cancel_left
+zmod_zadd_left_eq -> mod_add_left_eq
+zmod_zadd_right_eq -> mod_add_right_eq
+zmod_zadd_self1 -> mod_add_self1
+zmod_zadd_self2 -> mod_add_self2
+zmod_zdiff1_eq -> mod_diff_eq
+zmod_zdvd_zmod -> mod_mod_cancel
+zmod_zmod_cancel -> mod_mod_cancel
+zmod_zmult_self1 -> mod_mult_self2_is_0
+zmod_zmult_self2 -> mod_mult_self1_is_0
+zmod_1 -> mod_by_1
+zdiv_1 -> div_by_1
+zdvd_abs1 -> abs_dvd_iff
+zdvd_abs2 -> dvd_abs_iff
+zdvd_refl -> dvd_refl
+zdvd_trans -> dvd_trans
+zdvd_zadd -> dvd_add
+zdvd_zdiff -> dvd_diff
+zdvd_zminus_iff -> dvd_minus_iff
+zdvd_zminus2_iff -> minus_dvd_iff
+zdvd_zmultD -> dvd_mult_right
+zdvd_zmultD2 -> dvd_mult_left
+zdvd_zmult_mono -> mult_dvd_mono
+zdvd_0_right -> dvd_0_right
+zdvd_0_left -> dvd_0_left_iff
+zdvd_1_left -> one_dvd
+zminus_dvd_iff -> minus_dvd_iff
+
* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
zlcm (for int); carried together from various gcd/lcm developements in
the HOL Distribution. zgcd and zlcm replace former igcd and ilcm;
--- a/src/HOL/Algebra/Exponent.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Algebra/Exponent.thy Sun Feb 22 10:22:46 2009 +0100
@@ -215,7 +215,7 @@
prefer 2 apply (blast intro: dvd_mult2)
apply (drule dvd_diffD1)
apply assumption
- prefer 2 apply (blast intro: dvd_diff)
+ prefer 2 apply (blast intro: nat_dvd_diff)
apply (drule gr0_implies_Suc, auto)
done
@@ -231,7 +231,7 @@
prefer 2 apply (blast intro: dvd_mult2)
apply (drule dvd_diffD1)
apply assumption
- prefer 2 apply (blast intro: dvd_diff)
+ prefer 2 apply (blast intro: nat_dvd_diff)
apply (drule less_imp_Suc_add, auto)
done
--- a/src/HOL/Decision_Procs/Cooper.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Sun Feb 22 10:22:46 2009 +0100
@@ -620,7 +620,7 @@
{assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def)}
moreover
{assume i1: "abs i = 1"
- from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
+ from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
by (cases "i > 0", simp_all)}
moreover
@@ -640,7 +640,7 @@
{assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def)}
moreover
{assume i1: "abs i = 1"
- from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
+ from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
apply (cases "i > 0", simp_all) done}
moreover
@@ -990,7 +990,7 @@
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
moreover
{assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def)
- hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
+ hence ?case using prems by (simp del: zlfm.simps)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"]
@@ -1005,7 +1005,7 @@
moreover
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
+ hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ]
by (simp add: Let_def split_def) }
ultimately show ?case by blast
next
@@ -1019,7 +1019,7 @@
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
moreover
{assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def)
- hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
+ hence ?case using prems by (simp del: zlfm.simps)}
moreover
{assume "?c=0" and "j\<noteq>0" hence ?case
using zsplit0_I[OF spl, where x="i" and bs="bs"]
@@ -1034,7 +1034,7 @@
moreover
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
- hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
+ hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
by (simp add: Let_def split_def)}
ultimately show ?case by blast
qed auto
@@ -1092,10 +1092,10 @@
using lin ad d
proof(induct p rule: iszlfm.induct)
case (9 i c e) thus ?case using d
- by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+ by (simp add: dvd_trans[of "i" "d" "d'"])
next
case (10 i c e) thus ?case using d
- by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+ by (simp add: dvd_trans[of "i" "d" "d'"])
qed simp_all
lemma \<delta> : assumes lin:"iszlfm p"
@@ -1354,7 +1354,7 @@
case (9 j c e) hence nb: "numbound0 e" by simp
have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
also have "\<dots> = (j dvd (- (c*x - ?e)))"
- by (simp only: zdvd_zminus_iff)
+ by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
by (simp add: algebra_simps)
@@ -1366,7 +1366,7 @@
case (10 j c e) hence nb: "numbound0 e" by simp
have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
also have "\<dots> = (j dvd (- (c*x - ?e)))"
- by (simp only: zdvd_zminus_iff)
+ by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
by (simp add: algebra_simps)
@@ -1392,7 +1392,7 @@
and dr: "d\<beta> p l"
and d: "l dvd l'"
shows "d\<beta> p l'"
-using dr linp zdvd_trans[where n="l" and k="l'", simplified d]
+using dr linp dvd_trans[of _ "l" "l'", simplified d]
by (induct p rule: iszlfm.induct) simp_all
lemma \<alpha>_l: assumes lp: "iszlfm p"
@@ -1431,7 +1431,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
@@ -1449,7 +1449,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
@@ -1467,7 +1467,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
@@ -1485,7 +1485,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
@@ -1505,7 +1505,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
@@ -1523,7 +1523,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
@@ -1541,7 +1541,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
@@ -1558,7 +1558,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
--- a/src/HOL/Decision_Procs/Ferrack.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sun Feb 22 10:22:46 2009 +0100
@@ -501,9 +501,9 @@
assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
shows "dvdnumcoeff t g"
using dgt' gdg
- by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg])
+ by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
-declare zdvd_trans [trans add]
+declare dvd_trans [trans add]
lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
by arith
--- a/src/HOL/Decision_Procs/MIR.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Sun Feb 22 10:22:46 2009 +0100
@@ -132,13 +132,13 @@
assume d: "real d rdvd t"
from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real (floor t) = t" by auto
- from iffD2[OF zdvd_abs1] d2 have "(abs d) dvd (floor t)" by blast
+ from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast
with ti int_rdvd_real[symmetric] have "real (abs d) rdvd t" by blast
thus "abs (real d) rdvd t" by simp
next
assume "abs (real d) rdvd t" hence "real (abs d) rdvd t" by simp
with int_rdvd_real[where i="abs d" and x="t"] have d2: "abs d dvd floor t" and ti: "real (floor t) =t" by auto
- from iffD1[OF zdvd_abs1] d2 have "d dvd floor t" by blast
+ from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast
with ti int_rdvd_real[symmetric] show "real d rdvd t" by blast
qed
@@ -675,9 +675,9 @@
assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
shows "dvdnumcoeff t g"
using dgt' gdg
- by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg])
-
-declare zdvd_trans [trans add]
+ by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
+
+declare dvd_trans [trans add]
lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
by arith
@@ -2114,10 +2114,10 @@
using lin ad d
proof(induct p rule: iszlfm.induct)
case (9 i c e) thus ?case using d
- by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+ by (simp add: dvd_trans[of "i" "d" "d'"])
next
case (10 i c e) thus ?case using d
- by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+ by (simp add: dvd_trans[of "i" "d" "d'"])
qed simp_all
lemma \<delta> : assumes lin:"iszlfm p bs"
@@ -2496,7 +2496,7 @@
and dr: "d\<beta> p l"
and d: "l dvd l'"
shows "d\<beta> p l'"
-using dr linp zdvd_trans[where n="l" and k="l'", simplified d]
+using dr linp dvd_trans[of _ "l" "l'", simplified d]
by (induct p rule: iszlfm.induct) simp_all
lemma \<alpha>_l: assumes lp: "iszlfm p (a#bs)"
@@ -2535,7 +2535,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e < (0\<Colon>real)) =
@@ -2553,7 +2553,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<le> (0\<Colon>real)) =
@@ -2571,7 +2571,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e > (0\<Colon>real)) =
@@ -2589,7 +2589,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<ge> (0\<Colon>real)) =
@@ -2607,7 +2607,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e = (0\<Colon>real)) =
@@ -2625,7 +2625,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<noteq> (0\<Colon>real)) =
@@ -2643,7 +2643,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)" by simp
@@ -2660,7 +2660,7 @@
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: zdiv_self[OF cnz])
- have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+ have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
by simp
hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)" by simp
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Feb 22 10:22:46 2009 +0100
@@ -28,11 +28,9 @@
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
-val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
+val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
val int_mod_add_eq = @{thm mod_add_eq} RS sym;
-val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
-val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
@@ -70,14 +68,13 @@
val (t,np,nh) = prepare_for_linz q g
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset = HOL_basic_ss
- addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq,
- nat_mod_add_right_eq, int_mod_add_eq,
- int_mod_add_right_eq, int_mod_add_left_eq,
+ addsimps [refl,nat_mod_add_eq, mod_add_left_eq,
+ mod_add_right_eq, int_mod_add_eq,
nat_div_add_eq, int_div_add_eq,
@{thm mod_self}, @{thm "zmod_self"},
@{thm mod_by_0}, @{thm div_by_0},
@{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
- @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
Suc_plus1]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun Feb 22 10:22:46 2009 +0100
@@ -32,11 +32,9 @@
val imp_le_cong = @{thm imp_le_cong};
val conj_le_cong = @{thm conj_le_cong};
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
-val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
+val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
+val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
val int_mod_add_eq = @{thm mod_add_eq} RS sym;
-val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
-val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
--- a/src/HOL/Decision_Procs/mir_tac.ML Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Feb 22 10:22:46 2009 +0100
@@ -47,11 +47,9 @@
val imp_le_cong = @{thm "imp_le_cong"};
val conj_le_cong = @{thm "conj_le_cong"};
val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
-val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
-val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
+val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
+val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
-val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
-val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
@@ -99,7 +97,7 @@
addsimps [refl,nat_mod_add_eq,
@{thm "mod_self"}, @{thm "zmod_self"},
@{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
- @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
@{thm "Suc_plus1"}]
addsimps @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Divides.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Divides.thy Sun Feb 22 10:22:46 2009 +0100
@@ -813,9 +813,9 @@
interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
-lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
- unfolding dvd_def
- by (blast intro: diff_mult_distrib2 [symmetric])
+lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
+unfolding dvd_def
+by (blast intro: diff_mult_distrib2 [symmetric])
lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
@@ -823,7 +823,7 @@
done
lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
-by (drule_tac m = m in dvd_diff, auto)
+by (drule_tac m = m in nat_dvd_diff, auto)
lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
apply (rule iffI)
@@ -832,7 +832,7 @@
apply (subgoal_tac "n = (n+k) -k")
prefer 2 apply simp
apply (erule ssubst)
- apply (erule dvd_diff)
+ apply (erule nat_dvd_diff)
apply (rule dvd_refl)
done
--- a/src/HOL/Extraction/Euclid.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Extraction/Euclid.thy Sun Feb 22 10:22:46 2009 +0100
@@ -189,7 +189,7 @@
assume pn: "p \<le> n"
from `prime p` have "0 < p" by (rule prime_g_zero)
then have "p dvd n!" using pn by (rule dvd_factorial)
- with dvd have "p dvd ?k - n!" by (rule dvd_diff)
+ with dvd have "p dvd ?k - n!" by (rule nat_dvd_diff)
then have "p dvd 1" by simp
with prime show False using prime_nd_one by auto
qed
--- a/src/HOL/GCD.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/GCD.thy Sun Feb 22 10:22:46 2009 +0100
@@ -156,7 +156,6 @@
apply (simp add: gcd_assoc)
apply (simp add: gcd_commute)
apply (simp_all add: mult_commute)
- apply (blast intro: dvd_mult)
done
@@ -404,7 +403,7 @@
{fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
- from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
+ from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
have ?rhs by auto}
ultimately show ?thesis by blast
qed
@@ -597,8 +596,8 @@
from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
then show ?thesis
- apply (subst zdvd_abs1 [symmetric])
- apply (subst zdvd_abs2 [symmetric])
+ apply (subst abs_dvd_iff [symmetric])
+ apply (subst dvd_abs_iff [symmetric])
apply (unfold dvd_def)
apply (rule_tac x = "int h'" in exI, simp)
done
@@ -614,11 +613,11 @@
let ?m' = "nat \<bar>m\<bar>"
let ?n' = "nat \<bar>n\<bar>"
from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
- unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
+ unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
unfolding zgcd_def by (simp only: zdvd_int)
then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
- then show "k dvd zgcd m n" by (simp add: zdvd_abs1)
+ then show "k dvd zgcd m n" by simp
qed
lemma div_zgcd_relprime:
@@ -721,7 +720,7 @@
assumes "k dvd i" shows "k dvd (zlcm i j)"
proof -
have "nat(abs k) dvd nat(abs i)" using `k dvd i`
- by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
+ by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
@@ -729,7 +728,7 @@
assumes "k dvd j" shows "k dvd (zlcm i j)"
proof -
have "nat(abs k) dvd nat(abs j)" using `k dvd j`
- by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
+ by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
--- a/src/HOL/Groebner_Basis.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Sun Feb 22 10:22:46 2009 +0100
@@ -448,16 +448,16 @@
declare zmod_zminus2[algebra]
declare zdiv_zero[algebra]
declare zmod_zero[algebra]
-declare zmod_1[algebra]
-declare zdiv_1[algebra]
+declare mod_by_1[algebra]
+declare div_by_1[algebra]
declare zmod_minus1_right[algebra]
declare zdiv_minus1_right[algebra]
declare mod_div_trivial[algebra]
declare mod_mod_trivial[algebra]
-declare zmod_zmult_self1[algebra]
-declare zmod_zmult_self2[algebra]
+declare mod_mult_self2_is_0[algebra]
+declare mod_mult_self1_is_0[algebra]
declare zmod_eq_0_iff[algebra]
-declare zdvd_0_left[algebra]
+declare dvd_0_left_iff[algebra]
declare zdvd1_eq[algebra]
declare zmod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
--- a/src/HOL/Hoare/Arith2.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Hoare/Arith2.thy Sun Feb 22 10:22:46 2009 +0100
@@ -42,12 +42,12 @@
lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n"
apply (unfold cd_def)
- apply (blast intro: dvd_diff dest: dvd_diffD)
+ apply (fastsimp dest: dvd_diffD)
done
lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)"
apply (unfold cd_def)
- apply (blast intro: dvd_diff dest: dvd_diffD)
+ apply (fastsimp dest: dvd_diffD)
done
--- a/src/HOL/IntDiv.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/IntDiv.thy Sun Feb 22 10:22:46 2009 +0100
@@ -547,34 +547,6 @@
simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
{* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}
-(* The following 8 lemmas are made unnecessary by the above simprocs: *)
-
-lemmas div_pos_pos_number_of =
- div_pos_pos [of "number_of v" "number_of w", standard]
-
-lemmas div_neg_pos_number_of =
- div_neg_pos [of "number_of v" "number_of w", standard]
-
-lemmas div_pos_neg_number_of =
- div_pos_neg [of "number_of v" "number_of w", standard]
-
-lemmas div_neg_neg_number_of =
- div_neg_neg [of "number_of v" "number_of w", standard]
-
-
-lemmas mod_pos_pos_number_of =
- mod_pos_pos [of "number_of v" "number_of w", standard]
-
-lemmas mod_neg_pos_number_of =
- mod_neg_pos [of "number_of v" "number_of w", standard]
-
-lemmas mod_pos_neg_number_of =
- mod_pos_neg [of "number_of v" "number_of w", standard]
-
-lemmas mod_neg_neg_number_of =
- mod_neg_neg [of "number_of v" "number_of w", standard]
-
-
lemmas posDivAlg_eqn_number_of [simp] =
posDivAlg_eqn [of "number_of v" "number_of w", standard]
@@ -584,15 +556,6 @@
text{*Special-case simplification *}
-lemma zmod_1 [simp]: "a mod (1::int) = 0"
-apply (cut_tac a = a and b = 1 in pos_mod_sign)
-apply (cut_tac [2] a = a and b = 1 in pos_mod_bound)
-apply (auto simp del:pos_mod_bound pos_mod_sign)
-done
-
-lemma zdiv_1 [simp]: "a div (1::int) = a"
-by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto)
-
lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
apply (cut_tac a = a and b = "-1" in neg_mod_sign)
apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
@@ -784,41 +747,12 @@
show ?thesis by simp
qed
-lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
-by (rule div_add_self1) (* already declared [simp] *)
-
-lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
-by (rule div_add_self2) (* already declared [simp] *)
-
-lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (rule div_mult_self1_is_id) (* already declared [simp] *)
-
-lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
-by (rule mod_mult_self2_is_0) (* already declared [simp] *)
-
-lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
-by (rule mod_mult_self1_is_0) (* already declared [simp] *)
-
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
(* REVISIT: should this be generalized to all semiring_div types? *)
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
-lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
-by (rule mod_add_left_eq)
-
-lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
-by (rule mod_add_right_eq)
-
-lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
-by (rule mod_add_self1) (* already declared [simp] *)
-
-lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
-by (rule mod_add_self2) (* already declared [simp] *)
-
-lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
-by (rule mod_diff_eq)
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}
@@ -902,13 +836,6 @@
"(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
by (simp add:zdiv_zmult_zmult1)
-(*
-lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
-apply (drule zdiv_zmult_zmult1)
-apply (auto simp add: mult_commute)
-done
-*)
-
subsection{*Distribution of Factors over mod*}
@@ -933,9 +860,6 @@
apply (auto simp add: mult_commute)
done
-lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
-by (rule mod_mod_cancel)
-
subsection {*Splitting Rules for div and mod*}
@@ -1070,7 +994,7 @@
apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) =
1 + 2* ((-b - 1) mod (-a))")
apply (rule_tac [2] pos_zmod_mult_2)
-apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib)
+apply (auto simp add: right_diff_distrib)
apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
prefer 2 apply simp
apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
@@ -1132,38 +1056,8 @@
subsection {* The Divides Relation *}
-lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
- by (rule dvd_eq_mod_eq_0)
-
lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
- zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
-
-lemma zdvd_0_right: "(m::int) dvd 0"
- by (rule dvd_0_right) (* already declared [iff] *)
-
-lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
- by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
-
-lemma zdvd_1_left: "1 dvd (m::int)"
- by (rule one_dvd) (* already declared [simp] *)
-
-lemma zdvd_refl: "m dvd (m::int)"
- by (rule dvd_refl) (* already declared [simp] *)
-
-lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
- by (rule dvd_trans)
-
-lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
- by (rule dvd_minus_iff) (* already declared [simp] *)
-
-lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
- by (rule minus_dvd_iff) (* already declared [simp] *)
-
-lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
- by (rule abs_dvd_iff) (* already declared [simp] *)
-
-lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
- by (rule dvd_abs_iff) (* already declared [simp] *)
+ dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
lemma zdvd_anti_sym:
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
@@ -1171,58 +1065,32 @@
apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
done
-lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
- by (rule dvd_add)
-
-lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a"
+lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a"
shows "\<bar>a\<bar> = \<bar>b\<bar>"
proof-
- from ab obtain k where k:"b = a*k" unfolding dvd_def by blast
- from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast
+ from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
+ from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
from k k' have "a = a*k*k'" by simp
with mult_cancel_left1[where c="a" and b="k*k'"]
- have kk':"k*k' = 1" using anz by (simp add: mult_assoc)
+ have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
thus ?thesis using k k' by auto
qed
-lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
- by (rule Ring_and_Field.dvd_diff)
-
lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
apply (subgoal_tac "m = n + (m - n)")
apply (erule ssubst)
- apply (blast intro: zdvd_zadd, simp)
+ apply (blast intro: dvd_add, simp)
done
-lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
- by (rule dvd_mult)
-
-lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
- by (rule dvd_mult2)
-
-lemma zdvd_triv_right: "(k::int) dvd m * k"
- by (rule dvd_triv_right) (* already declared [simp] *)
-
-lemma zdvd_triv_left: "(k::int) dvd k * m"
- by (rule dvd_triv_left) (* already declared [simp] *)
-
-lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
- by (rule dvd_mult_left)
-
-lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
- by (rule dvd_mult_right)
-
-lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
- by (rule mult_dvd_mono)
-
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
- apply (rule iffI)
- apply (erule_tac [2] zdvd_zadd)
- apply (subgoal_tac "n = (n + k * m) - k * m")
- apply (erule ssubst)
- apply (erule zdvd_zdiff, simp_all)
- done
+apply (rule iffI)
+ apply (erule_tac [2] dvd_add)
+ apply (subgoal_tac "n = (n + k * m) - k * m")
+ apply (erule ssubst)
+ apply (erule dvd_diff)
+ apply(simp_all)
+done
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
apply (simp add: dvd_def)
@@ -1232,7 +1100,7 @@
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
apply (subgoal_tac "k dvd n * (m div n) + m mod n")
apply (simp add: zmod_zdiv_equality [symmetric])
- apply (simp only: zdvd_zadd zdvd_zmult2)
+ apply (simp only: dvd_add dvd_mult2)
done
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
@@ -1252,7 +1120,7 @@
lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
apply (subgoal_tac "m mod n = 0")
apply (simp add: zmult_div_cancel)
-apply (simp only: zdvd_iff_zmod_eq_0)
+apply (simp only: dvd_eq_mod_eq_0)
done
lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
@@ -1265,10 +1133,6 @@
thus ?thesis by simp
qed
-lemma zdvd_zmult_cancel_disj:
- "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
-by (rule dvd_mult_cancel_left) (* already declared [simp] *)
-
theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
apply (simp split add: split_nat)
@@ -1300,44 +1164,38 @@
then show ?thesis by (simp only: negative_eq_positive) auto
qed
qed
- then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
+ then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
qed
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
proof
- assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
+ assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
hence "nat \<bar>x\<bar> = 1" by simp
thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
next
assume "\<bar>x\<bar>=1" thus "x dvd 1"
- by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0)
+ by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
qed
lemma zdvd_mult_cancel1:
assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
proof
assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
- by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff)
+ by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
next
assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
qed
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
- unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
+ unfolding zdvd_int by (cases "z \<ge> 0") simp_all
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
- unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
+ unfolding zdvd_int by (cases "z \<ge> 0") simp_all
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
by (auto simp add: dvd_int_iff)
-lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
- by (rule minus_dvd_iff)
-
-lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
- by (rule dvd_minus_iff)
-
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
apply (rule_tac z=n in int_cases)
apply (auto simp add: dvd_int_iff)
@@ -1387,8 +1245,8 @@
by (rule mod_diff_right_eq [symmetric])
lemmas zmod_simps =
- IntDiv.zmod_zadd_left_eq [symmetric]
- IntDiv.zmod_zadd_right_eq [symmetric]
+ mod_add_left_eq [symmetric]
+ mod_add_right_eq [symmetric]
IntDiv.zmod_zmult1_eq [symmetric]
mod_mult_left_eq [symmetric]
IntDiv.zpower_zmod
@@ -1463,14 +1321,14 @@
assume H: "x mod n = y mod n"
hence "x mod n - y mod n = 0" by simp
hence "(x mod n - y mod n) mod n = 0" by simp
- hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
- thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
+ hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
+ thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
next
assume H: "n dvd x - y"
then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
hence "x = n*k + y" by simp
hence "x mod n = (n*k + y) mod n" by simp
- thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
+ thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
qed
lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
--- a/src/HOL/Library/Abstract_Rat.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy Sun Feb 22 10:22:46 2009 +0100
@@ -247,7 +247,7 @@
(of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
apply (frule of_int_div_aux [of d n, where ?'a = 'a])
apply simp
- apply (simp add: zdvd_iff_zmod_eq_0)
+ apply (simp add: dvd_eq_mod_eq_0)
done
--- a/src/HOL/Library/Determinants.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Determinants.thy Sun Feb 22 10:22:46 2009 +0100
@@ -1048,7 +1048,7 @@
note th0 = this
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"
{fix x:: "real ^'n" assume nx: "norm x = 1"
- have "?g x = f x" using nx by (simp add: norm_eq_0[symmetric])}
+ have "?g x = f x" using nx by auto}
hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast
have g0: "?g 0 = 0" by simp
{fix x y :: "real ^'n"
@@ -1057,15 +1057,15 @@
moreover
{assume "x = 0" "y \<noteq> 0"
then have "dist (?g x) (?g y) = dist x y"
- apply (simp add: dist_def norm_neg norm_mul norm_eq_0)
+ apply (simp add: dist_def norm_mul)
apply (rule f1[rule_format])
- by(simp add: norm_mul norm_eq_0 field_simps)}
+ by(simp add: norm_mul field_simps)}
moreover
{assume "x \<noteq> 0" "y = 0"
then have "dist (?g x) (?g y) = dist x y"
- apply (simp add: dist_def norm_neg norm_mul norm_eq_0)
+ apply (simp add: dist_def norm_mul)
apply (rule f1[rule_format])
- by(simp add: norm_mul norm_eq_0 field_simps)}
+ by(simp add: norm_mul field_simps)}
moreover
{assume z: "x \<noteq> 0" "y \<noteq> 0"
have th00: "x = norm x *s inverse (norm x) *s x" "y = norm y *s inverse (norm y) *s y" "norm x *s f (inverse (norm x) *s x) = norm x *s f (inverse (norm x) *s x)"
@@ -1077,7 +1077,7 @@
"norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) =
norm (inverse (norm x) *s x - inverse (norm y) *s y)"
using z
- by (auto simp add: norm_eq_0 vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def])
+ by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def])
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
by (simp add: dist_def)}
ultimately have "dist (?g x) (?g y) = dist x y" by blast}
@@ -1148,4 +1148,4 @@
by (simp add: ring_simps)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Euclidean_Space.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy Sun Feb 22 10:22:46 2009 +0100
@@ -8,6 +8,7 @@
theory Euclidean_Space
imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
+ Inner_Product
uses ("normarith.ML")
begin
@@ -84,7 +85,13 @@
instance by (intro_classes)
end
-text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in @{text real_vector} *}
+instantiation "^" :: (scaleR, type) scaleR
+begin
+definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
+instance ..
+end
+
+text{* Also the scalar-vector multiplication. *}
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
where "c *s x = (\<chi> i. c * (x$i))"
@@ -118,6 +125,7 @@
[@{thm vector_add_def}, @{thm vector_mult_def},
@{thm vector_minus_def}, @{thm vector_uminus_def},
@{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},
+ @{thm vector_scaleR_def},
@{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}]
fun vector_arith_tac ths =
simp_tac ss1
@@ -166,9 +174,18 @@
shows "(- x)$i = - (x$i)"
using i by vector
+lemma vector_scaleR_component:
+ fixes x :: "'a::scaleR ^ 'n"
+ assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}"
+ shows "(scaleR r x)$i = scaleR r (x$i)"
+ using i by vector
+
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
-lemmas vector_component = vec_component vector_add_component vector_mult_component vector_smult_component vector_minus_component vector_uminus_component cond_component
+lemmas vector_component =
+ vec_component vector_add_component vector_mult_component
+ vector_smult_component vector_minus_component vector_uminus_component
+ vector_scaleR_component cond_component
subsection {* Some frequently useful arithmetic lemmas over vectors. *}
@@ -199,6 +216,9 @@
apply (intro_classes)
by (vector Cart_eq)
+instance "^" :: (real_vector, type) real_vector
+ by default (vector scaleR_left_distrib scaleR_right_distrib)+
+
instance "^" :: (semigroup_mult,type) semigroup_mult
apply (intro_classes) by (vector mult_assoc)
@@ -242,6 +262,18 @@
instance "^" :: (ring,type) ring by (intro_classes)
instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes)
instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes)
+
+instance "^" :: (ring_1,type) ring_1 ..
+
+instance "^" :: (real_algebra,type) real_algebra
+ apply intro_classes
+ apply (simp_all add: vector_scaleR_def ring_simps)
+ apply vector
+ apply vector
+ done
+
+instance "^" :: (real_algebra_1,type) real_algebra_1 ..
+
lemma of_nat_index:
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
apply (induct n)
@@ -290,8 +322,7 @@
qed
instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes
- (* FIXME!!! Why does the axclass package complain here !!*)
-(* instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes *)
+instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
by (vector mult_assoc)
@@ -314,6 +345,241 @@
apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta )
using dimindex_ge_1 apply auto done
+subsection {* Square root of sum of squares *}
+
+definition
+ "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"
+
+lemma setL2_cong:
+ "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
+ unfolding setL2_def by simp
+
+lemma strong_setL2_cong:
+ "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
+ unfolding setL2_def simp_implies_def by simp
+
+lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_empty [simp]: "setL2 f {} = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_insert [simp]:
+ "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
+ setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"
+ unfolding setL2_def by (simp add: setsum_nonneg)
+
+lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
+ unfolding setL2_def by (simp add: setsum_nonneg)
+
+lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
+ unfolding setL2_def by simp
+
+lemma setL2_mono:
+ assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
+ assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
+ shows "setL2 f K \<le> setL2 g K"
+ unfolding setL2_def
+ by (simp add: setsum_nonneg setsum_mono power_mono prems)
+
+lemma setL2_right_distrib:
+ "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
+ unfolding setL2_def
+ apply (simp add: power_mult_distrib)
+ apply (simp add: setsum_right_distrib [symmetric])
+ apply (simp add: real_sqrt_mult setsum_nonneg)
+ done
+
+lemma setL2_left_distrib:
+ "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
+ unfolding setL2_def
+ apply (simp add: power_mult_distrib)
+ apply (simp add: setsum_left_distrib [symmetric])
+ apply (simp add: real_sqrt_mult setsum_nonneg)
+ done
+
+lemma setsum_nonneg_eq_0_iff:
+ fixes f :: "'a \<Rightarrow> 'b::pordered_ab_group_add"
+ shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ apply (induct set: finite, simp)
+ apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
+ done
+
+lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ unfolding setL2_def
+ by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
+
+lemma setL2_triangle_ineq:
+ shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
+proof (cases "finite A")
+ case False
+ thus ?thesis by simp
+next
+ case True
+ thus ?thesis
+ proof (induct set: finite)
+ case empty
+ show ?case by simp
+ next
+ case (insert x F)
+ hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>
+ sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"
+ by (intro real_sqrt_le_mono add_left_mono power_mono insert
+ setL2_nonneg add_increasing zero_le_power2)
+ also have
+ "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"
+ by (rule real_sqrt_sum_squares_triangle_ineq)
+ finally show ?case
+ using insert by simp
+ qed
+qed
+
+lemma sqrt_sum_squares_le_sum:
+ "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
+ apply (rule power2_le_imp_le)
+ apply (simp add: power2_sum)
+ apply (simp add: mult_nonneg_nonneg)
+ apply (simp add: add_nonneg_nonneg)
+ done
+
+lemma setL2_le_setsum [rule_format]:
+ "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply clarsimp
+ apply (erule order_trans [OF sqrt_sum_squares_le_sum])
+ apply simp
+ apply simp
+ apply simp
+ done
+
+lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
+ apply (rule power2_le_imp_le)
+ apply (simp add: power2_sum)
+ apply (simp add: mult_nonneg_nonneg)
+ apply (simp add: add_nonneg_nonneg)
+ done
+
+lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply simp
+ apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
+ apply simp
+ apply simp
+ done
+
+lemma setL2_mult_ineq_lemma:
+ fixes a b c d :: real
+ shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
+proof -
+ have "0 \<le> (a * d - b * c)\<twosuperior>" by simp
+ also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)"
+ by (simp only: power2_diff power_mult_distrib)
+ also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)"
+ by simp
+ finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
+ by simp
+qed
+
+lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply simp
+ apply (rule power2_le_imp_le, simp)
+ apply (rule order_trans)
+ apply (rule power_mono)
+ apply (erule add_left_mono)
+ apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)
+ apply (simp add: power2_sum)
+ apply (simp add: power_mult_distrib)
+ apply (simp add: right_distrib left_distrib)
+ apply (rule ord_le_eq_trans)
+ apply (rule setL2_mult_ineq_lemma)
+ apply simp
+ apply (intro mult_nonneg_nonneg setL2_nonneg)
+ apply simp
+ done
+
+lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
+ apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
+ apply fast
+ apply (subst setL2_insert)
+ apply simp
+ apply simp
+ apply simp
+ done
+
+subsection {* Norms *}
+
+instantiation "^" :: (real_normed_vector, type) real_normed_vector
+begin
+
+definition vector_norm_def:
+ "norm (x::'a^'b) = setL2 (\<lambda>i. norm (x$i)) {1 .. dimindex (UNIV:: 'b set)}"
+
+definition vector_sgn_def:
+ "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
+
+instance proof
+ fix a :: real and x y :: "'a ^ 'b"
+ show "0 \<le> norm x"
+ unfolding vector_norm_def
+ by (rule setL2_nonneg)
+ show "norm x = 0 \<longleftrightarrow> x = 0"
+ unfolding vector_norm_def
+ by (simp add: setL2_eq_0_iff Cart_eq)
+ show "norm (x + y) \<le> norm x + norm y"
+ unfolding vector_norm_def
+ apply (rule order_trans [OF _ setL2_triangle_ineq])
+ apply (rule setL2_mono)
+ apply (simp add: vector_component norm_triangle_ineq)
+ apply simp
+ done
+ show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
+ unfolding vector_norm_def
+ by (simp add: vector_component norm_scaleR setL2_right_distrib
+ cong: strong_setL2_cong)
+ show "sgn x = scaleR (inverse (norm x)) x"
+ by (rule vector_sgn_def)
+qed
+
+end
+
+subsection {* Inner products *}
+
+instantiation "^" :: (real_inner, type) real_inner
+begin
+
+definition vector_inner_def:
+ "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) {1 .. dimindex(UNIV::'b set)}"
+
+instance proof
+ fix r :: real and x y z :: "'a ^ 'b"
+ show "inner x y = inner y x"
+ unfolding vector_inner_def
+ by (simp add: inner_commute)
+ show "inner (x + y) z = inner x z + inner y z"
+ unfolding vector_inner_def
+ by (vector inner_left_distrib)
+ show "inner (scaleR r x) y = r * inner x y"
+ unfolding vector_inner_def
+ by (vector inner_scaleR_left)
+ show "0 \<le> inner x x"
+ unfolding vector_inner_def
+ by (simp add: setsum_nonneg)
+ show "inner x x = 0 \<longleftrightarrow> x = 0"
+ unfolding vector_inner_def
+ by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
+ show "norm x = sqrt (inner x x)"
+ unfolding vector_inner_def vector_norm_def setL2_def
+ by (simp add: power2_norm_eq_inner)
+qed
+
+end
+
subsection{* Properties of the dot product. *}
lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
@@ -363,18 +629,7 @@
lemma dot_pos_lt: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
by (auto simp add: le_less)
-subsection {* Introduce norms, but defer many properties till we get square roots. *}
-text{* FIXME : This is ugly *}
-defs (overloaded)
- real_of_real_def [code inline, simp]: "real == id"
-
-instantiation "^" :: ("{times, comm_monoid_add}", type) norm begin
-definition real_vector_norm_def: "norm \<equiv> (\<lambda>x. sqrt (real (x \<bullet> x)))"
-instance ..
-end
-
-
-subsection{* The collapse of the general concepts to dimention one. *}
+subsection{* The collapse of the general concepts to dimension one. *}
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
by (vector dimindex_def)
@@ -385,11 +640,15 @@
apply (simp only: vector_one[symmetric])
done
+lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
+ by (simp add: vector_norm_def dimindex_def)
+
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
- by (simp add: real_vector_norm_def)
+ by (simp add: norm_vector_1)
text{* Metric *}
+text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}
definition dist:: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real" where
"dist x y = norm (x - y)"
@@ -501,27 +760,18 @@
text{* Hence derive more interesting properties of the norm. *}
lemma norm_0: "norm (0::real ^ 'n) = 0"
- by (simp add: real_vector_norm_def dot_eq_0)
-
-lemma norm_pos_le: "0 <= norm (x::real^'n)"
- by (simp add: real_vector_norm_def dot_pos_le)
-lemma norm_neg: " norm(-x) = norm (x:: real ^ 'n)"
- by (simp add: real_vector_norm_def dot_lneg dot_rneg)
-lemma norm_sub: "norm(x - y) = norm(y - (x::real ^ 'n))"
- by (metis norm_neg minus_diff_eq)
+ by (rule norm_zero)
+
lemma norm_mul: "norm(a *s x) = abs(a) * norm x"
- by (simp add: real_vector_norm_def dot_lmult dot_rmult mult_assoc[symmetric] real_sqrt_mult)
+ by (simp add: vector_norm_def vector_component setL2_right_distrib
+ abs_mult cong: strong_setL2_cong)
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
+ by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)
+lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
+ by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)
+lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
by (simp add: real_vector_norm_def)
-lemma norm_eq_0: "norm x = 0 \<longleftrightarrow> x = (0::real ^ 'n)"
- by (simp add: real_vector_norm_def dot_eq_0)
-lemma norm_pos_lt: "0 < norm x \<longleftrightarrow> x \<noteq> (0::real ^ 'n)"
- by (metis less_le real_vector_norm_def norm_pos_le norm_eq_0)
-lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
- by (simp add: real_vector_norm_def dot_pos_le)
-lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_0)
-lemma norm_le_0: "norm x <= 0 \<longleftrightarrow> x = (0::real ^'n)"
- by (metis norm_eq_0 norm_pos_le order_antisym)
+lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
by vector
lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
@@ -535,14 +785,14 @@
lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y"
proof-
{assume "norm x = 0"
- hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
+ hence ?thesis by (simp add: dot_lzero dot_rzero)}
moreover
{assume "norm y = 0"
- hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
+ hence ?thesis by (simp add: dot_lzero dot_rzero)}
moreover
{assume h: "norm x \<noteq> 0" "norm y \<noteq> 0"
let ?z = "norm y *s x - norm x *s y"
- from h have p: "norm x * norm y > 0" by (metis norm_pos_le le_less zero_compare_simps)
+ from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps)
from dot_pos_le[of ?z]
have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2"
apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps)
@@ -553,26 +803,16 @@
ultimately show ?thesis by metis
qed
-lemma norm_abs[simp]: "abs (norm x) = norm (x::real ^'n)"
- using norm_pos_le[of x] by (simp add: real_abs_def linorder_linear)
-
lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
- by (simp add: real_abs_def dot_rneg norm_neg)
-lemma norm_triangle: "norm(x + y) <= norm x + norm (y::real ^'n)"
- unfolding real_vector_norm_def
- apply (rule real_le_lsqrt)
- apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1]
- apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1]
- apply (simp add: dot_ladd dot_radd dot_sym )
- by (simp add: norm_pow_2[symmetric] power2_eq_square ring_simps norm_cauchy_schwarz)
+ by (simp add: real_abs_def dot_rneg)
lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)"
- using norm_triangle[of "y" "x - y"] by (simp add: ring_simps)
+ using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e"
- by (metis order_trans norm_triangle)
+ by (metis order_trans norm_triangle_ineq)
lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e"
- by (metis basic_trans_rules(21) norm_triangle)
+ by (metis basic_trans_rules(21) norm_triangle_ineq)
lemma setsum_delta:
assumes fS: "finite S"
@@ -597,19 +837,10 @@
qed
lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x$i\<bar> <= norm (x::real ^ 'n)"
-proof(simp add: real_vector_norm_def, rule real_le_rsqrt, clarsimp)
- assume i: "Suc 0 \<le> i" "i \<le> dimindex (UNIV :: 'n set)"
- let ?S = "{1 .. dimindex(UNIV :: 'n set)}"
- let ?f = "(\<lambda>k. if k = i then x$i ^2 else 0)"
- have fS: "finite ?S" by simp
- from i setsum_delta[OF fS, of i "\<lambda>k. x$i ^ 2"]
- have th: "x$i^2 = setsum ?f ?S" by simp
- let ?g = "\<lambda>k. x$k * x$k"
- {fix x assume x: "x \<in> ?S" have "?f x \<le> ?g x" by (simp add: power2_eq_square)}
- with setsum_mono[of ?S ?f ?g]
- have "setsum ?f ?S \<le> setsum ?g ?S" by blast
- then show "x$i ^2 \<le> x \<bullet> (x:: real ^ 'n)" unfolding dot_def th[symmetric] .
-qed
+ apply (simp add: vector_norm_def)
+ apply (rule member_le_setL2, simp_all)
+ done
+
lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e
==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x$i\<bar> <= e"
by (metis component_le_norm order_trans)
@@ -619,24 +850,12 @@
by (metis component_le_norm basic_trans_rules(21))
lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x$i\<bar>) {1..dimindex(UNIV::'n set)}"
-proof (simp add: real_vector_norm_def, rule real_le_lsqrt,simp add: dot_pos_le, simp add: setsum_mono, simp add: dot_def, induct "dimindex(UNIV::'n set)")
- case 0 thus ?case by simp
-next
- case (Suc n)
- have th: "2 * (\<bar>x$(Suc n)\<bar> * (\<Sum>i = Suc 0..n. \<bar>x$i\<bar>)) \<ge> 0"
- apply simp
- apply (rule mult_nonneg_nonneg)
- by (simp_all add: setsum_abs_ge_zero)
-
- from Suc
- show ?case using th by (simp add: power2_eq_square ring_simps)
-qed
+ by (simp add: vector_norm_def setL2_le_setsum)
lemma real_abs_norm: "\<bar> norm x\<bar> = norm (x :: real ^'n)"
- by (simp add: norm_pos_le)
+ by (rule abs_norm_cancel)
lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n) - norm y\<bar> <= norm(x - y)"
- apply (simp add: abs_le_iff ring_simps)
- by (metis norm_triangle_sub norm_sub)
+ by (rule norm_triangle_ineq3)
lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
by (simp add: real_vector_norm_def)
lemma norm_lt: "norm(x::real ^'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
@@ -652,13 +871,7 @@
by (simp add: real_vector_norm_def dot_pos_le )
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
-proof-
- have th: "\<And>x y::real. x^2 = y^2 \<longleftrightarrow> x = y \<or> x = -y" by algebra
- show ?thesis using norm_pos_le[of x]
- apply (simp add: dot_square_norm th)
- apply arith
- done
-qed
+ by (auto simp add: real_vector_norm_def)
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
proof-
@@ -668,14 +881,14 @@
qed
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
- using norm_pos_le[of x]
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
+ using norm_ge_zero[of x]
apply arith
done
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
- using norm_pos_le[of x]
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
+ using norm_ge_zero[of x]
apply arith
done
@@ -746,14 +959,14 @@
lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
- by (atomize) (auto simp add: norm_pos_le)
+ by (atomize) (auto simp add: norm_ge_zero)
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
lemma norm_pths:
"(x::real ^'n) = y \<longleftrightarrow> norm (x - y) \<le> 0"
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
- using norm_pos_le[of "x - y"] by (auto simp add: norm_0 norm_eq_0)
+ using norm_ge_zero[of "x - y"] by auto
use "normarith.ML"
@@ -873,7 +1086,7 @@
assumes fS: "finite S"
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
proof(induct rule: finite_induct[OF fS])
- case 1 thus ?case by (simp add: norm_zero)
+ case 1 thus ?case by simp
next
case (2 x S)
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
@@ -887,10 +1100,10 @@
assumes fS: "finite S"
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
proof(induct rule: finite_induct[OF fS])
- case 1 thus ?case by simp norm
+ case 1 thus ?case by simp
next
case (2 x S)
- from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" apply (simp add: norm_triangle_ineq) by norm
+ from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"
using "2.hyps" by simp
finally show ?case using "2.hyps" by simp
@@ -936,45 +1149,6 @@
using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]
by simp
-instantiation "^" :: ("{scaleR, one, times}",type) scaleR
-begin
-
-definition vector_scaleR_def: "(scaleR :: real \<Rightarrow> 'a ^'b \<Rightarrow> 'a ^'b) \<equiv> (\<lambda> c x . (scaleR c 1) *s x)"
-instance ..
-end
-
-instantiation "^" :: ("ring_1",type) ring_1
-begin
-instance by intro_classes
-end
-
-instantiation "^" :: (real_algebra_1,type) real_vector
-begin
-
-instance
- apply intro_classes
- apply (simp_all add: vector_scaleR_def)
- apply (simp_all add: vector_sadd_rdistrib vector_add_ldistrib vector_smult_lid vector_smult_assoc scaleR_left_distrib mult_commute)
- done
-end
-
-instantiation "^" :: (real_algebra_1,type) real_algebra
-begin
-
-instance
- apply intro_classes
- apply (simp_all add: vector_scaleR_def ring_simps)
- apply vector
- apply vector
- done
-end
-
-instantiation "^" :: (real_algebra_1,type) real_algebra_1
-begin
-
-instance ..
-end
-
lemma setsum_vmul:
fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}"
assumes fS: "finite S"
@@ -1211,7 +1385,7 @@
by (auto simp add: setsum_component intro: abs_le_D1)
have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e"
using i component_le_norm[OF i, of "setsum (\<lambda>x. - f x) ?Pn"] fPs[OF PnP]
- by (auto simp add: setsum_negf norm_neg setsum_component vector_component intro: abs_le_D1)
+ by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1)
have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn"
apply (subst thp)
apply (rule setsum_Un_nonzero)
@@ -1535,7 +1709,7 @@
unfolding norm_mul
apply (simp only: mult_commute)
apply (rule mult_mono)
- by (auto simp add: ring_simps norm_pos_le) }
+ by (auto simp add: ring_simps norm_ge_zero) }
then have th: "\<forall>i\<in> ?S. norm ((x$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
from real_setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
@@ -1552,16 +1726,18 @@
let ?K = "\<bar>B\<bar> + 1"
have Kp: "?K > 0" by arith
{assume C: "B < 0"
- have "norm (1::real ^ 'n) > 0" by (simp add: norm_pos_lt)
+ have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff)
with C have "B * norm (1:: real ^ 'n) < 0"
by (simp add: zero_compare_simps)
- with B[rule_format, of 1] norm_pos_le[of "f 1"] have False by simp
+ with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp
}
then have Bp: "B \<ge> 0" by ferrack
{fix x::"real ^ 'n"
have "norm (f x) \<le> ?K * norm x"
- using B[rule_format, of x] norm_pos_le[of x] norm_pos_le[of "f x"] Bp
- by (auto simp add: ring_simps split add: abs_split)
+ using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
+ apply (auto simp add: ring_simps split add: abs_split)
+ apply (erule order_trans, simp)
+ done
}
then show ?thesis using Kp by blast
qed
@@ -1641,9 +1817,9 @@
apply simp
apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps)
apply (rule mult_mono)
- apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
+ apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
apply (rule mult_mono)
- apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
+ apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
done}
then show ?thesis by metis
qed
@@ -1663,7 +1839,7 @@
have "B * norm x * norm y \<le> ?K * norm x * norm y"
apply -
apply (rule mult_right_mono, rule mult_right_mono)
- by (auto simp add: norm_pos_le)
+ by (auto simp add: norm_ge_zero)
then have "norm (h x y) \<le> ?K * norm x * norm y"
using B[rule_format, of x y] by simp}
with Kp show ?thesis by blast
@@ -2276,21 +2452,21 @@
moreover
{assume H: ?lhs
from H[rule_format, of "basis 1"]
- have bp: "b \<ge> 0" using norm_pos_le[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
- by (auto simp add: norm_basis)
+ have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
+ by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])
{fix x :: "real ^'n"
{assume "x = 0"
- then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] norm_0 bp)}
+ then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
moreover
{assume x0: "x \<noteq> 0"
- hence n0: "norm x \<noteq> 0" by (metis norm_eq_0)
+ hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
let ?c = "1/ norm x"
- have "norm (?c*s x) = 1" by (simp add: n0 norm_mul)
+ have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
with H have "norm (f(?c*s x)) \<le> b" by blast
hence "?c * norm (f x) \<le> b"
by (simp add: linear_cmul[OF lf] norm_mul)
hence "norm (f x) \<le> b * norm x"
- using n0 norm_pos_le[of x] by (auto simp add: field_simps)}
+ using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
ultimately have "norm (f x) \<le> b * norm x" by blast}
then have ?rhs by blast}
ultimately show ?thesis by blast
@@ -2322,12 +2498,12 @@
qed
lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"
- using order_trans[OF norm_pos_le onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
+ using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
using onorm[OF lf]
- apply (auto simp add: norm_0 onorm_pos_le norm_le_0)
+ apply (auto simp add: onorm_pos_le)
apply atomize
apply (erule allE[where x="0::real"])
using onorm_pos_le[OF lf]
@@ -2365,7 +2541,7 @@
lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
shows "onorm (\<lambda>x. - f x) \<le> onorm f"
using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
- unfolding norm_neg by metis
+ unfolding norm_minus_cancel by metis
lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
shows "onorm (\<lambda>x. - f x) = onorm f"
@@ -2377,7 +2553,7 @@
shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
apply (rule order_trans)
- apply (rule norm_triangle)
+ apply (rule norm_triangle_ineq)
apply (simp add: distrib)
apply (rule add_mono)
apply (rule onorm(1)[OF lf])
@@ -2594,7 +2770,7 @@
by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square del: One_nat_def)
then show ?thesis
unfolding th0
- unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def real_sqrt_le_iff id_def
by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
qed
@@ -2626,7 +2802,7 @@
by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square setsum_reindex[OF finj, unfolded fS] del: One_nat_def)
then show ?thesis
unfolding th0
- unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def real_sqrt_le_iff id_def
by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
qed
@@ -2683,7 +2859,7 @@
qed
lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ _) + norm(y)"
- unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff real_of_real_def id_def
+ unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def
apply (rule power2_le_imp_le)
apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]])
apply (auto simp add: power2_eq_square ring_simps)
@@ -5007,7 +5183,7 @@
apply blast
by (rule abs_ge_zero)
from real_le_lsqrt[OF dot_pos_le th th1]
- show ?thesis unfolding real_vector_norm_def real_of_real_def id_def .
+ show ?thesis unfolding real_vector_norm_def id_def .
qed
(* Equality in Cauchy-Schwarz and triangle inequalities. *)
@@ -5015,10 +5191,10 @@
lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
{assume h: "x = 0"
- hence ?thesis by (simp add: norm_0)}
+ hence ?thesis by simp}
moreover
{assume h: "y = 0"
- hence ?thesis by (simp add: norm_0)}
+ hence ?thesis by simp}
moreover
{assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
from dot_eq_0[of "norm y *s x - norm x *s y"]
@@ -5032,7 +5208,7 @@
also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
by (simp add: ring_simps dot_sym)
also have "\<dots> \<longleftrightarrow> ?lhs" using x y
- apply (simp add: norm_eq_0)
+ apply simp
by metis
finally have ?thesis by blast}
ultimately show ?thesis by blast
@@ -5043,14 +5219,14 @@
proof-
have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a" by arith
have "?rhs \<longleftrightarrow> norm x *s y = norm y *s x \<or> norm (- x) *s y = norm y *s (- x)"
- apply (simp add: norm_neg) by vector
+ apply simp by vector
also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or>
(-x) \<bullet> y = norm x * norm y)"
unfolding norm_cauchy_schwarz_eq[symmetric]
- unfolding norm_neg
+ unfolding norm_minus_cancel
norm_mul by blast
also have "\<dots> \<longleftrightarrow> ?lhs"
- unfolding th[OF mult_nonneg_nonneg, OF norm_pos_le[of x] norm_pos_le[of y]] dot_lneg
+ unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg
by arith
finally show ?thesis ..
qed
@@ -5058,17 +5234,17 @@
lemma norm_triangle_eq: "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"
proof-
{assume x: "x =0 \<or> y =0"
- hence ?thesis by (cases "x=0", simp_all add: norm_0)}
+ hence ?thesis by (cases "x=0", simp_all)}
moreover
{assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
hence "norm x \<noteq> 0" "norm y \<noteq> 0"
- by (simp_all add: norm_eq_0)
+ by simp_all
hence n: "norm x > 0" "norm y > 0"
- using norm_pos_le[of x] norm_pos_le[of y]
+ using norm_ge_zero[of x] norm_ge_zero[of y]
by arith+
have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)" by algebra
have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
- apply (rule th) using n norm_pos_le[of "x + y"]
+ apply (rule th) using n norm_ge_zero[of "x + y"]
by arith
also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
unfolding norm_cauchy_schwarz_eq[symmetric]
@@ -5138,8 +5314,8 @@
lemma norm_cauchy_schwarz_equal: "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"
unfolding norm_cauchy_schwarz_abs_eq
-apply (cases "x=0", simp_all add: collinear_2 norm_0)
-apply (cases "y=0", simp_all add: collinear_2 norm_0 insert_commute)
+apply (cases "x=0", simp_all add: collinear_2)
+apply (cases "y=0", simp_all add: collinear_2 insert_commute)
unfolding collinear_lemma
apply simp
apply (subgoal_tac "norm x \<noteq> 0")
@@ -5164,8 +5340,8 @@
apply (simp add: ring_simps)
apply (case_tac "c <= 0", simp add: ring_simps)
apply (simp add: ring_simps)
-apply (simp add: norm_eq_0)
-apply (simp add: norm_eq_0)
+apply simp
+apply simp
done
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Float.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Float.thy Sun Feb 22 10:22:46 2009 +0100
@@ -795,7 +795,7 @@
have "x \<noteq> y"
proof (rule ccontr)
assume "\<not> x \<noteq> y" hence "x = y" by auto
- have "?X mod y = 0" unfolding `x = y` using zmod_zmult_self2 by auto
+ have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto
thus False using False by auto
qed
hence "x < y" using `x \<le> y` by auto
--- a/src/HOL/Library/Inner_Product.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy Sun Feb 22 10:22:46 2009 +0100
@@ -65,7 +65,7 @@
lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x"
by (simp add: norm_eq_sqrt_inner)
-lemma Cauchy_Schwartz_ineq:
+lemma Cauchy_Schwarz_ineq:
"(inner x y)\<twosuperior> \<le> inner x x * inner y y"
proof (cases)
assume "y = 0"
@@ -86,11 +86,11 @@
by (simp add: pos_divide_le_eq y)
qed
-lemma Cauchy_Schwartz_ineq2:
+lemma Cauchy_Schwarz_ineq2:
"\<bar>inner x y\<bar> \<le> norm x * norm y"
proof (rule power2_le_imp_le)
have "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
- using Cauchy_Schwartz_ineq .
+ using Cauchy_Schwarz_ineq .
thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"
by (simp add: power_mult_distrib power2_norm_eq_inner)
show "0 \<le> norm x * norm y"
@@ -108,7 +108,7 @@
show "norm (x + y) \<le> norm x + norm y"
proof (rule power2_le_imp_le)
have "inner x y \<le> norm x * norm y"
- by (rule order_trans [OF abs_ge_self Cauchy_Schwartz_ineq2])
+ by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
unfolding power2_sum power2_norm_eq_inner
by (simp add: inner_distrib inner_commute)
@@ -140,7 +140,7 @@
show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
proof
show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
- by (simp add: Cauchy_Schwartz_ineq2)
+ by (simp add: Cauchy_Schwarz_ineq2)
qed
qed
--- a/src/HOL/Library/Numeral_Type.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sun Feb 22 10:22:46 2009 +0100
@@ -267,6 +267,22 @@
subsection {* Number ring instances *}
+text {*
+ Unfortunately a number ring instance is not possible for
+ @{typ num1}, since 0 and 1 are not distinct.
+*}
+
+instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}"
+begin
+
+lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
+ by (induct x, induct y) simp
+
+instance proof
+qed (simp_all add: num1_eq_iff)
+
+end
+
instantiation
bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
begin
--- a/src/HOL/Library/Permutations.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Permutations.thy Sun Feb 22 10:22:46 2009 +0100
@@ -683,13 +683,13 @@
(* ------------------------------------------------------------------------- *)
lemma permutes_natset_le:
- assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S. p i <= i" shows "p = id"
+ assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i <= i" shows "p = id"
proof-
{fix n
have "p n = n"
using p le
- proof(induct n arbitrary: S rule: nat_less_induct)
- fix n S assume H: "\<forall> m< n. \<forall>S. p permutes S \<longrightarrow> (\<forall>i\<in>S. p i \<le> i) \<longrightarrow> p m = m"
+ proof(induct n arbitrary: S rule: less_induct)
+ fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m"
"p permutes S" "\<forall>i \<in>S. p i \<le> i"
{assume "n \<notin> S"
with H(2) have "p n = n" unfolding permutes_def by metis}
@@ -699,7 +699,7 @@
moreover{assume h: "p n < n"
from H h have "p (p n) = p n" by metis
with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
- with h have False by arith}
+ with h have False by simp}
ultimately have "p n = n" by blast }
ultimately show "p n = n" by blast
qed}
@@ -707,7 +707,7 @@
qed
lemma permutes_natset_ge:
- assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S. p i \<ge> i" shows "p = id"
+ assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i \<ge> i" shows "p = id"
proof-
{fix i assume i: "i \<in> S"
from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp
@@ -757,13 +757,13 @@
done
term setsum
-lemma setsum_permutations_inverse: "setsum f {p. p permutes {m..n}} = setsum (\<lambda>p. f(inv p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
+lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
proof-
- let ?S = "{p . p permutes {m .. n}}"
+ let ?S = "{p . p permutes S}"
have th0: "inj_on inv ?S"
proof(auto simp add: inj_on_def)
fix q r
- assume q: "q permutes {m .. n}" and r: "r permutes {m .. n}" and qr: "inv q = inv r"
+ assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r"
hence "inv (inv q) = inv (inv r)" by simp
with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
show "q = r" by metis
@@ -774,17 +774,17 @@
qed
lemma setum_permutations_compose_left:
- assumes q: "q permutes {m..n}"
- shows "setsum f {p. p permutes {m..n}} =
- setsum (\<lambda>p. f(q o p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
+ assumes q: "q permutes S"
+ shows "setsum f {p. p permutes S} =
+ setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs")
proof-
- let ?S = "{p. p permutes {m..n}}"
+ let ?S = "{p. p permutes S}"
have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
have th1: "inj_on (op o q) ?S"
apply (auto simp add: inj_on_def)
proof-
fix p r
- assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "q \<circ> p = q \<circ> r"
+ assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
with permutes_inj[OF q, unfolded inj_iff]
@@ -796,17 +796,17 @@
qed
lemma sum_permutations_compose_right:
- assumes q: "q permutes {m..n}"
- shows "setsum f {p. p permutes {m..n}} =
- setsum (\<lambda>p. f(p o q)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
+ assumes q: "q permutes S"
+ shows "setsum f {p. p permutes S} =
+ setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs")
proof-
- let ?S = "{p. p permutes {m..n}}"
+ let ?S = "{p. p permutes S}"
have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
have th1: "inj_on (\<lambda>p. p o q) ?S"
apply (auto simp add: inj_on_def)
proof-
fix p r
- assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "p o q = r o q"
+ assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q"
hence "p o (q o inv q) = r o (q o inv q)" by (simp add: o_assoc)
with permutes_surj[OF q, unfolded surj_iff]
--- a/src/HOL/Library/Pocklington.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Pocklington.thy Sun Feb 22 10:22:46 2009 +0100
@@ -873,7 +873,7 @@
from lh[unfolded nat_mod]
obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast
hence "a ^ d + n * q1 - n * q2 = 1" by simp
- with dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
+ with nat_dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
with p(3) have False by simp
hence ?rhs ..}
ultimately have ?rhs by blast}
--- a/src/HOL/Library/Primes.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Library/Primes.thy Sun Feb 22 10:22:46 2009 +0100
@@ -307,8 +307,8 @@
{fix e assume H: "e dvd a^n" "e dvd b^n"
from bezout_gcd_pow[of a n b] obtain x y
where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast
- from dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
- dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
+ from nat_dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
+ nat_dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)}
hence th: "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast
from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th
--- a/src/HOL/NumberTheory/Chinese.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/Chinese.thy Sun Feb 22 10:22:46 2009 +0100
@@ -90,10 +90,8 @@
"k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
apply (induct l)
apply auto
- apply (rule_tac [1] zdvd_zmult2)
- apply (rule_tac [2] zdvd_zmult)
- apply (subgoal_tac "i = Suc (k + l)")
- apply (simp_all (no_asm_simp))
+ apply (subgoal_tac "i = Suc (k + l)")
+ apply (simp_all (no_asm_simp))
done
lemma funsum_mod:
@@ -103,7 +101,7 @@
apply (rule trans)
apply (rule mod_add_eq)
apply simp
- apply (rule zmod_zadd_right_eq [symmetric])
+ apply (rule mod_add_right_eq [symmetric])
done
lemma funsum_zero [rule_format (no_asm)]:
@@ -196,8 +194,8 @@
apply (case_tac [2] "i = n")
apply (simp_all (no_asm_simp))
apply (case_tac [3] "j < i")
- apply (rule_tac [3] zdvd_zmult2)
- apply (rule_tac [4] zdvd_zmult)
+ apply (rule_tac [3] dvd_mult2)
+ apply (rule_tac [4] dvd_mult)
apply (rule_tac [!] funprod_zdvd)
apply arith
apply arith
@@ -217,8 +215,8 @@
apply (subst funsum_mod)
apply (subst funsum_oneelem)
apply auto
- apply (subst zdvd_iff_zmod_eq_0 [symmetric])
- apply (rule zdvd_zmult)
+ apply (subst dvd_eq_mod_eq_0 [symmetric])
+ apply (rule dvd_mult)
apply (rule x_sol_lin_aux)
apply auto
done
@@ -238,20 +236,20 @@
apply safe
apply (tactic {* stac (thm "zcong_zmod") 3 *})
apply (tactic {* stac (thm "mod_mult_eq") 3 *})
- apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
- apply (tactic {* stac (thm "x_sol_lin") 5 *})
- apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
- apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
- apply (subgoal_tac [7]
+ apply (tactic {* stac (thm "mod_mod_cancel") 3 *})
+ apply (tactic {* stac (thm "x_sol_lin") 4 *})
+ apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *})
+ apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *})
+ apply (subgoal_tac [6]
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
\<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
- prefer 7
+ prefer 6
apply (simp add: zmult_ac)
apply (unfold xilin_sol_def)
- apply (tactic {* asm_simp_tac @{simpset} 7 *})
- apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
- apply (rule_tac [7] unique_xi_sol)
- apply (rule_tac [4] funprod_zdvd)
+ apply (tactic {* asm_simp_tac @{simpset} 6 *})
+ apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
+ apply (rule_tac [6] unique_xi_sol)
+ apply (rule_tac [3] funprod_zdvd)
apply (unfold m_cond_def)
apply (rule funprod_pos [THEN pos_mod_sign])
apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
--- a/src/HOL/NumberTheory/Euler.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/Euler.thy Sun Feb 22 10:22:46 2009 +0100
@@ -272,7 +272,7 @@
text {* \medskip Prove the final part of Euler's Criterion: *}
lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
- by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div zdvd_trans)
+ by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))"
by (auto simp add: nat_mult_distrib)
--- a/src/HOL/NumberTheory/EulerFermat.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.thy Sun Feb 22 10:22:46 2009 +0100
@@ -155,7 +155,7 @@
prefer 2
apply (subst zdvd_iff_zgcd [symmetric])
apply (rule_tac [4] zgcd_zcong_zgcd)
- apply (simp_all add: zdvd_zminus_iff zcong_sym)
+ apply (simp_all add: zcong_sym)
done
--- a/src/HOL/NumberTheory/Gauss.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy Sun Feb 22 10:22:46 2009 +0100
@@ -64,14 +64,14 @@
qed
lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
- using zdiv_zmult_self2 [of 2 "p - 1"] by auto
+ using div_mult_self1_is_id [of 2 "p - 1"] by auto
lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
apply (frule odd_minus_one_even)
apply (simp add: zEven_def)
apply (subgoal_tac "2 \<noteq> 0")
- apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)
+ apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
apply (auto simp add: even_div_2_prop2)
done
--- a/src/HOL/NumberTheory/Int2.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/Int2.thy Sun Feb 22 10:22:46 2009 +0100
@@ -18,7 +18,7 @@
lemma zpower_zdvd_prop1:
"0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
- by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
+ by (induct n) (auto simp add: dvd_mult2 [of p y])
lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m"
proof -
@@ -42,7 +42,7 @@
apply simp
apply (frule zprime_zdvd_zmult_better)
apply simp
- apply force
+ apply (force simp del:dvd_mult)
done
lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
@@ -86,7 +86,7 @@
by (auto simp add: zcong_def)
lemma zcong_id: "[m = 0] (mod m)"
- by (auto simp add: zcong_def zdvd_0_right)
+ by (auto simp add: zcong_def)
lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
by (auto simp add: zcong_refl zcong_zadd)
--- a/src/HOL/NumberTheory/IntPrimes.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Sun Feb 22 10:22:46 2009 +0100
@@ -50,7 +50,7 @@
lemma zrelprime_zdvd_zmult_aux:
"zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
- by (metis abs_of_nonneg zdvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
+ by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
apply (case_tac "0 \<le> m")
@@ -73,7 +73,7 @@
lemma zprime_imp_zrelprime:
"zprime p ==> \<not> p dvd n ==> zgcd n p = 1"
apply (auto simp add: zprime_def)
- apply (metis zgcd_commute zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
+ apply (metis zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
done
lemma zless_zprime_imp_zrelprime:
@@ -93,9 +93,7 @@
done
lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
- apply (simp add: zgcd_greatest_iff)
- apply (blast intro: zdvd_trans dvd_triv_right)
- done
+by (simp add: zgcd_greatest_iff)
lemma zgcd_zmult_zdvd_zgcd:
"zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n"
@@ -127,20 +125,20 @@
by (unfold zcong_def, auto)
lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
- unfolding zcong_def minus_diff_eq [of a, symmetric] zdvd_zminus_iff ..
+ unfolding zcong_def minus_diff_eq [of a, symmetric] dvd_minus_iff ..
lemma zcong_zadd:
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
apply (unfold zcong_def)
apply (rule_tac s = "(a - b) + (c - d)" in subst)
- apply (rule_tac [2] zdvd_zadd, auto)
+ apply (rule_tac [2] dvd_add, auto)
done
lemma zcong_zdiff:
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a - c = b - d] (mod m)"
apply (unfold zcong_def)
apply (rule_tac s = "(a - b) - (c - d)" in subst)
- apply (rule_tac [2] zdvd_zdiff, auto)
+ apply (rule_tac [2] dvd_diff, auto)
done
lemma zcong_trans:
@@ -151,8 +149,8 @@
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
apply (rule_tac b = "b * c" in zcong_trans)
apply (unfold zcong_def)
- apply (metis zdiff_zmult_distrib2 zdvd_zmult zmult_commute)
- apply (metis zdiff_zmult_distrib2 zdvd_zmult)
+ apply (metis zdiff_zmult_distrib2 dvd_mult zmult_commute)
+ apply (metis zdiff_zmult_distrib2 dvd_mult)
done
lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)"
@@ -163,7 +161,7 @@
lemma zcong_zmult_self: "[a * m = b * m] (mod m)"
apply (unfold zcong_def)
- apply (rule zdvd_zdiff, simp_all)
+ apply (rule dvd_diff, simp_all)
done
lemma zcong_square:
@@ -191,7 +189,7 @@
apply (simp_all add: zdiff_zmult_distrib)
apply (subgoal_tac "m dvd (-(a * k - b * k))")
apply simp
- apply (subst zdvd_zminus_iff, assumption)
+ apply (subst dvd_minus_iff, assumption)
done
lemma zcong_cancel2:
@@ -206,10 +204,10 @@
apply (subgoal_tac "m dvd n * ka")
apply (subgoal_tac "m dvd ka")
apply (case_tac [2] "0 \<le> ka")
- apply (metis zdvd_mult_div_cancel zdvd_refl zdvd_zminus2_iff zdvd_zmultD2 zgcd_zminus zmult_commute zmult_zminus zrelprime_zdvd_zmult)
- apply (metis IntDiv.zdvd_abs1 abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)
- apply (metis abs_eq_0 int_0_neq_1 mult_le_0_iff zdvd_mono zdvd_mult_cancel zdvd_mult_cancel1 zdvd_refl zdvd_triv_left zdvd_zmult2 zero_le_mult_iff zgcd_greatest_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
- apply (metis zdvd_triv_left)
+ apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult)
+ apply (metis abs_dvd_iff abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)
+ apply (metis mult_le_0_iff zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
+ apply (metis dvd_triv_left)
done
lemma zcong_zless_imp_eq:
@@ -217,7 +215,7 @@
a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
apply (unfold zcong_def dvd_def, auto)
apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
- apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff zmod_zadd_right_eq)
+ apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff mod_add_right_eq)
done
lemma zcong_square_zless:
@@ -237,7 +235,7 @@
lemma zcong_zless_0:
"0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
apply (unfold zcong_def dvd_def, auto)
- apply (metis div_pos_pos_trivial linorder_not_less zdiv_zmult_self2 zle_refl zle_trans)
+ apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id)
done
lemma zcong_zless_unique:
@@ -302,7 +300,7 @@
lemma zmod_zdvd_zmod:
"0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
- by (rule zmod_zmod_cancel)
+ by (rule mod_mod_cancel)
subsection {* Extended GCD *}
@@ -403,7 +401,7 @@
prefer 2
apply simp
apply (unfold zcong_def)
- apply (simp (no_asm) add: zmult_commute zdvd_zminus_iff)
+ apply (simp (no_asm) add: zmult_commute)
done
lemma zcong_lineq_unique:
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Sun Feb 22 10:22:46 2009 +0100
@@ -322,7 +322,7 @@
by (rule zdiv_mono1) (insert p_g_2, auto)
then show "b \<le> (q * a) div p"
apply (subgoal_tac "p \<noteq> 0")
- apply (frule zdiv_zmult_self2, force)
+ apply (frule div_mult_self1_is_id, force)
apply (insert p_g_2, auto)
done
qed
@@ -356,7 +356,7 @@
by (rule zdiv_mono1) (insert q_g_2, auto)
then show "a \<le> (p * b) div q"
apply (subgoal_tac "q \<noteq> 0")
- apply (frule zdiv_zmult_self2, force)
+ apply (frule div_mult_self1_is_id, force)
apply (insert q_g_2, auto)
done
qed
--- a/src/HOL/NumberTheory/Residues.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/Residues.thy Sun Feb 22 10:22:46 2009 +0100
@@ -48,7 +48,7 @@
by (auto simp add: StandardRes_def zcong_zmod_eq)
lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))"
- by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
+ by (auto simp add: StandardRes_def zcong_def dvd_eq_mod_eq_0)
lemma StandardRes_prop4: "2 < m
==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
--- a/src/HOL/NumberTheory/WilsonBij.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/WilsonBij.thy Sun Feb 22 10:22:46 2009 +0100
@@ -57,7 +57,7 @@
apply (rule_tac [2] zdvd_not_zless)
apply (subgoal_tac "p dvd 1")
prefer 2
- apply (subst zdvd_zminus_iff [symmetric])
+ apply (subst dvd_minus_iff [symmetric])
apply auto
done
@@ -79,7 +79,7 @@
apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
apply (simp add: mult_commute)
- apply (subst zdvd_zminus_iff)
+ apply (subst dvd_minus_iff)
apply (subst zdvd_reduce)
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
apply (subst zdvd_reduce)
--- a/src/HOL/NumberTheory/WilsonRuss.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Sun Feb 22 10:22:46 2009 +0100
@@ -68,7 +68,7 @@
apply (rule_tac [2] zdvd_not_zless)
apply (subgoal_tac "p dvd 1")
prefer 2
- apply (subst zdvd_zminus_iff [symmetric], auto)
+ apply (subst dvd_minus_iff [symmetric], auto)
done
lemma inv_not_1:
@@ -87,7 +87,7 @@
apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
apply (simp add: mult_commute)
- apply (subst zdvd_zminus_iff)
+ apply (subst dvd_minus_iff)
apply (subst zdvd_reduce)
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
apply (subst zdvd_reduce, auto)
--- a/src/HOL/Presburger.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Presburger.thy Sun Feb 22 10:22:46 2009 +0100
@@ -412,14 +412,10 @@
"(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
by (rule eq_number_of_eq)
-lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
-unfolding dvd_eq_mod_eq_0[symmetric] ..
-
-lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
-unfolding zdvd_iff_zmod_eq_0[symmetric] ..
+declare dvd_eq_mod_eq_0[symmetric, presburger]
declare mod_1[presburger]
declare mod_0[presburger]
-declare zmod_1[presburger]
+declare mod_by_1[presburger]
declare zmod_zero[presburger]
declare zmod_self[presburger]
declare mod_self[presburger]
--- a/src/HOL/RealDef.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/RealDef.thy Sun Feb 22 10:22:46 2009 +0100
@@ -655,7 +655,7 @@
real(n div d) = real n / real d"
apply (frule real_of_int_div_aux [of d n])
apply simp
- apply (simp add: zdvd_iff_zmod_eq_0)
+ apply (simp add: dvd_eq_mod_eq_0)
done
lemma real_of_int_div2:
--- a/src/HOL/Ring_and_Field.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Sun Feb 22 10:22:46 2009 +0100
@@ -147,10 +147,10 @@
lemma one_dvd [simp]: "1 dvd a"
by (auto intro!: dvdI)
-lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
by (auto intro!: mult_left_commute dvdI elim!: dvdE)
-lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
apply (subst mult_commute)
apply (erule dvd_mult)
done
@@ -162,12 +162,12 @@
by (rule dvd_mult2) (rule dvd_refl)
lemma mult_dvd_mono:
- assumes ab: "a dvd b"
- and "cd": "c dvd d"
+ assumes "a dvd b"
+ and "c dvd d"
shows "a * c dvd b * d"
proof -
- from ab obtain b' where "b = a * b'" ..
- moreover from "cd" obtain d' where "d = c * d'" ..
+ from `a dvd b` obtain b' where "b = a * b'" ..
+ moreover from `c dvd d` obtain d' where "d = c * d'" ..
ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
then show ?thesis ..
qed
@@ -310,8 +310,8 @@
then show "- x dvd y" ..
qed
-lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
-by (simp add: diff_minus dvd_add dvd_minus_iff)
+lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+by (simp add: diff_minus dvd_minus_iff)
end
--- a/src/HOL/Tools/Qelim/presburger.ML Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Sun Feb 22 10:22:46 2009 +0100
@@ -122,14 +122,13 @@
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
val div_mod_ss = HOL_basic_ss addsimps simp_thms
@ map (symmetric o mk_meta_eq)
- [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
+ [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add1_eq"},
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
- @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"},
- @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
+ @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"},
- @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"},
+ @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
@{thm "mod_1"}, @{thm "Suc_plus1"}]
@ @{thms add_ac}
addsimprocs [cancel_div_mod_proc]
--- a/src/HOL/Tools/int_factor_simprocs.ML Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML Sun Feb 22 10:22:46 2009 +0100
@@ -216,7 +216,7 @@
(** Final simplification for the CancelFactor simprocs **)
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
- [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, @{thm numeral_1_eq_1}];
+ [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
fun cancel_simplify_meta_eq cancel_th ss th =
simplify_one ss (([th, cancel_th]) MRS trans);
--- a/src/HOL/Word/BinGeneral.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Word/BinGeneral.thy Sun Feb 22 10:22:46 2009 +0100
@@ -433,7 +433,7 @@
"!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
apply (induct n)
apply clarsimp
- apply (subst zmod_zadd_left_eq)
+ apply (subst mod_add_left_eq)
apply (simp add: bin_last_mod)
apply (simp add: number_of_eq)
apply clarsimp
@@ -767,23 +767,23 @@
lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard]
lemmas brdmod1s' [symmetric] =
- zmod_zadd_left_eq zmod_zadd_right_eq
+ mod_add_left_eq mod_add_right_eq
zmod_zsub_left_eq zmod_zsub_right_eq
zmod_zmult1_eq zmod_zmult1_eq_rev
lemmas brdmods' [symmetric] =
zpower_zmod' [symmetric]
- trans [OF zmod_zadd_left_eq zmod_zadd_right_eq]
+ trans [OF mod_add_left_eq mod_add_right_eq]
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq]
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev]
zmod_uminus' [symmetric]
- zmod_zadd_left_eq [where b = "1"]
+ mod_add_left_eq [where b = "1::int"]
zmod_zsub_left_eq [where b = "1"]
lemmas bintr_arith1s =
- brdmod1s' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
+ brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
lemmas bintr_ariths =
- brdmods' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
+ brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard]
--- a/src/HOL/Word/Num_Lemmas.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy Sun Feb 22 10:22:46 2009 +0100
@@ -95,7 +95,7 @@
lemma z1pdiv2:
"(2 * b + 1) div 2 = (b::int)" by arith
-lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2,
+lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
simplified int_one_le_iff_zero_less, simplified, standard]
lemma axxbyy:
@@ -127,12 +127,12 @@
lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
apply (unfold diff_int_def)
- apply (rule trans [OF _ zmod_zadd_right_eq [symmetric]])
- apply (simp add : zmod_uminus zmod_zadd_right_eq [symmetric])
+ apply (rule trans [OF _ mod_add_right_eq [symmetric]])
+ apply (simp add : zmod_uminus mod_add_right_eq [symmetric])
done
lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
- by (rule zmod_zadd_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
+ by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
lemma zmod_zsub_self [simp]:
"((b :: int) - a) mod a = b mod a"
@@ -146,8 +146,8 @@
done
lemmas rdmods [symmetric] = zmod_uminus [symmetric]
- zmod_zsub_left_eq zmod_zsub_right_eq zmod_zadd_left_eq
- zmod_zadd_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
+ zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
+ mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
lemma mod_plus_right:
"((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
@@ -169,7 +169,8 @@
lemmas push_mods = push_mods' [THEN eq_reflection, standard]
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard]
lemmas mod_simps =
- zmod_zmult_self1 [THEN eq_reflection] zmod_zmult_self2 [THEN eq_reflection]
+ mod_mult_self2_is_0 [THEN eq_reflection]
+ mod_mult_self1_is_0 [THEN eq_reflection]
mod_mod_trivial [THEN eq_reflection]
lemma nat_mod_eq:
@@ -313,7 +314,7 @@
"a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
apply clarsimp
apply safe
- apply (simp add: zdvd_iff_zmod_eq_0 [symmetric])
+ apply (simp add: dvd_eq_mod_eq_0 [symmetric])
apply (drule le_iff_add [THEN iffD1])
apply (force simp: zpower_zadd_distrib)
apply (rule mod_pos_pos_trivial)
--- a/src/HOL/Word/WordGenLib.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Word/WordGenLib.thy Sun Feb 22 10:22:46 2009 +0100
@@ -273,7 +273,7 @@
have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
show ?thesis
apply (subst x)
- apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2)
+ apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
apply simp
done
qed
--- a/src/HOL/Word/WordShift.thy Sun Feb 22 10:22:30 2009 +0100
+++ b/src/HOL/Word/WordShift.thy Sun Feb 22 10:22:46 2009 +0100
@@ -530,7 +530,7 @@
done
lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
- apply (simp add: zdvd_iff_zmod_eq_0 and_mask_mod_2p)
+ apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
apply (subst word_uint.norm_Rep [symmetric])
apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)