given up trivial definition
authorhaftmann
Fri Jun 12 08:53:23 2015 +0200 (2015-06-12)
changeset 6043268d75cff8809
parent 60431 db9c67b760f1
child 60433 720f210c5b1d
given up trivial definition
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     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.63        by (simp add: mult_ac)
    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.181      by (simp add: mult_ac)
   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)),