1(* Author: Florian Haftmann, TU Muenchen *)
2
3section \<open>Small examples for evaluation mechanisms\<close>
4
5theory Eval_Examples
6imports Complex_Main
7begin
8
9text \<open>evaluation oracle\<close>
10
11lemma "True \<or> False" by eval
12lemma "Suc 0 \<noteq> Suc 1" by eval
13lemma "[] = ([] :: int list)" by eval
14lemma "[()] = [()]" by eval
15lemma "fst ([] :: nat list, Suc 0) = []" by eval
16
17text \<open>normalization\<close>
18
19lemma "True \<or> False" by normalization
20lemma "Suc 0 \<noteq> Suc 1" by normalization
21lemma "[] = ([] :: int list)" by normalization
22lemma "[()] = [()]" by normalization
23lemma "fst ([] :: nat list, Suc 0) = []" by normalization
24
25text \<open>term evaluation\<close>
26
27value "(Suc 2 + 1) * 4"
28
29value "(Suc 2 + Suc 0) * Suc 3"
30
31value "nat 100"
32
33value "(10::int) \<le> 12"
34
35value "max (2::int) 4"
36
37value "of_int 2 / of_int 4 * (1::rat)"
38
39value "[] :: nat list"
40
41value "[(nat 100, ())]"
42
43text \<open>a fancy datatype\<close>
44
45datatype ('a, 'b) foo =
46    Foo "'a::order" 'b
47  | Bla "('a, 'b) bar"
48  | Dummy nat
49and ('a, 'b) bar =
50    Bar 'a 'b
51  | Blubb "('a, 'b) foo"
52
53value "Bla (Bar (4::nat) [Suc 0])"
54
55end
56