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
haftmann@25963
     1
(*  Title:      HOL/ex/Efficient_Nat_examples.thy
haftmann@25963
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@25963
     3
*)
haftmann@25963
     4
haftmann@28523
     5
header {* Simple examples for Efficient\_Nat theory. *}
haftmann@25963
     6
haftmann@25963
     7
theory Efficient_Nat_examples
wenzelm@41413
     8
imports Complex_Main "~~/src/HOL/Library/Efficient_Nat"
haftmann@25963
     9
begin
haftmann@25963
    10
haftmann@28661
    11
fun to_n :: "nat \<Rightarrow> nat list" where
haftmann@25963
    12
  "to_n 0 = []"
haftmann@25963
    13
  | "to_n (Suc 0) = []"
haftmann@25963
    14
  | "to_n (Suc (Suc 0)) = []"
haftmann@25963
    15
  | "to_n (Suc n) = n # to_n n"
haftmann@25963
    16
haftmann@28661
    17
definition naive_prime :: "nat \<Rightarrow> bool" where
haftmann@25963
    18
  "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
haftmann@25963
    19
haftmann@28661
    20
primrec fac :: "nat \<Rightarrow> nat" where
haftmann@25963
    21
  "fac 0 = 1"
haftmann@25963
    22
  | "fac (Suc n) = Suc n * fac n"
haftmann@25963
    23
haftmann@28661
    24
primrec rat_of_nat :: "nat \<Rightarrow> rat" where
haftmann@25963
    25
  "rat_of_nat 0 = 0"
haftmann@25963
    26
  | "rat_of_nat (Suc n) = rat_of_nat n + 1"
haftmann@25963
    27
haftmann@28661
    28
primrec harmonic :: "nat \<Rightarrow> rat" where
haftmann@25963
    29
  "harmonic 0 = 0"
haftmann@25963
    30
  | "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n"
haftmann@25963
    31
haftmann@25963
    32
lemma "harmonic 200 \<ge> 5"
haftmann@25963
    33
  by eval
haftmann@25963
    34
haftmann@25963
    35
lemma "harmonic 20 \<ge> 3"
haftmann@25963
    36
  by normalization
haftmann@25963
    37
haftmann@25963
    38
lemma "naive_prime 89"
haftmann@25963
    39
  by eval
haftmann@25963
    40
haftmann@25963
    41
lemma "naive_prime 89"
haftmann@25963
    42
  by normalization
haftmann@25963
    43
haftmann@25963
    44
lemma "\<not> naive_prime 87"
haftmann@25963
    45
  by eval
haftmann@25963
    46
haftmann@25963
    47
lemma "\<not> naive_prime 87"
haftmann@25963
    48
  by normalization
haftmann@25963
    49
haftmann@25963
    50
lemma "fac 10 > 3000000"
haftmann@25963
    51
  by eval
haftmann@25963
    52
haftmann@25963
    53
lemma "fac 10 > 3000000"
haftmann@25963
    54
  by normalization
haftmann@25963
    55
haftmann@25963
    56
end