# HG changeset patch # User wenzelm # Date 1236101601 -3600 # Node ID 2bf6432b9740e76f6c71a4586e05cf9a75f0ae41 # Parent 79136ce06bdbb26d7d0940603d64fbd2716bf3e9# Parent 24d97535287997e7a380cca40e824e5d6d47953b merged diff -r 24d975352879 -r 2bf6432b9740 NEWS --- a/NEWS Tue Mar 03 18:32:01 2009 +0100 +++ b/NEWS Tue Mar 03 18:33:21 2009 +0100 @@ -376,12 +376,16 @@ 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 +* HOL/IntDiv: removed many 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 +mod_add1_eq -> mod_add_eq +mod_mult1_eq -> mod_mult_right_eq +mod_mult1_eq' -> mod_mult_left_eq +mod_mult_distrib_mod -> mod_mult_eq 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 @@ -398,7 +402,7 @@ zmod_zadd_right_eq -> mod_add_right_eq zmod_zadd_self1 -> mod_add_self1 zmod_zadd_self2 -> mod_add_self2 -zmod_zadd1_eq -> mod_add1_eq +zmod_zadd1_eq -> mod_add_eq zmod_zdiff1_eq -> mod_diff_eq zmod_zdvd_zmod -> mod_mod_cancel zmod_zmod_cancel -> mod_mod_cancel diff -r 24d975352879 -r 2bf6432b9740 doc-src/TutorialI/Types/Numbers.thy --- a/doc-src/TutorialI/Types/Numbers.thy Tue Mar 03 18:32:01 2009 +0100 +++ b/doc-src/TutorialI/Types/Numbers.thy Tue Mar 03 18:33:21 2009 +0100 @@ -100,8 +100,8 @@ @{thm[display] div_mult1_eq[no_vars]} \rulename{div_mult1_eq} -@{thm[display] mod_mult1_eq[no_vars]} -\rulename{mod_mult1_eq} +@{thm[display] mod_mult_right_eq[no_vars]} +\rulename{mod_mult_right_eq} @{thm[display] div_mult2_eq[no_vars]} \rulename{div_mult2_eq} @@ -147,8 +147,8 @@ @{thm[display] zdiv_zadd1_eq[no_vars]} \rulename{zdiv_zadd1_eq} -@{thm[display] mod_add1_eq[no_vars]} -\rulename{mod_add1_eq} +@{thm[display] mod_add_eq[no_vars]} +\rulename{mod_add_eq} @{thm[display] zdiv_zmult1_eq[no_vars]} \rulename{zdiv_zmult1_eq} diff -r 24d975352879 -r 2bf6432b9740 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Mar 03 18:32:01 2009 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Mar 03 18:33:21 2009 +0100 @@ -244,7 +244,7 @@ \begin{isabelle}% a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c% \end{isabelle} -\rulename{mod_mult1_eq} +\rulename{mod_mult_right_eq} \begin{isabelle}% a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% @@ -318,7 +318,7 @@ \begin{isabelle}% {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c% \end{isabelle} -\rulename{mod_add1_eq} +\rulename{mod_add_eq} \begin{isabelle}% a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c% diff -r 24d975352879 -r 2bf6432b9740 doc-src/TutorialI/Types/numerics.tex --- a/doc-src/TutorialI/Types/numerics.tex Tue Mar 03 18:32:01 2009 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Tue Mar 03 18:33:21 2009 +0100 @@ -154,7 +154,7 @@ a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c% \rulename{div_mult1_eq}\isanewline a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c% -\rulename{mod_mult1_eq}\isanewline +\rulename{mod_mult_right_eq}\isanewline a\ div\ (b*c)\ =\ a\ div\ b\ div\ c% \rulename{div_mult2_eq}\isanewline a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b% @@ -276,7 +276,7 @@ \rulename{zdiv_zadd1_eq} \par\smallskip (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c% -\rulename{mod_add1_eq} +\rulename{mod_add_eq} \end{isabelle} \begin{isabelle} diff -r 24d975352879 -r 2bf6432b9740 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Mar 03 18:32:01 2009 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Mar 03 18:33:21 2009 +0100 @@ -27,10 +27,9 @@ val Suc_plus1 = @{thm Suc_plus1}; 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 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 mod_add_eq = @{thm mod_add_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; @@ -68,8 +67,8 @@ 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, mod_add_left_eq, - mod_add_right_eq, int_mod_add_eq, + addsimps [refl,mod_add_eq, mod_add_left_eq, + mod_add_right_eq, nat_div_add_eq, int_div_add_eq, @{thm mod_self}, @{thm "zmod_self"}, @{thm mod_by_0}, @{thm div_by_0}, diff -r 24d975352879 -r 2bf6432b9740 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Tue Mar 03 18:32:01 2009 +0100 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Mar 03 18:33:21 2009 +0100 @@ -31,10 +31,8 @@ val Suc_plus1 = @{thm Suc_plus1}; 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 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 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; diff -r 24d975352879 -r 2bf6432b9740 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Tue Mar 03 18:32:01 2009 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Mar 03 18:33:21 2009 +0100 @@ -46,10 +46,9 @@ val Suc_plus1 = @{thm "Suc_plus1"}; 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 mod_add_eq = @{thm "mod_add_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 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; @@ -94,7 +93,7 @@ val (t,np,nh) = prepare_for_mir thy 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, + addsimps [refl, mod_add_eq, @{thm "mod_self"}, @{thm "zmod_self"}, @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, diff -r 24d975352879 -r 2bf6432b9740 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Mar 03 18:32:01 2009 +0100 +++ b/src/HOL/Divides.thy Tue Mar 03 18:33:21 2009 +0100 @@ -684,16 +684,6 @@ apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq]) done -lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)" -by (rule mod_mult_right_eq) - -lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c" -by (rule mod_mult_left_eq) - -lemma mod_mult_distrib_mod: - "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c" -by (rule mod_mult_eq) - lemma divmod_rel_add1_eq: "[| divmod_rel a c aq ar; divmod_rel b c bq br; c > 0 |] ==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)" @@ -706,9 +696,6 @@ apply (blast intro: divmod_rel_add1_eq [THEN div_eq] divmod_rel) done -lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c" -by (rule mod_add_eq) - lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c" apply (cut_tac m = q and n = c in mod_less_divisor) apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto) diff -r 24d975352879 -r 2bf6432b9740 src/HOL/Library/Char_nat.thy --- a/src/HOL/Library/Char_nat.thy Tue Mar 03 18:32:01 2009 +0100 +++ b/src/HOL/Library/Char_nat.thy Tue Mar 03 18:33:21 2009 +0100 @@ -132,7 +132,7 @@ lemma Char_char_of_nat: "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)" unfolding char_of_nat_def Let_def nibble_pair_of_nat_def - by (auto simp add: div_add1_eq mod_add1_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble) + by (auto simp add: div_add1_eq mod_add_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble) lemma char_of_nat_of_char: "char_of_nat (nat_of_char c) = c" @@ -165,7 +165,7 @@ show ?thesis by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair nat_of_nibble_of_nat mod_mult_distrib - n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256) + n aux3 mod_mult_self3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256) qed lemma nibble_pair_of_nat_char: diff -r 24d975352879 -r 2bf6432b9740 src/HOL/Library/Pocklington.thy --- a/src/HOL/Library/Pocklington.thy Tue Mar 03 18:32:01 2009 +0100 +++ b/src/HOL/Library/Pocklington.thy Tue Mar 03 18:33:21 2009 +0100 @@ -142,10 +142,10 @@ shows "[x * y = x' * y'] (mod n)" proof- have "(x * y) mod n = (x mod n) * (y mod n) mod n" - by (simp add: mod_mult1_eq'[of x y n] mod_mult1_eq[of "x mod n" y n]) + by (simp add: mod_mult_left_eq[of x y n] mod_mult_right_eq[of "x mod n" y n]) also have "\ = (x' mod n) * (y' mod n) mod n" using xx'[unfolded modeq_def] yy'[unfolded modeq_def] by simp also have "\ = (x' * y') mod n" - by (simp add: mod_mult1_eq'[of x' y' n] mod_mult1_eq[of "x' mod n" y' n]) + by (simp add: mod_mult_left_eq[of x' y' n] mod_mult_right_eq[of "x' mod n" y' n]) finally show ?thesis unfolding modeq_def . qed @@ -296,7 +296,7 @@ from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast let ?x = "x mod n" from x have th: "[a * ?x = b] (mod n)" - by (simp add: modeq_def mod_mult1_eq[of a x n]) + by (simp add: modeq_def mod_mult_right_eq[of a x n]) from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp {fix y assume Py: "y < n" "[a * y = b] (mod n)" from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: modeq_def) @@ -753,10 +753,10 @@ next case (Suc n) have "(x mod m)^(Suc n) mod m = ((x mod m) * (((x mod m) ^ n) mod m)) mod m" - by (simp add: mod_mult1_eq[symmetric]) + by (simp add: mod_mult_right_eq[symmetric]) also have "\ = ((x mod m) * (x^n mod m)) mod m" using Suc.hyps by simp also have "\ = x^(Suc n) mod m" - by (simp add: mod_mult1_eq'[symmetric] mod_mult1_eq[symmetric]) + by (simp add: mod_mult_left_eq[symmetric] mod_mult_right_eq[symmetric]) finally show ?case . qed @@ -891,9 +891,9 @@ hence "[(a^?o)^?q * (a^?r) = 1] (mod n)" by (simp add: modeq_def power_mult[symmetric] power_add[symmetric]) hence th: "[a^?r = 1] (mod n)" - using eqo mod_mult1_eq'[of "(a^?o)^?q" "a^?r" n] + using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n] apply (simp add: modeq_def del: One_nat_def) - by (simp add: mod_mult1_eq'[symmetric]) + by (simp add: mod_mult_left_eq[symmetric]) {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)} moreover {assume r: "?r \ 0" diff -r 24d975352879 -r 2bf6432b9740 src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Tue Mar 03 18:32:01 2009 +0100 +++ b/src/HOL/Library/Word.thy Tue Mar 03 18:33:21 2009 +0100 @@ -575,7 +575,7 @@ have "?lhs = (1 + 2 * bv_to_nat w) mod 2" by (simp add: add_commute) also have "... = 1" - by (subst mod_add1_eq) simp + by (subst mod_add_eq) simp finally have eq1: "?lhs = 1" . have "?rhs = 0" by simp with orig and eq1 diff -r 24d975352879 -r 2bf6432b9740 src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Tue Mar 03 18:32:01 2009 +0100 +++ b/src/HOL/Tools/Qelim/presburger.ML Tue Mar 03 18:33:21 2009 +0100 @@ -122,7 +122,7 @@ 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 "mod_add1_eq"}, + [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}] @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},