author | haftmann |
Wed, 08 Dec 2010 13:34:50 +0100 | |
changeset 41075 | 4bed56dc95fb |
parent 40760 | 86c43003742d |
child 44022 | 2d633b795d4a |
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 |
|
24292 | 17 |
text {* SML evaluation oracle *} |
18 |
||
19 |
lemma "True \<or> False" by evaluation |
|
40760 | 20 |
lemma "Suc 0 \<noteq> Suc 1" by evaluation |
21 |
lemma "[] = ([] :: int list)" by evaluation |
|
24292 | 22 |
lemma "[()] = [()]" by evaluation |
40760 | 23 |
lemma "fst ([] :: nat list, Suc 0) = []" by evaluation |
24292 | 24 |
|
25099 | 25 |
text {* normalization *} |
23268 | 26 |
|
25099 | 27 |
lemma "True \<or> False" by normalization |
40760 | 28 |
lemma "Suc 0 \<noteq> Suc 1" by normalization |
29 |
lemma "[] = ([] :: int list)" by normalization |
|
25099 | 30 |
lemma "[()] = [()]" by normalization |
40760 | 31 |
lemma "fst ([] :: nat list, Suc 0) = []" by normalization |
23268 | 32 |
|
33 |
text {* term evaluation *} |
|
34 |
||
24587 | 35 |
value "(Suc 2 + 1) * 4" |
28227 | 36 |
value [code] "(Suc 2 + 1) * 4" |
37 |
value [SML] "(Suc 2 + 1) * 4" |
|
38 |
value [nbe] "(Suc 2 + 1) * 4" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
39 |
|
24587 | 40 |
value "(Suc 2 + Suc 0) * Suc 3" |
28227 | 41 |
value [code] "(Suc 2 + Suc 0) * Suc 3" |
42 |
value [SML] "(Suc 2 + Suc 0) * Suc 3" |
|
43 |
value [nbe] "(Suc 2 + Suc 0) * Suc 3" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
44 |
|
24587 | 45 |
value "nat 100" |
28227 | 46 |
value [code] "nat 100" |
47 |
value [SML] "nat 100" |
|
48 |
value [nbe] "nat 100" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
49 |
|
40760 | 50 |
value "(10::int) \<le> 12" |
51 |
value [code] "(10::int) \<le> 12" |
|
52 |
value [SML] "(10::int) \<le> 12" |
|
53 |
value [nbe] "(10::int) \<le> 12" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
54 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
55 |
value "max (2::int) 4" |
28227 | 56 |
value [code] "max (2::int) 4" |
57 |
value [SML] "max (2::int) 4" |
|
58 |
value [nbe] "max (2::int) 4" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
59 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
60 |
value "of_int 2 / of_int 4 * (1::rat)" |
28227 | 61 |
value [code] "of_int 2 / of_int 4 * (1::rat)" |
62 |
value [SML] "of_int 2 / of_int 4 * (1::rat)" |
|
63 |
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
|
64 |
|
40760 | 65 |
value "[] :: nat list" |
66 |
value [code] "[] :: nat list" |
|
67 |
value [SML] "[] :: nat list" |
|
68 |
value [nbe] "[] :: nat list" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
69 |
|
24587 | 70 |
value "[(nat 100, ())]" |
28227 | 71 |
value [code] "[(nat 100, ())]" |
72 |
value [SML] "[(nat 100, ())]" |
|
73 |
value [nbe] "[(nat 100, ())]" |
|
24659 | 74 |
|
23268 | 75 |
text {* a fancy datatype *} |
76 |
||
40757 | 77 |
datatype ('a, 'b) foo = |
78 |
Foo "'a\<Colon>order" 'b |
|
79 |
| Bla "('a, 'b) bar" |
|
80 |
| Dummy nat |
|
81 |
and ('a, 'b) bar = |
|
82 |
Bar 'a 'b |
|
83 |
| Blubb "('a, 'b) foo" |
|
23268 | 84 |
|
40757 | 85 |
value "Bla (Bar (4::nat) [Suc 0])" |
86 |
value [code] "Bla (Bar (4::nat) [Suc 0])" |
|
87 |
value [SML] "Bla (Bar (4::nat) [Suc 0])" |
|
88 |
value [nbe] "Bla (Bar (4::nat) [Suc 0])" |
|
23268 | 89 |
|
90 |
end |