src/HOL/ex/Eval_Examples.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 26020 ffe1a032d24b
child 28227 77221ee0f7b9
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     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 "~~/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 ("normal_form") "(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 ("normal_form") "(Suc 2 + Suc 0) * Suc 3"
    46 
    47 value "nat 100"
    48 value (code) "nat 100"
    49 value (SML) "nat 100"
    50 value ("normal_form") "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 ("normal_form") "(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 ("normal_form") "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 ("normal_form") "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 ("normal_form") "[]::nat list"
    71 
    72 value "[(nat 100, ())]"
    73 value (code) "[(nat 100, ())]"
    74 value (SML) "[(nat 100, ())]"
    75 value ("normal_form") "[(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 ("normal_form") "Shift (Cair (4::nat) [Suc 0])"
    91 
    92 end