equal
deleted
inserted
replaced
56 |
56 |
57 lemma fact_diff_Suc [rule_format]: |
57 lemma fact_diff_Suc [rule_format]: |
58 "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)" |
58 "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)" |
59 apply (induct n arbitrary: m) |
59 apply (induct n arbitrary: m) |
60 apply auto |
60 apply auto |
61 apply (drule_tac x = "m - 1" in meta_spec, auto) |
61 apply (drule_tac x = "m - Suc 0" in meta_spec, auto) |
62 done |
62 done |
63 |
63 |
64 lemma fact_num0: "fact 0 = 1" |
64 lemma fact_num0: "fact 0 = 1" |
65 by auto |
65 by auto |
66 |
66 |