removed and renamed redundant lemmas
authornipkow
Tue Mar 03 17:05:18 2009 +0100 (2009-03-03)
changeset 3022479136ce06bdb
parent 30207 c56d27155041
child 30225 2bf6432b9740
child 30228 2aaf339fb7c1
child 30235 58d147683393
removed and renamed redundant lemmas
NEWS
doc-src/TutorialI/Types/Numbers.thy
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/numerics.tex
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Divides.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/Pocklington.thy
src/HOL/Library/Word.thy
src/HOL/Tools/Qelim/presburger.ML
     1.1 --- a/NEWS	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/NEWS	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -376,12 +376,16 @@
     1.4      mult_div ~>             div_mult_self2_is_id
     1.5      mult_mod ~>             mod_mult_self2_is_0
     1.6  
     1.7 -* HOL/IntDiv: removed most (all?) lemmas that are instances of class-based
     1.8 +* HOL/IntDiv: removed many lemmas that are instances of class-based
     1.9  generalizations (from Divides and Ring_and_Field).
    1.10  INCOMPATIBILITY. Rename old lemmas as follows:
    1.11  
    1.12  dvd_diff               -> nat_dvd_diff
    1.13  dvd_zminus_iff         -> dvd_minus_iff
    1.14 +mod_add1_eq            -> mod_add_eq
    1.15 +mod_mult1_eq           -> mod_mult_right_eq
    1.16 +mod_mult1_eq'          -> mod_mult_left_eq
    1.17 +mod_mult_distrib_mod   -> mod_mult_eq
    1.18  nat_mod_add_left_eq    -> mod_add_left_eq
    1.19  nat_mod_add_right_eq   -> mod_add_right_eq
    1.20  nat_mod_div_trivial    -> mod_div_trivial
    1.21 @@ -398,7 +402,7 @@
    1.22  zmod_zadd_right_eq     -> mod_add_right_eq
    1.23  zmod_zadd_self1        -> mod_add_self1
    1.24  zmod_zadd_self2        -> mod_add_self2
    1.25 -zmod_zadd1_eq          -> mod_add1_eq
    1.26 +zmod_zadd1_eq          -> mod_add_eq
    1.27  zmod_zdiff1_eq         -> mod_diff_eq
    1.28  zmod_zdvd_zmod         -> mod_mod_cancel
    1.29  zmod_zmod_cancel       -> mod_mod_cancel
     2.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Tue Mar 03 12:14:52 2009 +1100
     2.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Tue Mar 03 17:05:18 2009 +0100
     2.3 @@ -100,8 +100,8 @@
     2.4  @{thm[display] div_mult1_eq[no_vars]}
     2.5  \rulename{div_mult1_eq}
     2.6  
     2.7 -@{thm[display] mod_mult1_eq[no_vars]}
     2.8 -\rulename{mod_mult1_eq}
     2.9 +@{thm[display] mod_mult_right_eq[no_vars]}
    2.10 +\rulename{mod_mult_right_eq}
    2.11  
    2.12  @{thm[display] div_mult2_eq[no_vars]}
    2.13  \rulename{div_mult2_eq}
    2.14 @@ -147,8 +147,8 @@
    2.15  @{thm[display] zdiv_zadd1_eq[no_vars]}
    2.16  \rulename{zdiv_zadd1_eq}
    2.17  
    2.18 -@{thm[display] mod_add1_eq[no_vars]}
    2.19 -\rulename{mod_add1_eq}
    2.20 +@{thm[display] mod_add_eq[no_vars]}
    2.21 +\rulename{mod_add_eq}
    2.22  
    2.23  @{thm[display] zdiv_zmult1_eq[no_vars]}
    2.24  \rulename{zdiv_zmult1_eq}
     3.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Tue Mar 03 12:14:52 2009 +1100
     3.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Tue Mar 03 17:05:18 2009 +0100
     3.3 @@ -244,7 +244,7 @@
     3.4  \begin{isabelle}%
     3.5  a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c%
     3.6  \end{isabelle}
     3.7 -\rulename{mod_mult1_eq}
     3.8 +\rulename{mod_mult_right_eq}
     3.9  
    3.10  \begin{isabelle}%
    3.11  a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
    3.12 @@ -318,7 +318,7 @@
    3.13  \begin{isabelle}%
    3.14  {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c%
    3.15  \end{isabelle}
    3.16 -\rulename{mod_add1_eq}
    3.17 +\rulename{mod_add_eq}
    3.18  
    3.19  \begin{isabelle}%
    3.20  a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c%
     4.1 --- a/doc-src/TutorialI/Types/numerics.tex	Tue Mar 03 12:14:52 2009 +1100
     4.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Tue Mar 03 17:05:18 2009 +0100
     4.3 @@ -154,7 +154,7 @@
     4.4  a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
     4.5  \rulename{div_mult1_eq}\isanewline
     4.6  a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
     4.7 -\rulename{mod_mult1_eq}\isanewline
     4.8 +\rulename{mod_mult_right_eq}\isanewline
     4.9  a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
    4.10  \rulename{div_mult2_eq}\isanewline
    4.11  a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
    4.12 @@ -276,7 +276,7 @@
    4.13  \rulename{zdiv_zadd1_eq}
    4.14  \par\smallskip
    4.15  (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
    4.16 -\rulename{mod_add1_eq}
    4.17 +\rulename{mod_add_eq}
    4.18  \end{isabelle}
    4.19  
    4.20  \begin{isabelle}
     5.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 03 12:14:52 2009 +1100
     5.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 03 17:05:18 2009 +0100
     5.3 @@ -27,10 +27,9 @@
     5.4  val Suc_plus1 = @{thm Suc_plus1};
     5.5  val imp_le_cong = @{thm imp_le_cong};
     5.6  val conj_le_cong = @{thm conj_le_cong};
     5.7 -val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
     5.8  val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     5.9  val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    5.10 -val int_mod_add_eq = @{thm mod_add_eq} RS sym;
    5.11 +val mod_add_eq = @{thm mod_add_eq} RS sym;
    5.12  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    5.13  val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    5.14  
    5.15 @@ -68,8 +67,8 @@
    5.16      val (t,np,nh) = prepare_for_linz q g
    5.17      (* Some simpsets for dealing with mod div abs and nat*)
    5.18      val mod_div_simpset = HOL_basic_ss 
    5.19 -			addsimps [refl,nat_mod_add_eq, mod_add_left_eq, 
    5.20 -				  mod_add_right_eq, int_mod_add_eq, 
    5.21 +			addsimps [refl,mod_add_eq, mod_add_left_eq, 
    5.22 +				  mod_add_right_eq,
    5.23  				  nat_div_add_eq, int_div_add_eq,
    5.24  				  @{thm mod_self}, @{thm "zmod_self"},
    5.25  				  @{thm mod_by_0}, @{thm div_by_0},
     6.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 03 12:14:52 2009 +1100
     6.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 03 17:05:18 2009 +0100
     6.3 @@ -31,10 +31,8 @@
     6.4  val Suc_plus1 = @{thm Suc_plus1};
     6.5  val imp_le_cong = @{thm imp_le_cong};
     6.6  val conj_le_cong = @{thm conj_le_cong};
     6.7 -val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
     6.8  val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     6.9  val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    6.10 -val int_mod_add_eq = @{thm mod_add_eq} RS sym;
    6.11  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    6.12  val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    6.13  val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
     7.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 03 12:14:52 2009 +1100
     7.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 03 17:05:18 2009 +0100
     7.3 @@ -46,10 +46,9 @@
     7.4  val Suc_plus1 = @{thm "Suc_plus1"};
     7.5  val imp_le_cong = @{thm "imp_le_cong"};
     7.6  val conj_le_cong = @{thm "conj_le_cong"};
     7.7 -val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
     7.8 +val mod_add_eq = @{thm "mod_add_eq"} RS sym;
     7.9  val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
    7.10  val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
    7.11 -val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
    7.12  val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
    7.13  val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
    7.14  val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
    7.15 @@ -94,7 +93,7 @@
    7.16      val (t,np,nh) = prepare_for_mir thy q g
    7.17      (* Some simpsets for dealing with mod div abs and nat*)
    7.18      val mod_div_simpset = HOL_basic_ss 
    7.19 -                        addsimps [refl,nat_mod_add_eq, 
    7.20 +                        addsimps [refl, mod_add_eq, 
    7.21                                    @{thm "mod_self"}, @{thm "zmod_self"},
    7.22                                    @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
    7.23                                    @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     8.1 --- a/src/HOL/Divides.thy	Tue Mar 03 12:14:52 2009 +1100
     8.2 +++ b/src/HOL/Divides.thy	Tue Mar 03 17:05:18 2009 +0100
     8.3 @@ -684,16 +684,6 @@
     8.4  apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
     8.5  done
     8.6  
     8.7 -lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
     8.8 -by (rule mod_mult_right_eq)
     8.9 -
    8.10 -lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
    8.11 -by (rule mod_mult_left_eq)
    8.12 -
    8.13 -lemma mod_mult_distrib_mod:
    8.14 -  "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
    8.15 -by (rule mod_mult_eq)
    8.16 -
    8.17  lemma divmod_rel_add1_eq:
    8.18    "[| divmod_rel a c aq ar; divmod_rel b c bq br;  c > 0 |]
    8.19     ==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)"
    8.20 @@ -706,9 +696,6 @@
    8.21  apply (blast intro: divmod_rel_add1_eq [THEN div_eq] divmod_rel)
    8.22  done
    8.23  
    8.24 -lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
    8.25 -by (rule mod_add_eq)
    8.26 -
    8.27  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
    8.28    apply (cut_tac m = q and n = c in mod_less_divisor)
    8.29    apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
     9.1 --- a/src/HOL/Library/Char_nat.thy	Tue Mar 03 12:14:52 2009 +1100
     9.2 +++ b/src/HOL/Library/Char_nat.thy	Tue Mar 03 17:05:18 2009 +0100
     9.3 @@ -132,7 +132,7 @@
     9.4  lemma Char_char_of_nat:
     9.5    "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
     9.6    unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
     9.7 -  by (auto simp add: div_add1_eq mod_add1_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
     9.8 +  by (auto simp add: div_add1_eq mod_add_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
     9.9  
    9.10  lemma char_of_nat_of_char:
    9.11    "char_of_nat (nat_of_char c) = c"
    9.12 @@ -165,7 +165,7 @@
    9.13    show ?thesis
    9.14      by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
    9.15        nat_of_nibble_of_nat mod_mult_distrib
    9.16 -      n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
    9.17 +      n aux3 mod_mult_self3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
    9.18  qed
    9.19  
    9.20  lemma nibble_pair_of_nat_char:
    10.1 --- a/src/HOL/Library/Pocklington.thy	Tue Mar 03 12:14:52 2009 +1100
    10.2 +++ b/src/HOL/Library/Pocklington.thy	Tue Mar 03 17:05:18 2009 +0100
    10.3 @@ -142,10 +142,10 @@
    10.4    shows "[x * y = x' * y'] (mod n)"
    10.5  proof-
    10.6    have "(x * y) mod n = (x mod n) * (y mod n) mod n"  
    10.7 -    by (simp add: mod_mult1_eq'[of x y n] mod_mult1_eq[of "x mod n" y n])
    10.8 +    by (simp add: mod_mult_left_eq[of x y n] mod_mult_right_eq[of "x mod n" y n])
    10.9    also have "\<dots> = (x' mod n) * (y' mod n) mod n" using xx'[unfolded modeq_def] yy'[unfolded modeq_def] by simp  
   10.10    also have "\<dots> = (x' * y') mod n"
   10.11 -    by (simp add: mod_mult1_eq'[of x' y' n] mod_mult1_eq[of "x' mod n" y' n])
   10.12 +    by (simp add: mod_mult_left_eq[of x' y' n] mod_mult_right_eq[of "x' mod n" y' n])
   10.13    finally show ?thesis unfolding modeq_def . 
   10.14  qed
   10.15  
   10.16 @@ -296,7 +296,7 @@
   10.17    from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
   10.18    let ?x = "x mod n"
   10.19    from x have th: "[a * ?x = b] (mod n)"
   10.20 -    by (simp add: modeq_def mod_mult1_eq[of a x n])
   10.21 +    by (simp add: modeq_def mod_mult_right_eq[of a x n])
   10.22    from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
   10.23    {fix y assume Py: "y < n" "[a * y = b] (mod n)"
   10.24      from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: modeq_def)
   10.25 @@ -753,10 +753,10 @@
   10.26  next
   10.27    case (Suc n) 
   10.28    have "(x mod m)^(Suc n) mod m = ((x mod m) * (((x mod m) ^ n) mod m)) mod m" 
   10.29 -    by (simp add: mod_mult1_eq[symmetric])
   10.30 +    by (simp add: mod_mult_right_eq[symmetric])
   10.31    also have "\<dots> = ((x mod m) * (x^n mod m)) mod m" using Suc.hyps by simp
   10.32    also have "\<dots> = x^(Suc n) mod m"
   10.33 -    by (simp add: mod_mult1_eq'[symmetric] mod_mult1_eq[symmetric])
   10.34 +    by (simp add: mod_mult_left_eq[symmetric] mod_mult_right_eq[symmetric])
   10.35    finally show ?case .
   10.36  qed
   10.37  
   10.38 @@ -891,9 +891,9 @@
   10.39      hence "[(a^?o)^?q * (a^?r) = 1] (mod n)" 
   10.40        by (simp add: modeq_def power_mult[symmetric] power_add[symmetric])
   10.41      hence th: "[a^?r = 1] (mod n)"
   10.42 -      using eqo mod_mult1_eq'[of "(a^?o)^?q" "a^?r" n]
   10.43 +      using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
   10.44        apply (simp add: modeq_def del: One_nat_def)
   10.45 -      by (simp add: mod_mult1_eq'[symmetric])
   10.46 +      by (simp add: mod_mult_left_eq[symmetric])
   10.47      {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
   10.48      moreover
   10.49      {assume r: "?r \<noteq> 0" 
    11.1 --- a/src/HOL/Library/Word.thy	Tue Mar 03 12:14:52 2009 +1100
    11.2 +++ b/src/HOL/Library/Word.thy	Tue Mar 03 17:05:18 2009 +0100
    11.3 @@ -575,7 +575,7 @@
    11.4      have "?lhs = (1 + 2 * bv_to_nat w) mod 2"
    11.5        by (simp add: add_commute)
    11.6      also have "... = 1"
    11.7 -      by (subst mod_add1_eq) simp
    11.8 +      by (subst mod_add_eq) simp
    11.9      finally have eq1: "?lhs = 1" .
   11.10      have "?rhs  = 0" by simp
   11.11      with orig and eq1
    12.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Tue Mar 03 12:14:52 2009 +1100
    12.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Tue Mar 03 17:05:18 2009 +0100
    12.3 @@ -122,7 +122,7 @@
    12.4    addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    12.5  val div_mod_ss = HOL_basic_ss addsimps simp_thms 
    12.6    @ map (symmetric o mk_meta_eq) 
    12.7 -    [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add1_eq"}, 
    12.8 +    [@{thm "dvd_eq_mod_eq_0"},
    12.9       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
   12.10       @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   12.11    @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},