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
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
haftmann@51143
     5
header {* 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 \<Rightarrow> 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 \<Rightarrow> bool"
huffman@47108
    19
where
huffman@47108
    20
  "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
huffman@47108
    21
huffman@47108
    22
primrec fac :: "nat \<Rightarrow> 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 \<Rightarrow> 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 \<ge> 5"
huffman@47108
    33
  by eval
huffman@47108
    34
huffman@47108
    35
lemma "(let (q, r) = quotient_of (harmonic 8) in q div r) \<ge> 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 "\<not> naive_prime 87"
huffman@47108
    45
  by eval
huffman@47108
    46
huffman@47108
    47
lemma "\<not> 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