src/HOL/Old_Number_Theory/IntFact.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 38159 e9b4835a54ee
child 58889 5b7a9633cfa8
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/Old_Number_Theory/IntFact.thy
     2     Author:     Thomas M. Rasmussen
     3     Copyright   2000  University of Cambridge
     4 *)
     5 
     6 header {* Factorial on integers *}
     7 
     8 theory IntFact
     9 imports IntPrimes
    10 begin
    11 
    12 text {*
    13   Factorial on integers and recursively defined set including all
    14   Integers from @{text 2} up to @{text a}.  Plus definition of product
    15   of finite set.
    16 
    17   \bigskip
    18 *}
    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 {*
    28   \medskip @{term d22set} --- recursively defined set including all
    29   integers from @{text 2} up to @{text a}
    30 *}
    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