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
wenzelm@23268
     1
(*  ID:         $Id$
wenzelm@23268
     2
    Author:     Florian Haftmann, TU Muenchen
wenzelm@23268
     3
*)
wenzelm@23268
     4
wenzelm@23268
     5
header {* Small examples for evaluation mechanisms *}
wenzelm@23268
     6
wenzelm@23268
     7
theory Eval_Examples
haftmann@28227
     8
imports Code_Eval "~~/src/HOL/Real/Rational"
wenzelm@23268
     9
begin
wenzelm@23268
    10
haftmann@25099
    11
text {* evaluation oracle *}
haftmann@25099
    12
haftmann@25099
    13
lemma "True \<or> False" by eval
haftmann@25099
    14
lemma "\<not> (Suc 0 = Suc 1)" by eval
haftmann@25099
    15
lemma "[] = ([]\<Colon> int list)" by eval
haftmann@25099
    16
lemma "[()] = [()]" by eval
haftmann@25099
    17
lemma "fst ([]::nat list, Suc 0) = []" by eval
haftmann@25099
    18
haftmann@24292
    19
text {* SML evaluation oracle *}
haftmann@24292
    20
haftmann@24292
    21
lemma "True \<or> False" by evaluation
haftmann@24292
    22
lemma "\<not> (Suc 0 = Suc 1)" by evaluation
haftmann@24292
    23
lemma "[] = ([]\<Colon> int list)" by evaluation
haftmann@24292
    24
lemma "[()] = [()]" by evaluation
haftmann@24292
    25
lemma "fst ([]::nat list, Suc 0) = []" by evaluation
haftmann@24292
    26
haftmann@25099
    27
text {* normalization *}
wenzelm@23268
    28
haftmann@25099
    29
lemma "True \<or> False" by normalization
haftmann@25099
    30
lemma "\<not> (Suc 0 = Suc 1)" by normalization
haftmann@25099
    31
lemma "[] = ([]\<Colon> int list)" by normalization
haftmann@25099
    32
lemma "[()] = [()]" by normalization
haftmann@25099
    33
lemma "fst ([]::nat list, Suc 0) = []" by normalization
wenzelm@23268
    34
wenzelm@23268
    35
text {* term evaluation *}
wenzelm@23268
    36
haftmann@24587
    37
value "(Suc 2 + 1) * 4"
haftmann@28227
    38
value [code] "(Suc 2 + 1) * 4"
haftmann@28227
    39
value [SML] "(Suc 2 + 1) * 4"
haftmann@28227
    40
value [nbe] "(Suc 2 + 1) * 4"
haftmann@24835
    41
haftmann@24587
    42
value "(Suc 2 + Suc 0) * Suc 3"
haftmann@28227
    43
value [code] "(Suc 2 + Suc 0) * Suc 3"
haftmann@28227
    44
value [SML] "(Suc 2 + Suc 0) * Suc 3"
haftmann@28227
    45
value [nbe] "(Suc 2 + Suc 0) * Suc 3"
haftmann@24835
    46
haftmann@24587
    47
value "nat 100"
haftmann@28227
    48
value [code] "nat 100"
haftmann@28227
    49
value [SML] "nat 100"
haftmann@28227
    50
value [nbe] "nat 100"
haftmann@24835
    51
haftmann@24587
    52
value "(10\<Colon>int) \<le> 12"
haftmann@28227
    53
value [code] "(10\<Colon>int) \<le> 12"
haftmann@28227
    54
value [SML] "(10\<Colon>int) \<le> 12"
haftmann@28227
    55
value [nbe] "(10\<Colon>int) \<le> 12"
haftmann@24835
    56
haftmann@24835
    57
value "max (2::int) 4"
haftmann@28227
    58
value [code] "max (2::int) 4"
haftmann@28227
    59
value [SML] "max (2::int) 4"
haftmann@28227
    60
value [nbe] "max (2::int) 4"
haftmann@24835
    61
haftmann@24835
    62
value "of_int 2 / of_int 4 * (1::rat)"
haftmann@28227
    63
value [code] "of_int 2 / of_int 4 * (1::rat)"
haftmann@28227
    64
value [SML] "of_int 2 / of_int 4 * (1::rat)"
haftmann@28227
    65
value [nbe] "of_int 2 / of_int 4 * (1::rat)"
haftmann@24835
    66
haftmann@24587
    67
value "[]::nat list"
haftmann@28227
    68
value [code] "[]::nat list"
haftmann@28227
    69
value [SML] "[]::nat list"
haftmann@28227
    70
value [nbe] "[]::nat list"
haftmann@24835
    71
haftmann@24587
    72
value "[(nat 100, ())]"
haftmann@28227
    73
value [code] "[(nat 100, ())]"
haftmann@28227
    74
value [SML] "[(nat 100, ())]"
haftmann@28227
    75
value [nbe] "[(nat 100, ())]"
haftmann@24659
    76
wenzelm@23268
    77
wenzelm@23268
    78
text {* a fancy datatype *}
wenzelm@23268
    79
wenzelm@23268
    80
datatype ('a, 'b) bair =
wenzelm@23268
    81
    Bair "'a\<Colon>order" 'b
wenzelm@23268
    82
  | Shift "('a, 'b) cair"
wenzelm@23268
    83
  | Dummy unit
wenzelm@23268
    84
and ('a, 'b) cair =
wenzelm@23268
    85
    Cair 'a 'b
wenzelm@23268
    86
haftmann@24587
    87
value "Shift (Cair (4::nat) [Suc 0])"
haftmann@28227
    88
value [code] "Shift (Cair (4::nat) [Suc 0])"
haftmann@28227
    89
value [SML] "Shift (Cair (4::nat) [Suc 0])"
haftmann@28227
    90
value [nbe] "Shift (Cair (4::nat) [Suc 0])"
wenzelm@23268
    91
wenzelm@23268
    92
end