src/HOL/ex/Eval_Examples.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30021 19c06d4763e0
child 32067 e425fe0ff24a
permissions -rw-r--r--
added lemmas
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Small examples for evaluation mechanisms *}
     4 
     5 theory Eval_Examples
     6 imports Code_Eval Rational
     7 begin
     8 
     9 text {* evaluation oracle *}
    10 
    11 lemma "True \<or> False" by eval
    12 lemma "\<not> (Suc 0 = Suc 1)" by eval
    13 lemma "[] = ([]\<Colon> int list)" by eval
    14 lemma "[()] = [()]" by eval
    15 lemma "fst ([]::nat list, Suc 0) = []" by eval
    16 
    17 text {* SML evaluation oracle *}
    18 
    19 lemma "True \<or> False" by evaluation
    20 lemma "\<not> (Suc 0 = Suc 1)" by evaluation
    21 lemma "[] = ([]\<Colon> int list)" by evaluation
    22 lemma "[()] = [()]" by evaluation
    23 lemma "fst ([]::nat list, Suc 0) = []" by evaluation
    24 
    25 text {* normalization *}
    26 
    27 lemma "True \<or> False" by normalization
    28 lemma "\<not> (Suc 0 = Suc 1)" by normalization
    29 lemma "[] = ([]\<Colon> int list)" by normalization
    30 lemma "[()] = [()]" by normalization
    31 lemma "fst ([]::nat list, Suc 0) = []" by normalization
    32 
    33 text {* term evaluation *}
    34 
    35 value "(Suc 2 + 1) * 4"
    36 value [code] "(Suc 2 + 1) * 4"
    37 value [SML] "(Suc 2 + 1) * 4"
    38 value [nbe] "(Suc 2 + 1) * 4"
    39 
    40 value "(Suc 2 + Suc 0) * Suc 3"
    41 value [code] "(Suc 2 + Suc 0) * Suc 3"
    42 value [SML] "(Suc 2 + Suc 0) * Suc 3"
    43 value [nbe] "(Suc 2 + Suc 0) * Suc 3"
    44 
    45 value "nat 100"
    46 value [code] "nat 100"
    47 value [SML] "nat 100"
    48 value [nbe] "nat 100"
    49 
    50 value "(10\<Colon>int) \<le> 12"
    51 value [code] "(10\<Colon>int) \<le> 12"
    52 value [SML] "(10\<Colon>int) \<le> 12"
    53 value [nbe] "(10\<Colon>int) \<le> 12"
    54 
    55 value "max (2::int) 4"
    56 value [code] "max (2::int) 4"
    57 value [SML] "max (2::int) 4"
    58 value [nbe] "max (2::int) 4"
    59 
    60 value "of_int 2 / of_int 4 * (1::rat)"
    61 value [code] "of_int 2 / of_int 4 * (1::rat)"
    62 value [SML] "of_int 2 / of_int 4 * (1::rat)"
    63 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
    64 
    65 value "[]::nat list"
    66 value [code] "[]::nat list"
    67 value [SML] "[]::nat list"
    68 value [nbe] "[]::nat list"
    69 
    70 value "[(nat 100, ())]"
    71 value [code] "[(nat 100, ())]"
    72 value [SML] "[(nat 100, ())]"
    73 value [nbe] "[(nat 100, ())]"
    74 
    75 
    76 text {* a fancy datatype *}
    77 
    78 datatype ('a, 'b) bair =
    79     Bair "'a\<Colon>order" 'b
    80   | Shift "('a, 'b) cair"
    81   | Dummy unit
    82 and ('a, 'b) cair =
    83     Cair 'a 'b
    84 
    85 value "Shift (Cair (4::nat) [Suc 0])"
    86 value [code] "Shift (Cair (4::nat) [Suc 0])"
    87 value [SML] "Shift (Cair (4::nat) [Suc 0])"
    88 value [nbe] "Shift (Cair (4::nat) [Suc 0])"
    89 
    90 end