# HG changeset patch
# User haftmann
# Date 1456824979 -3600
# Node ID b5d8e57826dfb19c22693998a37cde92fcf1229f
# Parent  f2e8984adef7a8ac9a0dfa96cfd6d828a6770b06
tuned bootstrap order to provide type classes in a more sensible order

diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Binomial.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -697,9 +697,8 @@
   then show ?thesis by simp
 next
   case False
-  from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
-  have eq: "(- (1::'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
-    by auto
+  then have eq: "(- 1) ^ n = (\<Prod>i = 0..n - 1. - 1)"
+    by (auto simp add: setprod_constant)
   from False show ?thesis
     by (simp add: pochhammer_def gbinomial_def field_simps
       eq setprod.distrib[symmetric])
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Fields.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -10,7 +10,7 @@
 section \<open>Fields\<close>
 
 theory Fields
-imports Rings
+imports Nat
 begin
 
 subsection \<open>Division rings\<close>
@@ -29,6 +29,24 @@
 
 end
 
+text \<open>Setup for linear arithmetic prover\<close>
+
+ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
+ML_file "Tools/lin_arith.ML"
+setup \<open>Lin_Arith.global_setup\<close>
+declaration \<open>K Lin_Arith.setup\<close>
+
+simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
+  \<open>K Lin_Arith.simproc\<close>
+(* Because of this simproc, the arithmetic solver is really only
+useful to detect inconsistencies among the premises for subgoals which are
+*not* themselves (in)equalities, because the latter activate
+fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
+solver all the time rather than add the additional check. *)
+
+lemmas [arith_split] = nat_diff_split split_min split_max
+
+
 text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
 
 named_theorems divide_simps "rewrite rules to eliminate divisions"
@@ -490,6 +508,8 @@
 
 end
 
+class field_char_0 = field + ring_char_0
+
 
 subsection \<open>Ordered fields\<close>
 
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -6,7 +6,7 @@
 section \<open>Finite sets\<close>
 
 theory Finite_Set
-imports Product_Type Sum_Type Nat
+imports Product_Type Sum_Type Fields
 begin
 
 subsection \<open>Predicate for finite sets\<close>
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Groups_Big.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -6,7 +6,7 @@
 section \<open>Big sum and product over finite (non-empty) sets\<close>
 
 theory Groups_Big
-imports Finite_Set
+imports Finite_Set Power
 begin
 
 subsection \<open>Generic monoid operation over a set\<close>
@@ -1145,6 +1145,18 @@
   qed
 qed
 
+lemma setsum_zero_power [simp]:
+  fixes c :: "nat \<Rightarrow> 'a::division_ring"
+  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
+apply (cases "finite A")
+  by (induction A rule: finite_induct) auto
+
+lemma setsum_zero_power' [simp]:
+  fixes c :: "nat \<Rightarrow> 'a::field"
+  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)"
+  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
+  by auto
+
 lemma (in field) setprod_inversef:
   "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
   by (induct A rule: finite_induct) simp_all
@@ -1197,4 +1209,51 @@
   "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
   using setprod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
 
+lemma setprod_constant:
+  "(\<Prod>x\<in> A. (y::'a::comm_monoid_mult)) = y ^ card A"
+  by (induct A rule: infinite_finite_induct) simp_all
+
+lemma setprod_power_distrib:
+  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
+  shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
+proof (cases "finite A")
+  case True then show ?thesis
+    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
+next
+  case False then show ?thesis
+    by simp
+qed
+
+lemma power_setsum:
+  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
+  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
+
+lemma setprod_gen_delta:
+  assumes fS: "finite S"
+  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)"
+proof-
+  let ?f = "(\<lambda>k. if k=a then b k else c)"
+  {assume a: "a \<notin> S"
+    hence "\<forall> k\<in> S. ?f k = c" by simp
+    hence ?thesis using a setprod_constant by simp }
+  moreover
+  {assume a: "a \<in> S"
+    let ?A = "S - {a}"
+    let ?B = "{a}"
+    have eq: "S = ?A \<union> ?B" using a by blast
+    have dj: "?A \<inter> ?B = {}" by simp
+    from fS have fAB: "finite ?A" "finite ?B" by auto
+    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
+      by (rule setprod.cong) auto
+    have cA: "card ?A = card S - 1" using fS a by auto
+    have fA1: "setprod ?f ?A = c ^ card ?A"
+      unfolding fA0 by (rule setprod_constant)
+    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
+      using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
+      by simp
+    then have ?thesis using a cA
+      by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)}
+  ultimately show ?thesis by blast
+qed
+
 end
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -2305,7 +2305,7 @@
   have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
     by (simp add: Suc fps_power_nth del: replicate.simps power_Suc)
   also have "\<dots> = (a$0) ^ m"
-   unfolding c by (rule setprod_constant) simp
+   unfolding c by (rule setprod_constant)
  finally show ?thesis .
 qed
 
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Nat.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -8,14 +8,13 @@
 section \<open>Natural numbers\<close>
 
 theory Nat
-imports Inductive Typedef Fun Fields
+imports Inductive Typedef Fun Rings
 begin
 
 ML_file "~~/src/Tools/rat.ML"
 
 named_theorems arith "arith facts -- only ground formulas"
 ML_file "Tools/arith_data.ML"
-ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
 
 
 subsection \<open>Type \<open>ind\<close>\<close>
@@ -724,11 +723,16 @@
   by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
 
 text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
-lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
-apply(auto simp: gr0_conv_Suc)
-apply (induct_tac m)
-apply (simp_all add: add_less_mono)
-done
+lemma mult_less_mono2:
+  fixes i j :: nat
+  assumes "i < j" and "0 < k"
+  shows "k * i < k * j"
+using \<open>0 < k\<close> proof (induct k)
+  case 0 then show ?case by simp
+next
+  case (Suc k) with \<open>i < j\<close> show ?case
+    by (cases k) (simp_all add: add_less_mono)
+qed
 
 text \<open>Addition is the inverse of subtraction:
   if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
@@ -1103,8 +1107,18 @@
 lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
 by (induct j k rule: diff_induct) simp_all
 
+lemma add_diff_assoc [simp]:
+  fixes i j k :: nat
+  shows "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
+  by (fact diff_add_assoc [symmetric])
+
 lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
-by (simp add: add.commute diff_add_assoc)
+  by (simp add: ac_simps)
+
+lemma add_diff_assoc2 [simp]:
+  fixes i j k :: nat
+  shows "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
+  by (fact diff_add_assoc2 [symmetric])
 
 lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
 by auto
@@ -1457,6 +1471,14 @@
 
 declare of_nat_code [code]
 
+context ring_1
+begin
+
+lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
+by (simp add: algebra_simps of_nat_add [symmetric])
+
+end
+
 text\<open>Class for unital semirings with characteristic zero.
  Includes non-ordered rings like the complex numbers.\<close>
 
@@ -1485,6 +1507,8 @@
 
 end
 
+class ring_char_0 = ring_1 + semiring_char_0
+
 context linordered_semidom
 begin
 
@@ -1521,14 +1545,6 @@
 
 end
 
-context ring_1
-begin
-
-lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
-by (simp add: algebra_simps of_nat_add [symmetric])
-
-end
-
 context linordered_idom
 begin
 
@@ -1621,21 +1637,6 @@
   ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
   \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
 
-ML_file "Tools/lin_arith.ML"
-setup \<open>Lin_Arith.global_setup\<close>
-declaration \<open>K Lin_Arith.setup\<close>
-
-simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
-  \<open>K Lin_Arith.simproc\<close>
-(* Because of this simproc, the arithmetic solver is really only
-useful to detect inconsistencies among the premises for subgoals which are
-*not* themselves (in)equalities, because the latter activate
-fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
-solver all the time rather than add the additional check. *)
-
-
-lemmas [arith_split] = nat_diff_split split_min split_max
-
 context order
 begin
 
@@ -1695,62 +1696,95 @@
 
 text\<open>Subtraction laws, mostly by Clemens Ballarin\<close>
 
-lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
-by arith
-
-lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
-by arith
+lemma diff_less_mono:
+  fixes a b c :: nat
+  assumes "a < b" and "c \<le> a"
+  shows "a - c < b - c"
+proof -
+  from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0"
+    by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps)
+  then show ?thesis by simp
+qed
+
+lemma less_diff_conv:
+  fixes i j k :: nat
+  shows "i < j - k \<longleftrightarrow> i + k < j" (is "?P \<longleftrightarrow> ?Q")
+  by (cases "k \<le> j")
+    (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
 
 lemma less_diff_conv2:
   fixes j k i :: nat
   assumes "k \<le> j"
-  shows "j - k < i \<longleftrightarrow> j < i + k"
-  using assms by arith
-
-lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
-by arith
-
-lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
-by arith
-
-(*Replaces the previous diff_less and le_diff_less, which had the stronger
-  second premise n\<le>m*)
-lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
-by arith
+  shows "j - k < i \<longleftrightarrow> j < i + k" (is "?P \<longleftrightarrow> ?Q")
+  using assms by (auto dest: le_Suc_ex)
+
+lemma le_diff_conv:
+  fixes j k i :: nat
+  shows "j - k \<le> i \<longleftrightarrow> j \<le> i + k"
+  by (cases "k \<le> j")
+    (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
+
+lemma diff_diff_cancel [simp]:
+  fixes i n :: nat
+  shows "i \<le> n \<Longrightarrow> n - (n - i) = i"
+  by (auto dest: le_Suc_ex)
+
+lemma diff_less [simp]:
+  fixes i n :: nat
+  shows "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m"
+  by (auto dest: less_imp_Suc_add)
 
 text \<open>Simplification of relational expressions involving subtraction\<close>
 
-lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
-by (simp split add: nat_diff_split)
+lemma diff_diff_eq:
+  fixes m n k :: nat
+  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n"
+  by (auto dest!: le_Suc_ex)
 
 hide_fact (open) diff_diff_eq
 
-lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
-by (auto split add: nat_diff_split)
-
-lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
-by (auto split add: nat_diff_split)
-
-lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
-by (auto split add: nat_diff_split)
+lemma eq_diff_iff:
+  fixes m n k :: nat
+  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n"
+  by (auto dest: le_Suc_ex)
+
+lemma less_diff_iff:
+  fixes m n k :: nat
+  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n"
+  by (auto dest!: le_Suc_ex)
+
+lemma le_diff_iff:
+  fixes m n k :: nat
+  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
+  by (auto dest!: le_Suc_ex)
 
 text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
 
-(* Monotonicity of subtraction in first argument *)
-lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
-by (simp split add: nat_diff_split)
-
-lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
-by (simp split add: nat_diff_split)
-
-lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
-by (simp split add: nat_diff_split)
-
-lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
-by (simp split add: nat_diff_split)
-
-lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
-by auto
+lemma diff_le_mono:
+  fixes m n l :: nat
+  shows "m \<le> n \<Longrightarrow> m - l \<le> n - l"
+  by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
+
+lemma diff_le_mono2:
+  fixes m n l :: nat
+  shows "m \<le> n \<Longrightarrow> l - n \<le> l - m"
+  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
+
+lemma diff_less_mono2:
+  fixes m n l :: nat
+  shows "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
+  by (auto dest: less_imp_Suc_add split add: nat_diff_split)
+
+lemma diffs0_imp_equal:
+  fixes m n :: nat
+  shows "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
+  by (simp split add: nat_diff_split)
+
+lemma min_diff:
+  fixes m n i :: nat
+  shows "min (m - i) (n - i) = min m n - i" (is "?lhs = ?rhs")
+  by (cases m n rule: le_cases)
+    (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
 
 lemma inj_on_diff_nat:
   assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
@@ -1759,78 +1793,130 @@
   fix x y
   assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
   with k_le_n have "x - k + k = y - k + k" by auto
-  with a k_le_n show "x = y" by auto
+  with a k_le_n show "x = y" by (auto simp add: eq_diff_iff)
 qed
 
 text\<open>Rewriting to pull differences out\<close>
 
-lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
-by arith
-
-lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
-by arith
-
-lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
-by arith
-
-lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
-by simp
-
-(*The others are
-      i - j - k = i - (j + k),
-      k \<le> j ==> j - k + i = j + i - k,
-      k \<le> j ==> i + (j - k) = i + j - k *)
-lemmas add_diff_assoc = diff_add_assoc [symmetric]
-lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
-declare add_diff_assoc [simp] add_diff_assoc2[simp]
-
-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>
-
-text\<open>Lemmas for ex/Factorization\<close>
-
-lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
-by (cases m) auto
-
-lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
-by (cases m) auto
-
-lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
-by (cases m) auto
+lemma diff_diff_right [simp]:
+  fixes i j k :: nat
+  shows "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j"
+  by (fact diff_diff_right)
+
+lemma diff_Suc_diff_eq1 [simp]:
+  assumes "k \<le> j"
+  shows "i - Suc (j - k) = i + k - Suc j"
+proof -
+  from assms have *: "Suc (j - k) = Suc j - k"
+    by (simp add: Suc_diff_le)
+  from assms have "k \<le> Suc j"
+    by (rule order_trans) simp
+  with diff_diff_right [of k "Suc j" i] * show ?thesis
+    by simp
+qed
+
+lemma diff_Suc_diff_eq2 [simp]:
+  assumes "k \<le> j"
+  shows "Suc (j - k) - i = Suc j - (k + i)"
+proof -
+  from assms obtain n where "j = k + n"
+    by (auto dest: le_Suc_ex)
+  moreover have "Suc n - i = (k + Suc n) - (k + i)"
+    using add_diff_cancel_left [of k "Suc n" i] by simp
+  ultimately show ?thesis by simp
+qed
+
+lemma Suc_diff_Suc:
+  assumes "n < m"
+  shows "Suc (m - Suc n) = m - n"
+proof -
+  from assms obtain q where "m = n + Suc q"
+    by (auto dest: less_imp_Suc_add)
+  moreover def r \<equiv> "Suc q"
+  ultimately have "Suc (m - Suc n) = r" and "m = n + r"
+    by simp_all
+  then show ?thesis by simp
+qed
+
+lemma one_less_mult:
+  "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
+  using less_1_mult [of n m] by (simp add: ac_simps)
+
+lemma n_less_m_mult_n:
+  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
+  using mult_strict_right_mono [of 1 m n] by simp
+
+lemma n_less_n_mult_m:
+  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
+  using mult_strict_left_mono [of 1 m n] by simp
 
 text \<open>Specialized induction principles that work "backwards":\<close>
 
-lemma inc_induct[consumes 1, case_names base step]:
+lemma inc_induct [consumes 1, case_names base step]:
   assumes less: "i \<le> j"
   assumes base: "P j"
   assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
   shows "P i"
   using less step
-proof (induct d\<equiv>"j - i" arbitrary: i)
+proof (induct "j - i" arbitrary: i)
   case (0 i)
-  hence "i = j" by simp
+  then have "i = j" by simp
   with base show ?case by simp
 next
   case (Suc d n)
-  hence "n \<le> n" "n < j" "P (Suc n)"
-    by simp_all
-  then show "P n" by fact
+  from Suc.hyps have "n \<noteq> j" by auto
+  with Suc have "n < j" by (simp add: less_le)
+  from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
+  then have "d + 1 - 1 = j - n - 1" by simp
+  then have "d = j - n - 1" by simp
+  then have "d = j - (n + 1)" 
+    by (simp add: diff_diff_eq)
+  then have "d = j - Suc n"
+    by simp
+  moreover from \<open>n < j\<close> have "Suc n \<le> j"
+    by (simp add: Suc_le_eq)
+  ultimately have "P (Suc n)"
+  thm Suc.hyps TrueI Suc.prems
+  proof (rule Suc.hyps)
+    fix q
+    assume "Suc n \<le> q"
+    then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le)
+    moreover assume "q < j"
+    moreover assume "P (Suc q)"
+    ultimately show "P q"
+      by (rule Suc.prems)
+  qed
+  with order_refl \<open>n < j\<close> show "P n"
+    by (rule Suc.prems)
 qed
-
-lemma strict_inc_induct[consumes 1, case_names base step]:
+    
+lemma strict_inc_induct [consumes 1, case_names base step]:
   assumes less: "i < j"
-  assumes base: "!!i. j = Suc i ==> P i"
-  assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
+  assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
+  assumes step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
   shows "P i"
-  using less
-proof (induct d=="j - i - 1" arbitrary: i)
+using less proof (induct "j - i - 1" arbitrary: i)
   case (0 i)
-  with \<open>i < j\<close> have "j = Suc i" by simp
+  from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0"
+    by (auto dest!: less_imp_Suc_add)
+  with 0 have "j = Suc i"
+    by (auto intro: order_antisym simp add: Suc_le_eq)
   with base show ?case by simp
 next
   case (Suc d i)
-  hence "i < j" "P (Suc i)"
-    by simp_all
-  thus "P i" by (rule step)
+  from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i"
+    by (simp add: diff_diff_add)
+  then have "Suc d - 1 = j - Suc i - 1"
+    by simp
+  then have "d = j - Suc i - 1"
+    by simp
+  moreover from * have "j - Suc i \<noteq> 0"
+    by auto
+  then have "Suc i < j"
+    by (simp add: not_le)
+  ultimately have "P (Suc i)"
+    by (rule Suc.hyps)
+  with \<open>i < j\<close> show "P i" by (rule step)
 qed
 
 lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
@@ -1841,9 +1927,35 @@
 
 text \<open>Further induction rule similar to @{thm inc_induct}\<close>
 
-lemma dec_induct[consumes 1, case_names base step]:
+lemma dec_induct [consumes 1, case_names base step]:
   "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"
-  by (induct j arbitrary: i) (auto simp: le_Suc_eq)
+proof (induct j arbitrary: i)
+  case 0 then show ?case by simp
+next
+  case (Suc j)
+  from Suc.prems have "i \<le> j \<or> i = Suc j"
+    by (simp add: le_Suc_eq)
+  then show ?case proof
+    assume "i \<le> j"
+    moreover have "j < Suc j" by simp
+    moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close>
+    proof (rule Suc.hyps)
+      fix q
+      assume "i \<le> q"
+      moreover assume "q < j" then have "q < Suc j"
+        by (simp add: less_Suc_eq)
+      moreover assume "P q"
+      ultimately show "P (Suc q)"
+        by (rule Suc.prems)
+    qed
+    ultimately show "P (Suc j)"
+      by (rule Suc.prems)
+  next
+    assume "i = Suc j"
+    with \<open>P i\<close> show "P (Suc j)" by simp
+  qed
+qed
+
 
 subsection \<open> Monotonicity of funpow \<close>
 
@@ -1912,7 +2024,7 @@
 proof -
   from assms(1) obtain q where "k * n = (k * m) * q" ..
   then have "k * n = k * (m * q)" by (simp add: ac_simps)
-  with \<open>0 < k\<close> have "n = m * q" by simp
+  with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel)
   then show ?thesis ..
 qed
   
@@ -1949,7 +2061,7 @@
 lemma dvd_minus_self:
   fixes m n :: nat
   shows "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
-  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add)
+  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
 
 lemma dvd_minus_add:
   fixes m n q r :: nat
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Num.thy
--- a/src/HOL/Num.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Num.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -761,7 +761,7 @@
   Equality and negation: class \<open>ring_char_0\<close>
 \<close>
 
-class ring_char_0 = ring_1 + semiring_char_0
+context ring_char_0
 begin
 
 lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
@@ -833,10 +833,6 @@
 
 end
 
-text\<open>Also the class for fields with characteristic zero.\<close>
-
-class field_char_0 = field + ring_char_0
-
 
 subsubsection \<open>
   Structures with negation and order: class \<open>linordered_idom\<close>
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -96,11 +96,11 @@
   shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
   by (rule iffI, rule prime_dvd_mult_int, auto)
 
-lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
-    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
-  unfolding prime_def dvd_def apply auto
-  by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
-      n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
+lemma not_prime_eq_prod_nat:
+  "1 < n \<Longrightarrow> \<not> prime n \<Longrightarrow>
+    \<exists>m k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
+  unfolding prime_def dvd_def apply (auto simp add: ac_simps)
+  by (metis Suc_lessD Suc_lessI n_less_m_mult_n n_less_n_mult_m nat_0_less_mult_iff)
 
 lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   by (induct n) auto
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Old_Number_Theory/Factorization.thy
--- a/src/HOL/Old_Number_Theory/Factorization.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Old_Number_Theory/Factorization.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -220,10 +220,12 @@
   done
 
 lemma not_prime_ex_mk:
-  "Suc 0 < n \<and> \<not> prime n ==>
+  "Suc 0 < n \<and> \<not> prime n \<Longrightarrow>
     \<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
   apply (unfold prime_def dvd_def)
   apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
+  using n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k
+  apply (metis Suc_lessD Suc_lessI mult.commute)
   done
 
 lemma split_primel:
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -575,7 +575,7 @@
 lemma nproduct_cmul:
   assumes fS:"finite S"
   shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
-unfolding setprod.distrib setprod_constant[OF fS, of c] ..
+unfolding setprod.distrib setprod_constant [of c] ..
 
 lemma coprime_nproduct:
   assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)"
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Power.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -6,7 +6,7 @@
 section \<open>Exponentiation\<close>
 
 theory Power
-imports Num Equiv_Relations
+imports Num
 begin
 
 subsection \<open>Powers for Arbitrary Monoids\<close>
@@ -232,7 +232,7 @@
 
 end
 
-class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
+context semiring_1_no_zero_divisors
 begin
 
 subclass power .
@@ -251,13 +251,6 @@
 
 end
 
-context semidom
-begin
-
-subclass semiring_1_no_zero_divisors ..
-
-end
-
 context ring_1
 begin
 
@@ -307,8 +300,6 @@
 context ring_1_no_zero_divisors
 begin
 
-subclass semiring_1_no_zero_divisors ..
-
 lemma power2_eq_1_iff:
   "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   using square_eq_1_iff [of a] by (simp add: power2_eq_square)
@@ -851,70 +842,6 @@
 qed
 
 
-subsubsection \<open>Generalized sum over a set\<close>
-
-lemma setsum_zero_power [simp]:
-  fixes c :: "nat \<Rightarrow> 'a::division_ring"
-  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
-apply (cases "finite A")
-  by (induction A rule: finite_induct) auto
-
-lemma setsum_zero_power' [simp]:
-  fixes c :: "nat \<Rightarrow> 'a::field"
-  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)"
-  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
-  by auto
-
-
-subsubsection \<open>Generalized product over a set\<close>
-
-lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
-apply (erule finite_induct)
-apply auto
-done
-
-lemma setprod_power_distrib:
-  fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
-  shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
-proof (cases "finite A")
-  case True then show ?thesis
-    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
-next
-  case False then show ?thesis
-    by simp
-qed
-
-lemma power_setsum:
-  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
-  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
-
-lemma setprod_gen_delta:
-  assumes fS: "finite S"
-  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)"
-proof-
-  let ?f = "(\<lambda>k. if k=a then b k else c)"
-  {assume a: "a \<notin> S"
-    hence "\<forall> k\<in> S. ?f k = c" by simp
-    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
-  moreover
-  {assume a: "a \<in> S"
-    let ?A = "S - {a}"
-    let ?B = "{a}"
-    have eq: "S = ?A \<union> ?B" using a by blast
-    have dj: "?A \<inter> ?B = {}" by simp
-    from fS have fAB: "finite ?A" "finite ?B" by auto
-    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
-      apply (rule setprod.cong) by auto
-    have cA: "card ?A = card S - 1" using fS a by auto
-    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
-    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
-      using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
-      by simp
-    then have ?thesis using a cA
-      by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)}
-  ultimately show ?thesis by blast
-qed
-
 subsection \<open>Code generator tweak\<close>
 
 code_identifier
diff -r f2e8984adef7 -r b5d8e57826df src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/HOL/Rings.thy	Tue Mar 01 10:36:19 2016 +0100
@@ -441,6 +441,8 @@
 
 end
 
+class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
+
 class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
   assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
     and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
@@ -479,6 +481,8 @@
 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 begin
 
+subclass semiring_1_no_zero_divisors ..
+
 lemma square_eq_1_iff:
   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
 proof -
@@ -509,6 +513,11 @@
 end
 
 class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
+begin
+
+subclass semiring_1_no_zero_divisors ..
+
+end
 
 class idom = comm_ring_1 + semiring_no_zero_divisors
 begin