|
1 (* Title : Fact.ML |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Factorial function |
|
5 *) |
|
6 |
|
7 Goal "0 < fact n"; |
|
8 by (induct_tac "n" 1); |
|
9 by (Auto_tac); |
|
10 qed "fact_gt_zero"; |
|
11 Addsimps [fact_gt_zero]; |
|
12 |
|
13 Goal "fact n ~= 0"; |
|
14 by (Simp_tac 1); |
|
15 qed "fact_not_eq_zero"; |
|
16 Addsimps [fact_not_eq_zero]; |
|
17 |
|
18 Goal "real (fact n) ~= 0"; |
|
19 by Auto_tac; |
|
20 qed "real_of_nat_fact_not_zero"; |
|
21 Addsimps [real_of_nat_fact_not_zero]; |
|
22 |
|
23 Goal "0 < real(fact n)"; |
|
24 by Auto_tac; |
|
25 qed "real_of_nat_fact_gt_zero"; |
|
26 Addsimps [real_of_nat_fact_gt_zero]; |
|
27 |
|
28 Goal "0 <= real(fact n)"; |
|
29 by (Simp_tac 1); |
|
30 qed "real_of_nat_fact_ge_zero"; |
|
31 Addsimps [real_of_nat_fact_ge_zero]; |
|
32 |
|
33 Goal "1 <= fact n"; |
|
34 by (induct_tac "n" 1); |
|
35 by (Auto_tac); |
|
36 qed "fact_ge_one"; |
|
37 Addsimps [fact_ge_one]; |
|
38 |
|
39 Goal "m <= n ==> fact m <= fact n"; |
|
40 by (dtac le_imp_less_or_eq 1); |
|
41 by (auto_tac (claset() addSDs [less_imp_Suc_add],simpset())); |
|
42 by (induct_tac "k" 1); |
|
43 by (Auto_tac); |
|
44 qed "fact_mono"; |
|
45 |
|
46 Goal "[| 0 < m; m < n |] ==> fact m < fact n"; |
|
47 by (dres_inst_tac [("m","m")] less_imp_Suc_add 1); |
|
48 by Auto_tac; |
|
49 by (induct_tac "k" 1); |
|
50 by (Auto_tac); |
|
51 qed "fact_less_mono"; |
|
52 |
|
53 Goal "0 < inverse (real (fact n))"; |
|
54 by (auto_tac (claset(),simpset() addsimps [real_inverse_gt_0])); |
|
55 qed "inv_real_of_nat_fact_gt_zero"; |
|
56 Addsimps [inv_real_of_nat_fact_gt_zero]; |
|
57 |
|
58 Goal "0 <= inverse (real (fact n))"; |
|
59 by (auto_tac (claset() addIs [order_less_imp_le],simpset())); |
|
60 qed "inv_real_of_nat_fact_ge_zero"; |
|
61 Addsimps [inv_real_of_nat_fact_ge_zero]; |
|
62 |
|
63 Goal "ALL m. ma < Suc m --> fact (Suc m - ma) = (Suc m - ma) * fact (m - ma)"; |
|
64 by (induct_tac "ma" 1); |
|
65 by Auto_tac; |
|
66 by (dres_inst_tac [("x","m - 1")] spec 1); |
|
67 by Auto_tac; |
|
68 qed_spec_mp "fact_diff_Suc"; |
|
69 |
|
70 Goal "fact 0 = 1"; |
|
71 by Auto_tac; |
|
72 qed "fact_num0"; |
|
73 Addsimps [fact_num0]; |
|
74 |
|
75 Goal "fact m = (if m=0 then 1 else m * fact (m - 1))"; |
|
76 by (case_tac "m" 1); |
|
77 by Auto_tac; |
|
78 qed "fact_num_eq_if"; |
|
79 |
|
80 Goal "fact (m + n) = (if (m + n = 0) then 1 else (m + n) * (fact (m + n - 1)))"; |
|
81 by (case_tac "m+n" 1); |
|
82 by Auto_tac; |
|
83 qed "fact_add_num_eq_if"; |
|
84 |
|
85 Goal "fact (m + n) = (if (m = 0) then fact n \ |
|
86 \ else (m + n) * (fact ((m - 1) + n)))"; |
|
87 by (case_tac "m" 1); |
|
88 by Auto_tac; |
|
89 qed "fact_add_num_eq_if2"; |
|
90 |