src/HOL/NumberTheory/IntFact.thy
author wenzelm
Tue Sep 04 21:10:57 2001 +0200 (2001-09-04)
changeset 11549 e7265e70fd7c
parent 11049 7eef34adb852
child 11701 3d51fbf81c17
permissions -rw-r--r--
renamed "antecedent" case to "rule_context";
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
wenzelm@11049
     9
theory IntFact = IntPrimes:
wenzelm@11049
    10
wenzelm@11049
    11
text {*
wenzelm@11049
    12
  Factorial on integers and recursively defined set including all
wenzelm@11049
    13
  Integers from @{term 2} up to @{term 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
  setprod :: "int set => int"
wenzelm@11049
    22
  d22set :: "int => int set"
paulson@9508
    23
wenzelm@11049
    24
recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
wenzelm@11049
    25
  "zfact n = (if n \<le> #0 then #1 else n * zfact (n - #1))"
paulson@9508
    26
paulson@9508
    27
defs
wenzelm@11049
    28
  setprod_def: "setprod A == (if finite A then fold (op *) #1 A else #1)"
wenzelm@11049
    29
wenzelm@11049
    30
recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
wenzelm@11049
    31
  "d22set a = (if #1 < a then insert a (d22set (a - #1)) else {})"
wenzelm@11049
    32
wenzelm@11049
    33
wenzelm@11049
    34
text {* \medskip @{term setprod} --- product of finite set *}
wenzelm@11049
    35
wenzelm@11049
    36
lemma setprod_empty [simp]: "setprod {} = #1"
wenzelm@11049
    37
  apply (simp add: setprod_def)
wenzelm@11049
    38
  done
wenzelm@11049
    39
wenzelm@11049
    40
lemma setprod_insert [simp]:
wenzelm@11049
    41
    "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
wenzelm@11049
    42
  apply (unfold setprod_def)
wenzelm@11049
    43
  apply (simp add: zmult_left_commute fold_insert [standard])
wenzelm@11049
    44
  done
wenzelm@11049
    45
wenzelm@11049
    46
wenzelm@11049
    47
text {*
wenzelm@11049
    48
  \medskip @{term d22set} --- recursively defined set including all
wenzelm@11049
    49
  integers from @{term 2} up to @{term a}
wenzelm@11049
    50
*}
wenzelm@11049
    51
wenzelm@11049
    52
declare d22set.simps [simp del]
wenzelm@11049
    53
wenzelm@11049
    54
wenzelm@11049
    55
lemma d22set_induct:
wenzelm@11049
    56
  "(!!a. P {} a) ==>
wenzelm@11049
    57
    (!!a. #1 < (a::int) ==> P (d22set (a - #1)) (a - #1)
wenzelm@11049
    58
      ==> P (d22set a) a)
wenzelm@11049
    59
    ==> P (d22set u) u"
wenzelm@11049
    60
proof -
wenzelm@11549
    61
  case rule_context
wenzelm@11049
    62
  show ?thesis
wenzelm@11049
    63
    apply (rule d22set.induct)
wenzelm@11049
    64
    apply safe
wenzelm@11049
    65
     apply (case_tac [2] "#1 < a")
wenzelm@11549
    66
      apply (rule_tac [2] rule_context)
wenzelm@11049
    67
       apply (simp_all (no_asm_simp))
wenzelm@11549
    68
     apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
wenzelm@11049
    69
    done
wenzelm@11049
    70
qed
paulson@9508
    71
wenzelm@11049
    72
lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> #1 < b"
wenzelm@11049
    73
  apply (induct a rule: d22set_induct)
wenzelm@11049
    74
   prefer 2
wenzelm@11049
    75
   apply (subst d22set.simps)
wenzelm@11049
    76
   apply auto
wenzelm@11049
    77
  done
wenzelm@11049
    78
wenzelm@11049
    79
lemma d22set_le [rule_format]: "b \<in> d22set a --> b \<le> a"
wenzelm@11049
    80
  apply (induct a rule: d22set_induct)
wenzelm@11049
    81
   prefer 2
wenzelm@11049
    82
   apply (subst d22set.simps)
wenzelm@11049
    83
   apply auto
wenzelm@11049
    84
  done
wenzelm@11049
    85
wenzelm@11049
    86
lemma d22set_le_swap: "a < b ==> b \<notin> d22set a"
wenzelm@11049
    87
  apply (auto dest: d22set_le)
wenzelm@11049
    88
  done
wenzelm@11049
    89
wenzelm@11049
    90
lemma d22set_mem [rule_format]: "#1 < b --> b \<le> a --> b \<in> d22set a"
wenzelm@11049
    91
  apply (induct a rule: d22set.induct)
wenzelm@11049
    92
  apply auto
wenzelm@11049
    93
   apply (simp_all add: d22set.simps)
wenzelm@11049
    94
  done
paulson@9508
    95
wenzelm@11049
    96
lemma d22set_fin: "finite (d22set a)"
wenzelm@11049
    97
  apply (induct a rule: d22set_induct)
wenzelm@11049
    98
   prefer 2
wenzelm@11049
    99
   apply (subst d22set.simps)
wenzelm@11049
   100
   apply auto
wenzelm@11049
   101
  done
wenzelm@11049
   102
wenzelm@11049
   103
wenzelm@11049
   104
declare zfact.simps [simp del]
wenzelm@11049
   105
wenzelm@11049
   106
lemma d22set_prod_zfact: "setprod (d22set a) = zfact a"
wenzelm@11049
   107
  apply (induct a rule: d22set.induct)
wenzelm@11049
   108
  apply safe
wenzelm@11049
   109
   apply (simp add: d22set.simps zfact.simps)
wenzelm@11049
   110
  apply (subst d22set.simps)
wenzelm@11049
   111
  apply (subst zfact.simps)
wenzelm@11049
   112
  apply (case_tac "#1 < a")
wenzelm@11049
   113
   prefer 2
wenzelm@11049
   114
   apply (simp add: d22set.simps zfact.simps)
wenzelm@11049
   115
  apply (simp add: d22set_fin d22set_le_swap)
wenzelm@11049
   116
  done
wenzelm@11049
   117
wenzelm@11049
   118
end