49 |
49 |
50 val t = TermC.str2term "NTH 1 [a,b,c,d,e]"; |
50 val t = TermC.str2term "NTH 1 [a,b,c,d,e]"; |
51 TermC.atomty t; |
51 TermC.atomty t; |
52 val thm = Thm.prop_of @{thm NTH_NIL}; |
52 val thm = Thm.prop_of @{thm NTH_NIL}; |
53 TermC.atomty thm; |
53 TermC.atomty thm; |
54 val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_NIL} t; |
54 val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t; |
55 if UnparseC.term t' = "a" then () |
55 if UnparseC.term t' = "a" then () |
56 else error "NTH 1 [a,b,c,d,e] = a ..changed"; |
56 else error "NTH 1 [a,b,c,d,e] = a ..changed"; |
57 |
57 |
58 val t = TermC.str2term "NTH 3 [a,b,c,d,e]"; |
58 val t = TermC.str2term "NTH 3 [a,b,c,d,e]"; |
59 case TermC.str2term "NTH 3 [a,b,c,d,e]" of |
59 case TermC.str2term "NTH 3 [a,b,c,d,e]" of |
64 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $ |
64 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $ |
65 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => () |
65 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => () |
66 | _ => error "ListC.NTH changed"; |
66 | _ => error "ListC.NTH changed"; |
67 val thm = Thm.prop_of @{thm NTH_CONS}; |
67 val thm = Thm.prop_of @{thm NTH_CONS}; |
68 TermC.atomty thm; |
68 TermC.atomty thm; |
69 val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_CONS} t; |
69 val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_CONS} t; |
70 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () |
70 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () |
71 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed"; |
71 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed"; |
72 |
72 |
73 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *) |
73 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *) |
74 val t = TermC.str2term "NTH 3 [a,b,c,d,e]"; |
74 val t = TermC.str2term "NTH 3 [a,b,c,d,e]"; |