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
```