canonical multiplicative euclidean size
authorhaftmann
Mon Oct 09 19:10:52 2017 +0200 (19 months ago)
changeset 668400d689d71dbdc
parent 66839 909ba5ed93dd
child 66841 5c32a072ca8b
canonical multiplicative euclidean size
src/HOL/Computational_Algebra/Polynomial_Factorial.thy
src/HOL/Euclidean_Division.thy
src/HOL/Parity.thy
     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