src/HOL/ex/Efficient_Nat_examples.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 29938 a0e54cf21fd4
child 45170 7dd207fe7b6e
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     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