src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 60600 87fbfea0bd0a
parent 60599 f8bb070dc98b
child 60634 e3b6e516608b
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 27 20:20:36 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 27 20:26:33 2015 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    fixes euclidean_size :: "'a \<Rightarrow> nat"
     1.5    fixes normalization_factor :: "'a \<Rightarrow> 'a"
     1.6    assumes mod_size_less: 
     1.7 -    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
     1.8 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
     1.9    assumes size_mult_mono:
    1.10      "b \<noteq> 0 \<Longrightarrow> euclidean_size (a * b) \<ge> euclidean_size a"
    1.11    assumes normalization_factor_is_unit [intro,simp]: 
    1.12 @@ -145,7 +145,7 @@
    1.13  
    1.14  lemma euclidean_division:
    1.15    fixes a :: 'a and b :: 'a
    1.16 -  assumes "b \<noteq> 0" and "\<not> b dvd a"
    1.17 +  assumes "b \<noteq> 0"
    1.18    obtains s and t where "a = s * b + t" 
    1.19      and "euclidean_size t < euclidean_size b"
    1.20  proof -
    1.21 @@ -174,7 +174,6 @@
    1.22  function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.23  where
    1.24    "gcd_eucl a b = (if b = 0 then a div normalization_factor a
    1.25 -    else if b dvd a then b div normalization_factor b
    1.26      else gcd_eucl b (a mod b))"
    1.27    by pat_completeness simp
    1.28  termination
    1.29 @@ -193,15 +192,8 @@
    1.30      case True then show "P a b" by simp (rule H1)
    1.31    next
    1.32      case False
    1.33 -    have "P b (a mod b)"
    1.34 -    proof (cases "b dvd a")
    1.35 -      case False with \<open>b \<noteq> 0\<close> show "P b (a mod b)"
    1.36 -        by (rule "1.hyps")
    1.37 -    next
    1.38 -      case True then have "a mod b = 0"
    1.39 -        by (simp add: mod_eq_0_iff_dvd)
    1.40 -      then show "P b (a mod b)" by simp (rule H1)
    1.41 -    qed
    1.42 +    then have "P b (a mod b)"
    1.43 +      by (rule "1.hyps")
    1.44      with \<open>b \<noteq> 0\<close> show "P a b"
    1.45        by (blast intro: H2)
    1.46    qed
    1.47 @@ -231,16 +223,11 @@
    1.48  
    1.49  lemma gcd_eucl_0_left:
    1.50    "gcd_eucl 0 a = a div normalization_factor a"
    1.51 -  by (simp add: gcd_eucl.simps [of 0 a])
    1.52 +  by (simp_all add: gcd_eucl_0 gcd_eucl.simps [of 0 a])
    1.53  
    1.54  lemma gcd_eucl_non_0:
    1.55    "b \<noteq> 0 \<Longrightarrow> gcd_eucl a b = gcd_eucl b (a mod b)"
    1.56 -  by (cases "b dvd a")
    1.57 -    (simp_all add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0])
    1.58 -
    1.59 -lemma gcd_eucl_code [code]:
    1.60 -  "gcd_eucl a b = (if b = 0 then a div normalization_factor a else gcd_eucl b (a mod b))"
    1.61 -  by (auto simp add: gcd_eucl_non_0 gcd_eucl_0 gcd_eucl_0_left) 
    1.62 +  by (simp add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0])
    1.63  
    1.64  end
    1.65  
    1.66 @@ -251,8 +238,6 @@
    1.67    "euclid_ext a b = 
    1.68       (if b = 0 then 
    1.69          let c = 1 div normalization_factor a in (c, 0, a * c)
    1.70 -      else if b dvd a then
    1.71 -        let c = 1 div normalization_factor b in (0, c, b * c)
    1.72        else
    1.73          case euclid_ext b (a mod b) of
    1.74              (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
    1.75 @@ -268,13 +253,12 @@
    1.76  
    1.77  lemma euclid_ext_left_0: 
    1.78    "euclid_ext 0 a = (0, 1 div normalization_factor a, a div normalization_factor a)"
    1.79 -  by (simp add: euclid_ext.simps [of 0 a])
    1.80 +  by (simp add: euclid_ext_0 euclid_ext.simps [of 0 a])
    1.81  
    1.82  lemma euclid_ext_non_0: 
    1.83    "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
    1.84      (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
    1.85 -  by (cases "b dvd a")
    1.86 -    (simp_all add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
    1.87 +  by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
    1.88  
    1.89  lemma euclid_ext_code [code]:
    1.90    "euclid_ext a b = (if b = 0 then (1 div normalization_factor a, 0, a div normalization_factor a)
    1.91 @@ -1607,36 +1591,58 @@
    1.92  begin
    1.93  
    1.94  definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
    1.95 -  where "euclidean_size = (degree :: 'a poly \<Rightarrow> nat)"
    1.96 +  where "euclidean_size p = (if p = 0 then 0 else Suc (degree p))"
    1.97  
    1.98  definition normalization_factor_poly :: "'a poly \<Rightarrow> 'a poly"
    1.99    where "normalization_factor p = monom (coeff p (degree p)) 0"
   1.100  
   1.101 +lemma euclidean_size_poly_0 [simp]:
   1.102 +  "euclidean_size (0::'a poly) = 0"
   1.103 +  by (simp add: euclidean_size_poly_def)
   1.104 +
   1.105 +lemma euclidean_size_poly_not_0 [simp]:
   1.106 +  "p \<noteq> 0 \<Longrightarrow> euclidean_size p = Suc (degree p)"
   1.107 +  by (simp add: euclidean_size_poly_def)
   1.108 +
   1.109  instance
   1.110 -proof (default, unfold euclidean_size_poly_def normalization_factor_poly_def)
   1.111 +proof
   1.112    fix p q :: "'a poly"
   1.113 -  assume "q \<noteq> 0" and "\<not> q dvd p"
   1.114 -  then show "degree (p mod q) < degree q"
   1.115 -    using degree_mod_less [of q p] by (simp add: mod_eq_0_iff_dvd)
   1.116 +  assume "q \<noteq> 0"
   1.117 +  then have "p mod q = 0 \<or> degree (p mod q) < degree q"
   1.118 +    by (rule degree_mod_less [of q p])  
   1.119 +  with \<open>q \<noteq> 0\<close> show "euclidean_size (p mod q) < euclidean_size q"
   1.120 +    by (cases "p mod q = 0") simp_all
   1.121  next
   1.122    fix p q :: "'a poly"
   1.123    assume "q \<noteq> 0"
   1.124 -  from \<open>q \<noteq> 0\<close> show "degree p \<le> degree (p * q)"
   1.125 +  from \<open>q \<noteq> 0\<close> have "degree p \<le> degree (p * q)"
   1.126      by (rule degree_mult_right_le)
   1.127 -  from \<open>q \<noteq> 0\<close> show "is_unit (monom (coeff q (degree q)) 0)"
   1.128 +  with \<open>q \<noteq> 0\<close> show "euclidean_size p \<le> euclidean_size (p * q)"
   1.129 +    by (cases "p = 0") simp_all
   1.130 +  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
   1.131      by (auto intro: is_unit_monom_0)
   1.132 +  then show "is_unit (normalization_factor q)"
   1.133 +    by (simp add: normalization_factor_poly_def)
   1.134  next
   1.135    fix p :: "'a poly"
   1.136 -  show "monom (coeff p (degree p)) 0 = p" if "is_unit p"
   1.137 -    using that by (fact is_unit_monom_trival)
   1.138 +  assume "is_unit p"
   1.139 +  then have "monom (coeff p (degree p)) 0 = p"
   1.140 +    by (fact is_unit_monom_trival)
   1.141 +  then show "normalization_factor p = p"
   1.142 +    by (simp add: normalization_factor_poly_def)
   1.143  next
   1.144    fix p q :: "'a poly"
   1.145 -  show "monom (coeff (p * q) (degree (p * q))) 0 =
   1.146 +  have "monom (coeff (p * q) (degree (p * q))) 0 =
   1.147      monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
   1.148      by (simp add: monom_0 coeff_degree_mult)
   1.149 +  then show "normalization_factor (p * q) =
   1.150 +    normalization_factor p * normalization_factor q"
   1.151 +    by (simp add: normalization_factor_poly_def)
   1.152  next
   1.153 -  show "monom (coeff 0 (degree 0)) 0 = 0"
   1.154 +  have "monom (coeff 0 (degree 0)) 0 = 0"
   1.155      by simp
   1.156 +  then show "normalization_factor 0 = (0::'a poly)"
   1.157 +    by (simp add: normalization_factor_poly_def)
   1.158  qed
   1.159  
   1.160  end