1.1 --- a/test/Tools/isac/Interpret/inform.sml Wed Nov 30 12:09:24 2016 +0100
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Nov 30 13:05:08 2016 +0100
1.3 @@ -39,6 +39,9 @@
1.4 "--------- embed fun find_fillpatterns ---------------------------";
1.5 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.6 "--------- fun appl_adds -----------------------------------------";
1.7 +"--------- fun concat_deriv --------------------------------------";
1.8 +"--------- handle an input formula -------------------------------";
1.9 +"--------- fun dropwhile' ----------------------------------------";
1.10 "-----------------------------------------------------------------";
1.11 "-----------------------------------------------------------------";
1.12 "-----------------------------------------------------------------";
1.13 @@ -1322,3 +1325,120 @@
1.14 val itm = appl_add' dI oris ppc pbt selct;
1.15 val ppc = insert_ppc' itm ppc;
1.16 *)
1.17 +"--------- fun concat_deriv --------------------------------------";
1.18 +"--------- fun concat_deriv --------------------------------------";
1.19 +"--------- fun concat_deriv --------------------------------------";
1.20 +(*
1.21 + val ({rew_ord, erls, rules,...}, fo, ifo) =
1.22 + (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
1.23 + (tracing o trtas2str) fod';
1.24 +> ["
1.25 +(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
1.26 +(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
1.27 +(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
1.28 +(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
1.29 +val it = () : unit
1.30 + (tracing o trtas2str) (map rev_deriv' rifod');
1.31 +> ["
1.32 +(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
1.33 +(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
1.34 +(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
1.35 +val it = () : unit
1.36 +*)
1.37 +"--------- handle an input formula -------------------------------";
1.38 +"--------- handle an input formula -------------------------------";
1.39 +"--------- handle an input formula -------------------------------";
1.40 +(*
1.41 +Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
1.42 +Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
1.43 +wenn Abteilungen nur auf gleichem Level gesucht werden ?
1.44 +WN.040216
1.45 +
1.46 +Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
1.47 +
1.48 +------------------------------------------------------------------------------
1.49 +"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
1.50 +------------------------------------------------------------------------------
1.51 +1. "5 * x / (x - 2) - x / (x + 2) = 4"
1.52 +...
1.53 +4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly"..
1.54 +...
1.55 +4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
1.56 +...
1.57 +4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
1.58 +...
1.59 +"[x = -4 / 3]"
1.60 +------------------------------------------------------------------------------
1.61 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
1.62 +
1.63 +(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
1.64 +------------------------------------------------------------------------------
1.65 +
1.66 +
1.67 +------------------------------------------------------------------------------
1.68 +"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
1.69 +------------------------------------------------------------------------------
1.70 +1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
1.71 +...
1.72 +4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
1.73 + Subproblem["normalize", "polynomial", "univariate"..
1.74 +...
1.75 +4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
1.76 +...
1.77 +4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
1.78 +4.4.5. "[x = 0, x = 6 / 5]"
1.79 +...
1.80 +5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
1.81 + "[x = 6 / 5]"
1.82 +------------------------------------------------------------------------------
1.83 +(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
1.84 +
1.85 +(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
1.86 +------------------------------------------------------------------------------
1.87 +
1.88 +
1.89 +------------------------------------------------------------------------------
1.90 +"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
1.91 +------------------------------------------------------------------------------
1.92 +1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
1.93 +...
1.94 +6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
1.95 + Subproblem["sq", "root'", "univariate", "equation"]
1.96 +...
1.97 +6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
1.98 + Subproblem["normalize", "polynomial", "univariate", "equation"]
1.99 +...
1.100 +6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
1.101 +... Or_to_List
1.102 +6.6.3.2 "UniversalList"
1.103 +------------------------------------------------------------------------------
1.104 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
1.105 +
1.106 +(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
1.107 +------------------------------------------------------------------------------
1.108 +*)
1.109 +(*sh. comments auf 498*)
1.110 +"--------- fun dropwhile' ----------------------------------------";
1.111 +"--------- fun dropwhile' ----------------------------------------";
1.112 +"--------- fun dropwhile' ----------------------------------------";
1.113 +(*
1.114 + fun equal a b = a=b;
1.115 + val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
1.116 + val r_foder = rev foder; val r_ifoder = rev ifoder;
1.117 + dropwhile' equal r_foder r_ifoder;
1.118 +> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
1.119 +
1.120 + val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
1.121 + val r_foder = rev foder; val r_ifoder = rev ifoder;
1.122 + dropwhile' equal r_foder r_ifoder;
1.123 +> val it = ([3], [3, 12, 11]) : int list * int list
1.124 +
1.125 + val foder = [5]; val ifoder = [11,12,3,4,5];
1.126 + val r_foder = rev foder; val r_ifoder = rev ifoder;
1.127 + dropwhile' equal r_foder r_ifoder;
1.128 +> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
1.129 +
1.130 + val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
1.131 + val r_foder = rev foder; val r_ifoder = rev ifoder;
1.132 + dropwhile' equal r_foder r_ifoder;
1.133 +> *** dropwhile': did not start with equal elements*)