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.134 -class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   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.143 -subclass ordered_comm_monoid_add ..
   1.144 +subclass ordered_cancel_comm_monoid_add ..
   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.152 -lemma add_le_imp_le_diff: 
   1.153 +lemma add_le_imp_le_diff:
   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.156    apply (frule le_add_diff_inverse2)
   1.157    apply (simp only: add.assoc [symmetric])
   1.158    using add_implies_diff by fastforce
   1.159  
   1.160 -lemma add_le_add_imp_diff_le: 
   1.161 +lemma add_le_add_imp_diff_le:
   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