author | blanchet |
Tue, 10 Jun 2014 11:38:53 +0200 | |
changeset 57199 | 472360558b22 |
parent 51143 | 0a2371e7ced3 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
47108
diff
changeset
|
1 |
(* Title: HOL/ex/Code_Binary_Nat_examples.thy |
47108 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50023
diff
changeset
|
5 |
header {* Simple examples for natural numbers implemented in binary representation. *} |
47108 | 6 |
|
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
47108
diff
changeset
|
7 |
theory Code_Binary_Nat_examples |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50023
diff
changeset
|
8 |
imports Complex_Main "~~/src/HOL/Library/Code_Binary_Nat" |
47108 | 9 |
begin |
10 |
||
11 |
fun to_n :: "nat \<Rightarrow> nat list" |
|
12 |
where |
|
13 |
"to_n 0 = []" |
|
14 |
| "to_n (Suc 0) = []" |
|
15 |
| "to_n (Suc (Suc 0)) = []" |
|
16 |
| "to_n (Suc n) = n # to_n n" |
|
17 |
||
18 |
definition naive_prime :: "nat \<Rightarrow> bool" |
|
19 |
where |
|
20 |
"naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []" |
|
21 |
||
22 |
primrec fac :: "nat \<Rightarrow> nat" |
|
23 |
where |
|
24 |
"fac 0 = 1" |
|
25 |
| "fac (Suc n) = Suc n * fac n" |
|
26 |
||
27 |
primrec harmonic :: "nat \<Rightarrow> rat" |
|
28 |
where |
|
29 |
"harmonic 0 = 0" |
|
30 |
| "harmonic (Suc n) = 1 / of_nat (Suc n) + harmonic n" |
|
31 |
||
32 |
lemma "harmonic 200 \<ge> 5" |
|
33 |
by eval |
|
34 |
||
35 |
lemma "(let (q, r) = quotient_of (harmonic 8) in q div r) \<ge> 2" |
|
36 |
by normalization |
|
37 |
||
38 |
lemma "naive_prime 89" |
|
39 |
by eval |
|
40 |
||
41 |
lemma "naive_prime 89" |
|
42 |
by normalization |
|
43 |
||
44 |
lemma "\<not> naive_prime 87" |
|
45 |
by eval |
|
46 |
||
47 |
lemma "\<not> naive_prime 87" |
|
48 |
by normalization |
|
49 |
||
50 |
lemma "fac 10 > 3000000" |
|
51 |
by eval |
|
52 |
||
53 |
lemma "fac 10 > 3000000" |
|
54 |
by normalization |
|
55 |
||
56 |
end |
|
57 |