29106
|
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
|