(* Title: tests for ListC

   Author: Walther Neuper 030501

   (c) copyright due to lincense terms.

*)

"--------------------- nth_ ----------------------------------------------";

"--------------------- nth_ ----------------------------------------------";

"--------------------- nth_ ----------------------------------------------";

val t = str2term "nth_ 3 [a,b,c,d,e]";

atomty t;

val thm = (#prop o rep_thm o num_str) nth_Cons_;

atomty thm;

val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Cons_}) t;

if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 

else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";

val t = str2term "nth_ 1 [a,b,c,d,e]";

atomty t;

val thm = (#prop o rep_thm o num_str) nth_Nil_;

atomty thm;

val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Nil_}) t;

term2str t';

"a";

val t = str2term "nth_ 3 [a,b,c,d,e]";

atomty t;

trace_rewrite:=true;

val SOME (t',_) = rewrite_set_ thy false list_rls t;

trace_rewrite:=false;

term2str t';

"c";

(*-------------------------------------------------------------------*)

val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";

val ttt = (#prop o rep_thm) thm;

atomty ttt;

(*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)

"--------------------- length_ -------------------------------------------";

"--------------------- length_ -------------------------------------------";

"--------------------- length_ -------------------------------------------";

val thy' = "ListG";

val ct = "length_ [1,1,1]";

val thm = ("length_Cons_","");

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

val thm = ("length_Nil_","");

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);

if ct="1 + (1 + (1 + 0))"then()

else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);

val ct = "length_ [1,1,1]";

val rls = "list_rls";

val (ct,asm) = the (rewrite_set thy' false rls ct);

if ct="3"then()

else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);

val ct = "length_ [1,1,1]";

val t = (term_of o the o (parse ListG.thy)) ct;

val t = eval_listexpr_ ListG.thy list_rls t;

case t of Free ("3",_) => () 

| _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);