src/HOL/ex/Eval_Examples.thy
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24292 26ac9fe0e80e
child 24587 4f2cbf6e563f
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
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
wenzelm@23268
     8
imports Eval
wenzelm@23268
     9
begin
wenzelm@23268
    10
haftmann@24292
    11
text {* SML evaluation oracle *}
haftmann@24292
    12
haftmann@24292
    13
lemma "True \<or> False" by evaluation
haftmann@24292
    14
lemma "\<not> (Suc 0 = Suc 1)" by evaluation
haftmann@24292
    15
lemma "[] = ([]\<Colon> int list)" by evaluation
haftmann@24292
    16
lemma "[()] = [()]" by evaluation
haftmann@24292
    17
lemma "fst ([]::nat list, Suc 0) = []" by evaluation
haftmann@24292
    18
wenzelm@23268
    19
text {* evaluation oracle *}
wenzelm@23268
    20
wenzelm@23268
    21
lemma "True \<or> False" by eval
wenzelm@23268
    22
lemma "\<not> (Suc 0 = Suc 1)" by eval
haftmann@24280
    23
lemma "[] = ([]\<Colon> int list)" by eval
haftmann@24280
    24
lemma "[()] = [()]" by eval
haftmann@24292
    25
lemma "fst ([]::nat list, Suc 0) = []" by eval
wenzelm@23268
    26
wenzelm@23268
    27
text {* term evaluation *}
wenzelm@23268
    28
wenzelm@23268
    29
value (overloaded) "(Suc 2 + 1) * 4"
wenzelm@23268
    30
value (overloaded) "(Suc 2 + 1) * 4"
wenzelm@23268
    31
value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
haftmann@24280
    32
value (overloaded) "nat 100"
haftmann@24280
    33
value (overloaded) "(10\<Colon>int) \<le> 12"
haftmann@24423
    34
value (overloaded) "[]::nat list"
haftmann@24280
    35
value (overloaded) "[(nat 100, ())]"
wenzelm@23268
    36
wenzelm@23268
    37
text {* a fancy datatype *}
wenzelm@23268
    38
wenzelm@23268
    39
datatype ('a, 'b) bair =
wenzelm@23268
    40
    Bair "'a\<Colon>order" 'b
wenzelm@23268
    41
  | Shift "('a, 'b) cair"
wenzelm@23268
    42
  | Dummy unit
wenzelm@23268
    43
and ('a, 'b) cair =
wenzelm@23268
    44
    Cair 'a 'b
wenzelm@23268
    45
wenzelm@23268
    46
value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
wenzelm@23268
    47
wenzelm@23268
    48
end