src/HOL/ex/Eval_Examples.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45170 7dd207fe7b6e
child 56927 4044a7d1720f
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
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@32067
     6
imports Complex_Main
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@40760
    12
lemma "Suc 0 \<noteq> Suc 1" by eval
haftmann@40760
    13
lemma "[] = ([] :: int list)" by eval
haftmann@25099
    14
lemma "[()] = [()]" by eval
haftmann@40760
    15
lemma "fst ([] :: nat list, Suc 0) = []" by eval
haftmann@25099
    16
haftmann@25099
    17
text {* normalization *}
wenzelm@23268
    18
haftmann@25099
    19
lemma "True \<or> False" by normalization
haftmann@40760
    20
lemma "Suc 0 \<noteq> Suc 1" by normalization
haftmann@40760
    21
lemma "[] = ([] :: int list)" by normalization
haftmann@25099
    22
lemma "[()] = [()]" by normalization
haftmann@40760
    23
lemma "fst ([] :: nat list, Suc 0) = []" by normalization
wenzelm@23268
    24
wenzelm@23268
    25
text {* term evaluation *}
wenzelm@23268
    26
haftmann@24587
    27
value "(Suc 2 + 1) * 4"
haftmann@28227
    28
value [code] "(Suc 2 + 1) * 4"
haftmann@28227
    29
value [nbe] "(Suc 2 + 1) * 4"
haftmann@24835
    30
haftmann@24587
    31
value "(Suc 2 + Suc 0) * Suc 3"
haftmann@28227
    32
value [code] "(Suc 2 + Suc 0) * Suc 3"
haftmann@28227
    33
value [nbe] "(Suc 2 + Suc 0) * Suc 3"
haftmann@24835
    34
haftmann@24587
    35
value "nat 100"
haftmann@28227
    36
value [code] "nat 100"
haftmann@28227
    37
value [nbe] "nat 100"
haftmann@24835
    38
haftmann@40760
    39
value "(10::int) \<le> 12"
haftmann@40760
    40
value [code] "(10::int) \<le> 12"
haftmann@40760
    41
value [nbe] "(10::int) \<le> 12"
haftmann@24835
    42
haftmann@24835
    43
value "max (2::int) 4"
haftmann@28227
    44
value [code] "max (2::int) 4"
haftmann@28227
    45
value [nbe] "max (2::int) 4"
haftmann@24835
    46
haftmann@24835
    47
value "of_int 2 / of_int 4 * (1::rat)"
haftmann@28227
    48
value [code] "of_int 2 / of_int 4 * (1::rat)"
haftmann@28227
    49
value [nbe] "of_int 2 / of_int 4 * (1::rat)"
haftmann@24835
    50
haftmann@40760
    51
value "[] :: nat list"
haftmann@40760
    52
value [code] "[] :: nat list"
haftmann@40760
    53
value [nbe] "[] :: nat list"
haftmann@24835
    54
haftmann@24587
    55
value "[(nat 100, ())]"
haftmann@28227
    56
value [code] "[(nat 100, ())]"
haftmann@28227
    57
value [nbe] "[(nat 100, ())]"
haftmann@24659
    58
wenzelm@23268
    59
text {* a fancy datatype *}
wenzelm@23268
    60
haftmann@40757
    61
datatype ('a, 'b) foo =
haftmann@40757
    62
    Foo "'a\<Colon>order" 'b
haftmann@40757
    63
  | Bla "('a, 'b) bar"
haftmann@40757
    64
  | Dummy nat
haftmann@40757
    65
and ('a, 'b) bar =
haftmann@40757
    66
    Bar 'a 'b
haftmann@40757
    67
  | Blubb "('a, 'b) foo"
wenzelm@23268
    68
haftmann@40757
    69
value "Bla (Bar (4::nat) [Suc 0])"
haftmann@40757
    70
value [code] "Bla (Bar (4::nat) [Suc 0])"
haftmann@40757
    71
value [nbe] "Bla (Bar (4::nat) [Suc 0])"
wenzelm@23268
    72
wenzelm@23268
    73
end