# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1715552619 -3600
# Node ID 7fefa7839ac684949d60dc4cf12b13e55f12ecfa
# Parent  200107cdd3ace94795120c67770f74402ab1903e
syntax of gchoose now the same as choose

diff -r 200107cdd3ac -r 7fefa7839ac6 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Mon May 06 14:39:33 2024 +0100
+++ b/src/HOL/Binomial.thy	Sun May 12 23:23:39 2024 +0100
@@ -362,7 +362,7 @@
 
 subsection \<open>Generalized binomial coefficients\<close>
 
-definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "gchoose" 65)
+definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a"  (infix "gchoose" 64)
   where gbinomial_prod_rev: "a gchoose k = prod (\<lambda>i. a - of_nat i) {0..<k} div fact k"
 
 lemma gbinomial_0 [simp]:
@@ -379,6 +379,9 @@
 lemma gbinomial_Suc0 [simp]: "a gchoose Suc 0 = a"
   by (simp add: gbinomial_prod_rev lessThan_Suc)
 
+lemma gbinomial_0_left: "0 gchoose k = (if k = 0 then 1 else 0)"
+  by (cases k) simp_all
+
 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)
@@ -479,7 +482,7 @@
   for a :: "'a::field_char_0"
   by (simp add: mult.commute gbinomial_mult_1)
 
-lemma gbinomial_Suc_Suc: "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
+lemma gbinomial_Suc_Suc: "(a + 1) gchoose (Suc k) = (a gchoose k) + (a gchoose (Suc k))"
   for a :: "'a::field_char_0"
 proof (cases k)
   case 0
@@ -491,16 +494,13 @@
     show "{1..k} = Suc ` {0..h}"
       using Suc by (auto simp add: image_Suc_atMost)
   qed auto
-  have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
+  have "fact (Suc k) * ((a gchoose k) + (a gchoose (Suc k))) =
       (a gchoose Suc h) * (fact (Suc (Suc h))) +
       (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
     by (simp add: Suc field_simps del: fact_Suc)
   also have "\<dots> =
     (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (\<Prod>i=0..Suc h. a - of_nat i)"
-    apply (simp only: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
-    apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact
-      mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost)
-    done
+    by (metis atLeastLessThanSuc_atLeastAtMost fact_Suc gbinomial_mult_fact mult.commute of_nat_fact of_nat_mult)
   also have "\<dots> =
     (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + (\<Prod>i=0..Suc h. a - of_nat i)"
     by (simp only: fact_Suc mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
@@ -526,7 +526,7 @@
     using fact_nonzero [of "Suc k"] by auto
 qed
 
-lemma gbinomial_reduce_nat: "0 < k \<Longrightarrow> a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
+lemma gbinomial_reduce_nat: "0 < k \<Longrightarrow> a gchoose k = (a-1 gchoose k-1) + (a-1 gchoose k)"
   for a :: "'a::field_char_0"
   by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)