--- a/src/HOL/Hyperreal/Fact.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Fact.thy Sun Oct 21 14:53:44 2007 +0200
@@ -17,60 +17,60 @@
lemma fact_gt_zero [simp]: "0 < fact n"
- by (induct n) auto
+by (induct n) auto
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
- by (simp add: neq0_conv)
+by (simp add: neq0_conv)
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
- by auto
+by auto
lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
- by auto
+by auto
lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
- by simp
+by simp
lemma fact_ge_one [simp]: "1 \<le> fact n"
- by (induct n) auto
+by (induct n) auto
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
- apply (drule le_imp_less_or_eq)
- apply (auto dest!: less_imp_Suc_add)
- apply (induct_tac k, auto)
- done
+apply (drule le_imp_less_or_eq)
+apply (auto dest!: less_imp_Suc_add)
+apply (induct_tac k, auto)
+done
text{*Note that @{term "fact 0 = fact 1"}*}
lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
- apply (drule_tac m = m in less_imp_Suc_add, auto)
- apply (induct_tac k, auto)
- done
+apply (drule_tac m = m in less_imp_Suc_add, auto)
+apply (induct_tac k, auto)
+done
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
- by (auto simp add: positive_imp_inverse_positive)
+by (auto simp add: positive_imp_inverse_positive)
lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
- by (auto intro: order_less_imp_le)
+by (auto intro: order_less_imp_le)
lemma fact_diff_Suc [rule_format]:
- "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
- apply (induct n arbitrary: m)
- apply auto
- apply (drule_tac x = "m - 1" in meta_spec, auto)
- done
+ "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+apply (induct n arbitrary: m)
+apply auto
+apply (drule_tac x = "m - 1" in meta_spec, auto)
+done
lemma fact_num0 [simp]: "fact 0 = 1"
- by auto
+by auto
lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
- by (cases m) auto
+by (cases m) auto
lemma fact_add_num_eq_if:
- "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
- by (cases "m + n") auto
+ "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
+by (cases "m + n") auto
lemma fact_add_num_eq_if2:
- "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
- by (cases m) auto
+ "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
+by (cases m) auto
end