src/HOL/Fact.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 32047 c141f139ce26 child 32558 e6e1fc2e73cb permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
```     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 NatTransfer
```
```    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 class ordered_semiring_1 = ordered_semiring + semiring_1
```
```   270 class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
```
```   271
```
```   272 lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
```
```   273
```
```   274 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
```
```   275 by simp
```
```   276
```
```   277 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
```
```   278 by (auto simp add: positive_imp_inverse_positive)
```
```   279
```
```   280 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
```
```   281 by (auto intro: order_less_imp_le)
```
```   282
```
```   283 end
```