removed some lemma duplicates
authorhaftmann
Sun May 06 18:20:25 2018 +0000 (13 months ago)
changeset 68100b2d84b1114fa
parent 68099 305f9f3edf05
child 68107 3687109009c4
removed some lemma duplicates
NEWS
src/HOL/Divides.thy
src/HOL/Groebner_Basis.thy
src/HOL/Presburger.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Sun May 06 18:20:25 2018 +0000
     1.2 +++ b/NEWS	Sun May 06 18:20:25 2018 +0000
     1.3 @@ -278,10 +278,6 @@
     1.4  HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid
     1.8 -clash with fact mod_mult_self4 (on more generic semirings).
     1.9 -INCOMPATIBILITY.
    1.10 -
    1.11  * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
    1.12  sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
    1.13  interpretation of abstract locales. INCOMPATIBILITY.
    1.14 @@ -318,6 +314,18 @@
    1.15  * Code generation: Code generation takes an explicit option
    1.16  "case_insensitive" to accomodate case-insensitive file systems.
    1.17  
    1.18 +* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
    1.19 +clash with fact mod_mult_self4 (on more generic semirings).
    1.20 +INCOMPATIBILITY.
    1.21 +
    1.22 +* Eliminated some theorem aliasses:
    1.23 +
    1.24 +  even_times_iff ~> even_mult_iff
    1.25 +  mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
    1.26 +  even_of_nat ~> even_int_iff
    1.27 +
    1.28 +INCOMPATIBILITY.
    1.29 +
    1.30  
    1.31  *** System ***
    1.32  
     2.1 --- a/src/HOL/Divides.thy	Sun May 06 18:20:25 2018 +0000
     2.2 +++ b/src/HOL/Divides.thy	Sun May 06 18:20:25 2018 +0000
     2.3 @@ -1295,10 +1295,6 @@
     2.4  
     2.5  subsubsection \<open>Lemmas of doubtful value\<close>
     2.6  
     2.7 -lemma mod_mult_self3':
     2.8 -  "Suc (k * n + m) mod n = Suc m mod n"
     2.9 -  by (fact Suc_mod_mult_self3)
    2.10 -
    2.11  lemma mod_Suc_eq_Suc_mod:
    2.12    "Suc m mod n = Suc (m mod n) mod n"
    2.13    by (simp add: mod_simps)
    2.14 @@ -1327,16 +1323,6 @@
    2.15    then show ?thesis ..
    2.16  qed
    2.17  
    2.18 -lemmas even_times_iff = even_mult_iff \<comment> \<open>FIXME duplicate\<close>
    2.19 -
    2.20 -lemma mod_2_not_eq_zero_eq_one_nat:
    2.21 -  fixes n :: nat
    2.22 -  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
    2.23 -  by (fact not_mod_2_eq_0_eq_1)
    2.24 -
    2.25 -lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
    2.26 -  by (fact even_of_nat)
    2.27 -
    2.28  lemma is_unit_int:
    2.29    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    2.30    by auto
     3.1 --- a/src/HOL/Groebner_Basis.thy	Sun May 06 18:20:25 2018 +0000
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Sun May 06 18:20:25 2018 +0000
     3.3 @@ -78,7 +78,7 @@
     3.4  context semiring_parity
     3.5  begin
     3.6  
     3.7 -declare even_times_iff [algebra]
     3.8 +declare even_mult_iff [algebra]
     3.9  declare even_power [algebra]
    3.10  
    3.11  end
     4.1 --- a/src/HOL/Presburger.thy	Sun May 06 18:20:25 2018 +0000
     4.2 +++ b/src/HOL/Presburger.thy	Sun May 06 18:20:25 2018 +0000
     4.3 @@ -435,7 +435,7 @@
     4.4  context semiring_parity
     4.5  begin
     4.6  
     4.7 -declare even_times_iff [presburger]
     4.8 +declare even_mult_iff [presburger]
     4.9  
    4.10  declare even_power [presburger]
    4.11  
     5.1 --- a/src/HOL/Transcendental.thy	Sun May 06 18:20:25 2018 +0000
     5.2 +++ b/src/HOL/Transcendental.thy	Sun May 06 18:20:25 2018 +0000
     5.3 @@ -4173,10 +4173,10 @@
     5.4  lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
     5.5  proof safe
     5.6    assume "cos x = 0"
     5.7 -  then show "\<exists>n. odd n \<and> x = of_int n * (pi/2)"
     5.8 -    apply (simp add: cos_zero_iff)
     5.9 -    apply safe
    5.10 -     apply (metis even_int_iff of_int_of_nat_eq)
    5.11 +  then show "\<exists>n. odd n \<and> x = of_int n * (pi / 2)"
    5.12 +    unfolding cos_zero_iff
    5.13 +    apply (auto simp add: cos_zero_iff)
    5.14 +     apply (metis even_of_nat of_int_of_nat_eq)
    5.15      apply (rule_tac x="- (int n)" in exI)
    5.16      apply simp
    5.17      done
    5.18 @@ -4196,7 +4196,7 @@
    5.19    then show "\<exists>n. even n \<and> x = of_int n * (pi / 2)"
    5.20      apply (simp add: sin_zero_iff)
    5.21      apply safe
    5.22 -     apply (metis even_int_iff of_int_of_nat_eq)
    5.23 +     apply (metis even_of_nat of_int_of_nat_eq)
    5.24      apply (rule_tac x="- (int n)" in exI)
    5.25      apply simp
    5.26      done