src/HOL/ex/Code_Binary_Nat_examples.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 61343 5b5656a63bd6 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Title:      HOL/ex/Code_Binary_Nat_examples.thy
```
```     2     Author:     Florian Haftmann, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section \<open>Simple examples for natural numbers implemented in binary representation.\<close>
```
```     6
```
```     7 theory Code_Binary_Nat_examples
```
```     8 imports Complex_Main "~~/src/HOL/Library/Code_Binary_Nat"
```
```     9 begin
```
```    10
```
```    11 fun to_n :: "nat \<Rightarrow> nat list"
```
```    12 where
```
```    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
```
```    18 definition naive_prime :: "nat \<Rightarrow> bool"
```
```    19 where
```
```    20   "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
```
```    21
```
```    22 primrec fac :: "nat \<Rightarrow> nat"
```
```    23 where
```
```    24   "fac 0 = 1"
```
```    25 | "fac (Suc n) = Suc n * fac n"
```
```    26
```
```    27 primrec harmonic :: "nat \<Rightarrow> rat"
```
```    28 where
```
```    29   "harmonic 0 = 0"
```
```    30 | "harmonic (Suc n) = 1 / of_nat (Suc n) + harmonic n"
```
```    31
```
```    32 lemma "harmonic 200 \<ge> 5"
```
```    33   by eval
```
```    34
```
```    35 lemma "(let (q, r) = quotient_of (harmonic 8) in q div r) \<ge> 2"
```
```    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
```
```    57
```