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 @{thm nth_Cons_}) t; |
17 val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm 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 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; |
52 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); |
53 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); |
54 val thm = ("length_Nil_",""); |
54 val thm = ("length_Nil_",""); |
55 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); |
55 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); |
56 if ct="1 + (1 + (1 + 0))"then() |
56 if ct="1 + (1 + (1 + 0))"then() |
57 else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct); |
57 else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct); |
58 |
58 |
59 |
59 |
60 val ct = "length_ [1,1,1]"; |
60 val ct = "length_ [1,1,1]"; |
61 val rls = "list_rls"; |
61 val rls = "list_rls"; |
62 val (ct,asm) = the (rewrite_set thy' false rls ct); |
62 val (ct,asm) = the (rewrite_set thy' false rls ct); |
63 if ct="3"then() |
63 if ct="3"then() |
64 else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct); |
64 else error ("list_rls.sml 2: behaviour of test-expl changed: "^ct); |
65 |
65 |
66 |
66 |
67 val ct = "length_ [1,1,1]"; |
67 val ct = "length_ [1,1,1]"; |
68 val t = (term_of o the o (parse ListG.thy)) ct; |
68 val t = (term_of o the o (parse ListG.thy)) ct; |
69 val t = eval_listexpr_ ListG.thy list_rls t; |
69 val t = eval_listexpr_ ListG.thy list_rls t; |
70 case t of Free ("3",_) => () |
70 case t of Free ("3",_) => () |
71 | _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct); |
71 | _ => error ("list-rls.sml 3: behaviour of test-expl changed: "^ct); |
72 |
72 |
73 |
73 |