src/HOL/Old_Number_Theory/IntFact.thy
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 32479 521cc9bf2958
child 35440 bdf8ad377877
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
     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