src/HOL/Hyperreal/Fact.thy
changeset 19765 dfe940911617
parent 15241 a3949068537e
child 20503 503ac4c5ef91
--- a/src/HOL/Hyperreal/Fact.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -12,65 +12,65 @@
 
 consts fact :: "nat => nat"
 primrec
-   fact_0:     "fact 0 = 1"
-   fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
+  fact_0:     "fact 0 = 1"
+  fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
 
 
 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
+  by simp
 
 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]:
-     "\<forall>m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
-apply (induct n, auto)
-apply (drule_tac x = "m - 1" in spec, auto)
-done
+    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+  apply (induct n fixing: 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 (case_tac "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 (case_tac "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 (case_tac "m", auto)
-
+    "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
+  by (cases m) auto
 
 end