src/HOL/ex/Eval_Examples.thy
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 45170 7dd207fe7b6e
child 56927 4044a7d1720f
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30021
19c06d4763e0 stripped Id
haftmann
parents: 28952
diff changeset
     1
(* Author: Florian Haftmann, TU Muenchen *)
23268
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
     2
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
     3
header {* Small examples for evaluation mechanisms *}
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
     4
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
     5
theory Eval_Examples
32067
e425fe0ff24a more canonical import
haftmann
parents: 30021
diff changeset
     6
imports Complex_Main
23268
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
     7
begin
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
     8
25099
b2c19b9964db lemmas with normalization
haftmann
parents: 24916
diff changeset
     9
text {* evaluation oracle *}
b2c19b9964db lemmas with normalization
haftmann
parents: 24916
diff changeset
    10
b2c19b9964db lemmas with normalization
haftmann
parents: 24916
diff changeset
    11
lemma "True \<or> False" by eval
40760
haftmann
parents: 40757
diff changeset
    12
lemma "Suc 0 \<noteq> Suc 1" by eval
haftmann
parents: 40757
diff changeset
    13
lemma "[] = ([] :: int list)" by eval
25099
b2c19b9964db lemmas with normalization
haftmann
parents: 24916
diff changeset
    14
lemma "[()] = [()]" by eval
40760
haftmann
parents: 40757
diff changeset
    15
lemma "fst ([] :: nat list, Suc 0) = []" by eval
25099
b2c19b9964db lemmas with normalization
haftmann
parents: 24916
diff changeset
    16
b2c19b9964db lemmas with normalization
haftmann
parents: 24916
diff changeset
    17
text {* normalization *}
23268
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    18
25099
b2c19b9964db lemmas with normalization
haftmann
parents: 24916
diff changeset
    19
lemma "True \<or> False" by normalization
40760
haftmann
parents: 40757
diff changeset
    20
lemma "Suc 0 \<noteq> Suc 1" by normalization
haftmann
parents: 40757
diff changeset
    21
lemma "[] = ([] :: int list)" by normalization
25099
b2c19b9964db lemmas with normalization
haftmann
parents: 24916
diff changeset
    22
lemma "[()] = [()]" by normalization
40760
haftmann
parents: 40757
diff changeset
    23
lemma "fst ([] :: nat list, Suc 0) = []" by normalization
23268
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    24
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    25
text {* term evaluation *}
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    26
24587
4f2cbf6e563f multi-functional value keyword
haftmann
parents: 24423
diff changeset
    27
value "(Suc 2 + 1) * 4"
28227
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    28
value [code] "(Suc 2 + 1) * 4"
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    29
value [nbe] "(Suc 2 + 1) * 4"
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    30
24587
4f2cbf6e563f multi-functional value keyword
haftmann
parents: 24423
diff changeset
    31
value "(Suc 2 + Suc 0) * Suc 3"
28227
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    32
value [code] "(Suc 2 + Suc 0) * Suc 3"
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    33
value [nbe] "(Suc 2 + Suc 0) * Suc 3"
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    34
24587
4f2cbf6e563f multi-functional value keyword
haftmann
parents: 24423
diff changeset
    35
value "nat 100"
28227
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    36
value [code] "nat 100"
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    37
value [nbe] "nat 100"
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    38
40760
haftmann
parents: 40757
diff changeset
    39
value "(10::int) \<le> 12"
haftmann
parents: 40757
diff changeset
    40
value [code] "(10::int) \<le> 12"
haftmann
parents: 40757
diff changeset
    41
value [nbe] "(10::int) \<le> 12"
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    42
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    43
value "max (2::int) 4"
28227
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    44
value [code] "max (2::int) 4"
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    45
value [nbe] "max (2::int) 4"
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    46
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    47
value "of_int 2 / of_int 4 * (1::rat)"
28227
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    48
value [code] "of_int 2 / of_int 4 * (1::rat)"
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    49
value [nbe] "of_int 2 / of_int 4 * (1::rat)"
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    50
40760
haftmann
parents: 40757
diff changeset
    51
value "[] :: nat list"
haftmann
parents: 40757
diff changeset
    52
value [code] "[] :: nat list"
haftmann
parents: 40757
diff changeset
    53
value [nbe] "[] :: nat list"
24835
8c26128f8997 clarified relationship of code generator conversions and evaluations
haftmann
parents: 24659
diff changeset
    54
24587
4f2cbf6e563f multi-functional value keyword
haftmann
parents: 24423
diff changeset
    55
value "[(nat 100, ())]"
28227
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    56
value [code] "[(nat 100, ())]"
77221ee0f7b9 generic value command
haftmann
parents: 26020
diff changeset
    57
value [nbe] "[(nat 100, ())]"
24659
6b7ac2a43df8 more permissive
haftmann
parents: 24587
diff changeset
    58
23268
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    59
text {* a fancy datatype *}
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    60
40757
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    61
datatype ('a, 'b) foo =
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    62
    Foo "'a\<Colon>order" 'b
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    63
  | Bla "('a, 'b) bar"
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    64
  | Dummy nat
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    65
and ('a, 'b) bar =
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    66
    Bar 'a 'b
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    67
  | Blubb "('a, 'b) foo"
23268
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    68
40757
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    69
value "Bla (Bar (4::nat) [Suc 0])"
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    70
value [code] "Bla (Bar (4::nat) [Suc 0])"
b469a373df31 tuned example
haftmann
parents: 32067
diff changeset
    71
value [nbe] "Bla (Bar (4::nat) [Suc 0])"
23268
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    72
572a483de1b0 renamed ex/Eval_Examples.thy;
wenzelm
parents:
diff changeset
    73
end