src/HOL/Fact.thy
author haftmann
Thu Oct 29 11:41:37 2009 +0100 (2009-10-29)
changeset 33319 74f0dcc0b5fb
parent 32558 e6e1fc2e73cb
child 35028 108662d50512
permissions -rw-r--r--
moved algebraic classes to Ring_and_Field
     1 (*  Title       : Fact.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5     The integer version of factorial and other additions by Jeremy Avigad.
     6 *)
     7 
     8 header{*Factorial Function*}
     9 
    10 theory Fact
    11 imports Main
    12 begin
    13 
    14 class fact =
    15 
    16 fixes 
    17   fact :: "'a \<Rightarrow> 'a"
    18 
    19 instantiation nat :: fact
    20 
    21 begin 
    22 
    23 fun
    24   fact_nat :: "nat \<Rightarrow> nat"
    25 where
    26   fact_0_nat: "fact_nat 0 = Suc 0"
    27 | fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
    28 
    29 instance proof qed
    30 
    31 end
    32 
    33 (* definitions for the integers *)
    34 
    35 instantiation int :: fact
    36 
    37 begin 
    38 
    39 definition
    40   fact_int :: "int \<Rightarrow> int"
    41 where  
    42   "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
    43 
    44 instance proof qed
    45 
    46 end
    47 
    48 
    49 subsection {* Set up Transfer *}
    50 
    51 lemma transfer_nat_int_factorial:
    52   "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
    53   unfolding fact_int_def
    54   by auto
    55 
    56 
    57 lemma transfer_nat_int_factorial_closure:
    58   "x >= (0::int) \<Longrightarrow> fact x >= 0"
    59   by (auto simp add: fact_int_def)
    60 
    61 declare TransferMorphism_nat_int[transfer add return: 
    62     transfer_nat_int_factorial transfer_nat_int_factorial_closure]
    63 
    64 lemma transfer_int_nat_factorial:
    65   "fact (int x) = int (fact x)"
    66   unfolding fact_int_def by auto
    67 
    68 lemma transfer_int_nat_factorial_closure:
    69   "is_nat x \<Longrightarrow> fact x >= 0"
    70   by (auto simp add: fact_int_def)
    71 
    72 declare TransferMorphism_int_nat[transfer add return: 
    73     transfer_int_nat_factorial transfer_int_nat_factorial_closure]
    74 
    75 
    76 subsection {* Factorial *}
    77 
    78 lemma fact_0_int [simp]: "fact (0::int) = 1"
    79   by (simp add: fact_int_def)
    80 
    81 lemma fact_1_nat [simp]: "fact (1::nat) = 1"
    82   by simp
    83 
    84 lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
    85   by simp
    86 
    87 lemma fact_1_int [simp]: "fact (1::int) = 1"
    88   by (simp add: fact_int_def)
    89 
    90 lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
    91   by simp
    92 
    93 lemma fact_plus_one_int: 
    94   assumes "n >= 0"
    95   shows "fact ((n::int) + 1) = (n + 1) * fact n"
    96 
    97   using prems unfolding fact_int_def 
    98   by (simp add: nat_add_distrib algebra_simps int_mult)
    99 
   100 lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
   101   apply (subgoal_tac "n = Suc (n - 1)")
   102   apply (erule ssubst)
   103   apply (subst fact_Suc)
   104   apply simp_all
   105 done
   106 
   107 lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
   108   apply (subgoal_tac "n = (n - 1) + 1")
   109   apply (erule ssubst)
   110   apply (subst fact_plus_one_int)
   111   apply simp_all
   112 done
   113 
   114 lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
   115   apply (induct n)
   116   apply (auto simp add: fact_plus_one_nat)
   117 done
   118 
   119 lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
   120   by (simp add: fact_int_def)
   121 
   122 lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
   123   by (insert fact_nonzero_nat [of n], arith)
   124 
   125 lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
   126   by (auto simp add: fact_int_def)
   127 
   128 lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
   129   by (insert fact_nonzero_nat [of n], arith)
   130 
   131 lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
   132   by (insert fact_nonzero_nat [of n], arith)
   133 
   134 lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
   135   apply (auto simp add: fact_int_def)
   136   apply (subgoal_tac "1 = int 1")
   137   apply (erule ssubst)
   138   apply (subst zle_int)
   139   apply auto
   140 done
   141 
   142 lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
   143   apply (induct n)
   144   apply force
   145   apply (auto simp only: fact_Suc)
   146   apply (subgoal_tac "m = Suc n")
   147   apply (erule ssubst)
   148   apply (rule dvd_triv_left)
   149   apply auto
   150 done
   151 
   152 lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
   153   apply (case_tac "1 <= n")
   154   apply (induct n rule: int_ge_induct)
   155   apply (auto simp add: fact_plus_one_int)
   156   apply (subgoal_tac "m = i + 1")
   157   apply auto
   158 done
   159 
   160 lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow> 
   161   {i..j+1} = {i..j} Un {j+1}"
   162   by auto
   163 
   164 lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
   165   by auto
   166 
   167 lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
   168   by auto
   169 
   170 lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
   171   apply (induct n)
   172   apply force
   173   apply (subst fact_Suc)
   174   apply (subst interval_Suc)
   175   apply auto
   176 done
   177 
   178 lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
   179   apply (induct n rule: int_ge_induct)
   180   apply force
   181   apply (subst fact_plus_one_int, assumption)
   182   apply (subst interval_plus_one_int)
   183   apply auto
   184 done
   185 
   186 lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
   187 apply (drule le_imp_less_or_eq)
   188 apply (auto dest!: less_imp_Suc_add)
   189 apply (induct_tac k, auto)
   190 done
   191 
   192 lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
   193   unfolding fact_int_def by auto
   194 
   195 lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
   196   apply (case_tac "m >= 0")
   197   apply auto
   198   apply (frule fact_gt_zero_int)
   199   apply arith
   200 done
   201 
   202 lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow> 
   203     fact (m + k) >= fact m"
   204   apply (case_tac "m < 0")
   205   apply auto
   206   apply (induct k rule: int_ge_induct)
   207   apply auto
   208   apply (subst add_assoc [symmetric])
   209   apply (subst fact_plus_one_int)
   210   apply auto
   211   apply (erule order_trans)
   212   apply (subst mult_le_cancel_right1)
   213   apply (subgoal_tac "fact (m + i) >= 0")
   214   apply arith
   215   apply auto
   216 done
   217 
   218 lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
   219   apply (insert fact_mono_int_aux [of "n - m" "m"])
   220   apply auto
   221 done
   222 
   223 text{*Note that @{term "fact 0 = fact 1"}*}
   224 lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
   225 apply (drule_tac m = m in less_imp_Suc_add, auto)
   226 apply (induct_tac k, auto)
   227 done
   228 
   229 lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
   230     fact m < fact ((m + 1) + k)"
   231   apply (induct k rule: int_ge_induct)
   232   apply (simp add: fact_plus_one_int)
   233   apply (subst mult_less_cancel_right1)
   234   apply (insert fact_gt_zero_int [of m], arith)
   235   apply (subst (2) fact_reduce_int)
   236   apply (auto simp add: add_ac)
   237   apply (erule order_less_le_trans)
   238   apply (subst mult_le_cancel_right1)
   239   apply auto
   240   apply (subgoal_tac "fact (i + (1 + m)) >= 0")
   241   apply force
   242   apply (rule fact_ge_zero_int)
   243 done
   244 
   245 lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
   246   apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
   247   apply auto
   248 done
   249 
   250 lemma fact_num_eq_if_nat: "fact (m::nat) = 
   251   (if m=0 then 1 else m * fact (m - 1))"
   252 by (cases m) auto
   253 
   254 lemma fact_add_num_eq_if_nat:
   255   "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
   256 by (cases "m + n") auto
   257 
   258 lemma fact_add_num_eq_if2_nat:
   259   "fact ((m::nat) + n) = 
   260     (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
   261 by (cases m) auto
   262 
   263 
   264 subsection {* @{term fact} and @{term of_nat} *}
   265 
   266 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
   267 by auto
   268 
   269 lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
   270 
   271 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
   272 by simp
   273 
   274 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
   275 by (auto simp add: positive_imp_inverse_positive)
   276 
   277 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
   278 by (auto intro: order_less_imp_le)
   279 
   280 end