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"
|
|
30 |
value "(Suc 2 + 1) * 4"
|
|
31 |
value "(Suc 2 + Suc 0) * Suc 3"
|
|
32 |
value "nat 100"
|
|
33 |
value "(10\<Colon>int) \<le> 12"
|
|
34 |
value "[]::nat list"
|
|
35 |
value "[(nat 100, ())]"
|
|
36 |
value "max (2::int) 4"
|
24659
|
37 |
value "of_int 2 / of_int 4 * (1::rat)"
|
|
38 |
|
23268
|
39 |
|
|
40 |
text {* a fancy datatype *}
|
|
41 |
|
|
42 |
datatype ('a, 'b) bair =
|
|
43 |
Bair "'a\<Colon>order" 'b
|
|
44 |
| Shift "('a, 'b) cair"
|
|
45 |
| Dummy unit
|
|
46 |
and ('a, 'b) cair =
|
|
47 |
Cair 'a 'b
|
|
48 |
|
24587
|
49 |
value "Shift (Cair (4::nat) [Suc 0])"
|
23268
|
50 |
|
|
51 |
end
|