src/HOL/Rings.thy
 changeset 62376 85f38d5f8807 parent 62366 95c6cf433c91 child 62377 ace69956d018
```     1.1 --- a/src/HOL/Rings.thy	Tue Feb 09 09:21:10 2016 +0100
1.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 18:43:19 2016 +0100
1.3 @@ -635,7 +635,7 @@
1.4    case False then have "a * 0 div a = 0"
1.5      by (rule nonzero_mult_divide_cancel_left)
1.6    then show ?thesis by simp
1.7 -qed
1.8 +qed
1.9
1.10  lemma divide_1 [simp]:
1.11    "a div 1 = a"
1.12 @@ -663,16 +663,16 @@
1.13    with assms have "c = b * d" by (simp add: ac_simps)
1.14    then show ?Q ..
1.15  next
1.16 -  assume ?Q then obtain d where "c = b * d" ..
1.17 +  assume ?Q then obtain d where "c = b * d" ..
1.18    then have "a * c = a * b * d" by (simp add: ac_simps)
1.19    then show ?P ..
1.20  qed
1.21 -
1.22 +
1.23  lemma dvd_times_right_cancel_iff [simp]:
1.24    assumes "a \<noteq> 0"
1.25    shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
1.26  using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
1.27 -
1.28 +
1.29  lemma div_dvd_iff_mult:
1.30    assumes "b \<noteq> 0" and "b dvd a"
1.31    shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
1.32 @@ -991,7 +991,7 @@
1.33      and unit_factor_0 [simp]: "unit_factor 0 = 0"
1.34    assumes is_unit_normalize:
1.35      "is_unit a  \<Longrightarrow> normalize a = 1"
1.36 -  assumes unit_factor_is_unit [iff]:
1.37 +  assumes unit_factor_is_unit [iff]:
1.38      "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
1.39    assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
1.40  begin
1.41 @@ -1012,8 +1012,8 @@
1.42
1.43  lemma unit_factor_self [simp]:
1.44    "unit_factor a dvd a"
1.45 -  by (cases "a = 0") simp_all
1.46 -
1.47 +  by (cases "a = 0") simp_all
1.48 +
1.49  lemma normalize_mult_unit_factor [simp]:
1.50    "normalize a * unit_factor a = a"
1.51    using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
1.52 @@ -1023,7 +1023,7 @@
1.53  proof
1.54    assume ?P
1.55    moreover have "unit_factor a * normalize a = a" by simp
1.56 -  ultimately show ?Q by simp
1.57 +  ultimately show ?Q by simp
1.58  next
1.59    assume ?Q then show ?P by simp
1.60  qed
1.61 @@ -1033,14 +1033,14 @@
1.62  proof
1.63    assume ?P
1.64    moreover have "unit_factor a * normalize a = a" by simp
1.65 -  ultimately show ?Q by simp
1.66 +  ultimately show ?Q by simp
1.67  next
1.68    assume ?Q then show ?P by simp
1.69  qed
1.70
1.71  lemma is_unit_unit_factor:
1.72    assumes "is_unit a" shows "unit_factor a = a"
1.73 -proof -
1.74 +proof -
1.75    from assms have "normalize a = 1" by (rule is_unit_normalize)
1.76    moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
1.77    ultimately show ?thesis by simp
1.78 @@ -1069,13 +1069,13 @@
1.79      using \<open>a \<noteq> 0\<close> by simp
1.80    ultimately show ?Q by simp
1.81  qed
1.82 -
1.83 +
1.84  lemma div_normalize [simp]:
1.85    "a div normalize a = unit_factor a"
1.86  proof (cases "a = 0")
1.87    case True then show ?thesis by simp
1.88  next
1.89 -  case False then have "normalize a \<noteq> 0" by simp
1.90 +  case False then have "normalize a \<noteq> 0" by simp
1.91    with nonzero_mult_divide_cancel_right
1.92    have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
1.93    then show ?thesis by simp
1.94 @@ -1086,7 +1086,7 @@
1.95  proof (cases "a = 0")
1.96    case True then show ?thesis by simp
1.97  next
1.98 -  case False then have "unit_factor a \<noteq> 0" by simp
1.99 +  case False then have "unit_factor a \<noteq> 0" by simp
1.100    with nonzero_mult_divide_cancel_left
1.101    have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
1.102    then show ?thesis by simp
1.103 @@ -1126,7 +1126,7 @@
1.104      using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
1.105    finally show ?thesis .
1.106  qed
1.107 -
1.108 +
1.109  lemma unit_factor_idem [simp]:
1.110    "unit_factor (unit_factor a) = unit_factor a"
1.111    by (cases "a = 0") (auto intro: is_unit_unit_factor)
1.112 @@ -1134,7 +1134,7 @@
1.113  lemma normalize_unit_factor [simp]:
1.114    "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
1.115    by (rule is_unit_normalize) simp
1.116 -
1.117 +
1.118  lemma normalize_idem [simp]:
1.119    "normalize (normalize a) = normalize a"
1.120  proof (cases "a = 0")
1.121 @@ -1257,7 +1257,7 @@
1.122    proof (cases "a = 0 \<or> b = 0")
1.123      case True with \<open>?P\<close> show ?thesis by auto
1.124    next
1.125 -    case False
1.126 +    case False
1.127      then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
1.128        by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
1.129      with * show ?thesis by simp
1.130 @@ -1277,7 +1277,7 @@
1.131
1.132  end
1.133
1.135 +class ordered_semiring = semiring + ordered_comm_monoid_add +
1.136    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
1.137    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
1.138  begin
1.139 @@ -1324,7 +1324,7 @@
1.140
1.141  subclass ordered_cancel_semiring ..
1.142
1.145
1.146  lemma mult_left_less_imp_less:
1.147    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
1.148 @@ -1742,14 +1742,14 @@
1.149  lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
1.150    by simp
1.151
1.154    shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
1.155    apply (subst add_le_cancel_right [where c=k, symmetric])
1.157    apply (simp only: add.assoc [symmetric])
1.159
1.162    assumes a1: "i + k \<le> n"
1.163        and a2: "n \<le> j + k"
1.164    shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
1.165 @@ -2034,6 +2034,20 @@
1.166
1.167  end
1.168
1.169 +subsection \<open>Dioids\<close>
1.170 +
1.171 +text \<open>Dioids are the alternative extensions of semirings, a semiring can either be a ring or a dioid
1.172 +but never both.\<close>
1.173 +
1.174 +class dioid = semiring_1 + canonically_ordered_monoid_add
1.175 +begin
1.176 +
1.177 +subclass ordered_semiring
1.178 +  proof qed (auto simp: le_iff_add distrib_left distrib_right)
1.179 +
1.180 +end
1.181 +
1.182 +
1.183  hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
1.184
1.185  code_identifier
```