(* Title: HOL/ex/Code_Binary_Nat_examples.thy
Author: Florian Haftmann, TU Muenchen
*)
section \<open>Simple examples for natural numbers implemented in binary representation.\<close>
theory Code_Binary_Nat_examples
imports Complex_Main "HOL-Library.Code_Binary_Nat"
begin
fun to_n :: "nat \ nat list"
where
"to_n 0 = []"
| "to_n (Suc 0) = []"
| "to_n (Suc (Suc 0)) = []"
| "to_n (Suc n) = n # to_n n"
definition naive_prime :: "nat \ bool"
where
"naive_prime n \ n \ 2 \ filter (\m. n mod m = 0) (to_n n) = []"
primrec fac :: "nat \ nat"
where
"fac 0 = 1"
| "fac (Suc n) = Suc n * fac n"
primrec harmonic :: "nat \ rat"
where
"harmonic 0 = 0"
| "harmonic (Suc n) = 1 / of_nat (Suc n) + harmonic n"
lemma "harmonic 200 \ 5"
by eval
lemma "(let (q, r) = quotient_of (harmonic 8) in q div r) \ 2"
by normalization
lemma "naive_prime 89"
by eval
lemma "naive_prime 89"
by normalization
lemma "\ naive_prime 87"
by eval
lemma "\ naive_prime 87"
by normalization
lemma "fac 10 > 3000000"
by eval
lemma "fac 10 > 3000000"
by normalization
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
