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