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