author | wenzelm |
Sat, 20 Aug 2011 23:36:18 +0200 | |
changeset 44339 | eda6aef75939 |
parent 38159 | e9b4835a54ee |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
38159 | 1 |
(* Title: HOL/Old_Number_Theory/IntFact.thy |
2 |
Author: Thomas M. Rasmussen |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
3 |
Copyright 2000 University of Cambridge |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
4 |
*) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
5 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
6 |
header {* Factorial on integers *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
7 |
|
38159 | 8 |
theory IntFact |
9 |
imports IntPrimes |
|
10 |
begin |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
11 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
12 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
13 |
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
|
14 |
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
|
15 |
of finite set. |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
16 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
17 |
\bigskip |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
18 |
*} |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
19 |
|
38159 | 20 |
fun zfact :: "int => int" |
21 |
where "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
|
22 |
|
38159 | 23 |
fun d22set :: "int => int set" |
24 |
where "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
|
25 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
26 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
27 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
28 |
\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
|
29 |
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
|
30 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
31 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
32 |
declare d22set.simps [simp del] |
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 |
lemma d22set_induct: |
18369 | 36 |
assumes "!!a. P {} a" |
37 |
and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a" |
|
38 |
shows "P (d22set u) u" |
|
39 |
apply (rule d22set.induct) |
|
35440 | 40 |
apply (case_tac "1 < a") |
41 |
apply (rule_tac assms) |
|
42 |
apply (simp_all (no_asm_simp)) |
|
43 |
apply (simp_all (no_asm_simp) add: d22set.simps assms) |
|
18369 | 44 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
45 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
46 |
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
|
47 |
apply (induct a rule: d22set_induct) |
18369 | 48 |
apply simp |
49 |
apply (subst d22set.simps) |
|
50 |
apply auto |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
51 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
52 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
53 |
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
|
54 |
apply (induct a rule: d22set_induct) |
18369 | 55 |
apply simp |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
56 |
apply (subst d22set.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
57 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
58 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
59 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
60 |
lemma d22set_le_swap: "a < b ==> b \<notin> d22set a" |
18369 | 61 |
by (auto dest: d22set_le) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
62 |
|
18369 | 63 |
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
|
64 |
apply (induct a rule: d22set.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
65 |
apply auto |
35440 | 66 |
apply (subst d22set.simps) |
67 |
apply (case_tac "b < a", auto) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
68 |
done |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
69 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
70 |
lemma d22set_fin: "finite (d22set a)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
71 |
apply (induct a rule: d22set_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
72 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
73 |
apply (subst d22set.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
74 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
75 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
76 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
77 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
78 |
declare zfact.simps [simp del] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
79 |
|
15392 | 80 |
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
|
81 |
apply (induct a rule: d22set.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
82 |
apply (subst d22set.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
83 |
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
|
84 |
apply (case_tac "1 < a") |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
85 |
prefer 2 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
86 |
apply (simp add: d22set.simps zfact.simps) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
87 |
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
|
88 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
89 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9508
diff
changeset
|
90 |
end |