# HG changeset patch
# User haftmann
# Date 1534941178 0
# Node ID b129052644e92cfddaaba545af7af38b9128062a
# Parent  134be95e57878f1ba7620df0a61f0faa66d95c89
more uniform parameter naming convention for choose and gchoose

diff -r 134be95e5787 -r b129052644e9 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Aug 22 12:32:58 2018 +0000
+++ b/src/HOL/Binomial.thy	Wed Aug 22 12:32:58 2018 +0000
@@ -332,11 +332,11 @@
 subsection \<open>Generalized binomial coefficients\<close>
 
 definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "gchoose" 65)
-  where gbinomial_prod_rev: "a gchoose n = prod (\<lambda>i. a - of_nat i) {0..<n} div fact n"
+  where gbinomial_prod_rev: "a gchoose k = prod (\<lambda>i. a - of_nat i) {0..<k} div fact k"
 
 lemma gbinomial_0 [simp]:
   "a gchoose 0 = 1"
-  "0 gchoose (Suc n) = 0"
+  "0 gchoose (Suc k) = 0"
   by (simp_all add: gbinomial_prod_rev prod.atLeast0_lessThan_Suc_shift)
 
 lemma gbinomial_Suc: "a gchoose (Suc k) = prod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)"
@@ -348,28 +348,28 @@
 lemma gbinomial_Suc0 [simp]: "a gchoose Suc 0 = a"
   by (simp add: gbinomial_prod_rev lessThan_Suc)
 
-lemma gbinomial_mult_fact: "fact n * (a gchoose n) = (\<Prod>i = 0..<n. a - of_nat i)"
+lemma gbinomial_mult_fact: "fact k * (a gchoose k) = (\<Prod>i = 0..<k. a - of_nat i)"
   for a :: "'a::field_char_0"
   by (simp_all add: gbinomial_prod_rev field_simps)
 
-lemma gbinomial_mult_fact': "(a gchoose n) * fact n = (\<Prod>i = 0..<n. a - of_nat i)"
+lemma gbinomial_mult_fact': "(a gchoose k) * fact k = (\<Prod>i = 0..<k. a - of_nat i)"
   for a :: "'a::field_char_0"
-  using gbinomial_mult_fact [of n a] by (simp add: ac_simps)
+  using gbinomial_mult_fact [of k a] by (simp add: ac_simps)
 
-lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / fact n"
+lemma gbinomial_pochhammer: "a gchoose k = (- 1) ^ k * pochhammer (- a) k / fact k"
   for a :: "'a::field_char_0"
-  by (cases n)
+  by (cases k)
     (simp_all add: pochhammer_minus,
      simp_all add: gbinomial_prod_rev pochhammer_prod_rev
        power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost
        prod.atLeast_Suc_atMost_Suc_shift of_nat_diff)
 
-lemma gbinomial_pochhammer': "s gchoose n = pochhammer (s - of_nat n + 1) n / fact n"
-  for s :: "'a::field_char_0"
+lemma gbinomial_pochhammer': "a gchoose k = pochhammer (a - of_nat k + 1) k / fact k"
+  for a :: "'a::field_char_0"
 proof -
-  have "s gchoose n = ((-1)^n * (-1)^n) * pochhammer (s - of_nat n + 1) n / fact n"
+  have "a gchoose k = ((-1)^k * (-1)^k) * pochhammer (a - of_nat k + 1) k / fact k"
     by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac)
-  also have "(-1 :: 'a)^n * (-1)^n = 1"
+  also have "(-1 :: 'a)^k * (-1)^k = 1"
     by (subst power_add [symmetric]) simp
   finally show ?thesis
     by simp
@@ -429,10 +429,10 @@
 
 lemma gbinomial_mult_1:
   fixes a :: "'a::field_char_0"
-  shows "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
+  shows "a * (a gchoose k) = of_nat k * (a gchoose k) + of_nat (Suc k) * (a gchoose (Suc k))"
   (is "?l = ?r")
 proof -
