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