equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Efficient_Nat_examples.thy |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Simple examples for Efficient\_Nat theory. *} |
|
6 |
|
7 theory Efficient_Nat_examples |
|
8 imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" |
|
9 begin |
|
10 |
|
11 fun to_n :: "nat \<Rightarrow> nat list" where |
|
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 |
|
17 definition naive_prime :: "nat \<Rightarrow> bool" where |
|
18 "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []" |
|
19 |
|
20 primrec fac :: "nat \<Rightarrow> nat" where |
|
21 "fac 0 = 1" |
|
22 | "fac (Suc n) = Suc n * fac n" |
|
23 |
|
24 primrec rat_of_nat :: "nat \<Rightarrow> rat" where |
|
25 "rat_of_nat 0 = 0" |
|
26 | "rat_of_nat (Suc n) = rat_of_nat n + 1" |
|
27 |
|
28 primrec harmonic :: "nat \<Rightarrow> rat" where |
|
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 20 \<ge> 3" |
|
36 by normalization |
|
37 |
|
38 lemma "naive_prime 89" |
|
39 by eval |
|
40 |
|
41 lemma "naive_prime 89" |
|
42 by normalization |
|
43 |
|
44 lemma "\<not> naive_prime 87" |
|
45 by eval |
|
46 |
|
47 lemma "\<not> naive_prime 87" |
|
48 by normalization |
|
49 |
|
50 lemma "fac 10 > 3000000" |
|
51 by eval |
|
52 |
|
53 lemma "fac 10 > 3000000" |
|
54 by normalization |
|
55 |
|
56 end |
|