author haftmann Sat Jun 27 20:26:33 2015 +0200 (2015-06-27) changeset 60600 87fbfea0bd0a parent 60599 f8bb070dc98b child 60601 6e83d94760c4
simplified termination criterion for euclidean algorithm (again)
```     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
```