equal
deleted
inserted
replaced
79 by (etac dvd_imp_le 1); |
79 by (etac dvd_imp_le 1); |
80 by (Asm_full_simp_tac 1); |
80 by (Asm_full_simp_tac 1); |
81 qed "power_dvd_imp_le"; |
81 qed "power_dvd_imp_le"; |
82 |
82 |
83 |
83 |
|
84 (*** Logical equivalences for inequalities ***) |
84 |
85 |
85 (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***) |
86 Goal "(x^n = 0) = (x = (0::nat) & 0<n)"; |
|
87 by (induct_tac "n" 1); |
|
88 by Auto_tac; |
|
89 qed "power_eq_0_iff"; |
|
90 Addsimps [power_eq_0_iff]; |
|
91 |
|
92 Goal "(0 < x^n) = (x ~= (0::nat) | n=0)"; |
|
93 by (induct_tac "n" 1); |
|
94 by Auto_tac; |
|
95 qed "zero_less_power_iff"; |
|
96 Addsimps [zero_less_power_iff]; |
|
97 |
|
98 Goal "(0::nat) <= x^n"; |
|
99 by (induct_tac "n" 1); |
|
100 by Auto_tac; |
|
101 qed "zero_le_power"; |
|
102 Addsimps [zero_le_power]; |
|
103 |
|
104 |
|
105 (**** Binomial Coefficients, following Andy Gordon and Florian Kammueller ****) |
86 |
106 |
87 Goal "(n choose 0) = 1"; |
107 Goal "(n choose 0) = 1"; |
88 by (case_tac "n" 1); |
108 by (case_tac "n" 1); |
89 by (ALLGOALS Asm_simp_tac); |
109 by (ALLGOALS Asm_simp_tac); |
90 qed "binomial_n_0"; |
110 qed "binomial_n_0"; |