1(*  Title:      HOL/ex/Code_Binary_Nat_examples.thy
2    Author:     Florian Haftmann, TU Muenchen
3*)
4
5section \<open>Simple examples for natural numbers implemented in binary representation.\<close>
6
7theory Code_Binary_Nat_examples
8imports Complex_Main "HOL-Library.Code_Binary_Nat"
9begin
10
11fun to_n :: "nat \<Rightarrow> nat list"
12where
13  "to_n 0 = []"
14| "to_n (Suc 0) = []"
15| "to_n (Suc (Suc 0)) = []"
16| "to_n (Suc n) = n # to_n n"
17
18definition naive_prime :: "nat \<Rightarrow> bool"
19where
20  "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
21
22primrec fac :: "nat \<Rightarrow> nat"
23where
24  "fac 0 = 1"
25| "fac (Suc n) = Suc n * fac n"
26
27primrec harmonic :: "nat \<Rightarrow> rat"
28where
29  "harmonic 0 = 0"
30| "harmonic (Suc n) = 1 / of_nat (Suc n) + harmonic n"
31
32lemma "harmonic 200 \<ge> 5"
33  by eval
34
35lemma "(let (q, r) = quotient_of (harmonic 8) in q div r) \<ge> 2"
36  by normalization
37
38lemma "naive_prime 89"
39  by eval
40
41lemma "naive_prime 89"
42  by normalization
43
44lemma "\<not> naive_prime 87"
45  by eval
46
47lemma "\<not> naive_prime 87"
48  by normalization
49
50lemma "fac 10 > 3000000"
51  by eval
52
53lemma "fac 10 > 3000000"
54  by normalization
55
56end
57
58