# HG changeset patch
# User haftmann
# Date 1435237301 -7200
# Node ID f2f1f6860959670b3dd6400e3d11add54b8962e7
# Parent  a9b71c82647b103076bac6614cc0d465a0d28ddf
generalized to definition from literature, which covers also polynomials

diff -r a9b71c82647b -r f2f1f6860959 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 12:41:43 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:41 2015 +0200
@@ -22,8 +22,8 @@
 class euclidean_semiring = semiring_div + 
   fixes euclidean_size :: "'a \<Rightarrow> nat"
   fixes normalization_factor :: "'a \<Rightarrow> 'a"
-  assumes mod_size_less [simp]: 
-    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
+  assumes mod_size_less: 
+    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<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]: 
@@ -107,48 +107,102 @@
 lemma normed_associated_imp_eq:
   "associated a b \<Longrightarrow> normalization_factor a \<in> {0, 1} \<Longrightarrow> normalization_factor b \<in> {0, 1} \<Longrightarrow> a = b"
   by (simp add: associated_iff_normed_eq, elim disjE, simp_all)
-    
+
+lemma normed_dvd [iff]:
+  "a div normalization_factor a dvd a"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "a = a div normalization_factor a * normalization_factor a"
+    by (auto intro: unit_div_mult_self)
+  then show ?thesis ..
+qed
+
+lemma dvd_normed [iff]:
+  "a dvd a div normalization_factor a"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "a div normalization_factor a = a * (1 div normalization_factor a)"
+    by (auto intro: unit_mult_div_div)
+  then show ?thesis ..
+qed
+
+lemma associated_normed:
+  "associated (a div normalization_factor a) a"
+  by (rule associatedI) simp_all
+
+lemma normalization_factor_dvd' [simp]:
+  "normalization_factor a dvd a"
+  by (cases "a = 0", simp_all)
+
 lemmas normalization_factor_dvd_iff [simp] =
   unit_dvd_iff [OF normalization_factor_is_unit]
 
 lemma euclidean_division:
   fixes a :: 'a and b :: 'a
-  assumes "b \<noteq> 0"
+  assumes "b \<noteq> 0" and "\<not> b dvd a"
   obtains s and t where "a = s * b + t" 
     and "euclidean_size t < euclidean_size b"
 proof -
-  from div_mod_equality[of a b 0] 
+  from div_mod_equality [of a b 0] 
      have "a = a div b * b + a mod b" by simp
-  with that and assms show ?thesis by force
+  with that and assms show ?thesis by (auto simp add: mod_size_less)
 qed
 
 lemma dvd_euclidean_size_eq_imp_dvd:
   assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
   shows "a dvd b"
-proof (subst dvd_eq_mod_eq_0, rule ccontr)
-  assume "b mod a \<noteq> 0"
+proof (rule ccontr)
+  assume "\<not> a dvd b"
+  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
   from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
   from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
     with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
   with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
       using size_mult_mono by force
-  moreover from \<open>a \<noteq> 0\<close> have "euclidean_size (b mod a) < euclidean_size a"
+  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
+  have "euclidean_size (b mod a) < euclidean_size a"
       using mod_size_less by blast
   ultimately show False using size_eq by simp
 qed
 
 function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 where
-  "gcd_eucl a b = (if b = 0 then a div normalization_factor a else gcd_eucl b (a mod b))"
+  "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 by (relation "measure (euclidean_size \<circ> snd)", simp_all)
+termination
+  by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
 
 declare gcd_eucl.simps [simp del]
 
-lemma gcd_induct: "\<lbrakk>\<And>b. P b 0; \<And>a b. 0 \<noteq> b \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b\<rbrakk> \<Longrightarrow> P a b"
+lemma gcd_eucl_induct [case_names zero mod]:
+  assumes H1: "\<And>b. P b 0"
+  and H2: "\<And>a b. b \<noteq> 0 \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b"
+  shows "P a b"
 proof (induct a b rule: gcd_eucl.induct)
-  case ("1" m n)
-    then show ?case by (cases "n = 0") auto
+  case ("1" a b)
+  show ?case
+  proof (cases "b = 0")
+    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
+    with \<open>b \<noteq> 0\<close> show "P a b"
+      by (blast intro: H2)
+  qed
 qed
 
 definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
