10 imports "../Real/Real" |
10 imports "../Real/Real" |
11 begin |
11 begin |
12 |
12 |
13 consts fact :: "nat => nat" |
13 consts fact :: "nat => nat" |
14 primrec |
14 primrec |
15 fact_0: "fact 0 = 1" |
15 fact_0: "fact 0 = 1" |
16 fact_Suc: "fact (Suc n) = (Suc n) * fact n" |
16 fact_Suc: "fact (Suc n) = (Suc n) * fact n" |
17 |
17 |
18 |
18 |
19 lemma fact_gt_zero [simp]: "0 < fact n" |
19 lemma fact_gt_zero [simp]: "0 < fact n" |
20 by (induct "n", auto) |
20 by (induct n) auto |
21 |
21 |
22 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0" |
22 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0" |
23 by simp |
23 by simp |
24 |
24 |
25 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0" |
25 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0" |
26 by auto |
26 by auto |
27 |
27 |
28 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)" |
28 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)" |
29 by auto |
29 by auto |
30 |
30 |
31 lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)" |
31 lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)" |
32 by simp |
32 by simp |
33 |
33 |
34 lemma fact_ge_one [simp]: "1 \<le> fact n" |
34 lemma fact_ge_one [simp]: "1 \<le> fact n" |
35 by (induct "n", auto) |
35 by (induct n) auto |
36 |
36 |
37 lemma fact_mono: "m \<le> n ==> fact m \<le> fact n" |
37 lemma fact_mono: "m \<le> n ==> fact m \<le> fact n" |
38 apply (drule le_imp_less_or_eq) |
38 apply (drule le_imp_less_or_eq) |
39 apply (auto dest!: less_imp_Suc_add) |
39 apply (auto dest!: less_imp_Suc_add) |
40 apply (induct_tac "k", auto) |
40 apply (induct_tac k, auto) |
41 done |
41 done |
42 |
42 |
43 text{*Note that @{term "fact 0 = fact 1"}*} |
43 text{*Note that @{term "fact 0 = fact 1"}*} |
44 lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n" |
44 lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n" |
45 apply (drule_tac m = m in less_imp_Suc_add, auto) |
45 apply (drule_tac m = m in less_imp_Suc_add, auto) |
46 apply (induct_tac "k", auto) |
46 apply (induct_tac k, auto) |
47 done |
47 done |
48 |
48 |
49 lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))" |
49 lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))" |
50 by (auto simp add: positive_imp_inverse_positive) |
50 by (auto simp add: positive_imp_inverse_positive) |
51 |
51 |
52 lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))" |
52 lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))" |
53 by (auto intro: order_less_imp_le) |
53 by (auto intro: order_less_imp_le) |
54 |
54 |
55 lemma fact_diff_Suc [rule_format]: |
55 lemma fact_diff_Suc [rule_format]: |
56 "\<forall>m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)" |
56 "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)" |
57 apply (induct n, auto) |
57 apply (induct n fixing: m) |
58 apply (drule_tac x = "m - 1" in spec, auto) |
58 apply auto |
59 done |
59 apply (drule_tac x = "m - 1" in meta_spec, auto) |
|
60 done |
60 |
61 |
61 lemma fact_num0 [simp]: "fact 0 = 1" |
62 lemma fact_num0 [simp]: "fact 0 = 1" |
62 by auto |
63 by auto |
63 |
64 |
64 lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))" |
65 lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))" |
65 by (case_tac "m", auto) |
66 by (cases m) auto |
66 |
67 |
67 lemma fact_add_num_eq_if: |
68 lemma fact_add_num_eq_if: |
68 "fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n - 1)))" |
69 "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))" |
69 by (case_tac "m+n", auto) |
70 by (cases "m + n") auto |
70 |
71 |
71 lemma fact_add_num_eq_if2: |
72 lemma fact_add_num_eq_if2: |
72 "fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m - 1) + n)))" |
73 "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))" |
73 by (case_tac "m", auto) |
74 by (cases m) auto |
74 |
|
75 |
75 |
76 end |
76 end |