src/HOL/Fact.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40033 84200d970bf0
child 41550 efa734d9b221
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     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 transfer_morphism_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 transfer_morphism_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_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)"
   187   by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset)
   188 
   189 lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0"
   190   by (auto simp add: dvd_imp_mod_0 fact_dvd)
   191 
   192 lemma fact_div_fact:
   193   assumes "m \<ge> (n :: nat)"
   194   shows "(fact m) div (fact n) = \<Prod>{n + 1..m}"
   195 proof -
   196   obtain d where "d = m - n" by auto
   197   from assms this have "m = n + d" by auto
   198   have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
   199   proof (induct d)
   200     case 0
   201     show ?case by simp
   202   next
   203     case (Suc d')
   204     have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
   205       by simp
   206     also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}" 
   207       unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
   208     also have "... = \<Prod>{n + 1..n + Suc d'}"
   209       by (simp add: atLeastAtMostSuc_conv setprod_insert)
   210     finally show ?case .
   211   qed
   212   from this `m = n + d` show ?thesis by simp
   213 qed
   214 
   215 lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
   216 apply (drule le_imp_less_or_eq)
   217 apply (auto dest!: less_imp_Suc_add)
   218 apply (induct_tac k, auto)
   219 done
   220 
   221 lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
   222   unfolding fact_int_def by auto
   223 
   224 lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
   225   apply (case_tac "m >= 0")
   226   apply auto
   227   apply (frule fact_gt_zero_int)
   228   apply arith
   229 done
   230 
   231 lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow> 
   232     fact (m + k) >= fact m"
   233   apply (case_tac "m < 0")
   234   apply auto
   235   apply (induct k rule: int_ge_induct)
   236   apply auto
   237   apply (subst add_assoc [symmetric])
   238   apply (subst fact_plus_one_int)
   239   apply auto
   240   apply (erule order_trans)
   241   apply (subst mult_le_cancel_right1)
   242   apply (subgoal_tac "fact (m + i) >= 0")
   243   apply arith
   244   apply auto
   245 done
   246 
   247 lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
   248   apply (insert fact_mono_int_aux [of "n - m" "m"])
   249   apply auto
   250 done
   251 
   252 text{*Note that @{term "fact 0 = fact 1"}*}
   253 lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
   254 apply (drule_tac m = m in less_imp_Suc_add, auto)
   255 apply (induct_tac k, auto)
   256 done
   257 
   258 lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
   259     fact m < fact ((m + 1) + k)"
   260   apply (induct k rule: int_ge_induct)
   261   apply (simp add: fact_plus_one_int)
   262   apply (subst mult_less_cancel_right1)
   263   apply (insert fact_gt_zero_int [of m], arith)
   264   apply (subst (2) fact_reduce_int)
   265   apply (auto simp add: add_ac)
   266   apply (erule order_less_le_trans)
   267   apply (subst mult_le_cancel_right1)
   268   apply auto
   269   apply (subgoal_tac "fact (i + (1 + m)) >= 0")
   270   apply force
   271   apply (rule fact_ge_zero_int)
   272 done
   273 
   274 lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
   275   apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
   276   apply auto
   277 done
   278 
   279 lemma fact_num_eq_if_nat: "fact (m::nat) = 
   280   (if m=0 then 1 else m * fact (m - 1))"
   281 by (cases m) auto
   282 
   283 lemma fact_add_num_eq_if_nat:
   284   "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
   285 by (cases "m + n") auto
   286 
   287 lemma fact_add_num_eq_if2_nat:
   288   "fact ((m::nat) + n) = 
   289     (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
   290 by (cases m) auto
   291 
   292 
   293 subsection {* @{term fact} and @{term of_nat} *}
   294 
   295 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
   296 by auto
   297 
   298 lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto
   299 
   300 lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)"
   301 by simp
   302 
   303 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))"
   304 by (auto simp add: positive_imp_inverse_positive)
   305 
   306 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
   307 by (auto intro: order_less_imp_le)
   308 
   309 end