174 qed_spec_mp "Suc_times_binomial_eq"; |
174 qed_spec_mp "Suc_times_binomial_eq"; |
175 |
175 |
176 (*This is the well-known version, but it's harder to use because of the |
176 (*This is the well-known version, but it's harder to use because of the |
177 need to reason about division.*) |
177 need to reason about division.*) |
178 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; |
178 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; |
179 by (asm_simp_tac |
179 by (asm_simp_tac (simpset() |
180 (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, |
180 addsimps [Suc_times_binomial_eq, div_mult_self_is_m, zero_less_Suc] |
181 div_mult_self_is_m]) 1); |
181 delsimps [mult_Suc, mult_Suc_right]) 1); |
182 qed "binomial_Suc_Suc_eq_times"; |
182 qed "binomial_Suc_Suc_eq_times"; |
183 |
183 |
184 (*Another version, with -1 instead of Suc.*) |
184 (*Another version, with -1 instead of Suc.*) |
185 Goal "[|k <= n; 0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"; |
185 Goal "[|k <= n; 0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"; |
186 by (cut_inst_tac [("n","n - 1"),("k","k - 1")] Suc_times_binomial_eq 1); |
186 by (cut_inst_tac [("n","n - 1"),("k","k - 1")] Suc_times_binomial_eq 1); |