src/HOL/ex/Eval_examples.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 23134 6cd88d27f600
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  ID:         $Id$
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Small examples for evaluation mechanisms *}
     6 
     7 theory Eval_examples
     8 imports Eval
     9 begin
    10 
    11 text {* evaluation oracle *}
    12 
    13 lemma "True \<or> False" by eval
    14 lemma "\<not> (Suc 0 = Suc 1)" by eval
    15 
    16 text {* term evaluation *}
    17 
    18 value (overloaded) "(Suc 2 + 1) * 4"
    19 value (overloaded) "(Suc 2 + 1) * 4"
    20 value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
    21 value (overloaded) "[]::nat list"
    22 value (overloaded) "fst ([]::nat list, Suc 0) = []"
    23 value (overloaded) "nat 100"
    24 value (overloaded) "[(nat 100, ())]"
    25 value (overloaded) "int 10 \<le> 12"
    26 
    27 text {* a fancy datatype *}
    28 
    29 datatype ('a, 'b) bair =
    30     Bair "'a\<Colon>order" 'b
    31   | Shift "('a, 'b) cair"
    32   | Dummy unit
    33 and ('a, 'b) cair =
    34     Cair 'a 'b
    35 
    36 value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
    37 
    38 end