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.33    by (simp add: nat_add_distrib algebra_simps int_mult)
    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.58    by (simp add: fact_int_def)
    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}"