12 "--------------------- nth_ ----------------------------------------------"; |
12 "--------------------- nth_ ----------------------------------------------"; |
13 val t = str2term "nth_ 3 [a,b,c,d,e]"; |
13 val t = str2term "nth_ 3 [a,b,c,d,e]"; |
14 atomty t; |
14 atomty t; |
15 val thm = (#prop o rep_thm o num_str) nth_Cons_; |
15 val thm = (#prop o rep_thm o num_str) nth_Cons_; |
16 atomty thm; |
16 atomty thm; |
17 val Some (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Cons_) t; |
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 () |
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]"; |
19 else raise error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]"; |
20 |
20 |
21 val t = str2term "nth_ 1 [a,b,c,d,e]"; |
21 val t = str2term "nth_ 1 [a,b,c,d,e]"; |
22 atomty t; |
22 atomty t; |
23 val thm = (#prop o rep_thm o num_str) nth_Nil_; |
23 val thm = (#prop o rep_thm o num_str) nth_Nil_; |
24 atomty thm; |
24 atomty thm; |
25 val Some (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Nil_) t; |
25 val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Nil_) t; |
26 term2str t'; |
26 term2str t'; |
27 "a"; |
27 "a"; |
28 |
28 |
29 val t = str2term "nth_ 3 [a,b,c,d,e]"; |
29 val t = str2term "nth_ 3 [a,b,c,d,e]"; |
30 atomty t; |
30 atomty t; |
31 trace_rewrite:=true; |
31 trace_rewrite:=true; |
32 val Some (t',_) = rewrite_set_ thy false list_rls t; |
32 val SOME (t',_) = rewrite_set_ thy false list_rls t; |
33 trace_rewrite:=false; |
33 trace_rewrite:=false; |
34 term2str t'; |
34 term2str t'; |
35 "c"; |
35 "c"; |
36 |
36 |
37 (*-------------------------------------------------------------------*) |
37 (*-------------------------------------------------------------------*) |
38 val Some (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_"; |
38 val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_"; |
39 val ttt = (#prop o rep_thm) thm; |
39 val ttt = (#prop o rep_thm) thm; |
40 atomty ttt; |
40 atomty ttt; |
41 (*Free ( 1, real) ...OK, Var ((x, 0), ?'a) OK*) |
41 (*Free ( 1, real) ...OK, Var ((x, 0), ?'a) OK*) |
42 |
42 |
43 |
43 |