generalized to definition from literature, which covers also polynomials
authorhaftmann
Thu Jun 25 15:01:41 2015 +0200 (2015-06-25)
changeset 60569f2f1f6860959
parent 60568 a9b71c82647b
child 60570 7ed2cde6806d
generalized to definition from literature, which covers also polynomials
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 12:41:43 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:41 2015 +0200
     1.3 @@ -22,8 +22,8 @@
     1.4  class euclidean_semiring = semiring_div + 
     1.5    fixes euclidean_size :: "'a \<Rightarrow> nat"
     1.6    fixes normalization_factor :: "'a \<Rightarrow> 'a"
     1.7 -  assumes mod_size_less [simp]: 
     1.8 -    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
     1.9 +  assumes mod_size_less: 
    1.10 +    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    1.11    assumes size_mult_mono:
    1.12      "b \<noteq> 0 \<Longrightarrow> euclidean_size (a * b) \<ge> euclidean_size a"
    1.13    assumes normalization_factor_is_unit [intro,simp]: 
    1.14 @@ -107,48 +107,102 @@
    1.15  lemma normed_associated_imp_eq:
    1.16    "associated a b \<Longrightarrow> normalization_factor a \<in> {0, 1} \<Longrightarrow> normalization_factor b \<in> {0, 1} \<Longrightarrow> a = b"
    1.17    by (simp add: associated_iff_normed_eq, elim disjE, simp_all)
    1.18 -    
    1.19 +
    1.20 +lemma normed_dvd [iff]:
    1.21 +  "a div normalization_factor a dvd a"
    1.22 +proof (cases "a = 0")
    1.23 +  case True then show ?thesis by simp
    1.24 +next
    1.25 +  case False
    1.26 +  then have "a = a div normalization_factor a * normalization_factor a"
    1.27 +    by (auto intro: unit_div_mult_self)
    1.28 +  then show ?thesis ..
    1.29 +qed
    1.30 +
    1.31 +lemma dvd_normed [iff]:
    1.32 +  "a dvd a div normalization_factor a"
    1.33 +proof (cases "a = 0")
    1.34 +  case True then show ?thesis by simp
    1.35 +next
    1.36 +  case False
    1.37 +  then have "a div normalization_factor a = a * (1 div normalization_factor a)"
    1.38 +    by (auto intro: unit_mult_div_div)
    1.39 +  then show ?thesis ..
    1.40 +qed
    1.41 +
    1.42 +lemma associated_normed:
    1.43 +  "associated (a div normalization_factor a) a"
    1.44 +  by (rule associatedI) simp_all
    1.45 +
    1.46 +lemma normalization_factor_dvd' [simp]:
    1.47 +  "normalization_factor a dvd a"
    1.48 +  by (cases "a = 0", simp_all)
    1.49 +
    1.50  lemmas normalization_factor_dvd_iff [simp] =
    1.51    unit_dvd_iff [OF normalization_factor_is_unit]
    1.52  
    1.53  lemma euclidean_division:
    1.54    fixes a :: 'a and b :: 'a
    1.55 -  assumes "b \<noteq> 0"
    1.56 +  assumes "b \<noteq> 0" and "\<not> b dvd a"
    1.57    obtains s and t where "a = s * b + t" 
    1.58      and "euclidean_size t < euclidean_size b"
    1.59  proof -
    1.60 -  from div_mod_equality[of a b 0] 
    1.61 +  from div_mod_equality [of a b 0] 
    1.62       have "a = a div b * b + a mod b" by simp
    1.63 -  with that and assms show ?thesis by force
    1.64 +  with that and assms show ?thesis by (auto simp add: mod_size_less)
    1.65  qed
    1.66  
    1.67  lemma dvd_euclidean_size_eq_imp_dvd:
    1.68    assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
    1.69    shows "a dvd b"
    1.70 -proof (subst dvd_eq_mod_eq_0, rule ccontr)
    1.71 -  assume "b mod a \<noteq> 0"
    1.72 +proof (rule ccontr)
    1.73 +  assume "\<not> a dvd b"
    1.74 +  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
    1.75    from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
    1.76    from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
    1.77      with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
    1.78    with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
    1.79        using size_mult_mono by force
    1.80 -  moreover from \<open>a \<noteq> 0\<close> have "euclidean_size (b mod a) < euclidean_size a"
    1.81 +  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
    1.82 +  have "euclidean_size (b mod a) < euclidean_size a"
    1.83        using mod_size_less by blast
    1.84    ultimately show False using size_eq by simp
    1.85  qed
    1.86  
    1.87  function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.88  where
    1.89 -  "gcd_eucl a b = (if b = 0 then a div normalization_factor a else gcd_eucl b (a mod b))"
    1.90 +  "gcd_eucl a b = (if b = 0 then a div normalization_factor a
    1.91 +    else if b dvd a then b div normalization_factor b
    1.92 +    else gcd_eucl b (a mod b))"
    1.93    by (pat_completeness, simp)
    1.94 -termination by (relation "measure (euclidean_size \<circ> snd)", simp_all)
    1.95 +termination
    1.96 +  by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
    1.97  
    1.98  declare gcd_eucl.simps [simp del]
    1.99  
   1.100 -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"
   1.101 +lemma gcd_eucl_induct [case_names zero mod]:
   1.102 +  assumes H1: "\<And>b. P b 0"
   1.103 +  and H2: "\<And>a b. b \<noteq> 0 \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b"
   1.104 +  shows "P a b"
   1.105  proof (induct a b rule: gcd_eucl.induct)
   1.106 -  case ("1" m n)
   1.107 -    then show ?case by (cases "n = 0") auto
   1.108 +  case ("1" a b)
   1.109 +  show ?case
   1.110 +  proof (cases "b = 0")
   1.111 +    case True then show "P a b" by simp (rule H1)
   1.112 +  next
   1.113 +    case False
   1.114 +    have "P b (a mod b)"
   1.115 +    proof (cases "b dvd a")
   1.116 +      case False with \<open>b \<noteq> 0\<close> show "P b (a mod b)"
   1.117 +        by (rule "1.hyps")
   1.118 +    next
   1.119 +      case True then have "a mod b = 0"
   1.120 +        by (simp add: mod_eq_0_iff_dvd)
   1.121 +      then show "P b (a mod b)" by simp (rule H1)
   1.122 +    qed
   1.123 +    with \<open>b \<noteq> 0\<close> show "P a b"
   1.124 +      by (blast intro: H2)
   1.125 +  qed
   1.126  qed
   1.127  
   1.128  definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.129 @@ -179,7 +233,8 @@
   1.130  
   1.131  lemma gcd_red:
   1.132    "gcd a b = gcd b (a mod b)"
   1.133 -  by (metis gcd_eucl.simps mod_0 mod_by_0 gcd_gcd_eucl)
   1.134 +  by (cases "b dvd a")
   1.135 +    (auto simp add: gcd_gcd_eucl gcd_eucl.simps [of a b] gcd_eucl.simps [of 0 a] gcd_eucl.simps [of b 0])
   1.136  
   1.137  lemma gcd_non_0:
   1.138    "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
   1.139 @@ -195,22 +250,9 @@
   1.140  
   1.141  lemma gcd_dvd1 [iff]: "gcd a b dvd a"
   1.142    and gcd_dvd2 [iff]: "gcd a b dvd b"
   1.143 -proof (induct a b rule: gcd_eucl.induct)
   1.144 -  fix a b :: 'a
   1.145 -  assume IH1: "b \<noteq> 0 \<Longrightarrow> gcd b (a mod b) dvd b"
   1.146 -  assume IH2: "b \<noteq> 0 \<Longrightarrow> gcd b (a mod b) dvd (a mod b)"
   1.147 -  
   1.148 -  have "gcd a b dvd a \<and> gcd a b dvd b"
   1.149 -  proof (cases "b = 0")
   1.150 -    case True
   1.151 -      then show ?thesis by (cases "a = 0", simp_all add: gcd_0)
   1.152 -  next
   1.153 -    case False
   1.154 -      with IH1 and IH2 show ?thesis by (simp add: gcd_non_0 dvd_mod_iff)
   1.155 -  qed
   1.156 -  then show "gcd a b dvd a" "gcd a b dvd b" by simp_all
   1.157 -qed
   1.158 -
   1.159 +  by (induct a b rule: gcd_eucl_induct)
   1.160 +    (simp_all add: gcd_0 gcd_non_0 dvd_mod_iff)
   1.161 +    
   1.162  lemma dvd_gcd_D1: "k dvd gcd m n \<Longrightarrow> k dvd m"
   1.163    by (rule dvd_trans, assumption, rule gcd_dvd1)
   1.164  
   1.165 @@ -220,16 +262,12 @@
   1.166  lemma gcd_greatest:
   1.167    fixes k a b :: 'a
   1.168    shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b"
   1.169 -proof (induct a b rule: gcd_eucl.induct)
   1.170 -  case (1 a b)
   1.171 -  show ?case
   1.172 -    proof (cases "b = 0")
   1.173 -      assume "b = 0"
   1.174 -      with 1 show ?thesis by (cases "a = 0", simp_all add: gcd_0)
   1.175 -    next
   1.176 -      assume "b \<noteq> 0"
   1.177 -      with 1 show ?thesis by (simp add: gcd_non_0 dvd_mod_iff) 
   1.178 -    qed
   1.179 +proof (induct a b rule: gcd_eucl_induct)
   1.180 +  case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_0)
   1.181 +next
   1.182 +  case (mod a b)
   1.183 +  then show ?case
   1.184 +    by (simp add: gcd_non_0 dvd_mod_iff)
   1.185  qed
   1.186  
   1.187  lemma dvd_gcd_iff:
   1.188 @@ -244,11 +282,8 @@
   1.189  
   1.190  lemma normalization_factor_gcd [simp]:
   1.191    "normalization_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
   1.192 -proof (induct a b rule: gcd_eucl.induct)
   1.193 -  fix a b :: 'a
   1.194 -  assume IH: "b \<noteq> 0 \<Longrightarrow> ?f b (a mod b) = ?g b (a mod b)"
   1.195 -  then show "?f a b = ?g a b" by (cases "b = 0", auto simp: gcd_non_0 gcd_0)
   1.196 -qed
   1.197 +  by (induct a b rule: gcd_eucl_induct)
   1.198 +    (auto simp add: gcd_0 gcd_non_0)
   1.199  
   1.200  lemma gcdI:
   1.201    "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> (\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd k)
   1.202 @@ -329,25 +364,24 @@
   1.203    "gcd a (b mod a) = gcd a b"
   1.204    by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
   1.205           
   1.206 -lemma normalization_factor_dvd' [simp]:
   1.207 -  "normalization_factor a dvd a"
   1.208 -  by (cases "a = 0", simp_all)
   1.209 -
   1.210  lemma gcd_mult_distrib': 
   1.211 -  "k div normalization_factor k * gcd a b = gcd (k*a) (k*b)"
   1.212 -proof (induct a b rule: gcd_eucl.induct)
   1.213 -  case (1 a b)
   1.214 -  show ?case
   1.215 -  proof (cases "b = 0")
   1.216 -    case True
   1.217 -    then show ?thesis by (simp add: normalization_factor_mult gcd_0 algebra_simps div_mult_div_if_dvd)
   1.218 -  next
   1.219 -    case False
   1.220 -    hence "k div normalization_factor k * gcd a b =  gcd (k * b) (k * (a mod b))" 
   1.221 -      using 1 by (subst gcd_red, simp)
   1.222 -    also have "... = gcd (k * a) (k * b)"
   1.223 -      by (simp add: mult_mod_right gcd.commute)
   1.224 -    finally show ?thesis .
   1.225 +  "c div normalization_factor c * gcd a b = gcd (c * a) (c * b)"
   1.226 +proof (cases "c = 0")
   1.227 +  case True then show ?thesis by (simp_all add: gcd_0)
   1.228 +next
   1.229 +  case False then have [simp]: "is_unit (normalization_factor c)" by simp
   1.230 +  show ?thesis
   1.231 +  proof (induct a b rule: gcd_eucl_induct)
   1.232 +    case (zero a) show ?case
   1.233 +    proof (cases "a = 0")
   1.234 +      case True then show ?thesis by (simp add: gcd_0)
   1.235 +    next
   1.236 +      case False then have "is_unit (normalization_factor a)" by simp
   1.237 +      then show ?thesis
   1.238 +        by (simp add: gcd_0 unit_div_commute unit_div_mult_swap normalization_factor_mult is_unit_div_mult2_eq)
   1.239 +    qed
   1.240 +    case (mod a b)
   1.241 +    then show ?case by (simp add: mult_mod_right gcd.commute)
   1.242    qed
   1.243  qed
   1.244  
   1.245 @@ -1421,11 +1455,14 @@
   1.246    "euclid_ext a b = 
   1.247       (if b = 0 then 
   1.248          let c = 1 div normalization_factor a in (c, 0, a * c)
   1.249 -      else 
   1.250 +      else if b dvd a then
   1.251 +        let c = 1 div normalization_factor b in (0, c, b * c)
   1.252 +      else
   1.253          case euclid_ext b (a mod b) of
   1.254 -            (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.255 +            (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.256    by (pat_completeness, simp)
   1.257 -  termination by (relation "measure (euclidean_size \<circ> snd)", simp_all)
   1.258 +  termination by (relation "measure (euclidean_size \<circ> snd)")
   1.259 +    (simp_all add: mod_size_less)
   1.260  
   1.261  declare euclid_ext.simps [simp del]
   1.262  
   1.263 @@ -1435,51 +1472,41 @@
   1.264  
   1.265  lemma euclid_ext_non_0:
   1.266    "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of 
   1.267 -    (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.268 -  by (subst euclid_ext.simps) simp
   1.269 +    (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.270 +  apply (subst euclid_ext.simps)
   1.271 +  apply (auto simp add: split: if_splits)
   1.272 +  apply (subst euclid_ext.simps)
   1.273 +  apply (auto simp add: split: if_splits)
   1.274 +  done
   1.275  
   1.276  definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
   1.277  where
   1.278    "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
   1.279  
   1.280  lemma euclid_ext_gcd [simp]:
   1.281 -  "(case euclid_ext a b of (_,_,t) \<Rightarrow> t) = gcd a b"
   1.282 -proof (induct a b rule: euclid_ext.induct)
   1.283 -  case (1 a b)
   1.284 -  then show ?case
   1.285 -  proof (cases "b = 0")
   1.286 -    case True
   1.287 -      then show ?thesis by  
   1.288 -        (simp add: euclid_ext_0 unit_div mult_ac unit_simps gcd_0)
   1.289 -    next
   1.290 -    case False with 1 show ?thesis
   1.291 -      by (simp add: euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
   1.292 -    qed
   1.293 -qed
   1.294 +  "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
   1.295 +  by (induct a b rule: gcd_eucl_induct)
   1.296 +    (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
   1.297  
   1.298  lemma euclid_ext_gcd' [simp]:
   1.299    "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
   1.300    by (insert euclid_ext_gcd[of a b], drule (1) subst, simp)
   1.301  
   1.302  lemma euclid_ext_correct:
   1.303 -  "case euclid_ext a b of (s,t,c) \<Rightarrow> s*a + t*b = c"
   1.304 -proof (induct a b rule: euclid_ext.induct)
   1.305 -  case (1 a b)
   1.306 -  show ?case
   1.307 -  proof (cases "b = 0")
   1.308 -    case True
   1.309 -    then show ?thesis by (simp add: euclid_ext_0 mult_ac)
   1.310 -  next
   1.311 -    case False
   1.312 -    obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
   1.313 -      by (cases "euclid_ext b (a mod b)", blast)
   1.314 -    from 1 have "c = s * b + t * (a mod b)" by (simp add: stc False)
   1.315 -    also have "... = t*((a div b)*b + a mod b) + (s - t * (a div b))*b"
   1.316 -      by (simp add: algebra_simps) 
   1.317 -    also have "(a div b)*b + a mod b = a" using mod_div_equality .
   1.318 -    finally show ?thesis
   1.319 -      by (subst euclid_ext.simps, simp add: False stc)
   1.320 -    qed
   1.321 +  "case euclid_ext a b of (s, t, c) \<Rightarrow> s * a + t * b = c"
   1.322 +proof (induct a b rule: gcd_eucl_induct)
   1.323 +  case (zero a) then show ?case
   1.324 +    by (simp add: euclid_ext_0 ac_simps)
   1.325 +next
   1.326 +  case (mod a b)
   1.327 +  obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
   1.328 +    by (cases "euclid_ext b (a mod b)") blast
   1.329 +  with mod have "c = s * b + t * (a mod b)" by simp
   1.330 +  also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b"
   1.331 +    by (simp add: algebra_simps) 
   1.332 +  also have "(a div b) * b + a mod b = a" using mod_div_equality .
   1.333 +  finally show ?case
   1.334 +    by (subst euclid_ext.simps) (simp add: stc mod ac_simps)
   1.335  qed
   1.336  
   1.337  lemma euclid_ext'_correct: