author haftmann Mon Oct 09 19:10:52 2017 +0200 (19 months ago) changeset 66840 0d689d71dbdc parent 66839 909ba5ed93dd child 66841 5c32a072ca8b
canonical multiplicative euclidean size
```     1.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 09 19:10:51 2017 +0200
1.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 09 19:10:52 2017 +0200
1.3 @@ -759,8 +759,8 @@
1.4      with that show ?thesis
1.5        by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps)
1.6    qed
1.7 -qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le
1.8 -    split: if_splits)
1.9 +qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq power_add
1.10 +    intro!: degree_mod_less' split: if_splits)
1.11
1.12  end
1.13
```
```     2.1 --- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:51 2017 +0200
2.2 +++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:52 2017 +0200
2.3 @@ -20,6 +20,27 @@
2.4      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
2.5  begin
2.6
2.7 +lemma euclidean_size_eq_0_iff [simp]:
2.8 +  "euclidean_size b = 0 \<longleftrightarrow> b = 0"
2.9 +proof
2.10 +  assume "b = 0"
2.11 +  then show "euclidean_size b = 0"
2.12 +    by simp
2.13 +next
2.14 +  assume "euclidean_size b = 0"
2.15 +  show "b = 0"
2.16 +  proof (rule ccontr)
2.17 +    assume "b \<noteq> 0"
2.18 +    with mod_size_less have "euclidean_size (b mod b) < euclidean_size b" .
2.19 +    with \<open>euclidean_size b = 0\<close> show False
2.20 +      by simp
2.21 +  qed
2.22 +qed
2.23 +
2.24 +lemma euclidean_size_greater_0_iff [simp]:
2.25 +  "euclidean_size b > 0 \<longleftrightarrow> b \<noteq> 0"
2.26 +  using euclidean_size_eq_0_iff [symmetric, of b] by safe simp
2.27 +
2.28  lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
2.29    by (subst mult.commute) (rule size_mult_mono)
2.30
2.31 @@ -108,7 +129,7 @@
2.32
2.33  class euclidean_ring = idom_modulo + euclidean_semiring
2.34
2.35 -
2.36 +
2.37  subsection \<open>Euclidean (semi)rings with cancel rules\<close>
2.38
2.39  class euclidean_semiring_cancel = euclidean_semiring +
2.40 @@ -506,10 +527,7 @@
2.41  subsection \<open>Uniquely determined division\<close>
2.42
2.43  class unique_euclidean_semiring = euclidean_semiring +
2.44 -  assumes size_mono_mult:
2.45 -    "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
2.46 -      \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
2.47 -    -- \<open>FIXME justify\<close>
2.48 +  assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b"
2.49    fixes division_segment :: "'a \<Rightarrow> 'a"
2.50    assumes is_unit_division_segment [simp]: "is_unit (division_segment a)"
2.51      and division_segment_mult:
2.52 @@ -625,7 +643,7 @@
2.53      from remainder \<open>c \<noteq> 0\<close>
2.54      have "division_segment (r * c) = division_segment (b * c)"
2.55        and "euclidean_size (r * c) < euclidean_size (b * c)"
2.56 -      by (simp_all add: division_segment_mult division_segment_mod size_mono_mult)
2.57 +      by (simp_all add: division_segment_mult division_segment_mod euclidean_size_mult)
2.58      with remainder show ?thesis
2.59        by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
2.60          (use \<open>b * c \<noteq> 0\<close> in simp)
```
```     3.1 --- a/src/HOL/Parity.thy	Mon Oct 09 19:10:51 2017 +0200
3.2 +++ b/src/HOL/Parity.thy	Mon Oct 09 19:10:52 2017 +0200
3.3 @@ -135,15 +135,7 @@
3.4      show "euclidean_size (a mod 2) \<le> 1"
3.5        using mod_size_less [of 2 a] by simp
3.6      show "1 \<le> euclidean_size (a mod 2)"
3.7 -    proof (rule ccontr)
3.8 -      assume "\<not> 1 \<le> euclidean_size (a mod 2)"
3.9 -      then have "euclidean_size (a mod 2) = 0"
3.10 -        by simp
3.11 -      then have "division_segment (a mod 2) * of_nat (euclidean_size (a mod 2)) = division_segment (a mod 2) * of_nat 0"
3.12 -        by simp
3.13 -      with \<open>odd a\<close> show False
3.14 -        by (simp add: dvd_eq_mod_eq_0)
3.15 -    qed
3.16 +      using \<open>odd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
3.17    qed
3.18    from \<open>odd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
3.19      by simp
```