117 "----------------------------------------------------------"; |
117 "----------------------------------------------------------"; |
118 |
118 |
119 val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls |
119 val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls |
120 ((#rules o Rule_Set.rep) Test_simplify) |
120 ((#rules o Rule_Set.rep) Test_simplify) |
121 (sqrt_right false (@{theory "Pure"})) NONE |
121 (sqrt_right false (@{theory "Pure"})) NONE |
122 (TermC.str2term "x + 1 + - 1 * 2 = 0"); |
122 (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0"); |
123 (writeln o Derive.trtas2str) fod; |
123 (writeln o Derive.trtas2str) fod; |
124 |
124 |
125 val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls |
125 val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls |
126 ((#rules o Rule_Set.rep) Test_simplify) |
126 ((#rules o Rule_Set.rep) Test_simplify) |
127 (sqrt_right false (@{theory "Pure"})) NONE |
127 (sqrt_right false (@{theory "Pure"})) NONE |
128 (TermC.str2term "- 2 * 1 + (1 + x) = 0"); |
128 (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0"); |
129 (writeln o Derive.trtas2str) ifod; |
129 (writeln o Derive.trtas2str) ifod; |
130 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; |
130 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; |
131 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); |
131 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); |
132 val der = fod' @ (map Derive.rev_deriv' rifod'); |
132 val der = fod' @ (map Derive.rev_deriv' rifod'); |
133 (writeln o Derive.trtas2str) der; |
133 (writeln o Derive.trtas2str) der; |
635 DEconstrCalcTree 1; |
635 DEconstrCalcTree 1; |
636 |
636 |
637 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------"; |
637 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------"; |
638 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------"; |
638 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------"; |
639 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------"; |
639 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------"; |
640 val t = TermC.str2term "Diff (x \<up> 2 + x + 1, x)"; |
640 val t = TermC.parse_test @{context} "Diff (x \<up> 2 + x + 1, x)"; |
641 case t of Const (\<^const_name>\<open>Diff\<close>, _) $ _ => () |
641 case t of Const (\<^const_name>\<open>Diff\<close>, _) $ _ => () |
642 | _ => raise |
642 | _ => raise |
643 error "diff.sml behav.changed for CAS Diff (..., x)"; |
643 error "diff.sml behav.changed for CAS Diff (..., x)"; |
644 TermC.atomty t; |
644 TermC.atomty t; |
645 "-----------------------------------------------------------------"; |
645 "-----------------------------------------------------------------"; |
900 (*step into getFormulaeFromTo --- bug corrected...*) |
900 (*step into getFormulaeFromTo --- bug corrected...*) |
901 |
901 |
902 "--------- build fun check_for' ------------------------------"; |
902 "--------- build fun check_for' ------------------------------"; |
903 "--------- build fun check_for' ------------------------------"; |
903 "--------- build fun check_for' ------------------------------"; |
904 "--------- build fun check_for' ------------------------------"; |
904 "--------- build fun check_for' ------------------------------"; |
905 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst; |
905 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst; |
906 val rls = norm_Rational |
906 val rls = norm_Rational |
907 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c"; |
907 val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c"; |
908 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4"); |
908 val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4"); |
909 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2"); |
909 val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "1 / 2"); |
910 |
910 |
911 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) |
911 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) |
912 rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
912 rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
913 if rewritten then NONE else SOME "e_errpatID"; |
913 if rewritten then NONE else SOME "e_errpatID"; |
914 |
914 |
922 |
922 |
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.parse_test @{context} "(2 + 3)/2", TermC.parse_test @{context} "3"); |
928 if check_for' ctxt (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.parse_test @{context} "(2 + 3)/(2 + 4)", TermC.parse_test @{context} "3 / 4"); |
933 if check_for' ctxt (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.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4"); |
938 if check_for' ctxt (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.parse_test @{context} "1 / 2"; |
942 if check_for' ctxt (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 -------------------------"; |
948 val ctxt = Proof_Context.init_global @{theory} |
948 val ctxt = Proof_Context.init_global @{theory} |
949 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]: subst; |
949 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst; |
950 val t = TermC.str2term "d_d x (x \<up> 2 + sin (x \<up> 4))"; |
950 val t = TermC.parse_test @{context} "d_d x (x \<up> 2 + sin (x \<up> 4))"; |
951 val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t; |
951 val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t; |
952 if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then () |
952 if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then () |
953 else error "build fun check_for' ?bdv changed 1"; |
953 else error "build fun check_for' ?bdv changed 1"; |
954 |
954 |
955 val rls = norm_diff |
955 val rls = norm_diff |
956 val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; |
956 val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; |
957 val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)"); |
957 val (res, inf) = (TermC.parse_test @{context} "2 * x + d_d x (sin (x \<up> 4))", TermC.parse_test @{context} "2 * x + cos (4 * x \<up> 3)"); |
958 |
958 |
959 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) |
959 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) |
960 rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
960 rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; |
961 if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then () |
961 if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then () |
962 else error "build fun check_for' ?bdv changed 2"; |
962 else error "build fun check_for' ?bdv changed 2"; |
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 ------------------------"; |
986 val (res, inf) = |
986 val (res, inf) = |
987 (TermC.str2term "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))", |
987 (TermC.parse_test @{context} "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))", |
988 TermC.str2term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"); |
988 TermC.parse_test @{context} "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"); |
989 val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"] |
989 val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"] |
990 |
990 |
991 val env = [(TermC.str2term "v_v", TermC.str2term "x")]; |
991 val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")]; |
992 val errpats = |
992 val errpats = |
993 [Error_Pattern.empty, (*generalised for testing*) |
993 [Error_Pattern.empty, (*generalised for testing*) |
994 ("chain-rule-diff-both", |
994 ("chain-rule-diff-both", |
995 [TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
995 [TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
996 TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
996 TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
1275 "--------- fun concat_deriv --------------------------------------"; |
1275 "--------- fun concat_deriv --------------------------------------"; |
1276 "--------- fun concat_deriv --------------------------------------"; |
1276 "--------- fun concat_deriv --------------------------------------"; |
1277 "--------- fun concat_deriv --------------------------------------"; |
1277 "--------- fun concat_deriv --------------------------------------"; |
1278 (* |
1278 (* |
1279 val ({rew_ord, erls, rules,...}, fo, ifo) = |
1279 val ({rew_ord, erls, rules,...}, fo, ifo) = |
1280 (Rule_Set.rep Test_simplify, TermC.str2term "x+1+ - 1*2=0", TermC.str2term "-2*1+(x+1)=0"); |
1280 (Rule_Set.rep Test_simplify, TermC.parse_test @{context} "x+1+ - 1*2=0", TermC.parse_test @{context} "-2*1+(x+1)=0"); |
1281 (tracing o Derive.trtas2str) fod'; |
1281 (tracing o Derive.trtas2str) fod'; |
1282 > [" |
1282 > [" |
1283 (x + 1 + - 1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (x + 1) = 0, []))", " |
1283 (x + 1 + - 1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (x + 1) = 0, []))", " |
1284 (- 1 * 2 + (x + 1) = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (1 + x) = 0, []))", " |
1284 (- 1 * 2 + (x + 1) = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (1 + x) = 0, []))", " |
1285 (- 1 * 2 + (1 + x) = 0, Thm ("radd_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (- 1 * 2 + x) = 0, []))", " |
1285 (- 1 * 2 + (1 + x) = 0, Thm ("radd_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (- 1 * 2 + x) = 0, []))", " |