src/HOL/ex/Efficient_Nat_examples.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 41413 64cd30d6b0b8 child 45170 7dd207fe7b6e permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
```     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 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
```