1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* Small examples for evaluation mechanisms *}
9 text {* evaluation oracle *}
11 lemma "True \<or> False" by eval
12 lemma "\<not> (Suc 0 = Suc 1)" by eval
13 lemma "[] = ([]\<Colon> int list)" by eval
14 lemma "[()] = [()]" by eval
15 lemma "fst ([]::nat list, Suc 0) = []" by eval
17 text {* SML evaluation oracle *}
19 lemma "True \<or> False" by evaluation
20 lemma "\<not> (Suc 0 = Suc 1)" by evaluation
21 lemma "[] = ([]\<Colon> int list)" by evaluation
22 lemma "[()] = [()]" by evaluation
23 lemma "fst ([]::nat list, Suc 0) = []" by evaluation
25 text {* normalization *}
27 lemma "True \<or> False" by normalization
28 lemma "\<not> (Suc 0 = Suc 1)" by normalization
29 lemma "[] = ([]\<Colon> int list)" by normalization
30 lemma "[()] = [()]" by normalization
31 lemma "fst ([]::nat list, Suc 0) = []" by normalization
33 text {* term evaluation *}
35 value "(Suc 2 + 1) * 4"
36 value [code] "(Suc 2 + 1) * 4"
37 value [SML] "(Suc 2 + 1) * 4"
38 value [nbe] "(Suc 2 + 1) * 4"
40 value "(Suc 2 + Suc 0) * Suc 3"
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"
46 value [code] "nat 100"
50 value "(10\<Colon>int) \<le> 12"
51 value [code] "(10\<Colon>int) \<le> 12"
52 value [SML] "(10\<Colon>int) \<le> 12"
53 value [nbe] "(10\<Colon>int) \<le> 12"
55 value "max (2::int) 4"
56 value [code] "max (2::int) 4"
57 value [SML] "max (2::int) 4"
58 value [nbe] "max (2::int) 4"
60 value "of_int 2 / of_int 4 * (1::rat)"
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)"
66 value [code] "[]::nat list"
67 value [SML] "[]::nat list"
68 value [nbe] "[]::nat list"
70 value "[(nat 100, ())]"
71 value [code] "[(nat 100, ())]"
72 value [SML] "[(nat 100, ())]"
73 value [nbe] "[(nat 100, ())]"
76 text {* a fancy datatype *}
78 datatype ('a, 'b) foo =
79 Foo "'a\<Colon>order" 'b
84 | Blubb "('a, 'b) foo"
86 value "Bla (Bar (4::nat) [Suc 0])"
87 value [code] "Bla (Bar (4::nat) [Suc 0])"
88 value [SML] "Bla (Bar (4::nat) [Suc 0])"
89 value [nbe] "Bla (Bar (4::nat) [Suc 0])"