src/HOL/NumberTheory/IntFact.thy
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 18369 694ea14ab4f2
permissions -rw-r--r--
moved Finite_Set before Datatype
     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 imports IntPrimes begin
    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   d22set :: "int => int set"
    22 
    23 recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
    24   "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
    25 
    26 recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
    27   "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
    28 
    29 
    30 text {*
    31   \medskip @{term d22set} --- recursively defined set including all
    32   integers from @{text 2} up to @{text a}
    33 *}
    34 
    35 declare d22set.simps [simp del]
    36 
    37 
    38 lemma d22set_induct:
    39   assumes "!!a. P {} a"
    40     and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a"
    41   shows "P (d22set u) u"
    42   apply (rule d22set.induct)
    43   apply safe
    44    prefer 2
    45    apply (case_tac "1 < a")
    46     apply (rule_tac prems)
    47      apply (simp_all (no_asm_simp))
    48    apply (simp_all (no_asm_simp) add: d22set.simps prems)
    49   done
    50 
    51 lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
    52   apply (induct a rule: d22set_induct)
    53    apply simp
    54   apply (subst d22set.simps)
    55   apply auto
    56   done
    57 
    58 lemma d22set_le [rule_format]: "b \<in> d22set a --> b \<le> a"
    59   apply (induct a rule: d22set_induct)
    60   apply simp
    61    apply (subst d22set.simps)
    62    apply auto
    63   done
    64 
    65 lemma d22set_le_swap: "a < b ==> b \<notin> d22set a"
    66   by (auto dest: d22set_le)
    67 
    68 lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a"
    69   apply (induct a rule: d22set.induct)
    70   apply auto
    71    apply (simp_all add: d22set.simps)
    72   done
    73 
    74 lemma d22set_fin: "finite (d22set a)"
    75   apply (induct a rule: d22set_induct)
    76    prefer 2
    77    apply (subst d22set.simps)
    78    apply auto
    79   done
    80 
    81 
    82 declare zfact.simps [simp del]
    83 
    84 lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a"
    85   apply (induct a rule: d22set.induct)
    86   apply safe
    87    apply (simp add: d22set.simps zfact.simps)
    88   apply (subst d22set.simps)
    89   apply (subst zfact.simps)
    90   apply (case_tac "1 < a")
    91    prefer 2
    92    apply (simp add: d22set.simps zfact.simps)
    93   apply (simp add: d22set_fin d22set_le_swap)
    94   done
    95 
    96 end