src/HOL/ex/Eval_Examples.thy
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24292 26ac9fe0e80e
child 24587 4f2cbf6e563f
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
     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 {* SML evaluation oracle *}
    12 
    13 lemma "True \<or> False" by evaluation
    14 lemma "\<not> (Suc 0 = Suc 1)" by evaluation
    15 lemma "[] = ([]\<Colon> int list)" by evaluation
    16 lemma "[()] = [()]" by evaluation
    17 lemma "fst ([]::nat list, Suc 0) = []" by evaluation
    18 
    19 text {* evaluation oracle *}
    20 
    21 lemma "True \<or> False" by eval
    22 lemma "\<not> (Suc 0 = Suc 1)" by eval
    23 lemma "[] = ([]\<Colon> int list)" by eval
    24 lemma "[()] = [()]" by eval
    25 lemma "fst ([]::nat list, Suc 0) = []" by eval
    26 
    27 text {* term evaluation *}
    28 
    29 value (overloaded) "(Suc 2 + 1) * 4"
    30 value (overloaded) "(Suc 2 + 1) * 4"
    31 value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
    32 value (overloaded) "nat 100"
    33 value (overloaded) "(10\<Colon>int) \<le> 12"
    34 value (overloaded) "[]::nat list"
    35 value (overloaded) "[(nat 100, ())]"
    36 
    37 text {* a fancy datatype *}
    38 
    39 datatype ('a, 'b) bair =
    40     Bair "'a\<Colon>order" 'b
    41   | Shift "('a, 'b) cair"
    42   | Dummy unit
    43 and ('a, 'b) cair =
    44     Cair 'a 'b
    45 
    46 value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
    47 
    48 end