author haftmann Sat Jun 27 20:20:34 2015 +0200 (2015-06-27) changeset 60598 78ca5674c66a parent 60597 2da9b632069b child 60599 f8bb070dc98b
rings follow immediately their corresponding semirings
```     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 27 20:20:33 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 27 20:20:34 2015 +0200
1.3 @@ -242,6 +242,76 @@
1.4
1.5  end
1.6
1.7 +class euclidean_ring = euclidean_semiring + idom
1.8 +begin
1.9 +
1.10 +function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
1.11 +  "euclid_ext a b =
1.12 +     (if b = 0 then
1.13 +        let c = 1 div normalization_factor a in (c, 0, a * c)
1.14 +      else if b dvd a then
1.15 +        let c = 1 div normalization_factor b in (0, c, b * c)
1.16 +      else
1.17 +        case euclid_ext b (a mod b) of
1.18 +            (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
1.19 +  by pat_completeness simp
1.20 +termination
1.21 +  by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
1.22 +
1.23 +declare euclid_ext.simps [simp del]
1.24 +
1.25 +lemma euclid_ext_0:
1.26 +  "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)"
1.27 +  by (simp add: euclid_ext.simps [of a 0])
1.28 +
1.29 +lemma euclid_ext_left_0:
1.30 +  "euclid_ext 0 a = (0, 1 div normalization_factor a, a div normalization_factor a)"
1.31 +  by (simp add: euclid_ext.simps [of 0 a])
1.32 +
1.33 +lemma euclid_ext_non_0:
1.34 +  "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
1.35 +    (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
1.36 +  by (cases "b dvd a")
1.37 +    (simp_all add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
1.38 +
1.39 +lemma euclid_ext_code [code]:
1.40 +  "euclid_ext a b = (if b = 0 then (1 div normalization_factor a, 0, a div normalization_factor a)
1.41 +    else let (s, t, c) = euclid_ext b (a mod b) in  (t, s - t * (a div b), c))"
1.42 +  by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
1.43 +
1.44 +lemma euclid_ext_correct:
1.45 +  "case euclid_ext a b of (s, t, c) \<Rightarrow> s * a + t * b = c"
1.46 +proof (induct a b rule: gcd_eucl_induct)
1.47 +  case (zero a) then show ?case
1.48 +    by (simp add: euclid_ext_0 ac_simps)
1.49 +next
1.50 +  case (mod a b)
1.51 +  obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
1.52 +    by (cases "euclid_ext b (a mod b)") blast
1.53 +  with mod have "c = s * b + t * (a mod b)" by simp
1.54 +  also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b"
1.55 +    by (simp add: algebra_simps)
1.56 +  also have "(a div b) * b + a mod b = a" using mod_div_equality .
1.57 +  finally show ?case
1.58 +    by (subst euclid_ext.simps) (simp add: stc mod ac_simps)
1.59 +qed
1.60 +
1.61 +definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
1.62 +where
1.63 +  "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
1.64 +
1.65 +lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div normalization_factor a, 0)"
1.66 +  by (simp add: euclid_ext'_def euclid_ext_0)
1.67 +
1.68 +lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div normalization_factor a)"
1.69 +  by (simp add: euclid_ext'_def euclid_ext_left_0)
1.70 +
1.71 +lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
1.72 +  fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))"
1.73 +  by (simp add: euclid_ext'_def euclid_ext_non_0 split_def)
1.74 +
1.75 +end
1.76 +
1.77  class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd +
1.78    assumes gcd_gcd_eucl: "gcd = gcd_eucl" and lcm_lcm_eucl: "lcm = lcm_eucl"
1.79    assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl"
1.80 @@ -1416,76 +1486,6 @@
1.81    few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring.
1.82  \<close>
1.83
1.84 -class euclidean_ring = euclidean_semiring + idom
1.85 -begin
1.86 -
1.87 -function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
1.88 -  "euclid_ext a b =
1.89 -     (if b = 0 then
1.90 -        let c = 1 div normalization_factor a in (c, 0, a * c)
1.91 -      else if b dvd a then
1.92 -        let c = 1 div normalization_factor b in (0, c, b * c)
1.93 -      else
1.94 -        case euclid_ext b (a mod b) of
1.95 -            (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
1.96 -  by pat_completeness simp
1.97 -termination
1.98 -  by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
1.99 -
1.100 -declare euclid_ext.simps [simp del]
1.101 -
1.102 -lemma euclid_ext_0:
1.103 -  "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)"
1.104 -  by (simp add: euclid_ext.simps [of a 0])
1.105 -
1.106 -lemma euclid_ext_left_0:
1.107 -  "euclid_ext 0 a = (0, 1 div normalization_factor a, a div normalization_factor a)"
1.108 -  by (simp add: euclid_ext.simps [of 0 a])
1.109 -
1.110 -lemma euclid_ext_non_0:
1.111 -  "b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
1.112 -    (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
1.113 -  by (cases "b dvd a")
1.114 -    (simp_all add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
1.115 -
1.116 -lemma euclid_ext_code [code]:
1.117 -  "euclid_ext a b = (if b = 0 then (1 div normalization_factor a, 0, a div normalization_factor a)
1.118 -    else let (s, t, c) = euclid_ext b (a mod b) in  (t, s - t * (a div b), c))"
1.119 -  by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
1.120 -
1.121 -lemma euclid_ext_correct:
1.122 -  "case euclid_ext a b of (s, t, c) \<Rightarrow> s * a + t * b = c"
1.123 -proof (induct a b rule: gcd_eucl_induct)
1.124 -  case (zero a) then show ?case
1.125 -    by (simp add: euclid_ext_0 ac_simps)
1.126 -next
1.127 -  case (mod a b)
1.128 -  obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)"
1.129 -    by (cases "euclid_ext b (a mod b)") blast
1.130 -  with mod have "c = s * b + t * (a mod b)" by simp
1.131 -  also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b"
1.132 -    by (simp add: algebra_simps)
1.133 -  also have "(a div b) * b + a mod b = a" using mod_div_equality .
1.134 -  finally show ?case
1.135 -    by (subst euclid_ext.simps) (simp add: stc mod ac_simps)
1.136 -qed
1.137 -
1.138 -definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
1.139 -where
1.140 -  "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
1.141 -
1.142 -lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div normalization_factor a, 0)"
1.143 -  by (simp add: euclid_ext'_def euclid_ext_0)
1.144 -
1.145 -lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div normalization_factor a)"
1.146 -  by (simp add: euclid_ext'_def euclid_ext_left_0)
1.147 -
1.148 -lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
1.149 -  fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))"
1.150 -  by (simp add: euclid_ext'_def euclid_ext_non_0 split_def)
1.151 -
1.152 -end
1.153 -
1.154  class euclidean_ring_gcd = euclidean_semiring_gcd + idom
1.155  begin
1.156
```