src/HOL/ex/Code_Binary_Nat_examples.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 51143 0a2371e7ced3
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/ex/Code_Binary_Nat_examples.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Simple examples for natural numbers implemented in binary representation. *}
     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