prefer abbrev for is_unit
authorhaftmann
Wed Nov 26 15:59:46 2014 +0100 (2014-11-26)
changeset 5906167771d267ff2
parent 59060 5f060de2dfd6
child 59062 f26598b1a0da
prefer abbrev for is_unit
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Nov 26 15:46:19 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Nov 26 15:59:46 2014 +0100
     1.3 @@ -9,29 +9,29 @@
     1.4  context semiring_div
     1.5  begin 
     1.6  
     1.7 -definition ring_inv :: "'a \<Rightarrow> 'a"
     1.8 +abbreviation is_unit :: "'a \<Rightarrow> bool"
     1.9  where
    1.10 -  "ring_inv x = 1 div x"
    1.11 -
    1.12 -definition is_unit :: "'a \<Rightarrow> bool"
    1.13 -where
    1.14 -  "is_unit x \<longleftrightarrow> x dvd 1"
    1.15 +  "is_unit x \<equiv> x dvd 1"
    1.16  
    1.17  definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
    1.18  where
    1.19    "associated x y \<longleftrightarrow> x dvd y \<and> y dvd x"
    1.20  
    1.21 +definition ring_inv :: "'a \<Rightarrow> 'a"
    1.22 +where
    1.23 +  "ring_inv x = 1 div x"
    1.24 +
    1.25  lemma unit_prod [intro]:
    1.26    "is_unit x \<Longrightarrow> is_unit y \<Longrightarrow> is_unit (x * y)"
    1.27 -  unfolding is_unit_def by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono) 
    1.28 +  by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono) 
    1.29  
    1.30  lemma unit_ring_inv:
    1.31    "is_unit y \<Longrightarrow> x div y = x * ring_inv y"
    1.32 -  by (simp add: div_mult_swap ring_inv_def is_unit_def)
    1.33 +  by (simp add: div_mult_swap ring_inv_def)
    1.34  
    1.35  lemma unit_ring_inv_ring_inv [simp]:
    1.36    "is_unit x \<Longrightarrow> ring_inv (ring_inv x) = x"
    1.37 -  unfolding is_unit_def ring_inv_def
    1.38 +  unfolding ring_inv_def
    1.39    by (metis div_mult_mult1_if div_mult_self1_is_id dvd_mult_div_cancel mult_1_right)
    1.40  
    1.41  lemma inv_imp_eq_ring_inv:
    1.42 @@ -40,7 +40,7 @@
    1.43  
    1.44  lemma ring_inv_is_inv1 [simp]:
    1.45    "is_unit a \<Longrightarrow> a * ring_inv a = 1"
    1.46 -  unfolding is_unit_def ring_inv_def by simp
    1.47 +  unfolding ring_inv_def by simp
    1.48  
    1.49  lemma ring_inv_is_inv2 [simp]:
    1.50    "is_unit a \<Longrightarrow> ring_inv a * a = 1"
    1.51 @@ -51,7 +51,7 @@
    1.52    shows "is_unit (ring_inv x)"
    1.53  proof -
    1.54    from assms have "1 = ring_inv x * x" by simp
    1.55 -  then show "is_unit (ring_inv x)" unfolding is_unit_def by (rule dvdI)
    1.56 +  then show "is_unit (ring_inv x)" by (rule dvdI)
    1.57  qed
    1.58  
    1.59  lemma mult_unit_dvd_iff:
    1.60 @@ -104,11 +104,11 @@
    1.61  
    1.62  lemma unit_imp_dvd [dest]:
    1.63    "is_unit y \<Longrightarrow> y dvd x"
    1.64 -  by (rule dvd_trans [of _ 1]) (simp_all add: is_unit_def)
    1.65 +  by (rule dvd_trans [of _ 1]) simp_all
    1.66  
    1.67  lemma dvd_unit_imp_unit:
    1.68    "is_unit y \<Longrightarrow> x dvd y \<Longrightarrow> is_unit x"
    1.69 -  by (unfold is_unit_def) (rule dvd_trans)
    1.70 +  by (rule dvd_trans)
    1.71  
    1.72  lemma ring_inv_0 [simp]:
    1.73    "ring_inv 0 = 0"
    1.74 @@ -138,15 +138,15 @@
    1.75  
    1.76  lemma associated_unit:
    1.77    "is_unit x \<Longrightarrow> associated x y \<Longrightarrow> is_unit y"
    1.78 -  unfolding associated_def by (fast dest: dvd_unit_imp_unit)
    1.79 +  unfolding associated_def using dvd_unit_imp_unit by auto
    1.80  
    1.81  lemma is_unit_1 [simp]:
    1.82    "is_unit 1"
    1.83 -  unfolding is_unit_def by simp
    1.84 +  by simp
    1.85  
    1.86  lemma not_is_unit_0 [simp]:
    1.87    "\<not> is_unit 0"
    1.88 -  unfolding is_unit_def by auto
    1.89 +  by auto
    1.90  
    1.91  lemma unit_mult_left_cancel:
    1.92    assumes "is_unit x"
    1.93 @@ -193,7 +193,7 @@
    1.94          unfolding associated_def by simp_all
    1.95      hence "1 = x div y * (y div x)"
    1.96        by (simp add: div_mult_swap)
    1.97 -    hence "is_unit (x div y)" unfolding is_unit_def by (rule dvdI)
    1.98 +    hence "is_unit (x div y)" ..
    1.99      moreover have "x = (x div y) * y" by simp
   1.100      ultimately show ?thesis by blast
   1.101    qed
   1.102 @@ -218,21 +218,21 @@
   1.103  
   1.104  lemma is_unit_neg [simp]:
   1.105    "is_unit (- x) \<Longrightarrow> is_unit x"
   1.106 -  unfolding is_unit_def by simp
   1.107 +  by simp
   1.108  
   1.109  lemma is_unit_neg_1 [simp]:
   1.110    "is_unit (-1)"
   1.111 -  unfolding is_unit_def by simp
   1.112 +  by simp
   1.113  
   1.114  end
   1.115  
   1.116  lemma is_unit_nat [simp]:
   1.117    "is_unit (x::nat) \<longleftrightarrow> x = 1"
   1.118 -  unfolding is_unit_def by simp
   1.119 +  by simp
   1.120  
   1.121  lemma is_unit_int:
   1.122    "is_unit (x::int) \<longleftrightarrow> x = 1 \<or> x = -1"
   1.123 -  unfolding is_unit_def by auto
   1.124 +  by auto
   1.125  
   1.126  text {*
   1.127    A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
   1.128 @@ -741,7 +741,7 @@
   1.129    by (rule sym, rule gcdI, simp_all)
   1.130  
   1.131  lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
   1.132 -  by (auto simp: is_unit_def intro: coprimeI gcd_greatest dvd_gcd_D1 dvd_gcd_D2)
   1.133 +  by (auto intro: coprimeI gcd_greatest dvd_gcd_D1 dvd_gcd_D2)
   1.134  
   1.135  lemma div_gcd_coprime:
   1.136    assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   1.137 @@ -858,7 +858,7 @@
   1.138  lemma coprime_common_divisor: 
   1.139    "gcd a b = 1 \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> is_unit x"
   1.140    apply (subgoal_tac "x dvd gcd a b")
   1.141 -  apply (simp add: is_unit_def)
   1.142 +  apply simp
   1.143    apply (erule (1) gcd_greatest)
   1.144    done
   1.145  
   1.146 @@ -1144,14 +1144,15 @@
   1.147    "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
   1.148  proof
   1.149    assume "lcm a b = 1"
   1.150 -  then show "is_unit a \<and> is_unit b" unfolding is_unit_def by auto
   1.151 +  then show "is_unit a \<and> is_unit b" by auto
   1.152  next
   1.153    assume "is_unit a \<and> is_unit b"
   1.154 -  hence "a dvd 1" and "b dvd 1" unfolding is_unit_def by simp_all
   1.155 -  hence "is_unit (lcm a b)" unfolding is_unit_def by (rule lcm_least)
   1.156 +  hence "a dvd 1" and "b dvd 1" by simp_all
   1.157 +  hence "is_unit (lcm a b)" by (rule lcm_least)
   1.158    hence "lcm a b = normalisation_factor (lcm a b)"
   1.159      by (subst normalisation_factor_unit, simp_all)
   1.160 -  also have "\<dots> = 1" using `is_unit a \<and> is_unit b` by (auto simp add: is_unit_def)
   1.161 +  also have "\<dots> = 1" using `is_unit a \<and> is_unit b`
   1.162 +    by auto
   1.163    finally show "lcm a b = 1" .
   1.164  qed
   1.165  
   1.166 @@ -1389,7 +1390,7 @@
   1.167    "Lcm A = 1 \<longleftrightarrow> (\<forall>x\<in>A. is_unit x)"
   1.168  proof
   1.169    assume "Lcm A = 1"
   1.170 -  then show "\<forall>x\<in>A. is_unit x" unfolding is_unit_def by auto
   1.171 +  then show "\<forall>x\<in>A. is_unit x" by auto
   1.172  qed (rule LcmI [symmetric], auto)
   1.173  
   1.174  lemma Lcm_no_units:
   1.175 @@ -1733,7 +1734,7 @@
   1.176    "normalisation_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)"
   1.177  
   1.178  instance proof
   1.179 -qed (simp_all add: is_unit_def)
   1.180 +qed simp_all
   1.181  
   1.182  end
   1.183  
   1.184 @@ -1749,11 +1750,11 @@
   1.185  instance proof
   1.186    case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib)
   1.187  next
   1.188 -  case goal3 then show ?case by (simp add: zsgn_def is_unit_def)
   1.189 +  case goal3 then show ?case by (simp add: zsgn_def)
   1.190  next
   1.191 -  case goal5 then show ?case by (auto simp: zsgn_def is_unit_def)
   1.192 +  case goal5 then show ?case by (auto simp: zsgn_def)
   1.193  next
   1.194 -  case goal6 then show ?case by (auto split: abs_split simp: zsgn_def is_unit_def)
   1.195 +  case goal6 then show ?case by (auto split: abs_split simp: zsgn_def)
   1.196  qed (auto simp: sgn_times split: abs_split)
   1.197  
   1.198  end