more lemmas
authorhaftmann
Mon Sep 26 07:56:54 2016 +0200 (2016-09-26)
changeset 63947559f0882d6a6
parent 63946 d05da6b707dd
child 63948 429cfc5f2559
more lemmas
src/HOL/Divides.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Divides.thy	Mon Sep 26 07:56:53 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -2310,6 +2310,16 @@
     1.4      by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
     1.5  qed
     1.6  
     1.7 +lemma zmod_trival_iff:
     1.8 +  fixes i k :: int
     1.9 +  shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
    1.10 +proof -
    1.11 +  have "i mod k = i \<longleftrightarrow> i div k = 0"
    1.12 +    by safe (insert mod_div_equality [of i k], auto)
    1.13 +  with zdiv_eq_0_iff
    1.14 +  show ?thesis
    1.15 +    by simp
    1.16 +qed
    1.17  
    1.18  subsubsection \<open>Quotients of Signs\<close>
    1.19  
     2.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Sep 26 07:56:53 2016 +0200
     2.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Sep 26 07:56:54 2016 +0200
     2.3 @@ -26,6 +26,22 @@
     2.4      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
     2.5  begin
     2.6  
     2.7 +lemma euclidean_size_normalize [simp]:
     2.8 +  "euclidean_size (normalize a) = euclidean_size a"
     2.9 +proof (cases "a = 0")
    2.10 +  case True
    2.11 +  then show ?thesis
    2.12 +    by simp
    2.13 +next
    2.14 +  case [simp]: False
    2.15 +  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
    2.16 +    by (rule size_mult_mono) simp
    2.17 +  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
    2.18 +    by (rule size_mult_mono) simp
    2.19 +  ultimately show ?thesis
    2.20 +    by simp
    2.21 +qed
    2.22 +
    2.23  lemma euclidean_division:
    2.24    fixes a :: 'a and b :: 'a
    2.25    assumes "b \<noteq> 0"
     3.1 --- a/src/HOL/Rings.thy	Mon Sep 26 07:56:53 2016 +0200
     3.2 +++ b/src/HOL/Rings.thy	Mon Sep 26 07:56:54 2016 +0200
     3.3 @@ -1088,6 +1088,20 @@
     3.4  lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
     3.5    by (cases "b = 0") simp_all
     3.6  
     3.7 +lemma inv_unit_factor_eq_0_iff [simp]:
     3.8 +  "1 div unit_factor a = 0 \<longleftrightarrow> a = 0"
     3.9 +  (is "?lhs \<longleftrightarrow> ?rhs")
    3.10 +proof
    3.11 +  assume ?lhs
    3.12 +  then have "a * (1 div unit_factor a) = a * 0"
    3.13 +    by simp
    3.14 +  then show ?rhs
    3.15 +    by simp
    3.16 +next
    3.17 +  assume ?rhs
    3.18 +  then show ?lhs by simp
    3.19 +qed
    3.20 +
    3.21  lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
    3.22  proof (cases "a = 0 \<or> b = 0")
    3.23    case True