src/HOL/Fact.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 57514 bdc2c6b40bf2 child 58889 5b7a9633cfa8 permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
```     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   fixes fact :: "'a \<Rightarrow> 'a"
```
```    16
```
```    17 instantiation nat :: fact
```
```    18 begin
```
```    19
```
```    20 fun
```
```    21   fact_nat :: "nat \<Rightarrow> nat"
```
```    22 where
```
```    23   fact_0_nat: "fact_nat 0 = Suc 0"
```
```    24 | fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
```
```    25
```
```    26 instance ..
```
```    27
```
```    28 end
```
```    29
```
```    30 (* definitions for the integers *)
```
```    31
```
```    32 instantiation int :: fact
```
```    33
```
```    34 begin
```
```    35
```
```    36 definition
```
```    37   fact_int :: "int \<Rightarrow> int"
```
```    38 where
```
```    39   "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
```
```    40
```
```    41 instance proof qed
```
```    42
```
```    43 end
```
```    44
```
```    45
```
```    46 subsection {* Set up Transfer *}
```
```    47
```
```    48 lemma transfer_nat_int_factorial:
```
```    49   "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
```
```    50   unfolding fact_int_def
```
```    51   by auto
```
```    52
```
```    53
```
```    54 lemma transfer_nat_int_factorial_closure:
```
```    55   "x >= (0::int) \<Longrightarrow> fact x >= 0"
```
```    56   by (auto simp add: fact_int_def)
```
```    57
```
```    58 declare transfer_morphism_nat_int[transfer add return:
```
```    59     transfer_nat_int_factorial transfer_nat_int_factorial_closure]
```
```    60
```
```    61 lemma transfer_int_nat_factorial:
```
```    62   "fact (int x) = int (fact x)"
```
```    63   unfolding fact_int_def by auto
```
```    64
```
```    65 lemma transfer_int_nat_factorial_closure:
```
```    66   "is_nat x \<Longrightarrow> fact x >= 0"
```
```    67   by (auto simp add: fact_int_def)
```
```    68
```
```    69 declare transfer_morphism_int_nat[transfer add return:
```
```    70     transfer_int_nat_factorial transfer_int_nat_factorial_closure]
```
```    71
```
```    72
```
```    73 subsection {* Factorial *}
```
```    74
```
```    75 lemma fact_0_int [simp]: "fact (0::int) = 1"
```
```    76   by (simp add: fact_int_def)
```
```    77
```
```    78 lemma fact_1_nat [simp]: "fact (1::nat) = 1"
```
```    79   by simp
```
```    80
```
```    81 lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
```
```    82   by simp
```
```    83
```
```    84 lemma fact_1_int [simp]: "fact (1::int) = 1"
```
```    85   by (simp add: fact_int_def)
```
```    86
```
```    87 lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
```
```    88   by simp
```
```    89
```
```    90 lemma fact_plus_one_int:
```
```    91   assumes "n >= 0"
```
```    92   shows "fact ((n::int) + 1) = (n + 1) * fact n"
```
```    93   using assms unfolding fact_int_def
```
```    94   by (simp add: nat_add_distrib algebra_simps int_mult)
```
```    95
```
```    96 lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
```
```    97   apply (subgoal_tac "n = Suc (n - 1)")
```
```    98   apply (erule ssubst)
```
```    99   apply (subst fact_Suc)
```
```   100   apply simp_all
```
```   101   done
```
```   102
```
```   103 lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
```
```   104   apply (subgoal_tac "n = (n - 1) + 1")
```
```   105   apply (erule ssubst)
```
```   106   apply (subst fact_plus_one_int)
```
```   107   apply simp_all
```
```   108   done
```
```   109
```
```   110 lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
```
```   111   apply (induct n)
```
```   112   apply (auto simp add: fact_plus_one_nat)
```
```   113   done
```
```   114
```
```   115 lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
```
```   116   by (simp add: fact_int_def)
```
```   117
```
```   118 lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
```
```   119   by (insert fact_nonzero_nat [of n], arith)
```
```   120
```
```   121 lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
```
```   122   by (auto simp add: fact_int_def)
```
```   123
```
```   124 lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
```
```   125   by (insert fact_nonzero_nat [of n], arith)
```
```   126
```
```   127 lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
```
```   128   by (insert fact_nonzero_nat [of n], arith)
```
```   129
```
```   130 lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
```
```   131   apply (auto simp add: fact_int_def)
```
```   132   apply (subgoal_tac "1 = int 1")
```
```   133   apply (erule ssubst)
```
```   134   apply (subst zle_int)
```
```   135   apply auto
```
```   136   done
```
```   137
```
```   138 lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
```
```   139   apply (induct n)
```
```   140   apply force
```
```   141   apply (auto simp only: fact_Suc)
```
```   142   apply (subgoal_tac "m = Suc n")
```
```   143   apply (erule ssubst)
```
```   144   apply (rule dvd_triv_left)
```
```   145   apply auto
```
```   146   done
```
```   147
```
```   148 lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
```
```   149   apply (case_tac "1 <= n")
```
```   150   apply (induct n rule: int_ge_induct)
```
```   151   apply (auto simp add: fact_plus_one_int)
```
```   152   apply (subgoal_tac "m = i + 1")
```
```   153   apply auto
```
```   154   done
```
```   155
```
```   156 lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
```
```   157   {i..j+1} = {i..j} Un {j+1}"
```
```   158   by auto
```
```   159
```
```   160 lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
```
```   161   by auto
```
```   162
```
```   163 lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
```
```   164   by auto
```
```   165
```
```   166 lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
```
```   167   apply (induct n)
```
```   168   apply force
```
```   169   apply (subst fact_Suc)
```
```   170   apply (subst interval_Suc)
```
```   171   apply auto
```
```   172 done
```
```   173
```
```   174 lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
```
```   175   apply (induct n rule: int_ge_induct)
```
```   176   apply force
```
```   177   apply (subst fact_plus_one_int, assumption)
```
```   178   apply (subst interval_plus_one_int)
```
```   179   apply auto
```
```   180 done
```
```   181
```
```   182 lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)"
```
```   183   by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset)
```
```   184
```
```   185 lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0"
```
```   186   by (auto simp add: dvd_imp_mod_0 fact_dvd)
```
```   187
```
```   188 lemma fact_div_fact:
```
```   189   assumes "m \<ge> (n :: nat)"
```
```   190   shows "(fact m) div (fact n) = \<Prod>{n + 1..m}"
```
```   191 proof -
```
```   192   obtain d where "d = m - n" by auto
```
```   193   from assms this have "m = n + d" by auto
```
```   194   have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
```
```   195   proof (induct d)
```
```   196     case 0
```
```   197     show ?case by simp
```
```   198   next
```
```   199     case (Suc d')
```
```   200     have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
```
```   201       by simp
```
```   202     also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}"
```
```   203       unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
```
```   204     also have "... = \<Prod>{n + 1..n + Suc d'}"
```
```   205       by (simp add: atLeastAtMostSuc_conv setprod.insert)
```
```   206     finally show ?case .
```
```   207   qed
```
```   208   from this `m = n + d` show ?thesis by simp
```
```   209 qed
```
```   210
```
```   211 lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
```
```   212 apply (drule le_imp_less_or_eq)
```
```   213 apply (auto dest!: less_imp_Suc_add)
```
```   214 apply (induct_tac k, auto)
```
```   215 done
```
```   216
```
```   217 lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
```
```   218   unfolding fact_int_def by auto
```
```   219
```
```   220 lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
```
```   221   apply (case_tac "m >= 0")
```
```   222   apply auto
```
```   223   apply (frule fact_gt_zero_int)
```
```   224   apply arith
```
```   225 done
```
```   226
```
```   227 lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow>
```
```   228     fact (m + k) >= fact m"
```
```   229   apply (case_tac "m < 0")
```
```   230   apply auto
```
```   231   apply (induct k rule: int_ge_induct)
```
```   232   apply auto
```
```   233   apply (subst add.assoc [symmetric])
```
```   234   apply (subst fact_plus_one_int)
```
```   235   apply auto
```
```   236   apply (erule order_trans)
```
```   237   apply (subst mult_le_cancel_right1)
```
```   238   apply (subgoal_tac "fact (m + i) >= 0")
```
```   239   apply arith
```
```   240   apply auto
```
```   241 done
```
```   242
```
```   243 lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
```
```   244   apply (insert fact_mono_int_aux [of "n - m" "m"])
```
```   245   apply auto
```
```   246 done
```
```   247
```
```   248 text{*Note that @{term "fact 0 = fact 1"}*}
```
```   249 lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
```
```   250 apply (drule_tac m = m in less_imp_Suc_add, auto)
```
```   251 apply (induct_tac k, auto)
```
```   252 done
```
```   253
```
```   254 lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
```
```   255     fact m < fact ((m + 1) + k)"
```
```   256   apply (induct k rule: int_ge_induct)
```
```   257   apply (simp add: fact_plus_one_int)
```
```   258   apply (subst (2) fact_reduce_int)
```
```   259   apply (auto simp add: ac_simps)
```
```   260   apply (erule order_less_le_trans)
```
```   261   apply auto
```
```   262   done
```
```   263
```
```   264 lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
```
```   265   apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
```
```   266   apply auto
```
```   267 done
```
```   268
```
```   269 lemma fact_num_eq_if_nat: "fact (m::nat) =
```
```   270   (if m=0 then 1 else m * fact (m - 1))"
```
```   271 by (cases m) auto
```
```   272
```
```   273 lemma fact_add_num_eq_if_nat:
```
```   274   "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
```
```   275 by (cases "m + n") auto
```
```   276
```
```   277 lemma fact_add_num_eq_if2_nat:
```
```   278   "fact ((m::nat) + n) =
```
```   279     (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
```
```   280 by (cases m) auto
```
```   281
```
```   282 lemma fact_le_power: "fact n \<le> n^n"
```
```   283 proof (induct n)
```
```   284   case (Suc n)
```
```   285   then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
```
```   286   then show ?case by (simp add: add_le_mono)
```
```   287 qed simp
```
```   288
```
```   289 subsection {* @{term fact} and @{term of_nat} *}
```
```   290
```
```   291 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
```
```   292 by auto
```
```   293
```
```   294 lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto
```
```   295
```
```   296 lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)"
```
```   297 by simp
```
```   298
```
```   299 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))"
```
```   300 by (auto simp add: positive_imp_inverse_positive)
```
```   301
```
```   302 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
```
```   303 by (auto intro: order_less_imp_le)
```
```   304
```
```   305 lemma fact_eq_rev_setprod_nat: "fact (k::nat) = (\<Prod>i<k. k - i)"
```
```   306   unfolding fact_altdef_nat
```
```   307   by (rule setprod.reindex_bij_witness[where i="\<lambda>i. k - i" and j="\<lambda>i. k - i"]) auto
```
```   308
```
```   309 lemma fact_div_fact_le_pow:
```
```   310   assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r"
```
```   311 proof -
```
```   312   have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
```
```   313     by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
```
```   314   with assms show ?thesis
```
```   315     by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
```
```   316 qed
```
```   317
```
```   318 lemma fact_numeral:  --{*Evaluation for specific numerals*}
```
```   319   "fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
```
```   320   by (simp add: numeral_eq_Suc)
```
```   321
```
```   322 end
```