src/HOL/ex/Efficient_Nat_examples.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29938 a0e54cf21fd4
child 41413 64cd30d6b0b8
permissions -rw-r--r--
added lemmas
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
haftmann@29938
     8
imports Complex_Main 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 200 \<ge> 5"
haftmann@25963
    36
  by evaluation
haftmann@25963
    37
haftmann@25963
    38
lemma "harmonic 20 \<ge> 3"
haftmann@25963
    39
  by normalization
haftmann@25963
    40
haftmann@25963
    41
lemma "naive_prime 89"
haftmann@25963
    42
  by eval
haftmann@25963
    43
haftmann@25963
    44
lemma "naive_prime 89"
haftmann@25963
    45
  by evaluation
haftmann@25963
    46
haftmann@25963
    47
lemma "naive_prime 89"
haftmann@25963
    48
  by normalization
haftmann@25963
    49
haftmann@25963
    50
lemma "\<not> naive_prime 87"
haftmann@25963
    51
  by eval
haftmann@25963
    52
haftmann@25963
    53
lemma "\<not> naive_prime 87"
haftmann@25963
    54
  by evaluation
haftmann@25963
    55
haftmann@25963
    56
lemma "\<not> naive_prime 87"
haftmann@25963
    57
  by normalization
haftmann@25963
    58
haftmann@25963
    59
lemma "fac 10 > 3000000"
haftmann@25963
    60
  by eval
haftmann@25963
    61
haftmann@25963
    62
lemma "fac 10 > 3000000"
haftmann@25963
    63
  by evaluation
haftmann@25963
    64
haftmann@25963
    65
lemma "fac 10 > 3000000"
haftmann@25963
    66
  by normalization
haftmann@25963
    67
haftmann@25963
    68
end