author haftmann Wed Nov 26 15:59:46 2014 +0100 (2014-11-26) changeset 59061 67771d267ff2 parent 59060 5f060de2dfd6 child 59062 f26598b1a0da
prefer abbrev for is_unit
```     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.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.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
```