src/HOL/ex/Eval_Examples.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61343 5b5656a63bd6
permissions -rw-r--r--
bundle lifting_syntax;
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 section \<open>Small examples for evaluation mechanisms\<close>
     4 
     5 theory Eval_Examples
     6 imports Complex_Main
     7 begin
     8 
     9 text \<open>evaluation oracle\<close>
    10 
    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
    16 
    17 text \<open>normalization\<close>
    18 
    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
    24 
    25 text \<open>term evaluation\<close>
    26 
    27 value "(Suc 2 + 1) * 4"
    28 
    29 value "(Suc 2 + Suc 0) * Suc 3"
    30 
    31 value "nat 100"
    32 
    33 value "(10::int) \<le> 12"
    34 
    35 value "max (2::int) 4"
    36 
    37 value "of_int 2 / of_int 4 * (1::rat)"
    38 
    39 value "[] :: nat list"
    40 
    41 value "[(nat 100, ())]"
    42 
    43 text \<open>a fancy datatype\<close>
    44 
    45 datatype ('a, 'b) foo =
    46     Foo "'a::order" 'b
    47   | Bla "('a, 'b) bar"
    48   | Dummy nat
    49 and ('a, 'b) bar =
    50     Bar 'a 'b
    51   | Blubb "('a, 'b) foo"
    52 
    53 value "Bla (Bar (4::nat) [Suc 0])"
    54 
    55 end