1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 section {* Small examples for evaluation mechanisms *} |
3 section \<open>Small examples for evaluation mechanisms\<close> |
4 |
4 |
5 theory Eval_Examples |
5 theory Eval_Examples |
6 imports Complex_Main |
6 imports Complex_Main |
7 begin |
7 begin |
8 |
8 |
9 text {* evaluation oracle *} |
9 text \<open>evaluation oracle\<close> |
10 |
10 |
11 lemma "True \<or> False" by eval |
11 lemma "True \<or> False" by eval |
12 lemma "Suc 0 \<noteq> Suc 1" by eval |
12 lemma "Suc 0 \<noteq> Suc 1" by eval |
13 lemma "[] = ([] :: int list)" by eval |
13 lemma "[] = ([] :: int list)" by eval |
14 lemma "[()] = [()]" by eval |
14 lemma "[()] = [()]" by eval |
15 lemma "fst ([] :: nat list, Suc 0) = []" by eval |
15 lemma "fst ([] :: nat list, Suc 0) = []" by eval |
16 |
16 |
17 text {* normalization *} |
17 text \<open>normalization\<close> |
18 |
18 |
19 lemma "True \<or> False" by normalization |
19 lemma "True \<or> False" by normalization |
20 lemma "Suc 0 \<noteq> Suc 1" by normalization |
20 lemma "Suc 0 \<noteq> Suc 1" by normalization |
21 lemma "[] = ([] :: int list)" by normalization |
21 lemma "[] = ([] :: int list)" by normalization |
22 lemma "[()] = [()]" by normalization |
22 lemma "[()] = [()]" by normalization |
23 lemma "fst ([] :: nat list, Suc 0) = []" by normalization |
23 lemma "fst ([] :: nat list, Suc 0) = []" by normalization |
24 |
24 |
25 text {* term evaluation *} |
25 text \<open>term evaluation\<close> |
26 |
26 |
27 value "(Suc 2 + 1) * 4" |
27 value "(Suc 2 + 1) * 4" |
28 |
28 |
29 value "(Suc 2 + Suc 0) * Suc 3" |
29 value "(Suc 2 + Suc 0) * Suc 3" |
30 |
30 |