distributivity of partial minus establishes desired properties of dvd in semirings
authorhaftmann
Mon Mar 23 19:05:14 2015 +0100 (2015-03-23)
changeset 59816034b13f4efae
parent 59815 cce82e360c2f
child 59817 75433c3ee203
distributivity of partial minus establishes desired properties of dvd in semirings
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/NSA/StarDef.thy
src/HOL/NSA/transfer.ML
src/HOL/Nat.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Parity.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Mar 23 19:05:14 2015 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Mar 23 19:05:14 2015 +0100
     1.3 @@ -217,9 +217,7 @@
     1.4  
     1.5  instance integer :: semiring_numeral_div
     1.6    by intro_classes (transfer,
     1.7 -    fact semiring_numeral_div_class.diff_invert_add1
     1.8 -    semiring_numeral_div_class.le_add_diff_inverse2
     1.9 -    semiring_numeral_div_class.mult_div_cancel
    1.10 +    fact semiring_numeral_div_class.le_add_diff_inverse2
    1.11      semiring_numeral_div_class.div_less
    1.12      semiring_numeral_div_class.mod_less
    1.13      semiring_numeral_div_class.div_positive
     2.1 --- a/src/HOL/Divides.thy	Mon Mar 23 19:05:14 2015 +0100
     2.2 +++ b/src/HOL/Divides.thy	Mon Mar 23 19:05:14 2015 +0100
     2.3 @@ -548,7 +548,7 @@
     2.4  
     2.5  subsubsection {* Parity and division *}
     2.6  
     2.7 -class semiring_div_parity = semiring_div + semiring_numeral +
     2.8 +class semiring_div_parity = comm_semiring_1_diff_distrib + numeral + semiring_div +
     2.9    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    2.10    assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    2.11    assumes zero_not_eq_two: "0 \<noteq> 2"
    2.12 @@ -583,19 +583,6 @@
    2.13  
    2.14  subclass semiring_parity
    2.15  proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
    2.16 -  fix a b c
    2.17 -  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
    2.18 -    by simp
    2.19 -next
    2.20 -  fix a b c
    2.21 -  assume "(b + c) mod a = 0"
    2.22 -  with mod_add_eq [of b c a]
    2.23 -  have "(b mod a + c mod a) mod a = 0"
    2.24 -    by simp
    2.25 -  moreover assume "b mod a = 0"
    2.26 -  ultimately show "c mod a = 0"
    2.27 -    by simp
    2.28 -next
    2.29    show "1 mod 2 = 1"
    2.30      by (fact one_mod_two_eq_one)
    2.31  next
    2.32 @@ -651,11 +638,9 @@
    2.33    and less technical class hierarchy.
    2.34  *}
    2.35  
    2.36 -class semiring_numeral_div = linordered_semidom + minus + semiring_div +
    2.37 -  assumes diff_invert_add1: "a + b = c \<Longrightarrow> a = c - b"
    2.38 -    and le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
    2.39 -  assumes mult_div_cancel: "b * (a div b) = a - a mod b"
    2.40 -    and div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    2.41 +class semiring_numeral_div = comm_semiring_1_diff_distrib + linordered_semidom + semiring_div +
    2.42 +  assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
    2.43 +  assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    2.44      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    2.45      and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
    2.46      and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
    2.47 @@ -666,9 +651,16 @@
    2.48    assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
    2.49  begin
    2.50  
    2.51 -lemma diff_zero [simp]:
    2.52 -  "a - 0 = a"
    2.53 -  by (rule diff_invert_add1 [symmetric]) simp
    2.54 +lemma mult_div_cancel:
    2.55 +  "b * (a div b) = a - a mod b"
    2.56 +proof -
    2.57 +  have "b * (a div b) + a mod b = a"
    2.58 +    using mod_div_equality [of a b] by (simp add: ac_simps)
    2.59 +  then have "b * (a div b) + a mod b - a mod b = a - a mod b"
    2.60 +    by simp
    2.61 +  then show ?thesis
    2.62 +    by simp
    2.63 +qed
    2.64  
    2.65  subclass semiring_div_parity
    2.66  proof
    2.67 @@ -713,7 +705,7 @@
    2.68      by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
    2.69    with `w = 1` have div: "2 * (a div (2 * b)) = a div b - 1" by simp
    2.70    then show ?P and ?Q
    2.71 -    by (simp_all add: div mod diff_invert_add1 [symmetric] le_add_diff_inverse2)
    2.72 +    by (simp_all add: div mod add_implies_diff [symmetric] le_add_diff_inverse2)
    2.73  qed
    2.74  
    2.75  lemma divmod_digit_0:
    2.76 @@ -862,7 +854,7 @@
    2.77  
    2.78  end
    2.79  
    2.80 -hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero
    2.81 +hide_fact (open) le_add_diff_inverse2
    2.82    -- {* restore simple accesses for more general variants of theorems *}
    2.83  
    2.84    
     3.1 --- a/src/HOL/NSA/StarDef.thy	Mon Mar 23 19:05:14 2015 +0100
     3.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Mar 23 19:05:14 2015 +0100
     3.3 @@ -698,7 +698,7 @@
     3.4    star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
     3.5  
     3.6  instance
     3.7 -  by default (transfer star_inf_def, auto)+
     3.8 +  by default (transfer, auto)+
     3.9  
    3.10  end
    3.11  
    3.12 @@ -709,7 +709,7 @@
    3.13    star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
    3.14  
    3.15  instance
    3.16 -  by default (transfer star_sup_def, auto)+
    3.17 +  by default (transfer, auto)+
    3.18  
    3.19  end
    3.20  
    3.21 @@ -850,11 +850,8 @@
    3.22  
    3.23  declare dvd_def [transfer_refold]
    3.24  
    3.25 -instance star :: (semiring_dvd) semiring_dvd
    3.26 -apply intro_classes
    3.27 -apply(transfer, rule dvd_add_times_triv_left_iff)
    3.28 -apply(transfer, erule (1) dvd_addD)
    3.29 -done
    3.30 +instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib
    3.31 +by intro_classes (transfer, fact right_diff_distrib')
    3.32  
    3.33  instance star :: (no_zero_divisors) no_zero_divisors
    3.34  by (intro_classes, transfer, rule no_zero_divisors)
    3.35 @@ -1040,18 +1037,16 @@
    3.36  
    3.37  instance star :: (semiring_numeral_div) semiring_numeral_div
    3.38  apply intro_classes
    3.39 -apply(transfer, erule semiring_numeral_div_class.diff_invert_add1)
    3.40 -apply(transfer, erule semiring_numeral_div_class.le_add_diff_inverse2)
    3.41 -apply(transfer, rule semiring_numeral_div_class.mult_div_cancel)
    3.42 -apply(transfer, erule (1) semiring_numeral_div_class.div_less)
    3.43 -apply(transfer, erule (1) semiring_numeral_div_class.mod_less)
    3.44 -apply(transfer, erule (1) semiring_numeral_div_class.div_positive)
    3.45 -apply(transfer, erule semiring_numeral_div_class.mod_less_eq_dividend)
    3.46 -apply(transfer, erule semiring_numeral_div_class.pos_mod_bound)
    3.47 -apply(transfer, erule semiring_numeral_div_class.pos_mod_sign)
    3.48 -apply(transfer, erule semiring_numeral_div_class.mod_mult2_eq)
    3.49 -apply(transfer, erule semiring_numeral_div_class.div_mult2_eq)
    3.50 -apply(transfer, rule discrete)
    3.51 +apply(transfer, fact semiring_numeral_div_class.le_add_diff_inverse2)
    3.52 +apply(transfer, fact semiring_numeral_div_class.div_less)
    3.53 +apply(transfer, fact semiring_numeral_div_class.mod_less)
    3.54 +apply(transfer, fact semiring_numeral_div_class.div_positive)
    3.55 +apply(transfer, fact semiring_numeral_div_class.mod_less_eq_dividend)
    3.56 +apply(transfer, fact semiring_numeral_div_class.pos_mod_bound)
    3.57 +apply(transfer, fact semiring_numeral_div_class.pos_mod_sign)
    3.58 +apply(transfer, fact semiring_numeral_div_class.mod_mult2_eq)
    3.59 +apply(transfer, fact semiring_numeral_div_class.div_mult2_eq)
    3.60 +apply(transfer, fact discrete)
    3.61  done
    3.62  
    3.63  subsection {* Finite class *}
     4.1 --- a/src/HOL/NSA/transfer.ML	Mon Mar 23 19:05:14 2015 +0100
     4.2 +++ b/src/HOL/NSA/transfer.ML	Mon Mar 23 19:05:14 2015 +0100
     4.3 @@ -68,7 +68,7 @@
     4.4    in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
     4.5  
     4.6  fun transfer_tac ctxt ths =
     4.7 -    SUBGOAL (fn (t,i) =>
     4.8 +    SUBGOAL (fn (t, _) =>
     4.9          (fn th =>
    4.10              let
    4.11                val tr = transfer_thm_of ctxt ths t
     5.1 --- a/src/HOL/Nat.thy	Mon Mar 23 19:05:14 2015 +0100
     5.2 +++ b/src/HOL/Nat.thy	Mon Mar 23 19:05:14 2015 +0100
     5.3 @@ -366,12 +366,20 @@
     5.4  
     5.5  text {* Difference distributes over multiplication *}
     5.6  
     5.7 -lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
     5.8 -by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
     5.9 -
    5.10 -lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)"
    5.11 -by (simp add: diff_mult_distrib mult.commute [of k])
    5.12 -  -- {* NOT added as rewrites, since sometimes they are used from right-to-left *}
    5.13 +instance nat :: comm_semiring_1_diff_distrib
    5.14 +proof
    5.15 +  fix k m n :: nat
    5.16 +  show "k * ((m::nat) - n) = (k * m) - (k * n)"
    5.17 +    by (induct m n rule: diff_induct) simp_all
    5.18 +qed
    5.19 +
    5.20 +lemma diff_mult_distrib:
    5.21 +  "((m::nat) - n) * k = (m * k) - (n * k)"
    5.22 +  by (fact left_diff_distrib')
    5.23 +  
    5.24 +lemma diff_mult_distrib2:
    5.25 +  "k * ((m::nat) - n) = (k * m) - (k * n)"
    5.26 +  by (fact right_diff_distrib')
    5.27  
    5.28  
    5.29  subsubsection {* Multiplication *}
    5.30 @@ -1876,48 +1884,6 @@
    5.31  
    5.32  subsection {* The divides relation on @{typ nat} *}
    5.33  
    5.34 -instance nat :: semiring_dvd
    5.35 -proof
    5.36 -  fix m n q :: nat
    5.37 -  show "m dvd q * m + n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
    5.38 -  proof
    5.39 -    assume ?Q then show ?P by simp
    5.40 -  next
    5.41 -    assume ?P then obtain d where *: "q * m + n = m * d" ..
    5.42 -    show ?Q
    5.43 -    proof (cases "n = 0")
    5.44 -      case True then show ?Q by simp
    5.45 -    next
    5.46 -      case False
    5.47 -      with * have "q * m < m * d"
    5.48 -        using less_add_eq_less [of 0 n "q * m" "m * d"] by simp
    5.49 -      then have "q \<le> d" by (auto intro: ccontr simp add: mult.commute [of m])
    5.50 -      with * [symmetric] have "n = m * (d - q)"
    5.51 -        by (simp add: diff_mult_distrib2 mult.commute [of m])
    5.52 -      then show ?Q ..
    5.53 -    qed
    5.54 -  qed
    5.55 -  assume "m dvd n + q" and "m dvd n"
    5.56 -  show "m dvd q"
    5.57 -  proof -
    5.58 -    from `m dvd n` obtain d where "n = m * d" ..
    5.59 -    moreover from `m dvd n + q` obtain e where "n + q = m * e" ..
    5.60 -    ultimately have *: "m * d + q = m * e" by simp
    5.61 -    show "m dvd q"
    5.62 -    proof (cases "q = 0")
    5.63 -      case True then show ?thesis by simp
    5.64 -    next
    5.65 -      case False
    5.66 -      with * have "m * d < m * e"
    5.67 -        using less_add_eq_less [of 0 q "m * d" "m * e"] by simp
    5.68 -      then have "d \<le> e" by (auto intro: ccontr)
    5.69 -      with * have "q = m * (e - d)"
    5.70 -        by (simp add: diff_mult_distrib2)
    5.71 -      then show ?thesis ..
    5.72 -    qed
    5.73 -  qed
    5.74 -qed
    5.75 -
    5.76  lemma dvd_1_left [iff]: "Suc 0 dvd k"
    5.77  unfolding dvd_def by simp
    5.78  
     6.1 --- a/src/HOL/Number_Theory/Cong.thy	Mon Mar 23 19:05:14 2015 +0100
     6.2 +++ b/src/HOL/Number_Theory/Cong.thy	Mon Mar 23 19:05:14 2015 +0100
     6.3 @@ -443,7 +443,7 @@
     6.4    apply (erule ssubst)
     6.5    apply (subst zmod_zmult2_eq)
     6.6    apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
     6.7 -  apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+
     6.8 +  apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+
     6.9    done
    6.10  
    6.11  lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
     7.1 --- a/src/HOL/Parity.thy	Mon Mar 23 19:05:14 2015 +0100
     7.2 +++ b/src/HOL/Parity.thy	Mon Mar 23 19:05:14 2015 +0100
     7.3 @@ -11,13 +11,15 @@
     7.4  
     7.5  subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
     7.6  
     7.7 -class semiring_parity = semiring_dvd + semiring_numeral +
     7.8 +class semiring_parity = comm_semiring_1_diff_distrib + numeral +
     7.9    assumes odd_one [simp]: "\<not> 2 dvd 1"
    7.10    assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
    7.11    assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
    7.12    assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
    7.13  begin
    7.14  
    7.15 +subclass semiring_numeral ..
    7.16 +
    7.17  abbreviation even :: "'a \<Rightarrow> bool"
    7.18  where
    7.19    "even a \<equiv> 2 dvd a"
    7.20 @@ -97,9 +99,11 @@
    7.21  
    7.22  end
    7.23  
    7.24 -class ring_parity = comm_ring_1 + semiring_parity
    7.25 +class ring_parity = ring + semiring_parity
    7.26  begin
    7.27  
    7.28 +subclass comm_ring_1 ..
    7.29 +
    7.30  lemma even_minus [simp]:
    7.31    "even (- a) \<longleftrightarrow> even a"
    7.32    by (fact dvd_minus_iff)
     8.1 --- a/src/HOL/Rings.thy	Mon Mar 23 19:05:14 2015 +0100
     8.2 +++ b/src/HOL/Rings.thy	Mon Mar 23 19:05:14 2015 +0100
     8.3 @@ -228,35 +228,6 @@
     8.4  
     8.5  end
     8.6  
     8.7 -class semiring_dvd = comm_semiring_1 +
     8.8 -  assumes dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
     8.9 -  assumes dvd_addD: "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
    8.10 -begin
    8.11 -
    8.12 -lemma dvd_add_times_triv_right_iff [simp]:
    8.13 -  "a dvd b + c * a \<longleftrightarrow> a dvd b"
    8.14 -  using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
    8.15 -
    8.16 -lemma dvd_add_triv_left_iff [simp]:
    8.17 -  "a dvd a + b \<longleftrightarrow> a dvd b"
    8.18 -  using dvd_add_times_triv_left_iff [of a 1 b] by simp
    8.19 -
    8.20 -lemma dvd_add_triv_right_iff [simp]:
    8.21 -  "a dvd b + a \<longleftrightarrow> a dvd b"
    8.22 -  using dvd_add_times_triv_right_iff [of a b 1] by simp
    8.23 -
    8.24 -lemma dvd_add_right_iff:
    8.25 -  assumes "a dvd b"
    8.26 -  shows "a dvd b + c \<longleftrightarrow> a dvd c"
    8.27 -  using assms by (auto dest: dvd_addD)
    8.28 -
    8.29 -lemma dvd_add_left_iff:
    8.30 -  assumes "a dvd c"
    8.31 -  shows "a dvd b + c \<longleftrightarrow> a dvd b"
    8.32 -  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
    8.33 -
    8.34 -end
    8.35 -
    8.36  class no_zero_divisors = zero + times +
    8.37    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    8.38  begin
    8.39 @@ -293,6 +264,65 @@
    8.40  
    8.41  end
    8.42  
    8.43 +class comm_semiring_1_diff_distrib = comm_semiring_1_cancel +
    8.44 +  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
    8.45 +begin
    8.46 +
    8.47 +lemma left_diff_distrib' [algebra_simps]:
    8.48 +  "(b - c) * a = b * a - c * a"
    8.49 +  by (simp add: algebra_simps)
    8.50 +
    8.51 +lemma dvd_add_times_triv_left_iff [simp]:
    8.52 +  "a dvd c * a + b \<longleftrightarrow> a dvd b"
    8.53 +proof -
    8.54 +  have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
    8.55 +  proof
    8.56 +    assume ?Q then show ?P by simp
    8.57 +  next
    8.58 +    assume ?P
    8.59 +    then obtain d where "a * c + b = a * d" ..
    8.60 +    then have "a * c + b - a * c = a * d - a * c" by simp
    8.61 +    then have "b = a * d - a * c" by simp
    8.62 +    then have "b = a * (d - c)" by (simp add: algebra_simps) 
    8.63 +    then show ?Q ..
    8.64 +  qed
    8.65 +  then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
    8.66 +qed
    8.67 +
    8.68 +lemma dvd_add_times_triv_right_iff [simp]:
    8.69 +  "a dvd b + c * a \<longleftrightarrow> a dvd b"
    8.70 +  using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
    8.71 +
    8.72 +lemma dvd_add_triv_left_iff [simp]:
    8.73 +  "a dvd a + b \<longleftrightarrow> a dvd b"
    8.74 +  using dvd_add_times_triv_left_iff [of a 1 b] by simp
    8.75 +
    8.76 +lemma dvd_add_triv_right_iff [simp]:
    8.77 +  "a dvd b + a \<longleftrightarrow> a dvd b"
    8.78 +  using dvd_add_times_triv_right_iff [of a b 1] by simp
    8.79 +
    8.80 +lemma dvd_add_right_iff:
    8.81 +  assumes "a dvd b"
    8.82 +  shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")
    8.83 +proof
    8.84 +  assume ?P then obtain d where "b + c = a * d" ..
    8.85 +  moreover from `a dvd b` obtain e where "b = a * e" ..
    8.86 +  ultimately have "a * e + c = a * d" by simp
    8.87 +  then have "a * e + c - a * e = a * d - a * e" by simp
    8.88 +  then have "c = a * d - a * e" by simp
    8.89 +  then have "c = a * (d - e)" by (simp add: algebra_simps)
    8.90 +  then show ?Q ..
    8.91 +next
    8.92 +  assume ?Q with assms show ?P by simp
    8.93 +qed
    8.94 +
    8.95 +lemma dvd_add_left_iff:
    8.96 +  assumes "a dvd c"
    8.97 +  shows "a dvd b + c \<longleftrightarrow> a dvd b"
    8.98 +  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
    8.99 +
   8.100 +end
   8.101 +
   8.102  class ring = semiring + ab_group_add
   8.103  begin
   8.104  
   8.105 @@ -370,27 +400,8 @@
   8.106  subclass ring_1 ..
   8.107  subclass comm_semiring_1_cancel ..
   8.108  
   8.109 -subclass semiring_dvd
   8.110 -proof
   8.111 -  fix a b c
   8.112 -  show "a dvd c * a + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
   8.113 -  proof
   8.114 -    assume ?Q then show ?P by simp
   8.115 -  next
   8.116 -    assume ?P then obtain d where "c * a + b = a * d" ..
   8.117 -    then have "b = a * (d - c)" by (simp add: algebra_simps)
   8.118 -    then show ?Q ..
   8.119 -  qed
   8.120 -  assume "a dvd b + c" and "a dvd b"
   8.121 -  show "a dvd c"
   8.122 -  proof -
   8.123 -    from `a dvd b` obtain d where "b = a * d" ..
   8.124 -    moreover from `a dvd b + c` obtain e where "b + c = a * e" ..
   8.125 -    ultimately have "a * d + c = a * e" by simp
   8.126 -    then have "c = a * (e - d)" by (simp add: algebra_simps)
   8.127 -    then show "a dvd c" ..
   8.128 -  qed
   8.129 -qed
   8.130 +subclass comm_semiring_1_diff_distrib
   8.131 +  by unfold_locales (simp add: algebra_simps)
   8.132  
   8.133  lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   8.134  proof
   8.135 @@ -1265,4 +1276,3 @@
   8.136    code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   8.137  
   8.138  end
   8.139 -