src/HOL/Fact.thy
 changeset 41550 efa734d9b221 parent 40033 84200d970bf0 child 45930 2a882ef2cd73
```     1.1 --- a/src/HOL/Fact.thy	Fri Jan 14 15:43:04 2011 +0100
1.2 +++ b/src/HOL/Fact.thy	Fri Jan 14 15:44:47 2011 +0100
1.3 @@ -12,12 +12,9 @@
1.4  begin
1.5
1.6  class fact =
1.7 -
1.8 -fixes
1.9 -  fact :: "'a \<Rightarrow> 'a"
1.10 +  fixes fact :: "'a \<Rightarrow> 'a"
1.11
1.12  instantiation nat :: fact
1.13 -
1.14  begin
1.15
1.16  fun
1.17 @@ -26,7 +23,7 @@
1.18    fact_0_nat: "fact_nat 0 = Suc 0"
1.19  | fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
1.20
1.21 -instance proof qed
1.22 +instance ..
1.23
1.24  end
1.25
1.26 @@ -93,8 +90,7 @@
1.27  lemma fact_plus_one_int:
1.28    assumes "n >= 0"
1.29    shows "fact ((n::int) + 1) = (n + 1) * fact n"
1.30 -
1.31 -  using prems unfolding fact_int_def
1.32 +  using assms unfolding fact_int_def
1.34
1.35  lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.36 @@ -102,19 +98,19 @@
1.37    apply (erule ssubst)
1.38    apply (subst fact_Suc)
1.39    apply simp_all
1.40 -done
1.41 +  done
1.42
1.43  lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.44    apply (subgoal_tac "n = (n - 1) + 1")
1.45    apply (erule ssubst)
1.46    apply (subst fact_plus_one_int)
1.47    apply simp_all
1.48 -done
1.49 +  done
1.50
1.51  lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
1.52    apply (induct n)
1.53    apply (auto simp add: fact_plus_one_nat)
1.54 -done
1.55 +  done
1.56
1.57  lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
1.59 @@ -137,7 +133,7 @@
1.60    apply (erule ssubst)
1.61    apply (subst zle_int)
1.62    apply auto
1.63 -done
1.64 +  done
1.65
1.66  lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
1.67    apply (induct n)
1.68 @@ -147,7 +143,7 @@
1.69    apply (erule ssubst)
1.70    apply (rule dvd_triv_left)
1.71    apply auto
1.72 -done
1.73 +  done
1.74
1.75  lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
1.76    apply (case_tac "1 <= n")
1.77 @@ -155,7 +151,7 @@
1.78    apply (auto simp add: fact_plus_one_int)
1.79    apply (subgoal_tac "m = i + 1")
1.80    apply auto
1.81 -done
1.82 +  done
1.83
1.84  lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
1.85    {i..j+1} = {i..j} Un {j+1}"
```