src/HOL/ex/Efficient_Nat_examples.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45170 7dd207fe7b6e
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     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 20 \<ge> 3"
    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