-  have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"
+  have "?r = ((- 1) ^k * pochhammer (- a) k / fact k) * (of_nat k - (- a + of_nat k))"
     apply (simp only: gbinomial_pochhammer pochhammer_Suc right_diff_distrib power_Suc)
     apply (simp del: of_nat_Suc fact_Suc)
     apply (auto simp add: field_simps simp del: of_nat_Suc)
@@ -443,7 +443,7 @@
 qed
 
 lemma gbinomial_mult_1':
-  "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
+  "(a gchoose k) * a = of_nat k * (a gchoose k) + of_nat (Suc k) * (a gchoose (Suc k))"
   for a :: "'a::field_char_0"
   by (simp add: mult.commute gbinomial_mult_1)
 
@@ -623,34 +623,34 @@
 
 text \<open>Contributed by Manuel Eberl, generalised by LCP.
   Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"}.\<close>
-lemma gbinomial_altdef_of_nat: "x gchoose k = (\<Prod>i = 0..<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
-  for k :: nat and x :: "'a::field_char_0"
+lemma gbinomial_altdef_of_nat: "a gchoose k = (\<Prod>i = 0..<k. (a - of_nat i) / of_nat (k - i) :: 'a)"
+  for k :: nat and a :: "'a::field_char_0"
   by (simp add: prod_dividef gbinomial_prod_rev fact_prod_rev)
 
 lemma gbinomial_ge_n_over_k_pow_k:
   fixes k :: nat
-    and x :: "'a::linordered_field"
-  assumes "of_nat k \<le> x"
-  shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k"
+    and a :: "'a::linordered_field"
+  assumes "of_nat k \<le> a"
+  shows "(a / of_nat k :: 'a) ^ k \<le> a gchoose k"
 proof -
-  have x: "0 \<le> x"
+  have x: "0 \<le> a"
     using assms of_nat_0_le_iff order_trans by blast
-  have "(x / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. x / of_nat k :: 'a)"
+  have "(a / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. a / of_nat k :: 'a)"
     by simp
-  also have "\<dots> \<le> x gchoose k" (* FIXME *)
+  also have "\<dots> \<le> a gchoose k" (* FIXME *)
     unfolding gbinomial_altdef_of_nat
     apply (safe intro!: prod_mono)
     apply simp_all
     prefer 2
     subgoal premises for i
     proof -
-      from assms have "x * of_nat i \<ge> of_nat (i * k)"
+      from assms have "a * of_nat i \<ge> of_nat (i * k)"
         by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
-      then have "x * of_nat k - x * of_nat i \<le> x * of_nat k - of_nat (i * k)"
+      then have "a * of_nat k - a * of_nat i \<le> a * of_nat k - of_nat (i * k)"
         by arith
-      then have "x * of_nat (k - i) \<le> (x - of_nat i) * of_nat k"
+      then have "a * of_nat (k - i) \<le> (a - of_nat i) * of_nat k"
         using \<open>i < k\<close> by (simp add: algebra_simps zero_less_mult_iff of_nat_diff)
-      then have "x * of_nat (k - i) \<le> (x - of_nat i) * (of_nat k :: 'a)"
+      then have "a * of_nat (k - i) \<le> (a - of_nat i) * (of_nat k :: 'a)"
         by (simp only: of_nat_mult[symmetric] of_nat_le_iff)
       with assms show ?thesis
         using \<open>i < k\<close> by (simp add: field_simps)
@@ -660,14 +660,14 @@
   finally show ?thesis .
 qed
 
-lemma gbinomial_negated_upper: "(a gchoose b) = (-1) ^ b * ((of_nat b - a - 1) gchoose b)"
+lemma gbinomial_negated_upper: "(a gchoose k) = (-1) ^ k * ((of_nat k - a - 1) gchoose k)"
   by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps)
 
-lemma gbinomial_minus: "((-a) gchoose b) = (-1) ^ b * ((a + of_nat b - 1) gchoose b)"
+lemma gbinomial_minus: "((-a) gchoose k) = (-1) ^ k * ((a + of_nat k - 1) gchoose k)"
   by (subst gbinomial_negated_upper) (simp add: add_ac)
 
