1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Fri Oct 18 14:36:51 2013 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Mon Oct 21 09:03:50 2013 +0200
     1.3 @@ -3,69 +3,76 @@
     1.4     (c) copyright due to lincense terms.
     1.5  *)
     1.6  
     1.7 +"-----------------------------------------------------------------------------";
     1.8 +"-----------------------------------------------------------------------------";
     1.9 +"table of contents -----------------------------------------------------------";
    1.10 +"-----------------------------------------------------------------------------";
    1.11 +"--------------------- NTH ---------------------------------------------------";
    1.12 +"--------------------- LENGTH ------------------------------------------------";
    1.13 +"--------------------- tl ----------------------------------------------------";
    1.14 +"-----------------------------------------------------------------------------";
    1.15 +"-----------------------------------------------------------------------------";
    1.16  
    1.17  
    1.18 -"--------------------- nth_ ----------------------------------------------";
    1.19 -"--------------------- nth_ ----------------------------------------------";
    1.20 -"--------------------- nth_ ----------------------------------------------";
    1.21 -val t = str2term "nth_ 3 [a,b,c,d,e]";
    1.22 +"--------------------- NTH ---------------------------------------------------";
    1.23 +"--------------------- NTH ---------------------------------------------------";
    1.24 +"--------------------- NTH ---------------------------------------------------";
    1.25 +val list_rls = assoc_rls "list_rls"
    1.26 +
    1.27 +val t = str2term "NTH 1 [a,b,c,d,e]";
    1.28 +atomty t;
    1.29 +val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};
    1.30 +atomty thm;
    1.31 +val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_NIL}) t;
    1.32 +if term2str t' = "a" then () 
    1.33 +else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.34 +
    1.35 +val t = str2term "NTH 3 [a,b,c,d,e]";
    1.36 +val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
    1.37 +  (Const ("List.list.Cons", _) $ Free ("b", _) $ 
    1.38 +    (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
    1.39  atomty t;
    1.40  val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS};
    1.41  atomty thm;
    1.42 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_CONS}) t;
    1.43 -if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then () 
    1.44 -else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
    1.45 +val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_CONS}) t;
    1.46 +if term2str t' = "NTH (3 + -1) [b, c, d, e]" then () 
    1.47 +else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.48  
    1.49 -val t = str2term "nth_ 1 [a,b,c,d,e]";
    1.50 +(* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    1.51 +val t = str2term "NTH 3 [a,b,c,d,e]";
    1.52  atomty t;
    1.53 -val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};
    1.54 -atomty thm;
    1.55 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_NIL}) t;
    1.56 -term2str t';
    1.57 -"a";
    1.58 +trace_rewrite := true;
    1.59 +val SOME (t', _) = rewrite_set_ thy false list_rls t;
    1.60 +trace_rewrite := false;
    1.61 +if term2str t' = "c" then () 
    1.62 +else error "NTH 3 [a,b,c,d,e] = c ..changed";
    1.63  
    1.64 -val t = str2term "nth_ 3 [a,b,c,d,e]";
    1.65 -atomty t;
    1.66 -trace_rewrite:=true;
    1.67 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
    1.68 -trace_rewrite:=false;
    1.69 -term2str t';
    1.70 -"c";
    1.71 +"--------------------- LENGTH ------------------------------------------------";
    1.72 +"--------------------- LENGTH ------------------------------------------------";
    1.73 +"--------------------- LENGTH ------------------------------------------------";
    1.74 +val list_rls = assoc_rls "list_rls"
    1.75  
    1.76 -(*-------------------------------------------------------------------*)
    1.77 -val SOME (Thm (_,thm)) = rls_get_thm list_rls "NTH_NIL";
    1.78 -val ttt = (#prop o rep_thm) thm;
    1.79 -atomty ttt;
    1.80 -(*Free ( 1, real)   ...OK, Var ((x, 0), ?'a) OK*)
    1.81 +val thy = @{theory ListC};
    1.82 +val t = str2term "LENGTH [1, 1, 1]";
    1.83 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.84 +term2str t = "1 + LENGTH [1, 1]";
    1.85 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.86 +term2str t = "1 + (1 + LENGTH [1])";
    1.87 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.88 +term2str t = "1 + (1 + (1 + LENGTH []))";
    1.89 +val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.90 +val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.91 +val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.92 +if term2str t = "1 + (1 + (1 + 0))" then () 
    1.93 +else error "LENGTH [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
    1.94  
    1.95 +val t = str2term "LENGTH [1, 1, 1]";
    1.96 +val SOME (t, asm) = rewrite_set_ thy false list_rls t;
    1.97 +if term2str t = "3" then ()
    1.98 +else error "LENGTH [1, 1, 1] = 3  ..list_rls changed";
    1.99  
   1.100 +val t = str2term "LENGTH [1, 1, 1]";
   1.101 +val t = eval_listexpr_ thy list_rls t;
   1.102 +case t of Free ("3", _) => () 
   1.103 +| _ => error "LENGTH [1, 1, 1] = 3  ..eval_listexpr_ changed";
   1.104  
   1.105 -"--------------------- length_ -------------------------------------------";
   1.106 -"--------------------- length_ -------------------------------------------";
   1.107 -"--------------------- length_ -------------------------------------------";
   1.108 -val thy' = "ListG";
   1.109 -val ct = "length_ [1,1,1]";
   1.110 -val thm = (@{thm LENGTH_CONS},"");
   1.111 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
   1.112 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
   1.113 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
   1.114 -val thm = (@{thm LENGTH_NIL},"");
   1.115 -val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
   1.116 -if ct="1 + (1 + (1 + 0))"then()
   1.117 -else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
   1.118 -
   1.119 -
   1.120 -val ct = "length_ [1,1,1]";
   1.121 -val rls = "list_rls";
   1.122 -val (ct,asm) = the (rewrite_set thy' false rls ct);
   1.123 -if ct="3"then()
   1.124 -else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct);
   1.125 -
   1.126 -
   1.127 -val ct = "length_ [1,1,1]";
   1.128 -val t = (term_of o the o (parse ListG.thy)) ct;
   1.129 -val t = eval_listexpr_ ListG.thy list_rls t;
   1.130 -case t of Free ("3",_) => () 
   1.131 -| _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct);
   1.132 -
   1.133 -