@@ -179,7 +233,8 @@
 
 lemma gcd_red:
   "gcd a b = gcd b (a mod b)"
-  by (metis gcd_eucl.simps mod_0 mod_by_0 gcd_gcd_eucl)
+  by (cases "b dvd a")
+    (auto simp add: gcd_gcd_eucl gcd_eucl.simps [of a b] gcd_eucl.simps [of 0 a] gcd_eucl.simps [of b 0])
 
 lemma gcd_non_0:
   "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
@@ -195,22 +250,9 @@
 
 lemma gcd_dvd1 [iff]: "gcd a b dvd a"
   and gcd_dvd2 [iff]: "gcd a b dvd b"
-proof (induct a b rule: gcd_eucl.induct)
-  fix a b :: 'a
-  assume IH1: "b \<noteq> 0 \<Longrightarrow> gcd b (a mod b) dvd b"
-  assume IH2: "b \<noteq> 0 \<Longrightarrow> gcd b (a mod b) dvd (a mod b)"
-  
-  have "gcd a b dvd a \<and> gcd a b dvd b"
-  proof (cases "b = 0")
-    case True
-      then show ?thesis by (cases "a = 0", simp_all add: gcd_0)
-  next
-    case False
-      with IH1 and IH2 show ?thesis by (simp add: gcd_non_0 dvd_mod_iff)
-  qed
-  then show "gcd a b dvd a" "gcd a b dvd b" by simp_all
-qed
-
+  by (induct a b rule: gcd_eucl_induct)
+    (simp_all add: gcd_0 gcd_non_0 dvd_mod_iff)
+    
 lemma dvd_gcd_D1: "k dvd gcd m n \<Longrightarrow> k dvd m"
   by (rule dvd_trans, assumption, rule gcd_dvd1)
 
@@ -220,16 +262,12 @@
 lemma gcd_greatest:
   fixes k a b :: 'a
   shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b"
-proof (induct a b rule: gcd_eucl.induct)
-  case (1 a b)
-  show ?case
-    proof (cases "b = 0")
-      assume "b = 0"
-      with 1 show ?thesis by (cases "a = 0", simp_all add: gcd_0)
-    next
-      assume "b \<noteq> 0"
-      with 1 show ?thesis by (simp add: gcd_non_0 dvd_mod_iff) 
-    qed
+proof (induct a b rule: gcd_eucl_induct)
+  case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_0)
+next
+  case (mod a b)
+  then show ?case
+    by (simp add: gcd_non_0 dvd_mod_iff)
 qed
 
 lemma dvd_gcd_iff:
@@ -244,11 +282,8 @@
 
 lemma normalization_factor_gcd [simp]:
   "normalization_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
-proof (induct a b rule: gcd_eucl.induct)
-  fix a b :: 'a
-  assume IH: "b \<noteq> 0 \<Longrightarrow> ?f b (a mod b) = ?g b (a mod b)"
-  then show "?f a b = ?g a b" by (cases "b = 0", auto simp: gcd_non_0 gcd_0)
-qed
+  by (induct a b rule: gcd_eucl_induct)
+    (auto simp add: gcd_0 gcd_non_0)
 
 lemma gcdI:
   "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> (\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd k)
@@ -329,25 +364,24 @@
   "gcd a (b mod a) = gcd a b"
   by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
          
-lemma normalization_factor_dvd' [simp]:
-  "normalization_factor a dvd a"
-  by (cases "a = 0", simp_all)
-
 lemma gcd_mult_distrib': 