-lemma Suc_times_gbinomial: "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)"
-proof (cases b)
+lemma Suc_times_gbinomial: "of_nat (Suc k) * ((a + 1) gchoose (Suc k)) = (a + 1) * (a gchoose k)"
+proof (cases k)
   case 0
   then show ?thesis by simp
 next
@@ -681,8 +681,8 @@
   finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
 qed
 
-lemma gbinomial_factors: "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)"
-proof (cases b)
+lemma gbinomial_factors: "((a + 1) gchoose (Suc k)) = (a + 1) / of_nat (Suc k) * (a gchoose k)"
+proof (cases k)
   case 0
   then show ?thesis by simp
 next
@@ -697,8 +697,8 @@
     by (simp add: Suc)
 qed
 
-lemma gbinomial_rec: "((r + 1) gchoose (Suc k)) = (r gchoose k) * ((r + 1) / of_nat (Suc k))"
-  using gbinomial_mult_1[of r k]
+lemma gbinomial_rec: "((a + 1) gchoose (Suc k)) = (a gchoose k) * ((a + 1) / of_nat (Suc k))"
+  using gbinomial_mult_1[of a k]
   by (subst gbinomial_Suc_Suc) (simp add: field_simps del: of_nat_Suc, simp add: algebra_simps)
 
 lemma gbinomial_of_nat_symmetric: "k \<le> n \<Longrightarrow> (of_nat n) gchoose k = (of_nat n) gchoose (n - k)"
@@ -709,8 +709,8 @@
 \[
 {r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
 \]\<close>
-lemma gbinomial_absorption': "k > 0 \<Longrightarrow> r gchoose k = (r / of_nat k) * (r - 1 gchoose (k - 1))"
-  using gbinomial_rec[of "r - 1" "k - 1"]
+lemma gbinomial_absorption': "k > 0 \<Longrightarrow> a gchoose k = (a / of_nat k) * (a - 1 gchoose (k - 1))"
+  using gbinomial_rec[of "a - 1" "k - 1"]
   by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc)
 
 text \<open>The absorption identity is written in the following form to avoid
@@ -719,8 +719,8 @@
 \[
 k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
 \]\<close>
-lemma gbinomial_absorption: "of_nat (Suc k) * (r gchoose Suc k) = r * ((r - 1) gchoose k)"
-  using gbinomial_absorption'[of "Suc k" r] by (simp add: field_simps del: of_nat_Suc)
+lemma gbinomial_absorption: "of_nat (Suc k) * (a gchoose Suc k) = a * ((a - 1) gchoose k)"
+  using gbinomial_absorption'[of "Suc k" a] by (simp add: field_simps del: of_nat_Suc)
 
 text \<open>The absorption identity for natural number binomial coefficients:\<close>
 lemma binomial_absorption: "Suc k * (n choose Suc k) = n * ((n - 1) choose k)"
@@ -746,12 +746,12 @@
 qed
 
 text \<open>The generalised absorption companion identity:\<close>
-lemma gbinomial_absorb_comp: "(r - of_nat k) * (r gchoose k) = r * ((r - 1) gchoose k)"
-  using pochhammer_absorb_comp[of r k] by (simp add: gbinomial_pochhammer)
+lemma gbinomial_absorb_comp: "(a - of_nat k) * (a gchoose k) = a * ((a - 1) gchoose k)"
+  using pochhammer_absorb_comp[of a k] by (simp add: gbinomial_pochhammer)
 
 lemma gbinomial_addition_formula:
-  "r gchoose (Suc k) = ((r - 1) gchoose (Suc k)) + ((r - 1) gchoose k)"
-  using gbinomial_Suc_Suc[of "r - 1" k] by (simp add: algebra_simps)
+  "a gchoose (Suc k) = ((a - 1) gchoose (Suc k)) + ((a - 1) gchoose k)"
+  using gbinomial_Suc_Suc[of "a - 1" k] by (simp add: algebra_simps)
 
 lemma binomial_addition_formula:
   "0 < n \<Longrightarrow> n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)"
@@ -765,14 +765,14 @@
    \quad \textnormal{integer } n.
   \]
 \<close>
