tuned bootstrap order to provide type classes in a more sensible order
authorhaftmann
Tue Mar 01 10:36:19 2016 +0100 (2016-03-01)
changeset 62481b5d8e57826df
parent 62480 f2e8984adef7
child 62482 577199585ba0
child 62487 fc353b09325d
tuned bootstrap order to provide type classes in a more sensible order
src/HOL/Binomial.thy
src/HOL/Fields.thy
src/HOL/Finite_Set.thy
src/HOL/Groups_Big.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Nat.thy
src/HOL/Num.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Old_Number_Theory/Factorization.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Power.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Binomial.thy	Tue Mar 01 10:32:55 2016 +0100
     1.2 +++ b/src/HOL/Binomial.thy	Tue Mar 01 10:36:19 2016 +0100
     1.3 @@ -697,9 +697,8 @@
     1.4    then show ?thesis by simp
     1.5  next
     1.6    case False
     1.7 -  from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
     1.8 -  have eq: "(- (1::'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
     1.9 -    by auto
    1.10 +  then have eq: "(- 1) ^ n = (\<Prod>i = 0..n - 1. - 1)"
    1.11 +    by (auto simp add: setprod_constant)
    1.12    from False show ?thesis
    1.13      by (simp add: pochhammer_def gbinomial_def field_simps
    1.14        eq setprod.distrib[symmetric])
     2.1 --- a/src/HOL/Fields.thy	Tue Mar 01 10:32:55 2016 +0100
     2.2 +++ b/src/HOL/Fields.thy	Tue Mar 01 10:36:19 2016 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4  section \<open>Fields\<close>
     2.5  
     2.6  theory Fields
     2.7 -imports Rings
     2.8 +imports Nat
     2.9  begin
    2.10  
    2.11  subsection \<open>Division rings\<close>
    2.12 @@ -29,6 +29,24 @@
    2.13  
    2.14  end
    2.15  
    2.16 +text \<open>Setup for linear arithmetic prover\<close>
    2.17 +
    2.18 +ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
    2.19 +ML_file "Tools/lin_arith.ML"
    2.20 +setup \<open>Lin_Arith.global_setup\<close>
    2.21 +declaration \<open>K Lin_Arith.setup\<close>
    2.22 +
    2.23 +simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
    2.24 +  \<open>K Lin_Arith.simproc\<close>
    2.25 +(* Because of this simproc, the arithmetic solver is really only
    2.26 +useful to detect inconsistencies among the premises for subgoals which are
    2.27 +*not* themselves (in)equalities, because the latter activate
    2.28 +fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    2.29 +solver all the time rather than add the additional check. *)
    2.30 +
    2.31 +lemmas [arith_split] = nat_diff_split split_min split_max
    2.32 +
    2.33 +
    2.34  text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
    2.35  
    2.36  named_theorems divide_simps "rewrite rules to eliminate divisions"
    2.37 @@ -490,6 +508,8 @@
    2.38  
    2.39  end
    2.40  
    2.41 +class field_char_0 = field + ring_char_0
    2.42 +
    2.43  
    2.44  subsection \<open>Ordered fields\<close>
    2.45  
     3.1 --- a/src/HOL/Finite_Set.thy	Tue Mar 01 10:32:55 2016 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Tue Mar 01 10:36:19 2016 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  section \<open>Finite sets\<close>
     3.5  
     3.6  theory Finite_Set
     3.7 -imports Product_Type Sum_Type Nat
     3.8 +imports Product_Type Sum_Type Fields
     3.9  begin
    3.10  
    3.11  subsection \<open>Predicate for finite sets\<close>
     4.1 --- a/src/HOL/Groups_Big.thy	Tue Mar 01 10:32:55 2016 +0100
     4.2 +++ b/src/HOL/Groups_Big.thy	Tue Mar 01 10:36:19 2016 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  section \<open>Big sum and product over finite (non-empty) sets\<close>
     4.5  
     4.6  theory Groups_Big
     4.7 -imports Finite_Set
     4.8 +imports Finite_Set Power
     4.9  begin
    4.10  
    4.11  subsection \<open>Generic monoid operation over a set\<close>
    4.12 @@ -1145,6 +1145,18 @@
    4.13    qed
    4.14  qed
    4.15  
    4.16 +lemma setsum_zero_power [simp]:
    4.17 +  fixes c :: "nat \<Rightarrow> 'a::division_ring"
    4.18 +  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
    4.19 +apply (cases "finite A")
    4.20 +  by (induction A rule: finite_induct) auto
    4.21 +
    4.22 +lemma setsum_zero_power' [simp]:
    4.23 +  fixes c :: "nat \<Rightarrow> 'a::field"
    4.24 +  shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
    4.25 +  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
    4.26 +  by auto
    4.27 +
    4.28  lemma (in field) setprod_inversef:
    4.29    "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
    4.30    by (induct A rule: finite_induct) simp_all
    4.31 @@ -1197,4 +1209,51 @@
    4.32    "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
    4.33    using setprod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
    4.34  
    4.35 +lemma setprod_constant:
    4.36 +  "(\<Prod>x\<in> A. (y::'a::comm_monoid_mult)) = y ^ card A"
    4.37 +  by (induct A rule: infinite_finite_induct) simp_all
    4.38 +
    4.39 +lemma setprod_power_distrib:
    4.40 +  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
    4.41 +  shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
    4.42 +proof (cases "finite A")
    4.43 +  case True then show ?thesis
    4.44 +    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
    4.45 +next
    4.46 +  case False then show ?thesis
    4.47 +    by simp
    4.48 +qed
    4.49 +
    4.50 +lemma power_setsum:
    4.51 +  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
    4.52 +  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
    4.53 +
    4.54 +lemma setprod_gen_delta:
    4.55 +  assumes fS: "finite S"
    4.56 +  shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
    4.57 +proof-
    4.58 +  let ?f = "(\<lambda>k. if k=a then b k else c)"
    4.59 +  {assume a: "a \<notin> S"
    4.60 +    hence "\<forall> k\<in> S. ?f k = c" by simp
    4.61 +    hence ?thesis using a setprod_constant by simp }
    4.62 +  moreover
    4.63 +  {assume a: "a \<in> S"
    4.64 +    let ?A = "S - {a}"
    4.65 +    let ?B = "{a}"
    4.66 +    have eq: "S = ?A \<union> ?B" using a by blast
    4.67 +    have dj: "?A \<inter> ?B = {}" by simp
    4.68 +    from fS have fAB: "finite ?A" "finite ?B" by auto
    4.69 +    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
    4.70 +      by (rule setprod.cong) auto
    4.71 +    have cA: "card ?A = card S - 1" using fS a by auto
    4.72 +    have fA1: "setprod ?f ?A = c ^ card ?A"
    4.73 +      unfolding fA0 by (rule setprod_constant)
    4.74 +    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
    4.75 +      using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
    4.76 +      by simp
    4.77 +    then have ?thesis using a cA
    4.78 +      by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)}
    4.79 +  ultimately show ?thesis by blast
    4.80 +qed
    4.81 +
    4.82  end
     5.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 01 10:32:55 2016 +0100
     5.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 01 10:36:19 2016 +0100
     5.3 @@ -2305,7 +2305,7 @@
     5.4    have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
     5.5      by (simp add: Suc fps_power_nth del: replicate.simps power_Suc)
     5.6    also have "\<dots> = (a$0) ^ m"
     5.7 -   unfolding c by (rule setprod_constant) simp
     5.8 +   unfolding c by (rule setprod_constant)
     5.9   finally show ?thesis .
    5.10  qed
    5.11  
     6.1 --- a/src/HOL/Nat.thy	Tue Mar 01 10:32:55 2016 +0100
     6.2 +++ b/src/HOL/Nat.thy	Tue Mar 01 10:36:19 2016 +0100
     6.3 @@ -8,14 +8,13 @@
     6.4  section \<open>Natural numbers\<close>
     6.5  
     6.6  theory Nat
     6.7 -imports Inductive Typedef Fun Fields
     6.8 +imports Inductive Typedef Fun Rings
     6.9  begin
    6.10  
    6.11  ML_file "~~/src/Tools/rat.ML"
    6.12  
    6.13  named_theorems arith "arith facts -- only ground formulas"
    6.14  ML_file "Tools/arith_data.ML"
    6.15 -ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
    6.16  
    6.17  
    6.18  subsection \<open>Type \<open>ind\<close>\<close>
    6.19 @@ -724,11 +723,16 @@
    6.20    by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
    6.21  
    6.22  text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
    6.23 -lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
    6.24 -apply(auto simp: gr0_conv_Suc)
    6.25 -apply (induct_tac m)
    6.26 -apply (simp_all add: add_less_mono)
    6.27 -done
    6.28 +lemma mult_less_mono2:
    6.29 +  fixes i j :: nat
    6.30 +  assumes "i < j" and "0 < k"
    6.31 +  shows "k * i < k * j"
    6.32 +using \<open>0 < k\<close> proof (induct k)
    6.33 +  case 0 then show ?case by simp
    6.34 +next
    6.35 +  case (Suc k) with \<open>i < j\<close> show ?case
    6.36 +    by (cases k) (simp_all add: add_less_mono)
    6.37 +qed
    6.38  
    6.39  text \<open>Addition is the inverse of subtraction:
    6.40    if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
    6.41 @@ -1103,8 +1107,18 @@
    6.42  lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
    6.43  by (induct j k rule: diff_induct) simp_all
    6.44  
    6.45 +lemma add_diff_assoc [simp]:
    6.46 +  fixes i j k :: nat
    6.47 +  shows "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
    6.48 +  by (fact diff_add_assoc [symmetric])
    6.49 +
    6.50  lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
    6.51 -by (simp add: add.commute diff_add_assoc)
    6.52 +  by (simp add: ac_simps)
    6.53 +
    6.54 +lemma add_diff_assoc2 [simp]:
    6.55 +  fixes i j k :: nat
    6.56 +  shows "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
    6.57 +  by (fact diff_add_assoc2 [symmetric])
    6.58  
    6.59  lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
    6.60  by auto
    6.61 @@ -1457,6 +1471,14 @@
    6.62  
    6.63  declare of_nat_code [code]
    6.64  
    6.65 +context ring_1
    6.66 +begin
    6.67 +
    6.68 +lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
    6.69 +by (simp add: algebra_simps of_nat_add [symmetric])
    6.70 +
    6.71 +end
    6.72 +
    6.73  text\<open>Class for unital semirings with characteristic zero.
    6.74   Includes non-ordered rings like the complex numbers.\<close>
    6.75  
    6.76 @@ -1485,6 +1507,8 @@
    6.77  
    6.78  end
    6.79  
    6.80 +class ring_char_0 = ring_1 + semiring_char_0
    6.81 +
    6.82  context linordered_semidom
    6.83  begin
    6.84  
    6.85 @@ -1521,14 +1545,6 @@
    6.86  
    6.87  end
    6.88  
    6.89 -context ring_1
    6.90 -begin
    6.91 -
    6.92 -lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
    6.93 -by (simp add: algebra_simps of_nat_add [symmetric])
    6.94 -
    6.95 -end
    6.96 -
    6.97  context linordered_idom
    6.98  begin
    6.99  
   6.100 @@ -1621,21 +1637,6 @@
   6.101    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
   6.102    \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
   6.103  
   6.104 -ML_file "Tools/lin_arith.ML"
   6.105 -setup \<open>Lin_Arith.global_setup\<close>
   6.106 -declaration \<open>K Lin_Arith.setup\<close>
   6.107 -
   6.108 -simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
   6.109 -  \<open>K Lin_Arith.simproc\<close>
   6.110 -(* Because of this simproc, the arithmetic solver is really only
   6.111 -useful to detect inconsistencies among the premises for subgoals which are
   6.112 -*not* themselves (in)equalities, because the latter activate
   6.113 -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
   6.114 -solver all the time rather than add the additional check. *)
   6.115 -
   6.116 -
   6.117 -lemmas [arith_split] = nat_diff_split split_min split_max
   6.118 -
   6.119  context order
   6.120  begin
   6.121  
   6.122 @@ -1695,62 +1696,95 @@
   6.123  
   6.124  text\<open>Subtraction laws, mostly by Clemens Ballarin\<close>
   6.125  
   6.126 -lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
   6.127 -by arith
   6.128 -
   6.129 -lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
   6.130 -by arith
   6.131 +lemma diff_less_mono:
   6.132 +  fixes a b c :: nat
   6.133 +  assumes "a < b" and "c \<le> a"
   6.134 +  shows "a - c < b - c"
   6.135 +proof -
   6.136 +  from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0"
   6.137 +    by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps)
   6.138 +  then show ?thesis by simp
   6.139 +qed
   6.140 +
   6.141 +lemma less_diff_conv:
   6.142 +  fixes i j k :: nat
   6.143 +  shows "i < j - k \<longleftrightarrow> i + k < j" (is "?P \<longleftrightarrow> ?Q")
   6.144 +  by (cases "k \<le> j")
   6.145 +    (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
   6.146  
   6.147  lemma less_diff_conv2:
   6.148    fixes j k i :: nat
   6.149    assumes "k \<le> j"
   6.150 -  shows "j - k < i \<longleftrightarrow> j < i + k"
   6.151 -  using assms by arith
   6.152 -
   6.153 -lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
   6.154 -by arith
   6.155 -
   6.156 -lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
   6.157 -by arith
   6.158 -
   6.159 -(*Replaces the previous diff_less and le_diff_less, which had the stronger
   6.160 -  second premise n\<le>m*)
   6.161 -lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
   6.162 -by arith
   6.163 +  shows "j - k < i \<longleftrightarrow> j < i + k" (is "?P \<longleftrightarrow> ?Q")
   6.164 +  using assms by (auto dest: le_Suc_ex)
   6.165 +
   6.166 +lemma le_diff_conv:
   6.167 +  fixes j k i :: nat
   6.168 +  shows "j - k \<le> i \<longleftrightarrow> j \<le> i + k"
   6.169 +  by (cases "k \<le> j")
   6.170 +    (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
   6.171 +
   6.172 +lemma diff_diff_cancel [simp]:
   6.173 +  fixes i n :: nat
   6.174 +  shows "i \<le> n \<Longrightarrow> n - (n - i) = i"
   6.175 +  by (auto dest: le_Suc_ex)
   6.176 +
   6.177 +lemma diff_less [simp]:
   6.178 +  fixes i n :: nat
   6.179 +  shows "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m"
   6.180 +  by (auto dest: less_imp_Suc_add)
   6.181  
   6.182  text \<open>Simplification of relational expressions involving subtraction\<close>
   6.183  
   6.184 -lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
   6.185 -by (simp split add: nat_diff_split)
   6.186 +lemma diff_diff_eq:
   6.187 +  fixes m n k :: nat
   6.188 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n"
   6.189 +  by (auto dest!: le_Suc_ex)
   6.190  
   6.191  hide_fact (open) diff_diff_eq
   6.192  
   6.193 -lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
   6.194 -by (auto split add: nat_diff_split)
   6.195 -
   6.196 -lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
   6.197 -by (auto split add: nat_diff_split)
   6.198 -
   6.199 -lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
   6.200 -by (auto split add: nat_diff_split)
   6.201 +lemma eq_diff_iff:
   6.202 +  fixes m n k :: nat
   6.203 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n"
   6.204 +  by (auto dest: le_Suc_ex)
   6.205 +
   6.206 +lemma less_diff_iff:
   6.207 +  fixes m n k :: nat
   6.208 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n"
   6.209 +  by (auto dest!: le_Suc_ex)
   6.210 +
   6.211 +lemma le_diff_iff:
   6.212 +  fixes m n k :: nat
   6.213 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
   6.214 +  by (auto dest!: le_Suc_ex)
   6.215  
   6.216  text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
   6.217  
   6.218 -(* Monotonicity of subtraction in first argument *)
   6.219 -lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
   6.220 -by (simp split add: nat_diff_split)
   6.221 -
   6.222 -lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
   6.223 -by (simp split add: nat_diff_split)
   6.224 -
   6.225 -lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
   6.226 -by (simp split add: nat_diff_split)
   6.227 -
   6.228 -lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
   6.229 -by (simp split add: nat_diff_split)
   6.230 -
   6.231 -lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
   6.232 -by auto
   6.233 +lemma diff_le_mono:
   6.234 +  fixes m n l :: nat
   6.235 +  shows "m \<le> n \<Longrightarrow> m - l \<le> n - l"
   6.236 +  by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
   6.237 +
   6.238 +lemma diff_le_mono2:
   6.239 +  fixes m n l :: nat
   6.240 +  shows "m \<le> n \<Longrightarrow> l - n \<le> l - m"
   6.241 +  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
   6.242 +
   6.243 +lemma diff_less_mono2:
   6.244 +  fixes m n l :: nat
   6.245 +  shows "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
   6.246 +  by (auto dest: less_imp_Suc_add split add: nat_diff_split)
   6.247 +
   6.248 +lemma diffs0_imp_equal:
   6.249 +  fixes m n :: nat
   6.250 +  shows "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
   6.251 +  by (simp split add: nat_diff_split)
   6.252 +
   6.253 +lemma min_diff:
   6.254 +  fixes m n i :: nat
   6.255 +  shows "min (m - i) (n - i) = min m n - i" (is "?lhs = ?rhs")
   6.256 +  by (cases m n rule: le_cases)
   6.257 +    (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
   6.258  
   6.259  lemma inj_on_diff_nat:
   6.260    assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
   6.261 @@ -1759,78 +1793,130 @@
   6.262    fix x y
   6.263    assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
   6.264    with k_le_n have "x - k + k = y - k + k" by auto
   6.265 -  with a k_le_n show "x = y" by auto
   6.266 +  with a k_le_n show "x = y" by (auto simp add: eq_diff_iff)
   6.267  qed
   6.268  
   6.269  text\<open>Rewriting to pull differences out\<close>
   6.270  
   6.271 -lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
   6.272 -by arith
   6.273 -
   6.274 -lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
   6.275 -by arith
   6.276 -
   6.277 -lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
   6.278 -by arith
   6.279 -
   6.280 -lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
   6.281 -by simp
   6.282 -
   6.283 -(*The others are
   6.284 -      i - j - k = i - (j + k),
   6.285 -      k \<le> j ==> j - k + i = j + i - k,
   6.286 -      k \<le> j ==> i + (j - k) = i + j - k *)
   6.287 -lemmas add_diff_assoc = diff_add_assoc [symmetric]
   6.288 -lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
   6.289 -declare add_diff_assoc [simp] add_diff_assoc2[simp]
   6.290 -
   6.291 -text\<open>At present we prove no analogue of \<open>not_less_Least\<close> or \<open>Least_Suc\<close>, since there appears to be no need.\<close>
   6.292 -
   6.293 -text\<open>Lemmas for ex/Factorization\<close>
   6.294 -
   6.295 -lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
   6.296 -by (cases m) auto
   6.297 -
   6.298 -lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
   6.299 -by (cases m) auto
   6.300 -
   6.301 -lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
   6.302 -by (cases m) auto
   6.303 +lemma diff_diff_right [simp]:
   6.304 +  fixes i j k :: nat
   6.305 +  shows "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j"
   6.306 +  by (fact diff_diff_right)
   6.307 +
   6.308 +lemma diff_Suc_diff_eq1 [simp]:
   6.309 +  assumes "k \<le> j"
   6.310 +  shows "i - Suc (j - k) = i + k - Suc j"
   6.311 +proof -
   6.312 +  from assms have *: "Suc (j - k) = Suc j - k"
   6.313 +    by (simp add: Suc_diff_le)
   6.314 +  from assms have "k \<le> Suc j"
   6.315 +    by (rule order_trans) simp
   6.316 +  with diff_diff_right [of k "Suc j" i] * show ?thesis
   6.317 +    by simp
   6.318 +qed
   6.319 +
   6.320 +lemma diff_Suc_diff_eq2 [simp]:
   6.321 +  assumes "k \<le> j"
   6.322 +  shows "Suc (j - k) - i = Suc j - (k + i)"
   6.323 +proof -
   6.324 +  from assms obtain n where "j = k + n"
   6.325 +    by (auto dest: le_Suc_ex)
   6.326 +  moreover have "Suc n - i = (k + Suc n) - (k + i)"
   6.327 +    using add_diff_cancel_left [of k "Suc n" i] by simp
   6.328 +  ultimately show ?thesis by simp
   6.329 +qed
   6.330 +
   6.331 +lemma Suc_diff_Suc:
   6.332 +  assumes "n < m"
   6.333 +  shows "Suc (m - Suc n) = m - n"
   6.334 +proof -
   6.335 +  from assms obtain q where "m = n + Suc q"
   6.336 +    by (auto dest: less_imp_Suc_add)
   6.337 +  moreover def r \<equiv> "Suc q"
   6.338 +  ultimately have "Suc (m - Suc n) = r" and "m = n + r"
   6.339 +    by simp_all
   6.340 +  then show ?thesis by simp
   6.341 +qed
   6.342 +
   6.343 +lemma one_less_mult:
   6.344 +  "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
   6.345 +  using less_1_mult [of n m] by (simp add: ac_simps)
   6.346 +
   6.347 +lemma n_less_m_mult_n:
   6.348 +  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
   6.349 +  using mult_strict_right_mono [of 1 m n] by simp
   6.350 +
   6.351 +lemma n_less_n_mult_m:
   6.352 +  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
   6.353 +  using mult_strict_left_mono [of 1 m n] by simp
   6.354  
   6.355  text \<open>Specialized induction principles that work "backwards":\<close>
   6.356  
   6.357 -lemma inc_induct[consumes 1, case_names base step]:
   6.358 +lemma inc_induct [consumes 1, case_names base step]:
   6.359    assumes less: "i \<le> j"
   6.360    assumes base: "P j"
   6.361    assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
   6.362    shows "P i"
   6.363    using less step
   6.364 -proof (induct d\<equiv>"j - i" arbitrary: i)
   6.365 +proof (induct "j - i" arbitrary: i)
   6.366    case (0 i)
   6.367 -  hence "i = j" by simp
   6.368 +  then have "i = j" by simp
   6.369    with base show ?case by simp
   6.370  next
   6.371    case (Suc d n)
   6.372 -  hence "n \<le> n" "n < j" "P (Suc n)"
   6.373 -    by simp_all
   6.374 -  then show "P n" by fact
   6.375 +  from Suc.hyps have "n \<noteq> j" by auto
   6.376 +  with Suc have "n < j" by (simp add: less_le)
   6.377 +  from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
   6.378 +  then have "d + 1 - 1 = j - n - 1" by simp
   6.379 +  then have "d = j - n - 1" by simp
   6.380 +  then have "d = j - (n + 1)" 
   6.381 +    by (simp add: diff_diff_eq)
   6.382 +  then have "d = j - Suc n"
   6.383 +    by simp
   6.384 +  moreover from \<open>n < j\<close> have "Suc n \<le> j"
   6.385 +    by (simp add: Suc_le_eq)
   6.386 +  ultimately have "P (Suc n)"
   6.387 +  thm Suc.hyps TrueI Suc.prems
   6.388 +  proof (rule Suc.hyps)
   6.389 +    fix q
   6.390 +    assume "Suc n \<le> q"
   6.391 +    then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le)
   6.392 +    moreover assume "q < j"
   6.393 +    moreover assume "P (Suc q)"
   6.394 +    ultimately show "P q"
   6.395 +      by (rule Suc.prems)
   6.396 +  qed
   6.397 +  with order_refl \<open>n < j\<close> show "P n"
   6.398 +    by (rule Suc.prems)
   6.399  qed
   6.400 -
   6.401 -lemma strict_inc_induct[consumes 1, case_names base step]:
   6.402 +    
   6.403 +lemma strict_inc_induct [consumes 1, case_names base step]:
   6.404    assumes less: "i < j"
   6.405 -  assumes base: "!!i. j = Suc i ==> P i"
   6.406 -  assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
   6.407 +  assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
   6.408 +  assumes step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
   6.409    shows "P i"
   6.410 -  using less
   6.411 -proof (induct d=="j - i - 1" arbitrary: i)
   6.412 +using less proof (induct "j - i - 1" arbitrary: i)
   6.413    case (0 i)
   6.414 -  with \<open>i < j\<close> have "j = Suc i" by simp
   6.415 +  from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0"
   6.416 +    by (auto dest!: less_imp_Suc_add)
   6.417 +  with 0 have "j = Suc i"
   6.418 +    by (auto intro: order_antisym simp add: Suc_le_eq)
   6.419    with base show ?case by simp
   6.420  next
   6.421    case (Suc d i)
   6.422 -  hence "i < j" "P (Suc i)"
   6.423 -    by simp_all
   6.424 -  thus "P i" by (rule step)
   6.425 +  from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i"
   6.426 +    by (simp add: diff_diff_add)
   6.427 +  then have "Suc d - 1 = j - Suc i - 1"
   6.428 +    by simp
   6.429 +  then have "d = j - Suc i - 1"
   6.430 +    by simp
   6.431 +  moreover from * have "j - Suc i \<noteq> 0"
   6.432 +    by auto
   6.433 +  then have "Suc i < j"
   6.434 +    by (simp add: not_le)
   6.435 +  ultimately have "P (Suc i)"
   6.436 +    by (rule Suc.hyps)
   6.437 +  with \<open>i < j\<close> show "P i" by (rule step)
   6.438  qed
   6.439  
   6.440  lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
   6.441 @@ -1841,9 +1927,35 @@
   6.442  
   6.443  text \<open>Further induction rule similar to @{thm inc_induct}\<close>
   6.444  
   6.445 -lemma dec_induct[consumes 1, case_names base step]:
   6.446 +lemma dec_induct [consumes 1, case_names base step]:
   6.447    "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
   6.448 -  by (induct j arbitrary: i) (auto simp: le_Suc_eq)
   6.449 +proof (induct j arbitrary: i)
   6.450 +  case 0 then show ?case by simp
   6.451 +next
   6.452 +  case (Suc j)
   6.453 +  from Suc.prems have "i \<le> j \<or> i = Suc j"
   6.454 +    by (simp add: le_Suc_eq)
   6.455 +  then show ?case proof
   6.456 +    assume "i \<le> j"
   6.457 +    moreover have "j < Suc j" by simp
   6.458 +    moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close>
   6.459 +    proof (rule Suc.hyps)
   6.460 +      fix q
   6.461 +      assume "i \<le> q"
   6.462 +      moreover assume "q < j" then have "q < Suc j"
   6.463 +        by (simp add: less_Suc_eq)
   6.464 +      moreover assume "P q"
   6.465 +      ultimately show "P (Suc q)"
   6.466 +        by (rule Suc.prems)
   6.467 +    qed
   6.468 +    ultimately show "P (Suc j)"
   6.469 +      by (rule Suc.prems)
   6.470 +  next
   6.471 +    assume "i = Suc j"
   6.472 +    with \<open>P i\<close> show "P (Suc j)" by simp
   6.473 +  qed
   6.474 +qed
   6.475 +
   6.476  
   6.477  subsection \<open> Monotonicity of funpow \<close>
   6.478  
   6.479 @@ -1912,7 +2024,7 @@
   6.480  proof -
   6.481    from assms(1) obtain q where "k * n = (k * m) * q" ..
   6.482    then have "k * n = k * (m * q)" by (simp add: ac_simps)
   6.483 -  with \<open>0 < k\<close> have "n = m * q" by simp
   6.484 +  with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel)
   6.485    then show ?thesis ..
   6.486  qed
   6.487    
   6.488 @@ -1949,7 +2061,7 @@
   6.489  lemma dvd_minus_self:
   6.490    fixes m n :: nat
   6.491    shows "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
   6.492 -  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add)
   6.493 +  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
   6.494  
   6.495  lemma dvd_minus_add:
   6.496    fixes m n q r :: nat
     7.1 --- a/src/HOL/Num.thy	Tue Mar 01 10:32:55 2016 +0100
     7.2 +++ b/src/HOL/Num.thy	Tue Mar 01 10:36:19 2016 +0100
     7.3 @@ -761,7 +761,7 @@
     7.4    Equality and negation: class \<open>ring_char_0\<close>
     7.5  \<close>
     7.6  
     7.7 -class ring_char_0 = ring_1 + semiring_char_0
     7.8 +context ring_char_0
     7.9  begin
    7.10  
    7.11  lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
    7.12 @@ -833,10 +833,6 @@
    7.13  
    7.14  end
    7.15  
    7.16 -text\<open>Also the class for fields with characteristic zero.\<close>
    7.17 -
    7.18 -class field_char_0 = field + ring_char_0
    7.19 -
    7.20  
    7.21  subsubsection \<open>
    7.22    Structures with negation and order: class \<open>linordered_idom\<close>
     8.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 01 10:32:55 2016 +0100
     8.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Mar 01 10:36:19 2016 +0100
     8.3 @@ -96,11 +96,11 @@
     8.4    shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
     8.5    by (rule iffI, rule prime_dvd_mult_int, auto)
     8.6  
     8.7 -lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
     8.8 -    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
     8.9 -  unfolding prime_def dvd_def apply auto
    8.10 -  by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
    8.11 -      n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
    8.12 +lemma not_prime_eq_prod_nat:
    8.13 +  "1 < n \<Longrightarrow> \<not> prime n \<Longrightarrow>
    8.14 +    \<exists>m k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
    8.15 +  unfolding prime_def dvd_def apply (auto simp add: ac_simps)
    8.16 +  by (metis Suc_lessD Suc_lessI n_less_m_mult_n n_less_n_mult_m nat_0_less_mult_iff)
    8.17  
    8.18  lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
    8.19    by (induct n) auto
     9.1 --- a/src/HOL/Old_Number_Theory/Factorization.thy	Tue Mar 01 10:32:55 2016 +0100
     9.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy	Tue Mar 01 10:36:19 2016 +0100
     9.3 @@ -220,10 +220,12 @@
     9.4    done
     9.5  
     9.6  lemma not_prime_ex_mk:
     9.7 -  "Suc 0 < n \<and> \<not> prime n ==>
     9.8 +  "Suc 0 < n \<and> \<not> prime n \<Longrightarrow>
     9.9      \<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
    9.10    apply (unfold prime_def dvd_def)
    9.11    apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
    9.12 +  using n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k
    9.13 +  apply (metis Suc_lessD Suc_lessI mult.commute)
    9.14    done
    9.15  
    9.16  lemma split_primel:
    10.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Tue Mar 01 10:32:55 2016 +0100
    10.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Tue Mar 01 10:36:19 2016 +0100
    10.3 @@ -575,7 +575,7 @@
    10.4  lemma nproduct_cmul:
    10.5    assumes fS:"finite S"
    10.6    shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
    10.7 -unfolding setprod.distrib setprod_constant[OF fS, of c] ..
    10.8 +unfolding setprod.distrib setprod_constant [of c] ..
    10.9  
   10.10  lemma coprime_nproduct:
   10.11    assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)"
    11.1 --- a/src/HOL/Power.thy	Tue Mar 01 10:32:55 2016 +0100
    11.2 +++ b/src/HOL/Power.thy	Tue Mar 01 10:36:19 2016 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  section \<open>Exponentiation\<close>
    11.5  
    11.6  theory Power
    11.7 -imports Num Equiv_Relations
    11.8 +imports Num
    11.9  begin
   11.10  
   11.11  subsection \<open>Powers for Arbitrary Monoids\<close>
   11.12 @@ -232,7 +232,7 @@
   11.13  
   11.14  end
   11.15  
   11.16 -class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
   11.17 +context semiring_1_no_zero_divisors
   11.18  begin
   11.19  
   11.20  subclass power .
   11.21 @@ -251,13 +251,6 @@
   11.22  
   11.23  end
   11.24  
   11.25 -context semidom
   11.26 -begin
   11.27 -
   11.28 -subclass semiring_1_no_zero_divisors ..
   11.29 -
   11.30 -end
   11.31 -
   11.32  context ring_1
   11.33  begin
   11.34  
   11.35 @@ -307,8 +300,6 @@
   11.36  context ring_1_no_zero_divisors
   11.37  begin
   11.38  
   11.39 -subclass semiring_1_no_zero_divisors ..
   11.40 -
   11.41  lemma power2_eq_1_iff:
   11.42    "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   11.43    using square_eq_1_iff [of a] by (simp add: power2_eq_square)
   11.44 @@ -851,70 +842,6 @@
   11.45  qed
   11.46  
   11.47  
   11.48 -subsubsection \<open>Generalized sum over a set\<close>
   11.49 -
   11.50 -lemma setsum_zero_power [simp]:
   11.51 -  fixes c :: "nat \<Rightarrow> 'a::division_ring"
   11.52 -  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
   11.53 -apply (cases "finite A")
   11.54 -  by (induction A rule: finite_induct) auto
   11.55 -
   11.56 -lemma setsum_zero_power' [simp]:
   11.57 -  fixes c :: "nat \<Rightarrow> 'a::field"
   11.58 -  shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
   11.59 -  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
   11.60 -  by auto
   11.61 -
   11.62 -
   11.63 -subsubsection \<open>Generalized product over a set\<close>
   11.64 -
   11.65 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
   11.66 -apply (erule finite_induct)
   11.67 -apply auto
   11.68 -done
   11.69 -
   11.70 -lemma setprod_power_distrib:
   11.71 -  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
   11.72 -  shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
   11.73 -proof (cases "finite A")
   11.74 -  case True then show ?thesis
   11.75 -    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
   11.76 -next
   11.77 -  case False then show ?thesis
   11.78 -    by simp
   11.79 -qed
   11.80 -
   11.81 -lemma power_setsum:
   11.82 -  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
   11.83 -  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
   11.84 -
   11.85 -lemma setprod_gen_delta:
   11.86 -  assumes fS: "finite S"
   11.87 -  shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
   11.88 -proof-
   11.89 -  let ?f = "(\<lambda>k. if k=a then b k else c)"
   11.90 -  {assume a: "a \<notin> S"
   11.91 -    hence "\<forall> k\<in> S. ?f k = c" by simp
   11.92 -    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
   11.93 -  moreover
   11.94 -  {assume a: "a \<in> S"
   11.95 -    let ?A = "S - {a}"
   11.96 -    let ?B = "{a}"
   11.97 -    have eq: "S = ?A \<union> ?B" using a by blast
   11.98 -    have dj: "?A \<inter> ?B = {}" by simp
   11.99 -    from fS have fAB: "finite ?A" "finite ?B" by auto
  11.100 -    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  11.101 -      apply (rule setprod.cong) by auto
  11.102 -    have cA: "card ?A = card S - 1" using fS a by auto
  11.103 -    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  11.104 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  11.105 -      using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  11.106 -      by simp
  11.107 -    then have ?thesis using a cA
  11.108 -      by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)}
  11.109 -  ultimately show ?thesis by blast
  11.110 -qed
  11.111 -
  11.112  subsection \<open>Code generator tweak\<close>
  11.113  
  11.114  code_identifier
    12.1 --- a/src/HOL/Rings.thy	Tue Mar 01 10:32:55 2016 +0100
    12.2 +++ b/src/HOL/Rings.thy	Tue Mar 01 10:36:19 2016 +0100
    12.3 @@ -441,6 +441,8 @@
    12.4  
    12.5  end
    12.6  
    12.7 +class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
    12.8 +
    12.9  class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
   12.10    assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   12.11      and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   12.12 @@ -479,6 +481,8 @@
   12.13  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
   12.14  begin
   12.15  
   12.16 +subclass semiring_1_no_zero_divisors ..
   12.17 +
   12.18  lemma square_eq_1_iff:
   12.19    "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
   12.20  proof -
   12.21 @@ -509,6 +513,11 @@
   12.22  end
   12.23  
   12.24  class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
   12.25 +begin
   12.26 +
   12.27 +subclass semiring_1_no_zero_divisors ..
   12.28 +
   12.29 +end
   12.30  
   12.31  class idom = comm_ring_1 + semiring_no_zero_divisors
   12.32  begin