|
22525
|
1 |
(* ID: $Id$
|
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
|
3 |
*)
|
|
|
4 |
|
|
|
5 |
header {* Small examples for evaluation mechanisms *}
|
|
|
6 |
|
|
|
7 |
theory Eval_examples
|
|
|
8 |
imports Eval
|
|
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
text {* evaluation oracle *}
|
|
|
12 |
|
|
|
13 |
lemma "True \<or> False" by eval
|
|
|
14 |
lemma "\<not> (Suc 0 = Suc 1)" by eval
|
|
|
15 |
|
|
|
16 |
text {* term evaluation *}
|
|
|
17 |
|
|
22804
|
18 |
value (overloaded) "(Suc 2 + 1) * 4"
|
|
|
19 |
value (overloaded) "(Suc 2 + 1) * 4"
|
|
|
20 |
value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
|
|
|
21 |
value (overloaded) "[]::nat list"
|
|
|
22 |
value (overloaded) "fst ([]::nat list, Suc 0) = []"
|
|
22525
|
23 |
|
|
|
24 |
text {* a fancy datatype *}
|
|
|
25 |
|
|
|
26 |
datatype ('a, 'b) bair =
|
|
|
27 |
Bair "'a\<Colon>order" 'b
|
|
|
28 |
| Shift "('a, 'b) cair"
|
|
|
29 |
| Dummy unit
|
|
|
30 |
and ('a, 'b) cair =
|
|
|
31 |
Cair 'a 'b
|
|
|
32 |
|
|
22804
|
33 |
value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
|
|
22525
|
34 |
|
|
|
35 |
end |