-lemma gbinomial_parallel_sum: "(\<Sum>k\<le>n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n"
+lemma gbinomial_parallel_sum: "(\<Sum>k\<le>n. (a + of_nat k) gchoose k) = (a + of_nat n + 1) gchoose n"
 proof (induct n)
   case 0
   then show ?case by simp
 next
   case (Suc m)
   then show ?case
-    using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m]
+    using gbinomial_Suc_Suc[of "(a + of_nat m + 1)" m]
     by (simp add: add_ac)
 qed
 
@@ -785,38 +785,38 @@
   {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
 \<close>
 lemma gbinomial_sum_up_index:
-  "(\<Sum>k = 0..n. (of_nat k gchoose m) :: 'a::field_char_0) = (of_nat n + 1) gchoose (m + 1)"
+  "(\<Sum>j = 0..n. (of_nat j gchoose k) :: 'a::field_char_0) = (of_nat n + 1) gchoose (k + 1)"
 proof (induct n)
   case 0
   show ?case
-    using gbinomial_Suc_Suc[of 0 m]
-    by (cases m) auto
+    using gbinomial_Suc_Suc[of 0 k]
+    by (cases k) auto
 next
   case (Suc n)
   then show ?case
-    using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m]
+    using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" k]
     by (simp add: add_ac)
 qed
 
 lemma gbinomial_index_swap:
-  "((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)"
+  "((-1) ^ k) * ((- (of_nat n) - 1) gchoose k) = ((-1) ^ n) * ((- (of_nat k) - 1) gchoose n)"
   (is "?lhs = ?rhs")
 proof -
-  have "?lhs = (of_nat (m + n) gchoose m)"
+  have "?lhs = (of_nat (k + n) gchoose k)"
     by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric])
-  also have "\<dots> = (of_nat (m + n) gchoose n)"
+  also have "\<dots> = (of_nat (k + n) gchoose n)"
     by (subst gbinomial_of_nat_symmetric) simp_all
   also have "\<dots> = ?rhs"
     by (subst gbinomial_negated_upper) simp
   finally show ?thesis .
 qed
 
-lemma gbinomial_sum_lower_neg: "(\<Sum>k\<le>m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)"
+lemma gbinomial_sum_lower_neg: "(\<Sum>k\<le>m. (a gchoose k) * (- 1) ^ k) = (- 1) ^ m * (a - 1 gchoose m)"
   (is "?lhs = ?rhs")
 proof -
-  have "?lhs = (\<Sum>k\<le>m. -(r + 1) + of_nat k gchoose k)"
+  have "?lhs = (\<Sum>k\<le>m. -(a + 1) + of_nat k gchoose k)"
     by (intro sum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib)
-  also have "\<dots>  = - r + of_nat m gchoose m"
+  also have "\<dots>  = - a + of_nat m gchoose m"
     by (subst gbinomial_parallel_sum) simp
   also have "\<dots> = ?rhs"
     by (subst gbinomial_negated_upper) (simp add: power_mult_distrib)
@@ -824,18 +824,18 @@
 qed
 
 lemma gbinomial_partial_row_sum:
-  "(\<Sum>k\<le>m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))"
+  "(\<Sum>k\<le>m. (a gchoose k) * ((a / 2) - of_nat k)) = ((of_nat m + 1)/2) * (a gchoose (m + 1))"
 proof (induct m)
   case 0
   then show ?case by simp
 next
   case (Suc mm)
