src/HOL/Old_Number_Theory/IntFact.thy
 author haftmann Tue Sep 01 15:39:33 2009 +0200 (2009-09-01) changeset 32479 521cc9bf2958 parent 18369 src/HOL/NumberTheory/IntFact.thy@694ea14ab4f2 child 35440 bdf8ad377877 permissions -rw-r--r--
some reorganization of number theory
```     1 (*  Author:     Thomas M. Rasmussen
```
```     2     Copyright   2000  University of Cambridge
```
```     3 *)
```
```     4
```
```     5 header {* Factorial on integers *}
```
```     6
```
```     7 theory IntFact imports IntPrimes begin
```
```     8
```
```     9 text {*
```
```    10   Factorial on integers and recursively defined set including all
```
```    11   Integers from @{text 2} up to @{text a}.  Plus definition of product
```
```    12   of finite set.
```
```    13
```
```    14   \bigskip
```
```    15 *}
```
```    16
```
```    17 consts
```
```    18   zfact :: "int => int"
```
```    19   d22set :: "int => int set"
```
```    20
```
```    21 recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
```
```    22   "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
```
```    23
```
```    24 recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
```
```    25   "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
```
```    26
```
```    27
```
```    28 text {*
```
```    29   \medskip @{term d22set} --- recursively defined set including all
```
```    30   integers from @{text 2} up to @{text a}
```
```    31 *}
```
```    32
```
```    33 declare d22set.simps [simp del]
```
```    34
```
```    35
```
```    36 lemma d22set_induct:
```
```    37   assumes "!!a. P {} a"
```
```    38     and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a"
```
```    39   shows "P (d22set u) u"
```
```    40   apply (rule d22set.induct)
```
```    41   apply safe
```
```    42    prefer 2
```
```    43    apply (case_tac "1 < a")
```
```    44     apply (rule_tac prems)
```
```    45      apply (simp_all (no_asm_simp))
```
```    46    apply (simp_all (no_asm_simp) add: d22set.simps prems)
```
```    47   done
```
```    48
```
```    49 lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
```
```    50   apply (induct a rule: d22set_induct)
```
```    51    apply simp
```
```    52   apply (subst d22set.simps)
```
```    53   apply auto
```
```    54   done
```
```    55
```
```    56 lemma d22set_le [rule_format]: "b \<in> d22set a --> b \<le> a"
```
```    57   apply (induct a rule: d22set_induct)
```
```    58   apply simp
```
```    59    apply (subst d22set.simps)
```
```    60    apply auto
```
```    61   done
```
```    62
```
```    63 lemma d22set_le_swap: "a < b ==> b \<notin> d22set a"
```
```    64   by (auto dest: d22set_le)
```
```    65
```
```    66 lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a"
```
```    67   apply (induct a rule: d22set.induct)
```
```    68   apply auto
```
```    69    apply (simp_all add: d22set.simps)
```
```    70   done
```
```    71
```
```    72 lemma d22set_fin: "finite (d22set a)"
```
```    73   apply (induct a rule: d22set_induct)
```
```    74    prefer 2
```
```    75    apply (subst d22set.simps)
```
```    76    apply auto
```
```    77   done
```
```    78
```
```    79
```
```    80 declare zfact.simps [simp del]
```
```    81
```
```    82 lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a"
```
```    83   apply (induct a rule: d22set.induct)
```
```    84   apply safe
```
```    85    apply (simp add: d22set.simps zfact.simps)
```
```    86   apply (subst d22set.simps)
```
```    87   apply (subst zfact.simps)
```
```    88   apply (case_tac "1 < a")
```
```    89    prefer 2
```
```    90    apply (simp add: d22set.simps zfact.simps)
```
```    91   apply (simp add: d22set_fin d22set_le_swap)
```
```    92   done
```
```    93
```
```    94 end
```