src/HOL/ex/Eval_Examples.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 45170 7dd207fe7b6e child 56927 4044a7d1720f permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* Small examples for evaluation mechanisms *}
5 theory Eval_Examples
6 imports Complex_Main
7 begin
9 text {* evaluation oracle *}
11 lemma "True \<or> False" by eval
12 lemma "Suc 0 \<noteq> Suc 1" by eval
13 lemma "[] = ([] :: int list)" by eval
14 lemma "[()] = [()]" by eval
15 lemma "fst ([] :: nat list, Suc 0) = []" by eval
17 text {* normalization *}
19 lemma "True \<or> False" by normalization
20 lemma "Suc 0 \<noteq> Suc 1" by normalization
21 lemma "[] = ([] :: int list)" by normalization
22 lemma "[()] = [()]" by normalization
23 lemma "fst ([] :: nat list, Suc 0) = []" by normalization
25 text {* term evaluation *}
27 value "(Suc 2 + 1) * 4"
28 value [code] "(Suc 2 + 1) * 4"
29 value [nbe] "(Suc 2 + 1) * 4"
31 value "(Suc 2 + Suc 0) * Suc 3"
32 value [code] "(Suc 2 + Suc 0) * Suc 3"
33 value [nbe] "(Suc 2 + Suc 0) * Suc 3"
35 value "nat 100"
36 value [code] "nat 100"
37 value [nbe] "nat 100"
39 value "(10::int) \<le> 12"
40 value [code] "(10::int) \<le> 12"
41 value [nbe] "(10::int) \<le> 12"
43 value "max (2::int) 4"
44 value [code] "max (2::int) 4"
45 value [nbe] "max (2::int) 4"
47 value "of_int 2 / of_int 4 * (1::rat)"
48 value [code] "of_int 2 / of_int 4 * (1::rat)"
49 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
51 value "[] :: nat list"
52 value [code] "[] :: nat list"
53 value [nbe] "[] :: nat list"
55 value "[(nat 100, ())]"
56 value [code] "[(nat 100, ())]"
57 value [nbe] "[(nat 100, ())]"
59 text {* a fancy datatype *}
61 datatype ('a, 'b) foo =
62     Foo "'a\<Colon>order" 'b
63   | Bla "('a, 'b) bar"
64   | Dummy nat
65 and ('a, 'b) bar =
66     Bar 'a 'b
67   | Blubb "('a, 'b) foo"
69 value "Bla (Bar (4::nat) [Suc 0])"
70 value [code] "Bla (Bar (4::nat) [Suc 0])"
71 value [nbe] "Bla (Bar (4::nat) [Suc 0])"
73 end