-  "k div normalization_factor k * gcd a b = gcd (k*a) (k*b)"
-proof (induct a b rule: gcd_eucl.induct)
-  case (1 a b)
-  show ?case
-  proof (cases "b = 0")
-    case True
-    then show ?thesis by (simp add: normalization_factor_mult gcd_0 algebra_simps div_mult_div_if_dvd)
-  next
-    case False
-    hence "k div normalization_factor k * gcd a b =  gcd (k * b) (k * (a mod b))" 
-      using 1 by (subst gcd_red, simp)
-    also have "... = gcd (k * a) (k * b)"
-      by (simp add: mult_mod_right gcd.commute)
-    finally show ?thesis .
+  "c div normalization_factor c * gcd a b = gcd (c * a) (c * b)"
+proof (cases "c = 0")
+  case True then show ?thesis by (simp_all add: gcd_0)
+next
+  case False then have [simp]: "is_unit (normalization_factor c)" by simp
+  show ?thesis
+  proof (induct a b rule: gcd_eucl_induct)
+    case (zero a) show ?case
+    proof (cases "a = 0")
+      case True then show ?thesis by (simp add: gcd_0)
+    next
+      case False then have "is_unit (normalization_factor a)" by simp
+      then show ?thesis
+        by (simp add: gcd_0 unit_div_commute unit_div_mult_swap normalization_factor_mult is_unit_div_mult2_eq)
+    qed
+    case (mod a b)
+    then show ?case by (simp add: mult_mod_right gcd.commute)
   qed
 qed
 
@@ -1421,11 +1455,14 @@
   "euclid_ext a b = 
      (if b = 0 then 
         let c = 1 div normalization_factor a in (c, 0, a * c)
-      else 
+      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))"
+            (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
   by (pat_completeness, simp)
-  termination by (relation "measure (euclidean_size \<circ> snd)", simp_all)
+  termination by (relation "measure (euclidean_size \<circ> snd)")
+    (simp_all add: mod_size_less)
 
 declare euclid_ext.simps [simp del]
 
@@ -1435,51 +1472,41 @@
 
 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 (subst euclid_ext.simps) simp
+    (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
+  apply (subst euclid_ext.simps)
+  apply (auto simp add: split: if_splits)
+  apply (subst euclid_ext.simps)
+  apply (auto simp add: split: if_splits)
+  done
 
 definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
 where
   "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
 
 lemma euclid_ext_gcd [simp]:
-  "(case euclid_ext a b of (_,_,t) \<Rightarrow> t) = gcd a b"
-proof (induct a b rule: euclid_ext.induct)
-  case (1 a b)
-  then show ?case
-  proof (cases "b = 0")
-    case True
-      then show ?thesis by  
-        (simp add: euclid_ext_0 unit_div mult_ac unit_simps gcd_0)
-    next
-    case False with 1 show ?thesis
-      by (simp add: euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
-    qed
-qed
+  "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
+  by (induct a b rule: gcd_eucl_induct)
+    (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
 
 lemma euclid_ext_gcd' [simp]:
   "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
   by (insert euclid_ext_gcd[of a b], drule (1) subst, simp)
 
 lemma euclid_ext_correct:
-  "case euclid_ext a b of (s,t,c) \<Rightarrow> s*a + t*b = c"
-proof (induct a b rule: euclid_ext.induct)
-  case (1 a b)
-  show ?case
-  proof (cases "b = 0")
-    case True
-    then show ?thesis by (simp add: euclid_ext_0 mult_ac)
-  next
-    case False
-    obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
-      by (cases "euclid_ext b (a mod b)", blast)
-    from 1 have "c = s * b + t * (a mod b)" by (simp add: stc False)
-    also have "... = t*((a div b)*b + a mod b) + (s - t * (a div b))*b"
-      by (simp add: algebra_simps) 
-    also have "(a div b)*b + a mod b = a" using mod_div_equality .
-    finally show ?thesis
-      by (subst euclid_ext.simps, simp add: False stc)
-    qed
+  "case euclid_ext a b of (s, t, c) \<Rightarrow> s * a + t * b = c"
+proof (induct a b rule: gcd_eucl_induct)
+  case (zero a) then show ?case
+    by (simp add: euclid_ext_0 ac_simps)
+next
+  case (mod a b)
+  obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
+    by (cases "euclid_ext b (a mod b)") blast
+  with mod have "c = s * b + t * (a mod b)" by simp
+  also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b"
+    by (simp add: algebra_simps) 
+  also have "(a div b) * b + a mod b = a" using mod_div_equality .
+  finally show ?case
+    by (subst euclid_ext.simps) (simp add: stc mod ac_simps)
 qed
 
 lemma euclid_ext'_correct: