diff -r a2bd14226f9a -r de65ce2bfb32 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Thu Nov 09 11:58:47 2006 +0100
+++ b/src/HOL/Library/Binomial.thy	Thu Nov 09 11:58:49 2006 +0100
@@ -4,87 +4,82 @@
     Copyright   1997  University of Cambridge
 *)
 
-header{*Binomial Coefficients*}
+header {* Binomial Coefficients *}
 
 theory Binomial
 imports Main
 begin
 
-text{*This development is based on the work of Andy Gordon and
-Florian Kammueller*}
+text {* This development is based on the work of Andy Gordon and
+  Florian Kammueller. *}
 
 consts
   binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"      (infixl "choose" 65)
-
 primrec
-  binomial_0:   "(0     choose k) = (if k = 0 then 1 else 0)"
-
+  binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)"
   binomial_Suc: "(Suc n choose k) =
                  (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
 
 lemma binomial_n_0 [simp]: "(n choose 0) = 1"
-by (cases n) simp_all
+  by (cases n) simp_all
 
 lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
-by simp
+  by simp
 
 lemma binomial_Suc_Suc [simp]:
-     "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
-by simp
+    "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
+  by simp
 
-lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
-apply (induct "n")
-apply auto
-done
+lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0"
+  by (induct n) auto
 
 declare binomial_0 [simp del] binomial_Suc [simp del]
 
 lemma binomial_n_n [simp]: "(n choose n) = 1"
-apply (induct "n")
-apply (simp_all add: binomial_eq_0)
-done
+  by (induct n) (simp_all add: binomial_eq_0)
 
 lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
-by (induct "n", simp_all)
+  by (induct n) simp_all
 
 lemma binomial_1 [simp]: "(n choose Suc 0) = n"
-by (induct "n", simp_all)
+  by (induct n) simp_all
 
-lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
-by (rule_tac m = n and n = k in diff_induct, simp_all)
+lemma zero_less_binomial: "k \<le> n ==> 0 < (n choose k)"
+  by (induct n k rule: diff_induct) simp_all
 
 lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
-apply (safe intro!: binomial_eq_0)
-apply (erule contrapos_pp)
-apply (simp add: zero_less_binomial)
-done
+  apply (safe intro!: binomial_eq_0)
+  apply (erule contrapos_pp)
+  apply (simp add: zero_less_binomial)
+  done
 
 lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
-by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
+  by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
 
 (*Might be more useful if re-oriented*)
-lemma Suc_times_binomial_eq [rule_format]:
-     "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
-apply (induct "n")
-apply (simp add: binomial_0, clarify)
-apply (case_tac "k")
-apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
-                      binomial_eq_0)
-done
+lemma Suc_times_binomial_eq:
+    "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
+  apply (induct n)
+  apply (simp add: binomial_0)
+  apply (case_tac k)
+  apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
+    binomial_eq_0)
+  done
 
 text{*This is the well-known version, but it's harder to use because of the
   need to reason about division.*}
 lemma binomial_Suc_Suc_eq_times:
-     "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
-by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
-        del: mult_Suc mult_Suc_right)
+    "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
+  by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
+    del: mult_Suc mult_Suc_right)
 
 text{*Another version, with -1 instead of Suc.*}
 lemma times_binomial_minus1_eq:
-     "[|k \<le> n;  0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"
-apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq)
-apply (simp split add: nat_diff_split, auto)
-done
+    "[|k \<le> n;  0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"
+  apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq)
+  apply (simp split add: nat_diff_split, auto)
+  done
+
 
 subsubsection {* Theorems about @{text "choose"} *}
 
@@ -132,7 +127,7 @@
 *}
 
 lemma n_sub_lemma:
-  "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
+    "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   apply (induct k)
    apply (simp add: card_s_0_eq_empty, atomize)
   apply (rotate_tac -1, erule finite_induct)
@@ -166,10 +161,10 @@
     using Suc by simp
   also have "\<dots> =  a*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k)) +
                    b*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
-    by(rule nat_distrib)
+    by (rule nat_distrib)
   also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^(k+1) * b^(n-k)) +
                   (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k+1))"
-    by(simp add: setsum_right_distrib mult_ac)
+    by (simp add: setsum_right_distrib mult_ac)
   also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^k * b^(n+1-k)) +
                   (\<Sum>k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))"
     by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
@@ -177,10 +172,10 @@
   also have "\<dots> = a^(n+1) + b^(n+1) +
                   (\<Sum>k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) +
                   (\<Sum>k=1..n. (n choose k) * a^k * b^(n+1-k))"
-    by(simp add: decomp2)
+    by (simp add: decomp2)
   also have
-    "\<dots> = a^(n+1) + b^(n+1) + (\<Sum>k=1..n. (n+1 choose k) * a^k * b^(n+1-k))"
-    by(simp add: nat_distrib setsum_addf binomial.simps)
+      "\<dots> = a^(n+1) + b^(n+1) + (\<Sum>k=1..n. (n+1 choose k) * a^k * b^(n+1-k))"
+    by (simp add: nat_distrib setsum_addf binomial.simps)
   also have "\<dots> = (\<Sum>k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))"
     using decomp by simp
   finally show ?case by simp