# HG changeset patch
# User haftmann
# Date 1435429593 -7200
# Node ID 87fbfea0bd0a74f17d1ea8d5a0d058fcebdd73c3
# Parent  f8bb070dc98bb50c04fe0a961ef9a01935e2d64a
simplified termination criterion for euclidean algorithm (again)

diff -r f8bb070dc98b -r 87fbfea0bd0a src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 27 20:20:36 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 27 20:26:33 2015 +0200
@@ -23,7 +23,7 @@
   fixes euclidean_size :: "'a \<Rightarrow> nat"
   fixes normalization_factor :: "'a \<Rightarrow> 'a"
   assumes mod_size_less: 
-    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
+    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
   assumes size_mult_mono:
     "b \<noteq> 0 \<Longrightarrow> euclidean_size (a * b) \<ge> euclidean_size a"
   assumes normalization_factor_is_unit [intro,simp]: 
@@ -145,7 +145,7 @@
 
 lemma euclidean_division:
   fixes a :: 'a and b :: 'a
-  assumes "b \<noteq> 0" and "\<not> b dvd a"
+  assumes "b \<noteq> 0"
   obtains s and t where "a = s * b + t" 
     and "euclidean_size t < euclidean_size b"
 proof -
@@ -174,7 +174,6 @@
 function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 where
   "gcd_eucl a b = (if b = 0 then a div normalization_factor a
-    else if b dvd a then b div normalization_factor b
     else gcd_eucl b (a mod b))"
   by pat_completeness simp
 termination
@@ -193,15 +192,8 @@
     case True then show "P a b" by simp (rule H1)
   next
     case False
-    have "P b (a mod b)"
-    proof (cases "b dvd a")
-      case False with \<open>b \<noteq> 0\<close> show "P b (a mod b)"
-        by (rule "1.hyps")
-    next
-      case True then have "a mod b = 0"
-        by (simp add: mod_eq_0_iff_dvd)
-      then show "P b (a mod b)" by simp (rule H1)
-    qed
+    then have "P b (a mod b)"
+      by (rule "1.hyps")
     with \<open>b \<noteq> 0\<close> show "P a b"
       by (blast intro: H2)
   qed
@@ -231,16 +223,11 @@
 
 lemma gcd_eucl_0_left:
   "gcd_eucl 0 a = a div normalization_factor a"
-  by (simp add: gcd_eucl.simps [of 0 a])
+  by (simp_all add: gcd_eucl_0 gcd_eucl.simps [of 0 a])
 
 lemma gcd_eucl_non_0:
   "b \<noteq> 0 \<Longrightarrow> gcd_eucl a b = gcd_eucl b (a mod b)"
-  by (cases "b dvd a")
-    (simp_all add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0])
-
-lemma gcd_eucl_code [code]:
-  "gcd_eucl a b = (if b = 0 then a div normalization_factor a else gcd_eucl b (a mod b))"
-  by (auto simp add: gcd_eucl_non_0 gcd_eucl_0 gcd_eucl_0_left) 
+  by (simp add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0])
 
 end
 
@@ -251,8 +238,6 @@
   "euclid_ext a b = 
      (if b = 0 then 
         let c = 1 div normalization_factor a in (c, 0, a * c)
-      else if b dvd a then
-        let c = 1 div normalization_factor b in (0, c, b * c)
       else
         case euclid_ext b (a mod b) of
             (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
@@ -268,13 +253,12 @@
 
 lemma euclid_ext_left_0: 
   "euclid_ext 0 a = (0, 1 div normalization_factor a, a div normalization_factor a)"
-  by (simp add: euclid_ext.simps [of 0 a])
+  by (simp add: euclid_ext_0 euclid_ext.simps [of 0 a])
 
 lemma euclid_ext_non_0: 
   "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
     (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
-  by (cases "b dvd a")
-    (simp_all add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
+  by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
 
 lemma euclid_ext_code [code]:
   "euclid_ext a b = (if b = 0 then (1 div normalization_factor a, 0, a div normalization_factor a)
@@ -1607,36 +1591,58 @@
 begin
 
 definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
-  where "euclidean_size = (degree :: 'a poly \<Rightarrow> nat)"
+  where "euclidean_size p = (if p = 0 then 0 else Suc (degree p))"
 
 definition normalization_factor_poly :: "'a poly \<Rightarrow> 'a poly"
   where "normalization_factor p = monom (coeff p (degree p)) 0"
 
+lemma euclidean_size_poly_0 [simp]:
+  "euclidean_size (0::'a poly) = 0"
+  by (simp add: euclidean_size_poly_def)
+
+lemma euclidean_size_poly_not_0 [simp]:
+  "p \<noteq> 0 \<Longrightarrow> euclidean_size p = Suc (degree p)"
+  by (simp add: euclidean_size_poly_def)
+
 instance
-proof (default, unfold euclidean_size_poly_def normalization_factor_poly_def)
+proof
   fix p q :: "'a poly"
-  assume "q \<noteq> 0" and "\<not> q dvd p"
-  then show "degree (p mod q) < degree q"
-    using degree_mod_less [of q p] by (simp add: mod_eq_0_iff_dvd)
+  assume "q \<noteq> 0"
+  then have "p mod q = 0 \<or> degree (p mod q) < degree q"
+    by (rule degree_mod_less [of q p])  
+  with \<open>q \<noteq> 0\<close> show "euclidean_size (p mod q) < euclidean_size q"
+    by (cases "p mod q = 0") simp_all
 next
   fix p q :: "'a poly"
   assume "q \<noteq> 0"
-  from \<open>q \<noteq> 0\<close> show "degree p \<le> degree (p * q)"
+  from \<open>q \<noteq> 0\<close> have "degree p \<le> degree (p * q)"
     by (rule degree_mult_right_le)
-  from \<open>q \<noteq> 0\<close> show "is_unit (monom (coeff q (degree q)) 0)"
+  with \<open>q \<noteq> 0\<close> show "euclidean_size p \<le> euclidean_size (p * q)"
+    by (cases "p = 0") simp_all
+  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
     by (auto intro: is_unit_monom_0)
+  then show "is_unit (normalization_factor q)"
+    by (simp add: normalization_factor_poly_def)
 next
   fix p :: "'a poly"
-  show "monom (coeff p (degree p)) 0 = p" if "is_unit p"
-    using that by (fact is_unit_monom_trival)
+  assume "is_unit p"
+  then have "monom (coeff p (degree p)) 0 = p"
+    by (fact is_unit_monom_trival)
+  then show "normalization_factor p = p"
+    by (simp add: normalization_factor_poly_def)
 next
   fix p q :: "'a poly"
-  show "monom (coeff (p * q) (degree (p * q))) 0 =
+  have "monom (coeff (p * q) (degree (p * q))) 0 =
     monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
     by (simp add: monom_0 coeff_degree_mult)
+  then show "normalization_factor (p * q) =
+    normalization_factor p * normalization_factor q"
+    by (simp add: normalization_factor_poly_def)
 next
-  show "monom (coeff 0 (degree 0)) 0 = 0"
+  have "monom (coeff 0 (degree 0)) 0 = 0"
     by simp
+  then show "normalization_factor 0 = (0::'a poly)"
+    by (simp add: normalization_factor_poly_def)
 qed
 
 end