src/HOL/ex/Eval_Examples.thy
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 44022 2d633b795d4a
child 45170 7dd207fe7b6e
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Small examples for evaluation mechanisms *}
     4 
     5 theory Eval_Examples
     6 imports Complex_Main
     7 begin
     8 
     9 text {* evaluation oracle *}
    10 
    11 lemma "True \<or> False" by eval
    12 lemma "Suc 0 \<noteq> Suc 1" by eval
    13 lemma "[] = ([] :: int list)" by eval
    14 lemma "[()] = [()]" by eval
    15 lemma "fst ([] :: nat list, Suc 0) = []" by eval
    16 
    17 text {* SML evaluation oracle *}
    18 
    19 lemma "True \<or> False" by evaluation
    20 lemma "Suc 0 \<noteq> Suc 1" by evaluation
    21 lemma "[] = ([] :: int list)" by evaluation
    22 lemma "[()] = [()]" by evaluation
    23 lemma "fst ([] :: nat list, Suc 0) = []" by evaluation
    24 
    25 text {* normalization *}
    26 
    27 lemma "True \<or> False" by normalization
    28 lemma "Suc 0 \<noteq> Suc 1" by normalization
    29 lemma "[] = ([] :: int list)" by normalization
    30 lemma "[()] = [()]" by normalization
    31 lemma "fst ([] :: nat list, Suc 0) = []" by normalization
    32 
    33 text {* term evaluation *}
    34 
    35 value "(Suc 2 + 1) * 4"
    36 value [code] "(Suc 2 + 1) * 4"
    37 value [nbe] "(Suc 2 + 1) * 4"
    38 
    39 value "(Suc 2 + Suc 0) * Suc 3"
    40 value [code] "(Suc 2 + Suc 0) * Suc 3"
    41 value [nbe] "(Suc 2 + Suc 0) * Suc 3"
    42 
    43 value "nat 100"
    44 value [code] "nat 100"
    45 value [nbe] "nat 100"
    46 
    47 value "(10::int) \<le> 12"
    48 value [code] "(10::int) \<le> 12"
    49 value [nbe] "(10::int) \<le> 12"
    50 
    51 value "max (2::int) 4"
    52 value [code] "max (2::int) 4"
    53 value [nbe] "max (2::int) 4"
    54 
    55 value "of_int 2 / of_int 4 * (1::rat)"
    56 value [code] "of_int 2 / of_int 4 * (1::rat)"
    57 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
    58 
    59 value "[] :: nat list"
    60 value [code] "[] :: nat list"
    61 value [nbe] "[] :: nat list"
    62 
    63 value "[(nat 100, ())]"
    64 value [code] "[(nat 100, ())]"
    65 value [nbe] "[(nat 100, ())]"
    66 
    67 text {* a fancy datatype *}
    68 
    69 datatype ('a, 'b) foo =
    70     Foo "'a\<Colon>order" 'b
    71   | Bla "('a, 'b) bar"
    72   | Dummy nat
    73 and ('a, 'b) bar =
    74     Bar 'a 'b
    75   | Blubb "('a, 'b) foo"
    76 
    77 value "Bla (Bar (4::nat) [Suc 0])"
    78 value [code] "Bla (Bar (4::nat) [Suc 0])"
    79 value [nbe] "Bla (Bar (4::nat) [Suc 0])"
    80 
    81 end