author | wenzelm |
Wed, 29 Dec 2010 17:34:41 +0100 | |
changeset 41413 | 64cd30d6b0b8 |
parent 29938 | a0e54cf21fd4 |
child 45170 | 7dd207fe7b6e |
permissions | -rw-r--r-- |
25963 | 1 |
(* Title: HOL/ex/Efficient_Nat_examples.thy |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
28523 | 5 |
header {* Simple examples for Efficient\_Nat theory. *} |
25963 | 6 |
|
7 |
theory Efficient_Nat_examples |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
29938
diff
changeset
|
8 |
imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" |
25963 | 9 |
begin |
10 |
||
28661 | 11 |
fun to_n :: "nat \<Rightarrow> nat list" where |
25963 | 12 |
"to_n 0 = []" |
13 |
| "to_n (Suc 0) = []" |
|
14 |
| "to_n (Suc (Suc 0)) = []" |
|
15 |
| "to_n (Suc n) = n # to_n n" |
|
16 |
||
28661 | 17 |
definition naive_prime :: "nat \<Rightarrow> bool" where |
25963 | 18 |
"naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []" |
19 |
||
28661 | 20 |
primrec fac :: "nat \<Rightarrow> nat" where |
25963 | 21 |
"fac 0 = 1" |
22 |
| "fac (Suc n) = Suc n * fac n" |
|
23 |
||
28661 | 24 |
primrec rat_of_nat :: "nat \<Rightarrow> rat" where |
25963 | 25 |
"rat_of_nat 0 = 0" |
26 |
| "rat_of_nat (Suc n) = rat_of_nat n + 1" |
|
27 |
||
28661 | 28 |
primrec harmonic :: "nat \<Rightarrow> rat" where |
25963 | 29 |
"harmonic 0 = 0" |
30 |
| "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n" |
|
31 |
||
32 |
lemma "harmonic 200 \<ge> 5" |
|
33 |
by eval |
|
34 |
||
35 |
lemma "harmonic 200 \<ge> 5" |
|
36 |
by evaluation |
|
37 |
||
38 |
lemma "harmonic 20 \<ge> 3" |
|
39 |
by normalization |
|
40 |
||
41 |
lemma "naive_prime 89" |
|
42 |
by eval |
|
43 |
||
44 |
lemma "naive_prime 89" |
|
45 |
by evaluation |
|
46 |
||
47 |
lemma "naive_prime 89" |
|
48 |
by normalization |
|
49 |
||
50 |
lemma "\<not> naive_prime 87" |
|
51 |
by eval |
|
52 |
||
53 |
lemma "\<not> naive_prime 87" |
|
54 |
by evaluation |
|
55 |
||
56 |
lemma "\<not> naive_prime 87" |
|
57 |
by normalization |
|
58 |
||
59 |
lemma "fac 10 > 3000000" |
|
60 |
by eval |
|
61 |
||
62 |
lemma "fac 10 > 3000000" |
|
63 |
by evaluation |
|
64 |
||
65 |
lemma "fac 10 > 3000000" |
|
66 |
by normalization |
|
67 |
||
68 |
end |