author | haftmann |
Mon, 08 Oct 2007 22:03:28 +0200 | |
changeset 24916 | dc56dd1b3cda |
parent 24835 | 8c26128f8997 |
child 25099 | b2c19b9964db |
permissions | -rw-r--r-- |
23268 | 1 |
(* ID: $Id$ |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Small examples for evaluation mechanisms *} |
|
6 |
||
7 |
theory Eval_Examples |
|
24659 | 8 |
imports Eval "~~/src/HOL/Real/Rational" |
23268 | 9 |
begin |
10 |
||
24292 | 11 |
text {* SML evaluation oracle *} |
12 |
||
13 |
lemma "True \<or> False" by evaluation |
|
14 |
lemma "\<not> (Suc 0 = Suc 1)" by evaluation |
|
15 |
lemma "[] = ([]\<Colon> int list)" by evaluation |
|
16 |
lemma "[()] = [()]" by evaluation |
|
17 |
lemma "fst ([]::nat list, Suc 0) = []" by evaluation |
|
18 |
||
23268 | 19 |
text {* evaluation oracle *} |
20 |
||
21 |
lemma "True \<or> False" by eval |
|
22 |
lemma "\<not> (Suc 0 = Suc 1)" by eval |
|
24280 | 23 |
lemma "[] = ([]\<Colon> int list)" by eval |
24 |
lemma "[()] = [()]" by eval |
|
24292 | 25 |
lemma "fst ([]::nat list, Suc 0) = []" by eval |
23268 | 26 |
|
27 |
text {* term evaluation *} |
|
28 |
||
24587 | 29 |
value "(Suc 2 + 1) * 4" |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
30 |
value (code) "(Suc 2 + 1) * 4" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
31 |
value (SML) "(Suc 2 + 1) * 4" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
32 |
value ("normal_form") "(Suc 2 + 1) * 4" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
33 |
|
24587 | 34 |
value "(Suc 2 + Suc 0) * Suc 3" |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
35 |
value (code) "(Suc 2 + Suc 0) * Suc 3" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
36 |
value (SML) "(Suc 2 + Suc 0) * Suc 3" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
37 |
value ("normal_form") "(Suc 2 + Suc 0) * Suc 3" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
38 |
|
24587 | 39 |
value "nat 100" |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
40 |
value (code) "nat 100" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
41 |
value (SML) "nat 100" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
42 |
value ("normal_form") "nat 100" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
43 |
|
24587 | 44 |
value "(10\<Colon>int) \<le> 12" |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
45 |
value (code) "(10\<Colon>int) \<le> 12" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
46 |
value (SML) "(10\<Colon>int) \<le> 12" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
47 |
value ("normal_form") "(10\<Colon>int) \<le> 12" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
48 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
49 |
value "max (2::int) 4" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
50 |
value (code) "max (2::int) 4" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
51 |
value (SML) "max (2::int) 4" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
52 |
value ("normal_form") "max (2::int) 4" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
53 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
54 |
value "of_int 2 / of_int 4 * (1::rat)" |
24916 | 55 |
(*value (code) "of_int 2 / of_int 4 * (1::rat)"*) |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
56 |
value (SML) "of_int 2 / of_int 4 * (1::rat)" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
57 |
value ("normal_form") "of_int 2 / of_int 4 * (1::rat)" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
58 |
|
24587 | 59 |
value "[]::nat list" |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
60 |
value (code) "[]::nat list" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
61 |
(*value (SML) "[]::nat list" FIXME*) |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
62 |
value ("normal_form") "[]::nat list" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
63 |
|
24587 | 64 |
value "[(nat 100, ())]" |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
65 |
value (code) "[(nat 100, ())]" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
66 |
(*value (SML) "[(nat 100, ())]" FIXME*) |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
67 |
value ("normal_form") "[(nat 100, ())]" |
24659 | 68 |
|
23268 | 69 |
|
70 |
text {* a fancy datatype *} |
|
71 |
||
72 |
datatype ('a, 'b) bair = |
|
73 |
Bair "'a\<Colon>order" 'b |
|
74 |
| Shift "('a, 'b) cair" |
|
75 |
| Dummy unit |
|
76 |
and ('a, 'b) cair = |
|
77 |
Cair 'a 'b |
|
78 |
||
24587 | 79 |
value "Shift (Cair (4::nat) [Suc 0])" |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
80 |
value (code) "Shift (Cair (4::nat) [Suc 0])" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
81 |
value (SML) "Shift (Cair (4::nat) [Suc 0])" |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
82 |
value ("normal_form") "Shift (Cair (4::nat) [Suc 0])" |
23268 | 83 |
|
84 |
end |