Theory Eval_Examples

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Small examples for evaluation mechanisms›

theory Eval_Examples
imports Complex_Main
begin

text ‹evaluation oracle›

lemma "True ∨ False" by eval
lemma "Suc 0 ≠ Suc 1" by eval
lemma "[] = ([] :: int list)" by eval
lemma "[()] = [()]" by eval
lemma "fst ([] :: nat list, Suc 0) = []" by eval

text ‹normalization›

lemma "True ∨ False" by normalization
lemma "Suc 0 ≠ Suc 1" by normalization
lemma "[] = ([] :: int list)" by normalization
lemma "[()] = [()]" by normalization
lemma "fst ([] :: nat list, Suc 0) = []" by normalization

text ‹term evaluation›

value "(Suc 2 + 1) * 4"

value "(Suc 2 + Suc 0) * Suc 3"

value "nat 100"

value "(10::int) ≤ 12"

value "max (2::int) 4"

value "of_int 2 / of_int 4 * (1::rat)"

value "[] :: nat list"

value "[(nat 100, ())]"

text ‹a fancy datatype›

datatype ('a, 'b) foo =
    Foo "'a::order" 'b
  | Bla "('a, 'b) bar"
  | Dummy nat
and ('a, 'b) bar =
    Bar 'a 'b
  | Blubb "('a, 'b) foo"

value "Bla (Bar (4::nat) [Suc 0])"

end