author haftmann Fri Jun 12 08:53:23 2015 +0200 (2015-06-12) changeset 60432 68d75cff8809 parent 60431 db9c67b760f1 child 60433 720f210c5b1d
given up trivial definition
```     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
1.3 @@ -17,41 +17,28 @@
1.4  where
1.5    "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
1.6
1.7 -definition ring_inv :: "'a \<Rightarrow> 'a"
1.8 -where
1.9 -  "ring_inv a = 1 div a"
1.10 -
1.11  lemma unit_prod [intro]:
1.12    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
1.13    by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono)
1.14
1.15 -lemma unit_ring_inv:
1.16 -  "is_unit b \<Longrightarrow> a div b = a * ring_inv b"
1.17 -  by (simp add: div_mult_swap ring_inv_def)
1.18 +lemma unit_divide_1:
1.19 +  "is_unit b \<Longrightarrow> a div b = a * divide 1 b"
1.20 +  by (simp add: div_mult_swap)
1.21
1.22 -lemma unit_ring_inv_ring_inv [simp]:
1.23 -  "is_unit a \<Longrightarrow> ring_inv (ring_inv a) = a"
1.24 -  unfolding ring_inv_def
1.25 +lemma unit_divide_1_divide_1 [simp]:
1.26 +  "is_unit a \<Longrightarrow> divide 1 (divide 1 a) = a"
1.27    by (metis div_mult_mult1_if div_mult_self1_is_id dvd_mult_div_cancel mult_1_right)
1.28
1.29 -lemma inv_imp_eq_ring_inv:
1.30 -  "a * b = 1 \<Longrightarrow> ring_inv a = b"
1.31 -  by (metis dvd_mult_div_cancel dvd_mult_right mult_1_right mult.left_commute one_dvd ring_inv_def)
1.32 -
1.33 -lemma ring_inv_is_inv1 [simp]:
1.34 -  "is_unit a \<Longrightarrow> a * ring_inv a = 1"
1.35 -  unfolding ring_inv_def by simp
1.36 +lemma inv_imp_eq_divide_1:
1.37 +  "a * b = 1 \<Longrightarrow> divide 1 a = b"
1.38 +  by (metis dvd_mult_div_cancel dvd_mult_right mult_1_right mult.left_commute one_dvd)
1.39
1.40 -lemma ring_inv_is_inv2 [simp]:
1.41 -  "is_unit a \<Longrightarrow> ring_inv a * a = 1"
1.42 -  by (simp add: ac_simps)
1.43 -
1.44 -lemma unit_ring_inv_unit [simp, intro]:
1.45 +lemma unit_divide_1_unit [simp, intro]:
1.46    assumes "is_unit a"
1.47 -  shows "is_unit (ring_inv a)"
1.48 +  shows "is_unit (divide 1 a)"
1.49  proof -
1.50 -  from assms have "1 = ring_inv a * a" by simp
1.51 -  then show "is_unit (ring_inv a)" by (rule dvdI)
1.52 +  from assms have "1 = divide 1 a * a" by simp
1.53 +  then show "is_unit (divide 1 a)" by (rule dvdI)
1.54  qed
1.55
1.56  lemma mult_unit_dvd_iff:
1.57 @@ -62,21 +49,21 @@
1.58  next
1.59    assume "is_unit b" "a dvd c"
1.60    then obtain k where "c = a * k" unfolding dvd_def by blast
1.61 -  with `is_unit b` have "c = (a * b) * (ring_inv b * k)"
1.62 +  with `is_unit b` have "c = (a * b) * (divide 1 b * k)"
1.64    then show "a * b dvd c" by (rule dvdI)
1.65  qed
1.66
1.67  lemma div_unit_dvd_iff:
1.68    "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
1.69 -  by (subst unit_ring_inv) (assumption, simp add: mult_unit_dvd_iff)
1.70 +  by (subst unit_divide_1) (assumption, simp add: mult_unit_dvd_iff)
1.71
1.72  lemma dvd_mult_unit_iff:
1.73    "is_unit b \<Longrightarrow> a dvd c * b \<longleftrightarrow> a dvd c"
1.74  proof
1.75    assume "is_unit b" and "a dvd c * b"
1.76 -  have "c * b dvd c * (b * ring_inv b)" by (subst mult_assoc [symmetric]) simp
1.77 -  also from `is_unit b` have "b * ring_inv b = 1" by simp
1.78 +  have "c * b dvd c * (b * divide 1 b)" by (subst mult_assoc [symmetric]) simp
1.79 +  also from `is_unit b` have "b * divide 1 b = 1" by simp
1.80    finally have "c * b dvd c" by simp
1.81    with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
1.82  next
1.83 @@ -86,21 +73,21 @@
1.84
1.85  lemma dvd_div_unit_iff:
1.86    "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
1.87 -  by (subst unit_ring_inv) (assumption, simp add: dvd_mult_unit_iff)
1.88 +  by (subst unit_divide_1) (assumption, simp add: dvd_mult_unit_iff)
1.89
1.90  lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff dvd_div_unit_iff
1.91
1.92  lemma unit_div [intro]:
1.93    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
1.94 -  by (subst unit_ring_inv) (assumption, rule unit_prod, simp_all)
1.95 +  by (subst unit_divide_1) (assumption, rule unit_prod, simp_all)
1.96
1.97  lemma unit_div_mult_swap:
1.98    "is_unit c \<Longrightarrow> a * (b div c) = a * b div c"
1.99 -  by (simp only: unit_ring_inv [of _ b] unit_ring_inv [of _ "a*b"] ac_simps)
1.100 +  by (simp only: unit_divide_1 [of _ b] unit_divide_1 [of _ "a*b"] ac_simps)
1.101
1.102  lemma unit_div_commute:
1.103    "is_unit b \<Longrightarrow> a div b * c = a * c div b"
1.104 -  by (simp only: unit_ring_inv [of _ a] unit_ring_inv [of _ "a*c"] ac_simps)
1.105 +  by (simp only: unit_divide_1 [of _ a] unit_divide_1 [of _ "a*c"] ac_simps)
1.106
1.107  lemma unit_imp_dvd [dest]:
1.108    "is_unit b \<Longrightarrow> b dvd a"
1.109 @@ -110,19 +97,15 @@
1.110    "is_unit b \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
1.111    by (rule dvd_trans)
1.112
1.113 -lemma ring_inv_0 [simp]:
1.114 -  "ring_inv 0 = 0"
1.115 -  unfolding ring_inv_def by simp
1.116 -
1.117 -lemma unit_ring_inv'1:
1.118 +lemma unit_divide_1'1:
1.119    assumes "is_unit b"
1.120 -  shows "a div (b * c) = a * ring_inv b div c"
1.121 +  shows "a div (b * c) = a * divide 1 b div c"
1.122  proof -
1.123 -  from assms have "a div (b * c) = a * (ring_inv b * b) div (b * c)"
1.124 +  from assms have "a div (b * c) = a * (divide 1 b * b) div (b * c)"
1.125      by simp
1.126 -  also have "... = b * (a * ring_inv b) div (b * c)"
1.127 +  also have "... = b * (a * divide 1 b) div (b * c)"
1.128      by (simp only: mult_ac)
1.129 -  also have "... = a * ring_inv b div c"
1.130 +  also have "... = a * divide 1 b div c"
1.131      by (cases "b = 0", simp, rule div_mult_mult1)
1.132    finally show ?thesis .
1.133  qed
1.134 @@ -162,16 +145,16 @@
1.135
1.136  lemma unit_div_cancel:
1.137    "is_unit a \<Longrightarrow> (b div a) = (c div a) \<longleftrightarrow> b = c"
1.138 -  apply (subst unit_ring_inv[of _ b], assumption)
1.139 -  apply (subst unit_ring_inv[of _ c], assumption)
1.140 -  apply (rule unit_mult_right_cancel, erule unit_ring_inv_unit)
1.141 +  apply (subst unit_divide_1[of _ b], assumption)
1.142 +  apply (subst unit_divide_1[of _ c], assumption)
1.143 +  apply (rule unit_mult_right_cancel, erule unit_divide_1_unit)
1.144    done
1.145
1.146  lemma unit_eq_div1:
1.147    "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
1.148 -  apply (subst unit_ring_inv, assumption)
1.149 +  apply (subst unit_divide_1, assumption)
1.150    apply (subst unit_mult_right_cancel[symmetric], assumption)
1.151 -  apply (subst mult_assoc, subst ring_inv_is_inv2, assumption, simp)
1.152 +  apply (subst mult_assoc, subst dvd_div_mult_self, assumption, simp)
1.153    done
1.154
1.155  lemma unit_eq_div2:
1.156 @@ -200,7 +183,7 @@
1.157  next
1.158    assume "\<exists>c. is_unit c \<and> a = c * b"
1.159    then obtain c where "is_unit c" and "a = c * b" by blast
1.160 -  hence "b = a * ring_inv c" by (simp add: algebra_simps)
1.161 +  hence "b = a * divide 1 c" by (simp add: algebra_simps)
1.162    hence "a dvd b" by simp
1.163    moreover from `a = c * b` have "b dvd a" by simp
1.164    ultimately show "associated a b" unfolding associated_def by simp
1.165 @@ -630,10 +613,10 @@
1.166    by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute)
1.167
1.168  lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
1.169 -  by (simp add: unit_ring_inv gcd_mult_unit1)
1.170 +  by (subst unit_divide_1) (simp_all add: gcd_mult_unit1)
1.171
1.172  lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
1.173 -  by (simp add: unit_ring_inv gcd_mult_unit2)
1.174 +  by (subst unit_divide_1) (simp_all add: gcd_mult_unit2)
1.175
1.176  lemma gcd_idem: "gcd a a = a div normalisation_factor a"
1.177    by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
1.178 @@ -980,8 +963,8 @@
1.179    hence "gcd a b \<noteq> 0" by simp
1.180    from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))"
1.182 -  also from `a * b \<noteq> 0` have "... = a * b div ?nf (a*b)"
1.183 -    by (simp_all add: unit_ring_inv'1 unit_ring_inv)
1.184 +  also from `a * b \<noteq> 0` have "... = a * b div ?nf (a*b)"
1.185 +    by (simp add: div_mult_swap mult.commute)
1.186    finally show ?thesis .
1.187  qed (auto simp add: lcm_gcd)
1.188
1.189 @@ -990,10 +973,10 @@
1.190  proof (cases "a*b = 0")
1.191    assume "a * b \<noteq> 0"
1.192    hence "gcd a b \<noteq> 0" by simp
1.193 -  let ?c = "ring_inv (normalisation_factor (a*b))"
1.194 +  let ?c = "divide 1 (normalisation_factor (a*b))"
1.195    from `a * b \<noteq> 0` have [simp]: "is_unit (normalisation_factor (a*b))" by simp
1.196    from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
1.197 -    by (simp add: mult_ac unit_ring_inv)
1.198 +    by (simp add: div_mult_swap unit_div_commute)
1.199    hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
1.200    with `gcd a b \<noteq> 0` have "lcm a b = a * ?c * b div gcd a b"
1.201      by (subst (asm) div_mult_self2_is_id, simp_all)
1.202 @@ -1073,7 +1056,7 @@
1.203    from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b"
1.204      by (subst (2) div_mult_self2_is_id[OF `lcm a b \<noteq> 0`, symmetric], simp add: mult_ac)
1.205    also from `is_unit ?c` have "... = a * b div (?c * lcm a b)"
1.206 -    by (simp only: unit_ring_inv'1 unit_ring_inv)
1.207 +    by (metis local.unit_divide_1 local.unit_divide_1'1)
1.208    finally show ?thesis by (simp only: ac_simps)
1.209  qed
1.210
1.211 @@ -1266,11 +1249,11 @@
1.212
1.213  lemma lcm_div_unit1:
1.214    "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
1.215 -  by (simp add: unit_ring_inv lcm_mult_unit1)
1.216 +  by (metis lcm_mult_unit1 local.unit_divide_1 local.unit_divide_1_unit)
1.217
1.218  lemma lcm_div_unit2:
1.219    "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
1.220 -  by (simp add: unit_ring_inv lcm_mult_unit2)
1.221 +  by (metis lcm_mult_unit2 local.unit_divide_1 local.unit_divide_1_unit)
1.222
1.223  lemma lcm_left_idem:
1.224    "lcm a (lcm a b) = lcm a b"
1.225 @@ -1640,7 +1623,7 @@
1.226  function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
1.227    "euclid_ext a b =
1.228       (if b = 0 then
1.229 -        let c = ring_inv (normalisation_factor a) in (c, 0, a * c)
1.230 +        let c = divide 1 (normalisation_factor a) in (c, 0, a * c)
1.231        else
1.232          case euclid_ext b (a mod b) of
1.233              (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
1.234 @@ -1650,7 +1633,7 @@
1.235  declare euclid_ext.simps [simp del]
1.236
1.237  lemma euclid_ext_0:
1.238 -  "euclid_ext a 0 = (ring_inv (normalisation_factor a), 0, a * ring_inv (normalisation_factor a))"
1.239 +  "euclid_ext a 0 = (divide 1 (normalisation_factor a), 0, a * divide 1 (normalisation_factor a))"
1.240    by (subst euclid_ext.simps, simp add: Let_def)
1.241
1.242  lemma euclid_ext_non_0:
1.243 @@ -1714,7 +1697,7 @@
1.244  lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
1.245    using euclid_ext'_correct by blast
1.246
1.247 -lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (ring_inv (normalisation_factor a), 0)"
1.248 +lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (divide 1 (normalisation_factor a), 0)"
1.249    by (simp add: bezw_def euclid_ext'_def euclid_ext_0)
1.250
1.251  lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
```