-  then have "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) =
-      (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2"
+  then have "(\<Sum>k\<le>Suc mm. (a gchoose k) * (a / 2 - of_nat k)) =
+      (a - of_nat (Suc mm)) * (a gchoose Suc mm) / 2"
     by (simp add: field_simps)
-  also have "\<dots> = r * (r - 1 gchoose Suc mm) / 2"
+  also have "\<dots> = a * (a - 1 gchoose Suc mm) / 2"
     by (subst gbinomial_absorb_comp) (rule refl)
-  also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"
+  also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (a gchoose (Suc mm + 1))"
     by (subst gbinomial_absorption [symmetric]) simp
   finally show ?case .
 qed
@@ -844,15 +844,15 @@
   by (induct mm) simp_all
 
 lemma gbinomial_partial_sum_poly:
-  "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
-    (\<Sum>k\<le>m. (-r gchoose k) * (-x)^k * (x + y)^(m-k))"
+  "(\<Sum>k\<le>m. (of_nat m + a gchoose k) * x^k * y^(m-k)) =
+    (\<Sum>k\<le>m. (-a gchoose k) * (-x)^k * (x + y)^(m-k))"
   (is "?lhs m = ?rhs m")
 proof (induction m)
   case 0
   then show ?case by simp
 next
   case (Suc mm)
-  define G where "G i k = (of_nat i + r gchoose k) * x^k * y^(i - k)" for i k
+  define G where "G i k = (of_nat i + a gchoose k) * x^k * y^(i - k)" for i k
   define S where "S = ?lhs"
   have SG_def: "S = (\<lambda>i. (\<Sum>k\<le>i. (G i k)))"
     unfolding S_def G_def ..
@@ -861,61 +861,61 @@
     using SG_def by (simp add: sum_head_Suc atLeast0AtMost [symmetric])
   also have "(\<Sum>k=Suc 0..Suc mm. G (Suc mm) k) = (\<Sum>k=0..mm. G (Suc mm) (Suc k))"
     by (subst sum_shift_bounds_cl_Suc_ivl) simp
-  also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + r gchoose (Suc k)) +
-      (of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm - k))"
+  also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + a gchoose (Suc k)) +
+      (of_nat mm + a gchoose k)) * x^(Suc k) * y^(mm - k))"
     unfolding G_def by (subst gbinomial_addition_formula) simp
-  also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) +
-      (\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))"
+  also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + a gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) +
+      (\<Sum>k=0..mm. (of_nat mm + a gchoose k) * x^(Suc k) * y^(mm - k))"
     by (subst sum.distrib [symmetric]) (simp add: algebra_simps)
-  also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) =
-      (\<Sum>k<Suc mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))"
+  also have "(\<Sum>k=0..mm. (of_nat mm + a gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) =
+      (\<Sum>k<Suc mm. (of_nat mm + a gchoose (Suc k)) * x^(Suc k) * y^(mm - k))"
     by (simp only: atLeast0AtMost lessThan_Suc_atMost)
-  also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k)) +
-      (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
+  also have "\<dots> = (\<Sum>k<mm. (of_nat mm + a gchoose Suc k) * x^(Suc k) * y^(mm-k)) +
+      (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm)"
     (is "_ = ?A + ?B")
     by (subst sum_lessThan_Suc) simp
-  also have "?A = (\<Sum>k=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))"
+  also have "?A = (\<Sum>k=1..mm. (of_nat mm + a gchoose k) * x^k * y^(mm - k + 1))"
   proof (subst sum_bounds_lt_plus1 [symmetric], intro sum.cong[OF refl], clarify)
     fix k
     assume "k < mm"
     then have "mm - k = mm - Suc k + 1"
       by linarith
-    then show "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =
-        (of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)"
+    then show "(of_nat mm + a gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =
+        (of_nat mm + a gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)"
       by (simp only:)
   qed
-  also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
+  also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm)"
     unfolding G_def by (subst sum_distrib_left) (simp add: algebra_simps)
-  also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"
+  also have "(\<Sum>k=0..mm. (of_nat mm + a gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"
     unfolding S_def by (subst sum_distrib_left) (simp add: atLeast0AtMost algebra_simps)
   also have "(G (Suc mm) 0) = y * (G mm 0)"
     by (simp add: G_def)
   finally have "S (Suc mm) =
-      y * (G mm 0 + (\<Sum>k=1..mm. (G mm k))) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
+      y * (G mm 0 + (\<Sum>k=1..mm. (G mm k))) + (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
     by (simp add: ring_distribs)
   also have "G mm 0 + (\<Sum>k=1..mm. (G mm k)) = S mm"
     by (simp add: sum_head_Suc[symmetric] SG_def atLeast0AtMost)
-  finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
+  finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm)"
     by (simp add: algebra_simps)
