author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 45170 | 7dd207fe7b6e |
child 56927 | 4044a7d1720f |
permissions | -rw-r--r-- |
30021 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
23268 | 2 |
|
3 |
header {* Small examples for evaluation mechanisms *} |
|
4 |
||
5 |
theory Eval_Examples |
|
32067 | 6 |
imports Complex_Main |
23268 | 7 |
begin |
8 |
||
25099 | 9 |
text {* evaluation oracle *} |
10 |
||
11 |
lemma "True \<or> False" by eval |
|
40760 | 12 |
lemma "Suc 0 \<noteq> Suc 1" by eval |
13 |
lemma "[] = ([] :: int list)" by eval |
|
25099 | 14 |
lemma "[()] = [()]" by eval |
40760 | 15 |
lemma "fst ([] :: nat list, Suc 0) = []" by eval |
25099 | 16 |
|
17 |
text {* normalization *} |
|
23268 | 18 |
|
25099 | 19 |
lemma "True \<or> False" by normalization |
40760 | 20 |
lemma "Suc 0 \<noteq> Suc 1" by normalization |
21 |
lemma "[] = ([] :: int list)" by normalization |
|
25099 | 22 |
lemma "[()] = [()]" by normalization |
40760 | 23 |
lemma "fst ([] :: nat list, Suc 0) = []" by normalization |
23268 | 24 |
|
25 |
text {* term evaluation *} |
|
26 |
||
24587 | 27 |
value "(Suc 2 + 1) * 4" |
28227 | 28 |
value [code] "(Suc 2 + 1) * 4" |
29 |
value [nbe] "(Suc 2 + 1) * 4" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
30 |
|
24587 | 31 |
value "(Suc 2 + Suc 0) * Suc 3" |
28227 | 32 |
value [code] "(Suc 2 + Suc 0) * Suc 3" |
33 |
value [nbe] "(Suc 2 + Suc 0) * Suc 3" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
34 |
|
24587 | 35 |
value "nat 100" |
28227 | 36 |
value [code] "nat 100" |
37 |
value [nbe] "nat 100" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
38 |
|
40760 | 39 |
value "(10::int) \<le> 12" |
40 |
value [code] "(10::int) \<le> 12" |
|
41 |
value [nbe] "(10::int) \<le> 12" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
42 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
43 |
value "max (2::int) 4" |
28227 | 44 |
value [code] "max (2::int) 4" |
45 |
value [nbe] "max (2::int) 4" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
46 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
47 |
value "of_int 2 / of_int 4 * (1::rat)" |
28227 | 48 |
value [code] "of_int 2 / of_int 4 * (1::rat)" |
49 |
value [nbe] "of_int 2 / of_int 4 * (1::rat)" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
50 |
|
40760 | 51 |
value "[] :: nat list" |
52 |
value [code] "[] :: nat list" |
|
53 |
value [nbe] "[] :: nat list" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
54 |
|
24587 | 55 |
value "[(nat 100, ())]" |
28227 | 56 |
value [code] "[(nat 100, ())]" |
57 |
value [nbe] "[(nat 100, ())]" |
|
24659 | 58 |
|
23268 | 59 |
text {* a fancy datatype *} |
60 |
||
40757 | 61 |
datatype ('a, 'b) foo = |
62 |
Foo "'a\<Colon>order" 'b |
|
63 |
| Bla "('a, 'b) bar" |
|
64 |
| Dummy nat |
|
65 |
and ('a, 'b) bar = |
|
66 |
Bar 'a 'b |
|
67 |
| Blubb "('a, 'b) foo" |
|
23268 | 68 |
|
40757 | 69 |
value "Bla (Bar (4::nat) [Suc 0])" |
70 |
value [code] "Bla (Bar (4::nat) [Suc 0])" |
|
71 |
value [nbe] "Bla (Bar (4::nat) [Suc 0])" |
|
23268 | 72 |
|
73 |
end |