|
neuper@42185
|
1 |
(* Title: tests for ListC
|
|
neuper@42185
|
2 |
Author: Walther Neuper 030501
|
|
neuper@42185
|
3 |
(c) copyright due to lincense terms.
|
|
neuper@42185
|
4 |
*)
|
|
neuper@42185
|
5 |
|
|
neuper@52148
|
6 |
"-----------------------------------------------------------------------------";
|
|
neuper@52148
|
7 |
"-----------------------------------------------------------------------------";
|
|
neuper@52148
|
8 |
"table of contents -----------------------------------------------------------";
|
|
neuper@52148
|
9 |
"-----------------------------------------------------------------------------";
|
|
neuper@52148
|
10 |
"--------------------- NTH ---------------------------------------------------";
|
|
neuper@52148
|
11 |
"--------------------- LENGTH ------------------------------------------------";
|
|
neuper@52148
|
12 |
"--------------------- tl ----------------------------------------------------";
|
|
neuper@52148
|
13 |
"-----------------------------------------------------------------------------";
|
|
neuper@52148
|
14 |
"-----------------------------------------------------------------------------";
|
|
neuper@42185
|
15 |
|
|
neuper@42185
|
16 |
|
|
neuper@52148
|
17 |
"--------------------- NTH ---------------------------------------------------";
|
|
neuper@52148
|
18 |
"--------------------- NTH ---------------------------------------------------";
|
|
neuper@52148
|
19 |
"--------------------- NTH ---------------------------------------------------";
|
|
neuper@52148
|
20 |
val list_rls = assoc_rls "list_rls"
|
|
neuper@52148
|
21 |
|
|
neuper@52148
|
22 |
val t = str2term "NTH 1 [a,b,c,d,e]";
|
|
neuper@52148
|
23 |
atomty t;
|
|
neuper@52148
|
24 |
val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};
|
|
neuper@52148
|
25 |
atomty thm;
|
|
neuper@52148
|
26 |
val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_NIL}) t;
|
|
neuper@52148
|
27 |
if term2str t' = "a" then ()
|
|
neuper@52148
|
28 |
else error "NTH 1 [a,b,c,d,e] = a ..changed";
|
|
neuper@52148
|
29 |
|
|
neuper@52148
|
30 |
val t = str2term "NTH 3 [a,b,c,d,e]";
|
|
neuper@52148
|
31 |
val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
|
|
neuper@52148
|
32 |
(Const ("List.list.Cons", _) $ Free ("b", _) $
|
|
neuper@52148
|
33 |
(Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
|
|
neuper@42185
|
34 |
atomty t;
|
|
neuper@42390
|
35 |
val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS};
|
|
neuper@42185
|
36 |
atomty thm;
|
|
neuper@52148
|
37 |
val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_CONS}) t;
|
|
neuper@52148
|
38 |
if term2str t' = "NTH (3 + -1) [b, c, d, e]" then ()
|
|
neuper@52148
|
39 |
else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
|
|
neuper@42185
|
40 |
|
|
neuper@52148
|
41 |
(* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
|
|
neuper@52148
|
42 |
val t = str2term "NTH 3 [a,b,c,d,e]";
|
|
neuper@42185
|
43 |
atomty t;
|
|
neuper@52148
|
44 |
trace_rewrite := true;
|
|
neuper@52148
|
45 |
val SOME (t', _) = rewrite_set_ thy false list_rls t;
|
|
neuper@52148
|
46 |
trace_rewrite := false;
|
|
neuper@52148
|
47 |
if term2str t' = "c" then ()
|
|
neuper@52148
|
48 |
else error "NTH 3 [a,b,c,d,e] = c ..changed";
|
|
neuper@42185
|
49 |
|
|
neuper@52148
|
50 |
"--------------------- LENGTH ------------------------------------------------";
|
|
neuper@52148
|
51 |
"--------------------- LENGTH ------------------------------------------------";
|
|
neuper@52148
|
52 |
"--------------------- LENGTH ------------------------------------------------";
|
|
neuper@52148
|
53 |
val list_rls = assoc_rls "list_rls"
|
|
neuper@42185
|
54 |
|
|
neuper@52148
|
55 |
val thy = @{theory ListC};
|
|
neuper@52148
|
56 |
val t = str2term "LENGTH [1, 1, 1]";
|
|
neuper@52148
|
57 |
val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
|
|
neuper@52148
|
58 |
term2str t = "1 + LENGTH [1, 1]";
|
|
neuper@52148
|
59 |
val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
|
|
neuper@52148
|
60 |
term2str t = "1 + (1 + LENGTH [1])";
|
|
neuper@52148
|
61 |
val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
|
|
neuper@52148
|
62 |
term2str t = "1 + (1 + (1 + LENGTH []))";
|
|
neuper@52148
|
63 |
val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
|
|
neuper@52148
|
64 |
val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
|
|
neuper@52148
|
65 |
val NONE = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
|
|
neuper@52148
|
66 |
if term2str t = "1 + (1 + (1 + 0))" then ()
|
|
neuper@52148
|
67 |
else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed";
|
|
neuper@42185
|
68 |
|
|
neuper@52148
|
69 |
val t = str2term "LENGTH [1, 1, 1]";
|
|
neuper@52148
|
70 |
val SOME (t, asm) = rewrite_set_ thy false list_rls t;
|
|
neuper@52148
|
71 |
if term2str t = "3" then ()
|
|
neuper@52148
|
72 |
else error "LENGTH [1, 1, 1] = 3 ..list_rls changed";
|
|
neuper@42185
|
73 |
|
|
neuper@52148
|
74 |
val t = str2term "LENGTH [1, 1, 1]";
|
|
neuper@52148
|
75 |
val t = eval_listexpr_ thy list_rls t;
|
|
neuper@52148
|
76 |
case t of Free ("3", _) => ()
|
|
neuper@52148
|
77 |
| _ => error "LENGTH [1, 1, 1] = 3 ..eval_listexpr_ changed";
|
|
neuper@42185
|
78 |
|