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