src/HOL/NumberTheory/IntFact.thy
author wenzelm
Tue, 21 Oct 2008 23:54:42 +0200
changeset 28659 b4fd14ae8b8a
parent 18369 694ea14ab4f2
permissions -rw-r--r--
less ambitious default for JEDIT_JAVA_OPTIONS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
     1
(*  Title:      HOL/NumberTheory/IntFact.thy
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     2
    ID:         $Id$
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
     3
    Author:     Thomas M. Rasmussen
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
     4
    Copyright   2000  University of Cambridge
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     5
*)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     6
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
     7
header {* Factorial on integers *}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
     8
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15392
diff changeset
     9
theory IntFact imports IntPrimes begin
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    10
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    11
text {*
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    12
  Factorial on integers and recursively defined set including all
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11549
diff changeset
    13
  Integers from @{text 2} up to @{text a}.  Plus definition of product
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    14
  of finite set.
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    15
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    16
  \bigskip
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    17
*}
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    18
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    19
consts
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    20
  zfact :: "int => int"
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    21
  d22set :: "int => int set"
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    22
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    23
recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11701
diff changeset
    24
  "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    25
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    26
recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11701
diff changeset
    27
  "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    28
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    29
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    30
text {*
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    31
  \medskip @{term d22set} --- recursively defined set including all
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11549
diff changeset
    32
  integers from @{text 2} up to @{text a}
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    33
*}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    34
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    35
declare d22set.simps [simp del]
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    36
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    37
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    38
lemma d22set_induct:
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    39
  assumes "!!a. P {} a"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    40
    and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    41
  shows "P (d22set u) u"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    42
  apply (rule d22set.induct)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    43
  apply safe
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    44
   prefer 2
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    45
   apply (case_tac "1 < a")
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    46
    apply (rule_tac prems)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    47
     apply (simp_all (no_asm_simp))
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    48
   apply (simp_all (no_asm_simp) add: d22set.simps prems)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    49
  done
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    50
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11701
diff changeset
    51
lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    52
  apply (induct a rule: d22set_induct)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    53
   apply simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    54
  apply (subst d22set.simps)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    55
  apply auto
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    56
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    57
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    58
lemma d22set_le [rule_format]: "b \<in> d22set a --> b \<le> a"
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    59
  apply (induct a rule: d22set_induct)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    60
  apply simp
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    61
   apply (subst d22set.simps)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    62
   apply auto
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    63
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    64
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    65
lemma d22set_le_swap: "a < b ==> b \<notin> d22set a"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    66
  by (auto dest: d22set_le)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    67
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16417
diff changeset
    68
lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    69
  apply (induct a rule: d22set.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    70
  apply auto
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    71
   apply (simp_all add: d22set.simps)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    72
  done
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    73
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    74
lemma d22set_fin: "finite (d22set a)"
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    75
  apply (induct a rule: d22set_induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    76
   prefer 2
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    77
   apply (subst d22set.simps)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    78
   apply auto
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    79
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    80
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    81
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    82
declare zfact.simps [simp del]
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    83
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14271
diff changeset
    84
lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    85
  apply (induct a rule: d22set.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    86
  apply safe
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    87
   apply (simp add: d22set.simps zfact.simps)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    88
  apply (subst d22set.simps)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    89
  apply (subst zfact.simps)
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11701
diff changeset
    90
  apply (case_tac "1 < a")
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    91
   prefer 2
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    92
   apply (simp add: d22set.simps zfact.simps)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    93
  apply (simp add: d22set_fin d22set_le_swap)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    94
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    95
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 9508
diff changeset
    96
end