25963
|
1 |
(* Title: HOL/ex/Efficient_Nat_examples.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Simple examples for Efficient\_Nat theory. *}
|
|
7 |
|
|
8 |
theory Efficient_Nat_examples
|
26469
|
9 |
imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat
|
25963
|
10 |
begin
|
|
11 |
|
|
12 |
fun
|
|
13 |
to_n :: "nat \<Rightarrow> nat list"
|
|
14 |
where
|
|
15 |
"to_n 0 = []"
|
|
16 |
| "to_n (Suc 0) = []"
|
|
17 |
| "to_n (Suc (Suc 0)) = []"
|
|
18 |
| "to_n (Suc n) = n # to_n n"
|
|
19 |
|
|
20 |
definition
|
|
21 |
naive_prime :: "nat \<Rightarrow> bool"
|
|
22 |
where
|
|
23 |
"naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
|
|
24 |
|
|
25 |
primrec
|
|
26 |
fac :: "nat \<Rightarrow> nat"
|
|
27 |
where
|
|
28 |
"fac 0 = 1"
|
|
29 |
| "fac (Suc n) = Suc n * fac n"
|
|
30 |
|
|
31 |
primrec
|
|
32 |
rat_of_nat :: "nat \<Rightarrow> rat"
|
|
33 |
where
|
|
34 |
"rat_of_nat 0 = 0"
|
|
35 |
| "rat_of_nat (Suc n) = rat_of_nat n + 1"
|
|
36 |
|
|
37 |
primrec
|
|
38 |
harmonic :: "nat \<Rightarrow> rat"
|
|
39 |
where
|
|
40 |
"harmonic 0 = 0"
|
|
41 |
| "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n"
|
|
42 |
|
|
43 |
lemma "harmonic 200 \<ge> 5"
|
|
44 |
by eval
|
|
45 |
|
|
46 |
lemma "harmonic 200 \<ge> 5"
|
|
47 |
by evaluation
|
|
48 |
|
|
49 |
lemma "harmonic 20 \<ge> 3"
|
|
50 |
by normalization
|
|
51 |
|
|
52 |
lemma "naive_prime 89"
|
|
53 |
by eval
|
|
54 |
|
|
55 |
lemma "naive_prime 89"
|
|
56 |
by evaluation
|
|
57 |
|
|
58 |
lemma "naive_prime 89"
|
|
59 |
by normalization
|
|
60 |
|
|
61 |
lemma "\<not> naive_prime 87"
|
|
62 |
by eval
|
|
63 |
|
|
64 |
lemma "\<not> naive_prime 87"
|
|
65 |
by evaluation
|
|
66 |
|
|
67 |
lemma "\<not> naive_prime 87"
|
|
68 |
by normalization
|
|
69 |
|
|
70 |
lemma "fac 10 > 3000000"
|
|
71 |
by eval
|
|
72 |
|
|
73 |
lemma "fac 10 > 3000000"
|
|
74 |
by evaluation
|
|
75 |
|
|
76 |
lemma "fac 10 > 3000000"
|
|
77 |
by normalization
|
|
78 |
|
|
79 |
end
|