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--
 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 \ 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 \ bool" where ``` haftmann@25963 ` 18` ``` "naive_prime n \ n \ 2 \ filter (\m. n mod m = 0) (to_n n) = []" ``` haftmann@25963 ` 19` haftmann@28661 ` 20` ```primrec fac :: "nat \ 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 \ 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 \ 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 \ 5" ``` haftmann@25963 ` 33` ``` by eval ``` haftmann@25963 ` 34` haftmann@25963 ` 35` ```lemma "harmonic 200 \ 5" ``` haftmann@25963 ` 36` ``` by evaluation ``` haftmann@25963 ` 37` haftmann@25963 ` 38` ```lemma "harmonic 20 \ 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 "\ naive_prime 87" ``` haftmann@25963 ` 51` ``` by eval ``` haftmann@25963 ` 52` haftmann@25963 ` 53` ```lemma "\ naive_prime 87" ``` haftmann@25963 ` 54` ``` by evaluation ``` haftmann@25963 ` 55` haftmann@25963 ` 56` ```lemma "\ 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 ```