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
nipkow@29106
     1
(*  Title:      Test file for Stefan Berghofer's SML code generator
nipkow@29106
     2
    Author:     Tobias Nipkow, TU Muenchen
nipkow@29106
     3
*)
nipkow@29106
     4
nipkow@29106
     5
theory CodegenSML_Test
nipkow@29106
     6
imports Executable_Set
nipkow@29106
     7
begin
nipkow@29106
     8
nipkow@29106
     9
lemma "True : {False, True} & False ~: {True}"
nipkow@29106
    10
by evaluation
nipkow@29106
    11
nipkow@29106
    12
lemma
nipkow@29106
    13
"eq_set ({1::nat,2,3,2} \<union> {3,1,2,1}) {2,2,3,1} &
nipkow@29106
    14
 eq_set ({1::nat,2,3,2} \<union> {4,1,5,1}) {4,4,5,1,2,3}"
nipkow@29106
    15
by evaluation
nipkow@29106
    16
nipkow@29106
    17
lemma
nipkow@29106
    18
"eq_set ({1::nat,2,3,2} \<inter> {3,1,2,1}) {2,2,3,1} & 
nipkow@29106
    19
 eq_set ({1::nat,2,3,2} \<inter> {4,1,5,2}) {2,1,2}"
nipkow@29106
    20
by evaluation
nipkow@29106
    21
nipkow@29106
    22
lemma
nipkow@29106
    23
"eq_set ({1::nat,2,3,2} - {3,1,2,1}) {} & 
nipkow@29106
    24
 eq_set ({1::nat,2,3,2} - {4,1,5,2}) {3}"
nipkow@29106
    25
by evaluation
nipkow@29106
    26
nipkow@29106
    27
lemma
nipkow@29106
    28
"eq_set (Union{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} &
nipkow@29106
    29
 eq_set (Union{{1::nat,2,3,2}, {4,1,5,1}}) {4,4,5,1,2,3}"
nipkow@29106
    30
by evaluation
nipkow@29106
    31
nipkow@29106
    32
lemma
nipkow@29106
    33
"eq_set (Inter{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} & 
nipkow@29106
    34
 eq_set (Inter{{1::nat,2,3,2}, {4,1,5,2}}) {2,1,2}"
nipkow@29106
    35
by evaluation
nipkow@29106
    36
nipkow@29106
    37
lemma "eq_set ((%x. x+2) ` {1::nat,2,3,2}) {4,5,3,3}"
nipkow@29106
    38
by evaluation
nipkow@29106
    39
nipkow@29106
    40
lemma
nipkow@29106
    41
"(ALL x:{1::nat,2,3,2}. EX y : {4,5,2}. x < y) &
nipkow@29106
    42
 (EX x:{1::nat,2,3,2}. ALL y : {4,5,6}. x < y)"
nipkow@29106
    43
by evaluation
nipkow@29106
    44
nipkow@29106
    45
lemma
nipkow@29106
    46
"eq_set {x : {4::nat,7,10}. 2 dvd x } {4,10}"
nipkow@29106
    47
by evaluation
nipkow@29106
    48
nipkow@29106
    49
lemma
nipkow@29106
    50
"fold (op +) (5::int) {3,7,9} = 24 &
nipkow@29106
    51
 fold_image (op *) id (2::int) {3,4,5} = 120"
nipkow@29106
    52
by evaluation
nipkow@29106
    53
nipkow@29106
    54
end