src/HOL/ex/Eval_Examples.thy
author haftmann
Tue Sep 16 09:21:22 2008 +0200 (2008-09-16)
changeset 28227 77221ee0f7b9
parent 26020 ffe1a032d24b
child 28952 15a4b2cf8c34
permissions -rw-r--r--
generic value command
     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 Code_Eval "~~/src/HOL/Real/Rational"
     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 lemma "[] = ([]\<Colon> int list)" by eval
    16 lemma "[()] = [()]" by eval
    17 lemma "fst ([]::nat list, Suc 0) = []" by eval
    18 
    19 text {* SML evaluation oracle *}
    20 
    21 lemma "True \<or> False" by evaluation
    22 lemma "\<not> (Suc 0 = Suc 1)" by evaluation
    23 lemma "[] = ([]\<Colon> int list)" by evaluation
    24 lemma "[()] = [()]" by evaluation
    25 lemma "fst ([]::nat list, Suc 0) = []" by evaluation
    26 
    27 text {* normalization *}
    28 
    29 lemma "True \<or> False" by normalization
    30 lemma "\<not> (Suc 0 = Suc 1)" by normalization
    31 lemma "[] = ([]\<Colon> int list)" by normalization
    32 lemma "[()] = [()]" by normalization
    33 lemma "fst ([]::nat list, Suc 0) = []" by normalization
    34 
    35 text {* term evaluation *}
    36 
    37 value "(Suc 2 + 1) * 4"
    38 value [code] "(Suc 2 + 1) * 4"
    39 value [SML] "(Suc 2 + 1) * 4"
    40 value [nbe] "(Suc 2 + 1) * 4"
    41 
    42 value "(Suc 2 + Suc 0) * Suc 3"
    43 value [code] "(Suc 2 + Suc 0) * Suc 3"
    44 value [SML] "(Suc 2 + Suc 0) * Suc 3"
    45 value [nbe] "(Suc 2 + Suc 0) * Suc 3"
    46 
    47 value "nat 100"
    48 value [code] "nat 100"
    49 value [SML] "nat 100"
    50 value [nbe] "nat 100"
    51 
    52 value "(10\<Colon>int) \<le> 12"
    53 value [code] "(10\<Colon>int) \<le> 12"
    54 value [SML] "(10\<Colon>int) \<le> 12"
    55 value [nbe] "(10\<Colon>int) \<le> 12"
    56 
    57 value "max (2::int) 4"
    58 value [code] "max (2::int) 4"
    59 value [SML] "max (2::int) 4"
    60 value [nbe] "max (2::int) 4"
    61 
    62 value "of_int 2 / of_int 4 * (1::rat)"
    63 value [code] "of_int 2 / of_int 4 * (1::rat)"
    64 value [SML] "of_int 2 / of_int 4 * (1::rat)"
    65 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
    66 
    67 value "[]::nat list"
    68 value [code] "[]::nat list"
    69 value [SML] "[]::nat list"
    70 value [nbe] "[]::nat list"
    71 
    72 value "[(nat 100, ())]"
    73 value [code] "[(nat 100, ())]"
    74 value [SML] "[(nat 100, ())]"
    75 value [nbe] "[(nat 100, ())]"
    76 
    77 
    78 text {* a fancy datatype *}
    79 
    80 datatype ('a, 'b) bair =
    81     Bair "'a\<Colon>order" 'b
    82   | Shift "('a, 'b) cair"
    83   | Dummy unit
    84 and ('a, 'b) cair =
    85     Cair 'a 'b
    86 
    87 value "Shift (Cair (4::nat) [Suc 0])"
    88 value [code] "Shift (Cair (4::nat) [Suc 0])"
    89 value [SML] "Shift (Cair (4::nat) [Suc 0])"
    90 value [nbe] "Shift (Cair (4::nat) [Suc 0])"
    91 
    92 end