83 val t = str2term "LENGTH [x+y=1,y=2] = 2"; |
83 val t = str2term "LENGTH [x+y=1,y=2] = 2"; |
84 atomty t; |
84 atomty 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",ThmC.numerals_to_Free @{thm LENGTH_NIL})), |
86 [(Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL})), |
87 (Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS})), |
87 (Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS})), |
88 Num_Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
88 Eval ("Groups.plus_class.plus", eval_binop "#add_"), |
89 Num_Calc ("HOL.eq",eval_equal "#equal_") |
89 Eval ("HOL.eq",eval_equal "#equal_") |
90 ]; |
90 ]; |
91 val SOME (t',_) = rewrite_set_ thy false testrls t; |
91 val SOME (t',_) = rewrite_set_ thy 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 |
107 (Rule_Set.append_rules "prls_" Rule_Set.empty |
107 (Rule_Set.append_rules "prls_" Rule_Set.empty |
108 [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}), |
108 [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}), |
109 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}), |
109 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}), |
110 Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}), |
110 Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}), |
111 Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}), |
111 Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}), |
112 Num_Calc ("EqSystem.occur'_exactly'_in", eval_occur_exactly_in "#eval_occur_exactly_in_") |
112 Eval ("EqSystem.occur'_exactly'_in", eval_occur_exactly_in "#eval_occur_exactly_in_") |
113 ]) t; |
113 ]) t; |
114 if t = @{term True} then () |
114 if t = @{term True} then () |
115 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4.."; |
115 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4.."; |
116 |
116 |
117 "----------- rewrite-order ord_simplify_System -------------------"; |
117 "----------- rewrite-order ord_simplify_System -------------------"; |
369 nth_ (2 + - 1 + - 1) [] |
369 nth_ (2 + - 1 + - 1) [] |
370 #### rls: erls_prls_triangular on: 1 < 2 + - 1 |
370 #### rls: erls_prls_triangular on: 1 < 2 + - 1 |
371 ##### try calc: op <' |
371 ##### try calc: op <' |
372 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"] |
372 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"] |
373 |
373 |
374 ... i.e Num_Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*) |
374 ... i.e Eval ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*) |
375 trace_rewrite:=false; |
375 trace_rewrite:=false; |
376 |
376 |
377 "===== case 3: relaxed preconditions for triangular system ====="; |
377 "===== case 3: relaxed preconditions for triangular system ====="; |
378 val fmz = ["equalities [L * q_0 = c, \ |
378 val fmz = ["equalities [L * q_0 = c, \ |
379 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\ |
379 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\ |