2 author: Walther Neuper 1.5.03
4 use"../smltest/Scripts/listg.sml";
10 "--------------------- nth_ ----------------------------------------------";
11 "--------------------- nth_ ----------------------------------------------";
12 "--------------------- nth_ ----------------------------------------------";
13 val t = str2term "nth_ 3 [a,b,c,d,e]";
15 val thm = (#prop o rep_thm o num_str) nth_Cons_;
17 val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Cons_) t;
18 if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then ()
19 else raise error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
21 val t = str2term "nth_ 1 [a,b,c,d,e]";
23 val thm = (#prop o rep_thm o num_str) nth_Nil_;
25 val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Nil_) t;
29 val t = str2term "nth_ 3 [a,b,c,d,e]";
32 val SOME (t',_) = rewrite_set_ thy false list_rls t;
37 (*-------------------------------------------------------------------*)
38 val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";
39 val ttt = (#prop o rep_thm) thm;
41 (*Free ( 1, real) ...OK, Var ((x, 0), ?'a) OK*)
45 "--------------------- length_ -------------------------------------------";
46 "--------------------- length_ -------------------------------------------";
47 "--------------------- length_ -------------------------------------------";
48 val thy' = "ListG.thy";
49 val ct = "length_ [1,1,1]";
50 val thm = ("length_Cons_","");
51 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
52 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
53 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
54 val thm = ("length_Nil_","");
55 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
56 if ct="1 + (1 + (1 + 0))"then()
57 else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
60 val ct = "length_ [1,1,1]";
62 val (ct,asm) = the (rewrite_set thy' false rls ct);
64 else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
67 val ct = "length_ [1,1,1]";
68 val t = (term_of o the o (parse ListG.thy)) ct;
69 val t = eval_listexpr_ ListG.thy list_rls t;
70 case t of Free ("3",_) => ()
71 | _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);