src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 63947 559f0882d6a6
parent 63924 f91766530e13
child 64163 62c9e5c05928
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Sep 26 07:56:53 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -26,6 +26,22 @@
     1.4      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
     1.5  begin
     1.6  
     1.7 +lemma euclidean_size_normalize [simp]:
     1.8 +  "euclidean_size (normalize a) = euclidean_size a"
     1.9 +proof (cases "a = 0")
    1.10 +  case True
    1.11 +  then show ?thesis
    1.12 +    by simp
    1.13 +next
    1.14 +  case [simp]: False
    1.15 +  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
    1.16 +    by (rule size_mult_mono) simp
    1.17 +  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
    1.18 +    by (rule size_mult_mono) simp
    1.19 +  ultimately show ?thesis
    1.20 +    by simp
    1.21 +qed
    1.22 +
    1.23  lemma euclidean_division:
    1.24    fixes a :: 'a and b :: 'a
    1.25    assumes "b \<noteq> 0"