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