115 (writeln o istates2str) (get_obj g_loc pt [4]); |
115 (writeln o istates2str) (get_obj g_loc pt [4]); |
116 |
116 |
117 *) |
117 *) |
118 "----------------------------------------------------------"; |
118 "----------------------------------------------------------"; |
119 |
119 |
120 val fod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls |
120 val fod = Derive.make_deriv (@{theory "Isac_Knowledge"}) Atools_erls |
121 ((#rules o Rule_Set.rep) Test_simplify) |
121 ((#rules o Rule_Set.rep) Test_simplify) |
122 (sqrt_right false (@{theory "Pure"})) NONE |
122 (sqrt_right false (@{theory "Pure"})) NONE |
123 (str2term "x + 1 + -1 * 2 = 0"); |
123 (str2term "x + 1 + -1 * 2 = 0"); |
124 (writeln o trtas2str) fod; |
124 (writeln o Derive.trtas2str) fod; |
125 |
125 |
126 val ifod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls |
126 val ifod = Derive.make_deriv (@{theory "Isac_Knowledge"}) Atools_erls |
127 ((#rules o Rule_Set.rep) Test_simplify) |
127 ((#rules o Rule_Set.rep) Test_simplify) |
128 (sqrt_right false (@{theory "Pure"})) NONE |
128 (sqrt_right false (@{theory "Pure"})) NONE |
129 (str2term "-2 * 1 + (1 + x) = 0"); |
129 (str2term "-2 * 1 + (1 + x) = 0"); |
130 (writeln o trtas2str) ifod; |
130 (writeln o Derive.trtas2str) ifod; |
131 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; |
131 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; |
132 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); |
132 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); |
133 val der = fod' @ (map rev_deriv' rifod'); |
133 val der = fod' @ (map Derive.rev_deriv' rifod'); |
134 (writeln o trtas2str) der; |
134 (writeln o Derive.trtas2str) der; |
135 "----------------------------------------------------------"; |
135 "----------------------------------------------------------"; |
136 DEconstrCalcTree 1; |
136 DEconstrCalcTree 1; |
137 |
137 |
138 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
138 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
139 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
139 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
1270 "--------- fun concat_deriv --------------------------------------"; |
1270 "--------- fun concat_deriv --------------------------------------"; |
1271 "--------- fun concat_deriv --------------------------------------"; |
1271 "--------- fun concat_deriv --------------------------------------"; |
1272 (* |
1272 (* |
1273 val ({rew_ord, erls, rules,...}, fo, ifo) = |
1273 val ({rew_ord, erls, rules,...}, fo, ifo) = |
1274 (Rule_Set.rep Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0"); |
1274 (Rule_Set.rep Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0"); |
1275 (tracing o trtas2str) fod'; |
1275 (tracing o Derive.trtas2str) fod'; |
1276 > [" |
1276 > [" |
1277 (x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))"," |
1277 (x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))"," |
1278 (-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))"," |
1278 (-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))"," |
1279 (-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))"," |
1279 (-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))"," |
1280 (1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"] |
1280 (1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"] |
1281 val it = () : unit |
1281 val it = () : unit |
1282 (tracing o trtas2str) (map rev_deriv' rifod'); |
1282 (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod'); |
1283 > [" |
1283 > [" |
1284 (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))"," |
1284 (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))"," |
1285 (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))"," |
1285 (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))"," |
1286 (-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"] |
1286 (-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"] |
1287 val it = () : unit |
1287 val it = () : unit |