rings follow immediately their corresponding semirings
authorhaftmann
Sat Jun 27 20:20:34 2015 +0200 (2015-06-27)
changeset 6059878ca5674c66a
parent 60597 2da9b632069b
child 60599 f8bb070dc98b
rings follow immediately their corresponding semirings
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     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