# Theory Eval_Examples

theory Eval_Examples
imports Complex_Main
`(* Author: Florian Haftmann, TU Muenchen *)header {* Small examples for evaluation mechanisms *}theory Eval_Examplesimports Complex_Mainbegintext {* evaluation oracle *}lemma "True ∨ False" by evallemma "Suc 0 ≠ Suc 1" by evallemma "[] = ([] :: int list)" by evallemma "[()] = [()]" by evallemma "fst ([] :: nat list, Suc 0) = []" by evaltext {* normalization *}lemma "True ∨ False" by normalizationlemma "Suc 0 ≠ Suc 1" by normalizationlemma "[] = ([] :: int list)" by normalizationlemma "[()] = [()]" by normalizationlemma "fst ([] :: nat list, Suc 0) = []" by normalizationtext {* term evaluation *}value "(Suc 2 + 1) * 4"value [code] "(Suc 2 + 1) * 4"value [nbe] "(Suc 2 + 1) * 4"value "(Suc 2 + Suc 0) * Suc 3"value [code] "(Suc 2 + Suc 0) * Suc 3"value [nbe] "(Suc 2 + Suc 0) * Suc 3"value "nat 100"value [code] "nat 100"value [nbe] "nat 100"value "(10::int) ≤ 12"value [code] "(10::int) ≤ 12"value [nbe] "(10::int) ≤ 12"value "max (2::int) 4"value [code] "max (2::int) 4"value [nbe] "max (2::int) 4"value "of_int 2 / of_int 4 * (1::rat)"value [code] "of_int 2 / of_int 4 * (1::rat)"value [nbe] "of_int 2 / of_int 4 * (1::rat)"value "[] :: nat list"value [code] "[] :: nat list"value [nbe] "[] :: nat list"value "[(nat 100, ())]"value [code] "[(nat 100, ())]"value [nbe] "[(nat 100, ())]"text {* a fancy datatype *}datatype ('a, 'b) foo =    Foo "'a::order" 'b  | Bla "('a, 'b) bar"  | Dummy natand ('a, 'b) bar =    Bar 'a 'b  | Blubb "('a, 'b) foo"value "Bla (Bar (4::nat) [Suc 0])"value [code] "Bla (Bar (4::nat) [Suc 0])"value [nbe] "Bla (Bar (4::nat) [Suc 0])"end`