282 2.3. 1 + (x + - 1 * 2) = 0\n |
282 2.3. 1 + (x + - 1 * 2) = 0\n |
283 2.4. 1 + (x + -2) = 0\n |
283 2.4. 1 + (x + -2) = 0\n |
284 2.5. 1 + (x + -2 * 1) = 0\n |
284 2.5. 1 + (x + -2 * 1) = 0\n |
285 2.6. 1 + x + -2 * 1 = 0\n"; |
285 2.6. 1 + x + -2 * 1 = 0\n"; |
286 *) |
286 *) |
287 if str = |
287 if str = |
288 ". ----- pblobj -----\n"^ |
288 ". ----- pblobj -----\n"^ |
289 "1. x + 1 = 2\n"^ |
289 "1. x + 1 = 2\n"^ |
290 "2. x + 1 + - 1 * 2 = 0\n"^ |
290 "2. x + 1 + - 1 * 2 = 0\n"^ |
291 "2.1. x + 1 + - 1 * 2 = 0\n"^ |
291 "2.1. x + 1 + - 1 * 2 = 0\n"^ |
292 "2.2. 1 + x + - 1 * 2 = 0\n"^ |
292 "2.2. 1 + x + - 1 * 2 = 0\n"^ |
923 res' = inf; |
923 res' = inf; |
924 norm_res = norm_inf; |
924 norm_res = norm_inf; |
925 |
925 |
926 val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b"; |
926 val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b"; |
927 val (res, inf) = (TermC.str2term "(2 + 3)/2", TermC.str2term "3"); |
927 val (res, inf) = (TermC.str2term "(2 + 3)/2", TermC.str2term "3"); |
928 if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" |
928 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" |
929 then () else error "error patt example1 changed"; |
929 then () else error "error patt example1 changed"; |
930 |
930 |
931 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c"; |
931 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c"; |
932 val (res, inf) = (TermC.str2term "(2 + 3)/(2 + 4)", TermC.str2term "3 / 4"); |
932 val (res, inf) = (TermC.str2term "(2 + 3)/(2 + 4)", TermC.str2term "3 / 4"); |
933 if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" |
933 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" |
934 then () else error "error patt example2 changed"; |
934 then () else error "error patt example2 changed"; |
935 |
935 |
936 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c"; |
936 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c"; |
937 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4"); |
937 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4"); |
938 if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" |
938 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" |
939 then () else error "error patt example3 changed"; |
939 then () else error "error patt example3 changed"; |
940 |
940 |
941 val inf = TermC.str2term "1 / 2"; |
941 val inf = TermC.str2term "1 / 2"; |
942 if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" |
942 if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" |
943 then () else error "error patt example3 changed"; |
943 then () else error "error patt example3 changed"; |
944 |
944 |
945 "--------- build fun check_for' ?bdv -------------------------"; |
945 "--------- build fun check_for' ?bdv -------------------------"; |
946 "--------- build fun check_for' ?bdv -------------------------"; |
946 "--------- build fun check_for' ?bdv -------------------------"; |
947 "--------- build fun check_for' ?bdv -------------------------"; |
947 "--------- build fun check_for' ?bdv -------------------------"; |
975 |
975 |
976 res' = inf; |
976 res' = inf; |
977 if norm_res = norm_inf then () |
977 if norm_res = norm_inf then () |
978 else error "build fun check_for' ?bdv changed 5"; |
978 else error "build fun check_for' ?bdv changed 5"; |
979 |
979 |
980 if Error_Pattern.check_for' (res, inf) (subst: subst) ("errpatID": Error_Pattern.id, pat) rls = SOME "errpatID" |
980 if Error_Pattern.check_for' ctxt (res, inf) (subst: subst) ("errpatID": Error_Pattern.id, pat) rls = SOME "errpatID" |
981 then () else error "error patt example1 changed"; |
981 then () else error "error patt example1 changed"; |
982 |
982 |
983 "--------- build fun check_for ------------------------"; |
983 "--------- build fun check_for ------------------------"; |
984 "--------- build fun check_for ------------------------"; |
984 "--------- build fun check_for ------------------------"; |
985 "--------- build fun check_for ------------------------"; |
985 "--------- build fun check_for ------------------------"; |
997 TermC.parse_patt @{theory} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)", |
997 TermC.parse_patt @{theory} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)", |
998 TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u", |
998 TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u", |
999 TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"], |
999 TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"], |
1000 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, |
1000 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, |
1001 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]; |
1001 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]; |
1002 case Error_Pattern.check_for (res, inf) (prog, env) (errpats, rls) of SOME _ => () |
1002 case Error_Pattern.check_for ctxt (res, inf) (prog, env) (errpats, rls) of SOME _ => () |
1003 | NONE => error "Error_Pattern.check_for broken"; |
1003 | NONE => error "Error_Pattern.check_for broken"; |
1004 DEconstrCalcTree 1; |
1004 DEconstrCalcTree 1; |
1005 |
1005 |
1006 "--------- embed fun check_for ------------------------"; |
1006 "--------- embed fun check_for ------------------------"; |
1007 "--------- embed fun check_for ------------------------"; |
1007 "--------- embed fun check_for ------------------------"; |
1051 ; |
1051 ; |
1052 (*+*)if UnparseC.term f_pred = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso |
1052 (*+*)if UnparseC.term f_pred = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso |
1053 (*+*) UnparseC.term f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" |
1053 (*+*) UnparseC.term f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" |
1054 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2"; |
1054 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2"; |
1055 |
1055 |
1056 val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*); |
1056 val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for ctxt (f_pred, f_in) (prog, env) (errpats, nrls) (*of*); |
1057 |
1057 |
1058 "--- final check:"; |
1058 "--- final check:"; |
1059 (*+*)val (_, _, ptp') = cs'; |
1059 (*+*)val (_, _, ptp') = cs'; |
1060 case Step_Solve.by_term ptp' (encode ifo) of |
1060 case Step_Solve.by_term ptp' (encode ifo) of |
1061 ("error pattern #chain-rule-diff-both#", calcstate') => () |
1061 ("error pattern #chain-rule-diff-both#", calcstate') => () |