-  also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (- r gchoose (Suc mm))"
+  also have "(of_nat mm + a gchoose (Suc mm)) = (-1) ^ (Suc mm) * (- a gchoose (Suc mm))"
     by (subst gbinomial_negated_upper) simp
-  also have "(-1) ^ Suc mm * (- r gchoose Suc mm) * x ^ Suc mm =
-      (- r gchoose (Suc mm)) * (-x) ^ Suc mm"
+  also have "(-1) ^ Suc mm * (- a gchoose Suc mm) * x ^ Suc mm =
+      (- a gchoose (Suc mm)) * (-x) ^ Suc mm"
     by (simp add: power_minus[of x])
-  also have "(x + y) * S mm + \<dots> = (x + y) * ?rhs mm + (- r gchoose (Suc mm)) * (- x)^Suc mm"
+  also have "(x + y) * S mm + \<dots> = (x + y) * ?rhs mm + (- a gchoose (Suc mm)) * (- x)^Suc mm"
     unfolding S_def by (subst Suc.IH) simp
-  also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"
+  also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. ((- a gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"
     by (subst sum_distrib_left, rule sum.cong) (simp_all add: Suc_diff_le)
-  also have "\<dots> + (-r gchoose (Suc mm)) * (-x)^Suc mm =
-      (\<Sum>n\<le>Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))"
+  also have "\<dots> + (-a gchoose (Suc mm)) * (-x)^Suc mm =
+      (\<Sum>n\<le>Suc mm. (- a gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))"
     by simp
   finally show ?case
     by (simp only: S_def)
 qed
 
 lemma gbinomial_partial_sum_poly_xpos:
-    "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
-     (\<Sum>k\<le>m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"
+    "(\<Sum>k\<le>m. (of_nat m + a gchoose k) * x^k * y^(m-k)) =
+     (\<Sum>k\<le>m. (of_nat k + a - 1 gchoose k) * x^k * (x + y)^(m-k))"
   apply (subst gbinomial_partial_sum_poly)
   apply (subst gbinomial_negated_upper)
   apply (intro sum.cong, rule refl)
@@ -964,7 +964,7 @@
   also have "\<dots> = (\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k))"
     using gbinomial_r_part_sum ..
   also have "\<dots> = (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) * 2 ^ (m - k))"
-    using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and r="of_nat m + 1" and m="m"]
+    using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and a="of_nat m + 1" and m="m"]
     by (simp add: add_ac)
   also have "\<dots> = 2 ^ m * (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) / 2 ^ k)"
     by (subst sum_distrib_left) (simp add: algebra_simps power_diff)
@@ -974,11 +974,11 @@
 
 lemma gbinomial_trinomial_revision:
   assumes "k \<le> m"
-  shows "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))"
+  shows "(a gchoose m) * (of_nat m gchoose k) = (a gchoose k) * (a - of_nat k gchoose (m - k))"
 proof -
-  have "(r gchoose m) * (of_nat m gchoose k) = (r gchoose m) * fact m / (fact k * fact (m - k))"
+  have "(a gchoose m) * (of_nat m gchoose k) = (a gchoose m) * fact m / (fact k * fact (m - k))"
     using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)
-  also have "\<dots> = (r gchoose k) * (r - of_nat k gchoose (m - k))"
+  also have "\<dots> = (a gchoose k) * (a - of_nat k gchoose (m - k))"
     using assms by (simp add: gbinomial_pochhammer power_diff pochhammer_product)
   finally show ?thesis .
 qed
@@ -1288,10 +1288,10 @@
 subsection \<open>Executable code\<close>
 
 lemma gbinomial_code [code]:
-  "a gchoose n =
-    (if n = 0 then 1
-     else fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
-  by (cases n)
+  "a gchoose k =
+    (if k = 0 then 1
+     else fold_atLeastAtMost_nat (\<lambda>k acc. (a - of_nat k) * acc) 0 (k - 1) 1 / fact k)"
+  by (cases k)
     (simp_all add: gbinomial_prod_rev prod_atLeastAtMost_code [symmetric]
       atLeastLessThanSuc_atLeastAtMost)