src/HOL/ex/CodegenSML_Test.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29106 25e28a4070f3
child 41959 b460124855b8
permissions -rw-r--r--
added lemmas
     1 (*  Title:      Test file for Stefan Berghofer's SML code generator
     2     Author:     Tobias Nipkow, TU Muenchen
     3 *)
     4 
     5 theory CodegenSML_Test
     6 imports Executable_Set
     7 begin
     8 
     9 lemma "True : {False, True} & False ~: {True}"
    10 by evaluation
    11 
    12 lemma
    13 "eq_set ({1::nat,2,3,2} \<union> {3,1,2,1}) {2,2,3,1} &
    14  eq_set ({1::nat,2,3,2} \<union> {4,1,5,1}) {4,4,5,1,2,3}"
    15 by evaluation
    16 
    17 lemma
    18 "eq_set ({1::nat,2,3,2} \<inter> {3,1,2,1}) {2,2,3,1} & 
    19  eq_set ({1::nat,2,3,2} \<inter> {4,1,5,2}) {2,1,2}"
    20 by evaluation
    21 
    22 lemma
    23 "eq_set ({1::nat,2,3,2} - {3,1,2,1}) {} & 
    24  eq_set ({1::nat,2,3,2} - {4,1,5,2}) {3}"
    25 by evaluation
    26 
    27 lemma
    28 "eq_set (Union{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} &
    29  eq_set (Union{{1::nat,2,3,2}, {4,1,5,1}}) {4,4,5,1,2,3}"
    30 by evaluation
    31 
    32 lemma
    33 "eq_set (Inter{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} & 
    34  eq_set (Inter{{1::nat,2,3,2}, {4,1,5,2}}) {2,1,2}"
    35 by evaluation
    36 
    37 lemma "eq_set ((%x. x+2) ` {1::nat,2,3,2}) {4,5,3,3}"
    38 by evaluation
    39 
    40 lemma
    41 "(ALL x:{1::nat,2,3,2}. EX y : {4,5,2}. x < y) &
    42  (EX x:{1::nat,2,3,2}. ALL y : {4,5,6}. x < y)"
    43 by evaluation
    44 
    45 lemma
    46 "eq_set {x : {4::nat,7,10}. 2 dvd x } {4,10}"
    47 by evaluation
    48 
    49 lemma
    50 "fold (op +) (5::int) {3,7,9} = 24 &
    51  fold_image (op *) id (2::int) {3,4,5} = 120"
    52 by evaluation
    53 
    54 end