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