79 |
79 |
80 "----------- problems --------------------------------------------"; |
80 "----------- problems --------------------------------------------"; |
81 "----------- problems --------------------------------------------"; |
81 "----------- problems --------------------------------------------"; |
82 "----------- problems --------------------------------------------"; |
82 "----------- problems --------------------------------------------"; |
83 val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2"; |
83 val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2"; |
84 TermC.atomty t; |
84 TermC.atom_trace_detail @{context} t; |
85 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty |
85 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty |
86 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})), |
86 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})), |
87 (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})), |
87 (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})), |
88 Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"), |
88 Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"), |
89 Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_") |
89 Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_") |
91 val SOME (t',_) = rewrite_set_ ctxt false testrls t; |
91 val SOME (t',_) = rewrite_set_ ctxt false testrls t; |
92 if UnparseC.term t' = "True" then () |
92 if UnparseC.term t' = "True" then () |
93 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2"; |
93 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2"; |
94 |
94 |
95 val SOME t = TermC.parseNEW ctxt "solution LL"; |
95 val SOME t = TermC.parseNEW ctxt "solution LL"; |
96 TermC.atomty t; |
96 TermC.atom_trace_detail @{context} t; |
97 val SOME t = TermC.parseNEW ctxt "solution LL"; |
97 val SOME t = TermC.parseNEW ctxt "solution LL"; |
98 TermC.atomty t; |
98 TermC.atom_trace_detail @{context} t; |
99 |
99 |
100 val t = TermC.parse_test @{context} |
100 val t = TermC.parse_test @{context} |
101 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"; |
101 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"; |
102 TermC.atomty t; |
102 TermC.atom_trace_detail @{context} t; |
103 val t = TermC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^ |
103 val t = TermC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^ |
104 "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])"); |
104 "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])"); |
105 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\ |
105 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\ |
106 assume flawed test setup hidden by "handle _ => ..." |
106 assume flawed test setup hidden by "handle _ => ..." |
107 ERROR rewrite__set_ called with 'Erls' for '1 < 1' |
107 ERROR rewrite__set_ called with 'Erls' for '1 < 1' |
500 |
500 |
501 > val es_ = (fst o hd) env; |
501 > val es_ = (fst o hd) env; |
502 val es_ = Free ("es_", "bool List.list") : Term.term |
502 val es_ = Free ("es_", "bool List.list") : Term.term |
503 |
503 |
504 > val pre1 = hd pres; |
504 > val pre1 = hd pres; |
505 TermC.atomty pre1; |
505 TermC.atom_trace_detail @{context} pre1; |
506 *** |
506 *** |
507 *** Const (op =, [real, real] => bool) |
507 *** Const (op =, [real, real] => bool) |
508 *** . Const (ListG.length_, real list => real) |
508 *** . Const (ListG.length_, real list => real) |
509 *** . . Free (es_, real list) |
509 *** . . Free (es_, real list) |
510 ~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~ |
510 ~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~ |