src/HOL/ex/Code_Binary_Nat_examples.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 58889 5b7a9633cfa8 child 61343 5b5656a63bd6 permissions -rw-r--r--
prefer symbols;
 haftmann@50023 1 (* Title: HOL/ex/Code_Binary_Nat_examples.thy huffman@47108 2 Author: Florian Haftmann, TU Muenchen huffman@47108 3 *) huffman@47108 4 wenzelm@58889 5 section {* Simple examples for natural numbers implemented in binary representation. *} huffman@47108 6 haftmann@50023 7 theory Code_Binary_Nat_examples haftmann@51143 8 imports Complex_Main "~~/src/HOL/Library/Code_Binary_Nat" huffman@47108 9 begin huffman@47108 10 huffman@47108 11 fun to_n :: "nat \ nat list" huffman@47108 12 where huffman@47108 13 "to_n 0 = []" huffman@47108 14 | "to_n (Suc 0) = []" huffman@47108 15 | "to_n (Suc (Suc 0)) = []" huffman@47108 16 | "to_n (Suc n) = n # to_n n" huffman@47108 17 huffman@47108 18 definition naive_prime :: "nat \ bool" huffman@47108 19 where huffman@47108 20 "naive_prime n \ n \ 2 \ filter (\m. n mod m = 0) (to_n n) = []" huffman@47108 21 huffman@47108 22 primrec fac :: "nat \ nat" huffman@47108 23 where huffman@47108 24 "fac 0 = 1" huffman@47108 25 | "fac (Suc n) = Suc n * fac n" huffman@47108 26 huffman@47108 27 primrec harmonic :: "nat \ rat" huffman@47108 28 where huffman@47108 29 "harmonic 0 = 0" huffman@47108 30 | "harmonic (Suc n) = 1 / of_nat (Suc n) + harmonic n" huffman@47108 31 huffman@47108 32 lemma "harmonic 200 \ 5" huffman@47108 33 by eval huffman@47108 34 huffman@47108 35 lemma "(let (q, r) = quotient_of (harmonic 8) in q div r) \ 2" huffman@47108 36 by normalization huffman@47108 37 huffman@47108 38 lemma "naive_prime 89" huffman@47108 39 by eval huffman@47108 40 huffman@47108 41 lemma "naive_prime 89" huffman@47108 42 by normalization huffman@47108 43 huffman@47108 44 lemma "\ naive_prime 87" huffman@47108 45 by eval huffman@47108 46 huffman@47108 47 lemma "\ naive_prime 87" huffman@47108 48 by normalization huffman@47108 49 huffman@47108 50 lemma "fac 10 > 3000000" huffman@47108 51 by eval huffman@47108 52 huffman@47108 53 lemma "fac 10 > 3000000" huffman@47108 54 by normalization huffman@47108 55 huffman@47108 56 end huffman@47108 57