1(* Title: HOL/ex/Code_Binary_Nat_examples.thy 2 Author: Florian Haftmann, TU Muenchen 3*) 4 5section \<open>Simple examples for natural numbers implemented in binary representation.\<close> 6 7theory Code_Binary_Nat_examples 8imports Complex_Main "HOL-Library.Code_Binary_Nat" 9begin 10 11fun to_n :: "nat \<Rightarrow> nat list" 12where 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 18definition naive_prime :: "nat \<Rightarrow> bool" 19where 20 "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []" 21 22primrec fac :: "nat \<Rightarrow> nat" 23where 24 "fac 0 = 1" 25| "fac (Suc n) = Suc n * fac n" 26 27primrec harmonic :: "nat \<Rightarrow> rat" 28where 29 "harmonic 0 = 0" 30| "harmonic (Suc n) = 1 / of_nat (Suc n) + harmonic n" 31 32lemma "harmonic 200 \<ge> 5" 33 by eval 34 35lemma "(let (q, r) = quotient_of (harmonic 8) in q div r) \<ge> 2" 36 by normalization 37 38lemma "naive_prime 89" 39 by eval 40 41lemma "naive_prime 89" 42 by normalization 43 44lemma "\<not> naive_prime 87" 45 by eval 46 47lemma "\<not> naive_prime 87" 48 by normalization 49 50lemma "fac 10 > 3000000" 51 by eval 52 53lemma "fac 10 > 3000000" 54 by normalization 55 56end 57 58