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