src/HOL/NumberTheory/IntFact.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 14271 8ed6989228bb child 15392 290bc97038c7 permissions -rw-r--r--
import -> imports
```     1 (*  Title:      HOL/NumberTheory/IntFact.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Thomas M. Rasmussen
```
```     4     Copyright   2000  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header {* Factorial on integers *}
```
```     8
```
```     9 theory IntFact = IntPrimes:
```
```    10
```
```    11 text {*
```
```    12   Factorial on integers and recursively defined set including all
```
```    13   Integers from @{text 2} up to @{text a}.  Plus definition of product
```
```    14   of finite set.
```
```    15
```
```    16   \bigskip
```
```    17 *}
```
```    18
```
```    19 consts
```
```    20   zfact :: "int => int"
```
```    21   setprod :: "int set => int"
```
```    22   d22set :: "int => int set"
```
```    23
```
```    24 recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
```
```    25   "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
```
```    26
```
```    27 defs
```
```    28   setprod_def: "setprod A == (if finite A then fold (op *) 1 A else 1)"
```
```    29
```
```    30 recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
```
```    31   "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
```
```    32
```
```    33
```
```    34 text {* \medskip @{term setprod} --- product of finite set *}
```
```    35
```
```    36 lemma setprod_empty [simp]: "setprod {} = 1"
```
```    37   apply (simp add: setprod_def)
```
```    38   done
```
```    39
```
```    40 lemma setprod_insert [simp]:
```
```    41     "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
```
```    42   by (simp add: setprod_def mult_left_commute LC.fold_insert [OF LC.intro])
```
```    43
```
```    44 text {*
```
```    45   \medskip @{term d22set} --- recursively defined set including all
```
```    46   integers from @{text 2} up to @{text a}
```
```    47 *}
```
```    48
```
```    49 declare d22set.simps [simp del]
```
```    50
```
```    51
```
```    52 lemma d22set_induct:
```
```    53   "(!!a. P {} a) ==>
```
```    54     (!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1)
```
```    55       ==> P (d22set a) a)
```
```    56     ==> P (d22set u) u"
```
```    57 proof -
```
```    58   case rule_context
```
```    59   show ?thesis
```
```    60     apply (rule d22set.induct)
```
```    61     apply safe
```
```    62      apply (case_tac [2] "1 < a")
```
```    63       apply (rule_tac [2] rule_context)
```
```    64        apply (simp_all (no_asm_simp))
```
```    65      apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
```
```    66     done
```
```    67 qed
```
```    68
```
```    69 lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
```
```    70   apply (induct a rule: d22set_induct)
```
```    71    prefer 2
```
```    72    apply (subst d22set.simps)
```
```    73    apply auto
```
```    74   done
```
```    75
```
```    76 lemma d22set_le [rule_format]: "b \<in> d22set a --> b \<le> a"
```
```    77   apply (induct a rule: d22set_induct)
```
```    78    prefer 2
```
```    79    apply (subst d22set.simps)
```
```    80    apply auto
```
```    81   done
```
```    82
```
```    83 lemma d22set_le_swap: "a < b ==> b \<notin> d22set a"
```
```    84   apply (auto dest: d22set_le)
```
```    85   done
```
```    86
```
```    87 lemma d22set_mem [rule_format]: "1 < b --> b \<le> a --> b \<in> d22set a"
```
```    88   apply (induct a rule: d22set.induct)
```
```    89   apply auto
```
```    90    apply (simp_all add: d22set.simps)
```
```    91   done
```
```    92
```
```    93 lemma d22set_fin: "finite (d22set a)"
```
```    94   apply (induct a rule: d22set_induct)
```
```    95    prefer 2
```
```    96    apply (subst d22set.simps)
```
```    97    apply auto
```
```    98   done
```
```    99
```
```   100
```
```   101 declare zfact.simps [simp del]
```
```   102
```
```   103 lemma d22set_prod_zfact: "setprod (d22set a) = zfact a"
```
```   104   apply (induct a rule: d22set.induct)
```
```   105   apply safe
```
```   106    apply (simp add: d22set.simps zfact.simps)
```
```   107   apply (subst d22set.simps)
```
```   108   apply (subst zfact.simps)
```
```   109   apply (case_tac "1 < a")
```
```   110    prefer 2
```
```   111    apply (simp add: d22set.simps zfact.simps)
```
```   112   apply (simp add: d22set_fin d22set_le_swap)
```
```   113   done
```
```   114
```
```   115 end
```