walther@59909: (* Title: "Interpret/error-pattern.sml" akargl@42176: Author: Walther Neuper 060225, neuper@37906: (c) due to copyright terms walther@59860: walther@59860: Strange ERROR "Undefined fact: "all_left"" neuper@37906: *) neuper@37906: neuper@37906: "-----------------------------------------------------------------"; neuper@37906: "table of contents -----------------------------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: "appendForm with miniscript with mini-subpbl:"; neuper@37906: "--------- appendFormula: on Res + equ_nrls ----------------------"; neuper@37906: "--------- appendFormula: on Frm + equ_nrls ----------------------"; neuper@37906: "--------- appendFormula: on Res + NO deriv ----------------------"; neuper@37906: "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--"; neuper@37906: "replaceForm with miniscript with mini-subpbl:"; neuper@37906: "--------- replaceFormula: on Res + = ----------------------------"; neuper@37906: "--------- replaceFormula: on Res + = 1st Nd ---------------------"; neuper@37906: "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; neuper@37906: "--------- replaceFormula: cut calculation -----------------------"; neuper@37906: "--------- replaceFormula: cut calculation -----------------------"; neuper@37906: (* 040307 copied from informtest.sml ... old versions neuper@37906: "--------- maximum-example, UC: Modeling / modifyCalcHead --------";*) neuper@37906: "--------- syntax error ------------------------------------------"; neuper@37906: "CAS-command:"; Walther@60571: (*"--------- CAS-command on ([],Pbl) -------------------------------";*) Walther@60571: (*"--------- CAS-command on ([],Pbl) FE-interface ------------------";*) walther@59772: "--------- locate_input_term [rational,simplification] ----------------------"; Walther@60571: (*"--------- Take as 1st tac, start with (CAS input) ---------";*) neuper@37906: "--------- Take as 1st tac, start from exp -----------------------"; Walther@60571: (*"--------- implicit_take, start with (CAS input) ---------------";*) walther@59909: "--------- build fun check_for' ------------------------------"; walther@59909: "--------- build fun check_for' ?bdv -------------------------"; walther@59909: "--------- build fun check_for ------------------------"; walther@59909: "--------- embed fun check_for ------------------------"; Walther@60637: "----------- re-build: fill_from_store without thy-hierarchy -----------------------------------"; walther@59909: "--------- embed fun find_fill_patterns ---------------------------"; neuper@48895: "--------- build fun is_exactly_equal, inputFillFormula ----------"; wneuper@59262: "--------- fun appl_adds -----------------------------------------"; wneuper@59264: "--------- fun concat_deriv --------------------------------------"; wneuper@59264: "--------- handle an input formula -------------------------------"; wneuper@59264: "--------- fun dropwhile' ----------------------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: neuper@37906: neuper@37906: "--------- appendFormula: on Res + equ_nrls ----------------------"; neuper@37906: "--------- appendFormula: on Res + equ_nrls ----------------------"; neuper@37906: "--------- appendFormula: on Res + equ_nrls ----------------------"; Walther@60586: val Prog sc = (#program o MethodC.from_store ctxt) ["Test", "squ-equ-test-subpbl1"]; walther@59868: (writeln o UnparseC.term) sc; Walther@60586: val Prog sc = (#program o MethodC.from_store ctxt) ["Test", "solve_linear"]; walther@59868: (writeln o UnparseC.term) sc; neuper@37906: Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*) Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); neuper@37906: Walther@60549: appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (States.get_pos 1 1); Walther@60549: val ((pt,_),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; neuper@48895: if str = neuper@48895: (". ----- pblobj -----\n" ^ neuper@48895: "1. x + 1 = 2\n" ^ walther@60324: "2. x + 1 + - 1 * 2 = 0\n" ^ walther@60324: "2.1. x + 1 + - 1 * 2 = 0\n" ^ walther@60324: "2.2. 1 + x + - 1 * 2 = 0\n" ^ walther@60324: "2.3. 1 + (x + - 1 * 2) = 0\n" ^ walther@60324: "2.4. 1 + (x + - 2) = 0\n" ^ walther@60324: "2.5. 1 + (x + - 2 * 1) = 0\n" ^ walther@60324: "2.6. 1 + x + - 2 * 1 = 0\n" ) then () neuper@48895: else error "inform.sml: diff.behav.appendFormula: on Res + equ 1"; neuper@37906: neuper@37906: moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*) walther@60324: moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + - 1 * 2 = 0*) neuper@37906: neuper@37906: (*the seven steps of detailed derivation*) neuper@37906: moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm); neuper@37906: moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res); neuper@37906: moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res); neuper@37906: moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res); neuper@37906: moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res); neuper@37906: moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res); neuper@37906: moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res); Walther@60549: val ((pt,_),_) = States.get_calc 1; walther@60324: if "- 2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then() neuper@38031: else error "inform.sml: diff.behav.appendFormula: on Res + equ 2"; neuper@37906: neuper@37906: fetchProposedTactic 1; (*takes Iterator 1 _1_*) neuper@48895: (* error in kernel ALREADY IN 2009-2*) neuper@48895: (*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============= Walther@60549: val (_,(tac,_,_)::_) = States.get_calc 1; neuper@37906: if tac = Rewrite_Set "Test_simplify" then () neuper@38031: else error "inform.sml: diff.behav.appendFormula: on Res + equ 3"; neuper@48895: ============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*) akargl@42209: wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,_),_) = States.get_calc 1; walther@59868: if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () neuper@38031: else error "inform.sml: diff.behav.appendFormula: on Res + equ 4"; wneuper@59248: (* autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,p),_) = States.get_calc 1; neuper@37906: (writeln o istates2str) (get_obj g_loc pt [ ]); neuper@37906: (writeln o istates2str) (get_obj g_loc pt [1]); neuper@37906: (writeln o istates2str) (get_obj g_loc pt [2]); neuper@37906: (writeln o istates2str) (get_obj g_loc pt [3]); neuper@37906: (writeln o istates2str) (get_obj g_loc pt [3,1]); neuper@37906: (writeln o istates2str) (get_obj g_loc pt [3,2]); neuper@37906: (writeln o istates2str) (get_obj g_loc pt [4]); neuper@37906: neuper@37906: *) neuper@37906: "----------------------------------------------------------"; akargl@42176: Walther@60500: val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls walther@59852: ((#rules o Rule_Set.rep) Test_simplify) Walther@60594: (sqrt_right false) NONE Walther@60565: (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0"); Walther@60611: (writeln o (Derive.trtas2str ctxt)) fod; neuper@37906: Walther@60500: val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls walther@59852: ((#rules o Rule_Set.rep) Test_simplify) Walther@60594: (sqrt_right false) NONE Walther@60565: (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0"); Walther@60611: (writeln o (Derive.trtas2str ctxt)) ifod; akargl@42176: fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; neuper@37906: val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); Walther@60630: val der = fod' @ (map (Derive.rev_deriv' ctxt) rifod'); Walther@60611: (writeln o (Derive.trtas2str ctxt)) der; neuper@37906: "----------------------------------------------------------"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: neuper@37906: "--------- appendFormula: on Frm + equ_nrls ----------------------"; neuper@37906: "--------- appendFormula: on Frm + equ_nrls ----------------------"; neuper@37906: "--------- appendFormula: on Frm + equ_nrls ----------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 = 2*); Walther@60549: appendFormula 1 "2+ - 1 + x = 2" (*|> Future.join*); refFormula 1 (States.get_pos 1 1); neuper@37906: neuper@37906: moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*); neuper@37906: neuper@37906: moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm); neuper@37906: moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res); neuper@37906: moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res); neuper@37906: moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res); neuper@37906: moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res); neuper@37906: moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res); neuper@37906: moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res); Walther@60549: val ((pt,_),_) = States.get_calc 1; walther@60324: if "2 + - 1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then() neuper@38031: else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1"; neuper@37906: neuper@37906: fetchProposedTactic 1; (*takes Iterator 1 _1_*) Walther@60549: val (_,(tac,_,_)::_) = States.get_calc 1; wneuper@59253: case tac of Rewrite_Set "norm_equation" => () wneuper@59253: | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2"; wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,_),_) = States.get_calc 1; walther@59868: if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () neuper@38031: else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: neuper@37906: "--------- appendFormula: on Res + NO deriv ----------------------"; neuper@37906: "--------- appendFormula: on Res + NO deriv ----------------------"; neuper@37906: "--------- appendFormula: on Res + NO deriv ----------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*) Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); neuper@37906: wneuper@59123: appendFormula 1 "x = 2" (*|> Future.join*); Walther@60549: val ((pt,p),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; neuper@37906: writeln str; neuper@37906: if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res) neuper@37906: then () neuper@38031: else error "inform.sml: diff.behav.appendFormula: Res + NOder 1"; neuper@37906: neuper@37906: fetchProposedTactic 1; Walther@60549: val (_,(tac,_,_)::_) = States.get_calc 1; wneuper@59253: case tac of Rewrite_Set "Test_simplify" => () wneuper@59253: | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2"; wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,_),_) = States.get_calc 1; walther@59868: if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () neuper@38031: else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: neuper@37906: "--------- appendFormula: on Res + late deriv --------------------"; neuper@37906: "--------- appendFormula: on Res + late deriv --------------------"; neuper@37906: "--------- appendFormula: on Res + late deriv --------------------"; walther@59794: (*cp with "fun me" to test/../lucas-interpreter.sml: walther@59794: re-build: fun locate_input_term ---------------------------------------------------"; walther@59794: *) Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*) Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); neuper@37906: wneuper@59123: appendFormula 1 "x = 1" (*|> Future.join*); Walther@60549: val ((pt,p),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; neuper@37906: writeln str; walther@60324: if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n3.2.1. x = 0 + - 1 * - 1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res) neuper@37906: then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*) neuper@38031: else error "inform.sml: diff.behav.appendFormula: Res + late d 1"; akargl@42176: neuper@37906: fetchProposedTactic 1; Walther@60549: val (_,(tac,_,_)::_) = States.get_calc 1; wneuper@59253: case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => () wneuper@59253: | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2"; wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,_),_) = States.get_calc 1; walther@59868: if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () neuper@38031: else error "inform.sml: diff.behav.appendFormula: Res + late d 3"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: walther@60324: "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--"; walther@60324: "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--"; walther@60324: "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*) Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); wneuper@59123: appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*); Walther@60549: val ((pt,p),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; neuper@37906: writeln str; walther@60324: if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = - 2 + 3]\n4.3. [x = 3 + - 2]\n" then () neuper@38031: else error "inform.sml: diff.behav.appendFormula: Res + latEE 1"; wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,p),_) = States.get_calc 1; walther@60324: if "[x = 3 + - 2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then () neuper@37906: (* ~~~~~~~~~~ simplify as last step in any script ?!*) neuper@38031: else error "inform.sml: diff.behav.appendFormula: Res + latEE 2"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: neuper@37906: "--------- replaceFormula: on Res + = ----------------------------"; neuper@37906: "--------- replaceFormula: on Res + = ----------------------------"; neuper@37906: "--------- replaceFormula: on Res + = ----------------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*) Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*- 1 + x*); neuper@37906: Walther@60549: replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (States.get_pos 1 1); Walther@60549: val ((pt,_),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; akargl@42176: neuper@48895: (* before AK110725 this was neuper@48895: ". ----- pblobj -----\n neuper@48895: 1. x + 1 = 2\n walther@60324: 2. x + 1 + - 1 * 2 = 0\n walther@60324: 2.1. x + 1 + - 1 * 2 = 0\n walther@60324: 2.2. 1 + x + - 1 * 2 = 0\n walther@60324: 2.3. 1 + (x + - 1 * 2) = 0\n neuper@48895: 2.4. 1 + (x + -2) = 0\n neuper@48895: 2.5. 1 + (x + -2 * 1) = 0\n neuper@48895: 2.6. 1 + x + -2 * 1 = 0\n"; neuper@48895: *) Walther@60523: if str = neuper@48895: ". ----- pblobj -----\n"^ neuper@48895: "1. x + 1 = 2\n"^ walther@60324: "2. x + 1 + - 1 * 2 = 0\n"^ walther@60324: "2.1. x + 1 + - 1 * 2 = 0\n"^ walther@60324: "2.2. 1 + x + - 1 * 2 = 0\n"^ walther@60324: "2.3. 1 + (x + - 1 * 2) = 0\n"^ walther@60324: "2.4. 1 + (x + - 2) = 0\n"^ walther@60324: "2.5. 1 + (x + - 2 * 1) = 0\n"^ walther@60324: "2.6. 1 + x + - 2 * 1 = 0\n" then() neuper@48895: else error "inform.sml: diff.behav.replaceFormula: on Res += 1"; akargl@42176: wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,pos as (p,_)),_) = States.get_calc 1; walther@59868: if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then() neuper@38031: else error "inform.sml: diff.behav.replaceFormula: on Res + = 2"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: neuper@37906: "--------- replaceFormula: on Res + = 1st Nd ---------------------"; neuper@37906: "--------- replaceFormula: on Res + = 1st Nd ---------------------"; neuper@37906: "--------- replaceFormula: on Res + = 1st Nd ---------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*) Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); neuper@37906: Walther@60549: replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1); Walther@60549: val ((pt,_),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; neuper@37906: writeln str; walther@60324: if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then () neuper@38031: else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1"; wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,pos as (p,_)),_) = States.get_calc 1; walther@59868: if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then() neuper@38031: else error "inform.sml: diff.behav.replaceFormula: on Res + = 2"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: neuper@37906: "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; neuper@37906: "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; neuper@37906: "--------- replaceFormula: on Frm + = 1st Nd ---------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*) neuper@37906: Walther@60549: replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1); Walther@60549: val ((pt,_),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; walther@60340: writeln str; walther@60324: if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then () neuper@38031: else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1"; wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,pos as (p,_)),_) = States.get_calc 1; walther@59868: if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then() neuper@38031: else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: neuper@37906: "--------- replaceFormula: cut calculation -----------------------"; neuper@37906: "--------- replaceFormula: cut calculation -----------------------"; neuper@37906: "--------- replaceFormula: cut calculation -----------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@37906: moveActiveRoot 1; moveActiveDown 1; Walther@60549: if States.get_pos 1 1 = ([1], Frm) then () neuper@38031: else error "inform.sml: diff.behav. cut calculation 1"; neuper@37906: Walther@60549: replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1); Walther@60549: val ((pt,p),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; neuper@37906: writeln str; neuper@37906: if p = ([1], Res) then () neuper@38031: else error "inform.sml: diff.behav. cut calculation 2"; neuper@37906: neuper@37906: neuper@37906: (* 040307 copied from informtest.sml; ... old version neuper@37906: "---------------- maximum-example, UC: Modeling / modifyCalcHead -"; neuper@37906: "---------------- maximum-example, UC: Modeling / modifyCalcHead -"; neuper@37906: "---------------- maximum-example, UC: Modeling / modifyCalcHead -"; neuper@37906: neuper@37906: val p = ([],Pbl); walther@59997: val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]", walther@60242: "relations [A=a*b, (a/2) \ 2 + (b/2) \ 2 = r \ 2]", walther@60242: "relations [A=a*b, (a/2) \ 2 + (b/2) \ 2 = r \ 2]", wneuper@59582: "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]", walther@60242: (* \ these are the elements for the root-problem (in variants)*) neuper@37906: (*vvv these are elements required for subproblems*) walther@59997: "boundVariable a", "boundVariable b", "boundVariable alpha", neuper@37906: "interval {x::real. 0 <= x & x <= 2*r}", neuper@37906: "interval {x::real. 0 <= x & x <= 2*r}", neuper@37906: "interval {x::real. 0 <= x & x <= pi}", neuper@37906: "errorBound (eps=(0::real))"] neuper@37906: (*specifying is not interesting for this example*) Walther@60458: val spec = ("Diff_App", ["maximum_of", "function"], Walther@60458: ["Diff_App", "max_by_calculus"]); neuper@37906: (*the empty model with descriptions for user-guidance by Model_Problem*) neuper@37906: val empty_model = [Given ["fixedValues []"], neuper@37906: Find ["maximum", "valuesFor"], neuper@37906: Relate ["relations []"]]; neuper@37906: neuper@37906: neuper@37906: (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*) Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(elems, spec)]; neuper@37906: (*val nxt = ("Model_Problem", ...*) walther@59942: val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl; neuper@37906: neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@37906: (*nxt = Add_Given "fixedValues [r = Arbfix]"*) walther@59942: val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl; neuper@37906: (*[ neuper@37906: (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])), neuper@37906: (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])), neuper@37906: (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])), neuper@37906: (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*) neuper@37906: neuper@37906: (*the empty CalcHead is checked w.r.t the model and re-established as such*) walther@59976: val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, References.empty); walther@59942: val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl; walther@59879: if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1"; neuper@37906: neuper@37906: (*there is one input to the model (could be more)*) neuper@37906: val (b,pt,ocalhd) = neuper@37906: input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"], neuper@37906: Find ["maximum", "valuesFor"], walther@59976: Relate ["relations"]], Pbl, References.empty); walther@59942: val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl; walther@59879: if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () neuper@38031: else error "informtest.sml: diff.behav. max 2"; neuper@37906: neuper@37906: (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME neuper@37906: val (b,pt''''',ocalhd) = neuper@37906: input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"], neuper@37906: Find ["maximum A", "valuesFor [a,b]"], neuper@37906: Relate ["relations [A=a*b, a/2=r*sin alpha, \ walther@59976: \b/2=r*cos alpha]"]], Pbl, References.empty); walther@59942: val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl; walther@60242: if ocalhd2str ocalhd = ------------ \ \ \ ^ missing !!!*) neuper@37906: neuper@37906: (*this input is complete in variant 1 (variant 3 does not work yet)*) neuper@37906: val (b,pt''''',ocalhd) = neuper@37906: input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"], neuper@37906: Find ["maximum A", "valuesFor [a,b]"], neuper@37906: Relate ["relations [A=a*b, \ walther@60242: \(a/2) \ 2 + (b/2) \ 2 = r \ 2]"]], walther@59976: Pbl, References.empty); walther@59942: val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl; neuper@37906: neuper@37906: modifycalcheadOK2xml 111 (bool2str b) ocalhd; neuper@37906: *) wneuper@59252: DEconstrCalcTree 1; neuper@37906: neuper@37906: "--------- syntax error ------------------------------------------"; neuper@37906: "--------- syntax error ------------------------------------------"; neuper@37906: "--------- syntax error ------------------------------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], walther@59997: ("Test", ["sqroot-test", "univariate", "equation", "test"], walther@59997: ["Test", "squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*) Walther@60549: autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*); neuper@37906: neuper@37906: appendFormula 1 " x - "; (* syntax error in ' x - ' *) Walther@60549: val ((pt,_),_) = States.get_calc 1; Walther@60608: val str = pr_ctree ctxt pr_short pt; neuper@37906: writeln str; neuper@37906: if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then () neuper@38031: else error "inform.sml: diff.behav.appendFormula: syntax error"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: Walther@60571: (*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd) neuper@37906: "--------- CAS-command on ([],Pbl) -------------------------------"; neuper@37906: "--------- CAS-command on ([],Pbl) -------------------------------"; neuper@37906: "--------- CAS-command on ([],Pbl) -------------------------------"; neuper@37906: val (p,_,f,nxt,_,pt) = Walther@60571: Test_Code.init_calc @{context} [([], References.empty)]; walther@60340: val ifo = "solve(x+1=2,x)"; walther@60340: val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)"; Walther@60571: ( * walther@60242: This trick \ \ \ micked input of \ \ \ \ \ ^^ in the front-end. walther@59921: The trick worked in changeset fbaff8cf0179, it does not work in 59c5dd27d589 anymore walther@59921: (TODO hg bisect ?) and raises the ERROR Undefined fact: "xfoldr_Nil". walther@59921: walther@59921: Compare tests "CAS-command" in test/../inssort.sml etc. walther@59921: --------------------------------------------------------------------------------------------- walther@59983: Test_Tool.show_pt pt; walther@59997: val nxt = (Apply_Method ["Test", "squ-equ-test-subpbl1"]); neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@37906: if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then () neuper@38031: else error "inform.sml: diff.behav. CAScmd ([],Pbl)"; wneuper@59252: DEconstrCalcTree 1; walther@59921: -----------------------------------------------------------------------------------------------*) neuper@37906: Walther@60571: (*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd) neuper@37906: "--------- CAS-command on ([],Pbl) FE-interface ------------------"; neuper@37906: "--------- CAS-command on ([],Pbl) FE-interface ------------------"; neuper@37906: "--------- CAS-command on ([],Pbl) FE-interface ------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [([], References.empty)]; neuper@37906: Iterator 1; neuper@37906: moveActiveRoot 1; walther@60340: replaceFormula 1 "solve(x+1=2,x)"; wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,p),_) = States.get_calc 1; walther@59983: Test_Tool.show_pt pt; neuper@37906: if p = ([], Res) then () neuper@38031: else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface"; wneuper@59252: DEconstrCalcTree 1; Walther@60571: -----------------------------------------------------------------------------------------------*) neuper@37906: wneuper@59562: "--------- inform [rational,simplification] ----------------------"; wneuper@59562: "--------- inform [rational,simplification] ----------------------"; wneuper@59562: "--------- inform [rational,simplification] ----------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"], neuper@52105: ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))]; neuper@37906: Iterator 1; moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; neuper@52105: walther@60324: "--- (- 1) give a preview on the calculation without any input"; neuper@52105: (* wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt, p), _) = States.get_calc 1; walther@59983: Test_Tool.show_pt pt; neuper@52105: [ neuper@52105: (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)), neuper@52105: (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f), neuper@52105: (([1], Res), a / b + c / d + e / f), <--- (1) input arbitrary neuper@52105: (([2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([3], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))), neuper@52105: (([4], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)), <--- (2) input next neuper@52105: (([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))] <--- (3) is also final result neuper@52105: EXAMPLE NOT OPTIMAL neuper@52105: *) neuper@52105: "--- (0) user input as the *first* step does not work, thus impdo at least 1 step"; walther@59747: autoCalculate 1 (Steps 1); walther@59747: autoCalculate 1 (Steps 1); Walther@60549: val ((pt, p), _) = States.get_calc 1; walther@59983: (*Test_Tool.show_pt pt; neuper@52105: [ neuper@52105: (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)), neuper@52105: (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f), neuper@52105: (([1], Res), a / b + c / d + e / f)] neuper@52105: *) neuper@52105: "--- (1) input an arbitrary next formula"; wneuper@59123: appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*); Walther@60549: val ((pt, p), _) = States.get_calc 1; walther@59983: (*Test_Tool.show_pt pt; neuper@52105: [ neuper@52105: (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)), neuper@52105: (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f), neuper@52105: (([1], Res), a / b + c / d + e / f), neuper@52105: (([2,1], Frm), a / b + c / d + e / f), neuper@52105: (([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([2,2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([2], Res), (a * d + c * b) / (b * d) + e / f)] neuper@52105: *) Walther@60549: val ((pt,p),_) = States.get_calc 1; neuper@52105: if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then () neuper@38031: else error ("inform.sml: [rational,simplification] 1"); neuper@37906: neuper@52105: "--- (2) input the next formula that would be presented by mat-engine"; neuper@52105: (* generate a preview: walther@59747: autoCalculate 1 (Steps 1); Walther@60549: val ((pt, p), _) = States.get_calc 1; walther@59983: Test_Tool.show_pt pt; neuper@52105: [ neuper@52105: (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)), neuper@52105: (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f), neuper@52105: (([1], Res), a / b + c / d + e / f), neuper@52105: (([2,1], Frm), a / b + c / d + e / f), neuper@52105: (([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([2,2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this neuper@52105: *) wneuper@59123: appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*); Walther@60549: val ((pt, p), _) = States.get_calc 1; walther@59983: (*Test_Tool.show_pt pt; neuper@52105: [ neuper@52105: (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)), neuper@52105: (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f), neuper@52105: (([1], Res), a / b + c / d + e / f), neuper@52105: (([2,1], Frm), a / b + c / d + e / f), neuper@52105: (([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([2,2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] neuper@52105: *) neuper@52105: if p = ([3], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then () neuper@38031: else error ("inform.sml: [rational,simplification] 2"); neuper@37906: neuper@52105: "--- (3) input the exact final result"; wneuper@59123: appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*); Walther@60549: val ((pt, p), _) = States.get_calc 1; walther@59983: (*Test_Tool.show_pt pt; neuper@52105: [ neuper@52105: (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)), neuper@52105: (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f), neuper@52105: (([1], Res), a / b + c / d + e / f), neuper@52105: (([2,1], Frm), a / b + c / d + e / f), neuper@52105: (([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([2,2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))), neuper@52105: (([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] neuper@52105: *) neuper@52105: if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then () neuper@38031: else error ("inform.sml: [rational,simplification] 3"); neuper@52105: neuper@52105: "--- (4) finish the calculation + check the postcondition (in the future)"; wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt, p), _) = States.get_calc 1; neuper@52105: val (t, asm) = get_obj g_result pt []; walther@59868: if UnparseC.term t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso walther@59921: UnparseC.terms asm =(*"[\"b * d * f \ 0\",\"d \ 0\",\"b \ 0\",\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"*) walther@59921: "[]" (*..found broken in child of 33913fe24685, error covered by CAS-command *) neuper@52105: then () else error "inform [rational,simplification] changed at end"; walther@59983: (*Test_Tool.show_pt pt; neuper@52105: [ neuper@52105: (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)), neuper@52105: (([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f), neuper@52105: (([1], Res), a / b + c / d + e / f), neuper@52105: (([2,1], Frm), a / b + c / d + e / f), neuper@52105: (([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([2,2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([2], Res), (a * d + c * b) / (b * d) + e / f), neuper@52105: (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))), neuper@52105: (([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)), neuper@52105: (([5], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))), neuper@52105: (([6], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)), neuper@52105: (([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))] neuper@52105: *) wneuper@59252: DEconstrCalcTree 1; neuper@37906: Walther@60571: (*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd) neuper@37906: "--------- Take as 1st tac, start with (CAS input) ---------"; neuper@37906: "--------- Take as 1st tac, start with (CAS input) ---------"; neuper@37906: "--------- Take as 1st tac, start with (CAS input) ---------"; Walther@60565: val t = TermC.parse_test @{context} "Diff (x \ 2 + x + 1, x)"; walther@60336: case t of Const (\<^const_name>\Diff\, _) $ _ => () neuper@37906: | _ => raise neuper@37906: error "diff.sml behav.changed for CAS Diff (..., x)"; Walther@60650: TermC.atom_trace_detail @{context} t; neuper@37906: "-----------------------------------------------------------------"; Walther@60549: (*1>*)States.reset (); Walther@60571: (*2>*)CalcTree @{context} [([], References.empty)]; neuper@37906: (*3>*)Iterator 1;moveActiveRoot 1; neuper@37906: "----- here the Headline has been finished"; neuper@37906: (*4>*)moveActiveFormula 1 ([],Pbl); walther@60242: (*5>*)replaceFormula 1 "Diff (x \ 2 + x + 1, x)"; Walther@60549: val ((pt,_),_) = States.get_calc 1; walther@59921: val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt []; neuper@37926: val (SOME istate, NONE) = loc; wneuper@59348: (*default_print_depth 5;*) neuper@37906: writeln"-----------------------------------------------------------"; neuper@37906: spec; walther@59942: writeln (I_Model.to_string ctxt probl); walther@59942: writeln (I_Model.to_string ctxt meth); Walther@60646: writeln (Istate.string_of ctxt (fst istate)); neuper@37906: neuper@37906: refFormula 1 ([],Pbl) (*--> correct CalcHead*); neuper@37906: (*081016 NOT necessary (but leave it in Java):*) wneuper@59248: (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead; neuper@37906: "----- here the CalcHead has been completed --- ONCE MORE ?????"; neuper@37906: neuper@37906: (***difference II***) Walther@60549: val ((pt,p),_) = States.get_calc 1; neuper@37906: (*val p = ([], Pbl)*) walther@59921: val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt []; neuper@37926: val (SOME istate, NONE) = loc; Walther@60646: (*default_print_depth 5;*) writeln (Istate.string_of ctxt (fst istate)); (*default_print_depth 3;*) wneuper@59583: (*Pstate ([], neuper@37926: [], NONE, neuper@37906: ??.empty, Sundef, false)*) wneuper@59348: (*default_print_depth 5;*) spec; (*default_print_depth 3;*) wneuper@59592: (*("Isac_Knowledge", neuper@37906: ["derivative_of", "function"], neuper@37906: ["diff", "differentiate_on_R"]) : spec*) walther@59942: writeln (I_Model.to_string ctxt probl); neuper@37906: (*[ walther@60242: (1 ,[1] ,true ,#Given ,Cor functionTerm (x \ 2 + x + 1) ,(f_, [x \ 2 + x + 1])), neuper@37906: (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), akargl@42176: (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) walther@59942: writeln (I_Model.to_string ctxt meth); neuper@37906: (*[ walther@60242: (1 ,[1] ,true ,#Given ,Cor functionTerm (x \ 2 + x + 1) ,(f_, [x \ 2 + x + 1])), neuper@37906: (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), akargl@42176: (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) neuper@37906: writeln"-----------------------------------------------------------"; neuper@37906: (*7>*)fetchProposedTactic 1 (*--> Apply_Method*); neuper@37906: (*WN081028 fixed helpless by inform returning ...(.,Met)*) wneuper@59248: autoCalculate 1 CompleteCalc; Walther@60549: val ((pt,p),_) = States.get_calc 1; walther@59983: val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res)); walther@59983: Test_Tool.show_pt pt; walther@60242: walther@59868: if p = ([], Res) andalso UnparseC.term res = "1 + 2 * x" then () walther@60242: else error "diff.sml behav.changed for Diff (x \ 2 + x + 1, x)"; wneuper@59252: DEconstrCalcTree 1; Walther@60571: -----------------------------------------------------------------------------------------------*) neuper@37906: neuper@37906: "--------- Take as 1st tac, start from exp -----------------------"; neuper@37906: "--------- Take as 1st tac, start from exp -----------------------"; neuper@37906: "--------- Take as 1st tac, start from exp -----------------------"; neuper@37906: (*the following input is copied from BridgeLog Java <==> SML, neuper@37906: omitting unnecessary inputs*) Walther@60549: (*1>*)States.reset (); Walther@60571: (*2>*)CalcTree @{context} [(["functionTerm (x \ 2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of", "function"],["diff", "differentiate_on_R"]))]; neuper@37906: (*3>*)Iterator 1; moveActiveRoot 1; neuper@37906: wneuper@59248: (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead; neuper@37906: (***difference II***) Walther@60549: val ((pt,_),_) = States.get_calc 1; walther@59921: val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt []; neuper@37926: val (SOME istate, NONE) = loc; Walther@60646: (*default_print_depth 5;*) writeln (Istate.string_of ctxt (fst istate)); (*default_print_depth 3;*) wneuper@59583: (*Pstate ([], neuper@37926: [], NONE, neuper@37906: ??.empty, Sundef, false)*) wneuper@59348: (*default_print_depth 5;*) spec; (*default_print_depth 3;*) wneuper@59592: (*("Isac_Knowledge", neuper@37906: ["derivative_of", "function"], neuper@37906: ["diff", "differentiate_on_R"]) : spec*) walther@59942: writeln (I_Model.to_string ctxt probl); neuper@37906: (*[ walther@60242: (1 ,[1] ,true ,#Given ,Cor functionTerm (x \ 2 + x + 1) ,(f_, [x \ 2 + x + 1])), neuper@37906: (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), akargl@42176: (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) walther@59942: writeln (I_Model.to_string ctxt meth); neuper@37906: (*[ walther@60242: (1 ,[1] ,true ,#Given ,Cor functionTerm (x \ 2 + x + 1) ,(f_, [x \ 2 + x + 1])), neuper@37906: (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), akargl@42176: (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) neuper@37906: writeln"-----------------------------------------------------------"; neuper@37906: (*7>*)fetchProposedTactic 1 (*--> Apply_Method*); walther@59747: autoCalculate 1 (Steps 1); Walther@60549: val ((pt,p),_) = States.get_calc 1; Walther@60577: val Form res = (#1 o (ME_Misc.pt_extract ctxt)) (pt, p); walther@60242: if UnparseC.term res = "d_d x (x \ 2 + x + 1)" then () walther@60242: else error "diff.sml Diff (x \ 2 + x + 1, x) from exp"; wneuper@59252: DEconstrCalcTree 1; neuper@37906: Walther@60571: (*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd) walther@59845: "--------- implicit_take, start with (CAS input) ---------------"; walther@59845: "--------- implicit_take, start with (CAS input) ---------------"; walther@59845: "--------- implicit_take, start with (CAS input) ---------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} [([], References.empty)]; neuper@37906: (*[[from sml: > @@@@@begin@@@@@ neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: @@@@@end@@@@@*) neuper@37906: Iterator 1; neuper@37906: (*[[from sml: > @@@@@begin@@@@@ neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: 1 neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: @@@@@end@@@@@*) neuper@37906: moveActiveRoot 1; neuper@37906: (*[[from sml: > @@@@@begin@@@@@ neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: Pbl neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: @@@@@end@@@@@*) neuper@37906: getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; neuper@37906: (*[[from sml: > @@@@@begin@@@@@ STILL CORRECT neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: Pbl neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: ________________________________________________ neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: @@@@@end@@@@@*) neuper@37906: refFormula 1 ([],Pbl); neuper@37906: (*[[from sml: > @@@@@begin@@@@@ STILL CORRECT neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: Pbl neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: walther@59879: [[from sml: Problem (ThyC.id_empty, [e_pblID]) neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: Pbl neuper@37906: [[from sml: walther@59879: [[from sml: ThyC.id_empty neuper@37906: [[from sml: neuper@37906: [[from sml: walther@59903: [[from sml: Problem.id_empty neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: e_metID neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: @@@@@end@@@@@*) neuper@37906: moveActiveFormula 1 ([],Pbl); neuper@37906: (*[[from sml: > @@@@@begin@@@@@ neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: Pbl neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: @@@@@end@@@@@*) neuper@37906: replaceFormula 1 "Simplify (1+2)"; neuper@37906: (*[[from sml: > @@@@@begin@@@@@ neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: Pbl neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: Pbl neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: Met DIFFERENCE: Pbl neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: neuper@37906: [[from sml: @@@@@end@@@@@*) neuper@37906: getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(* DIFFERENCE: Pbl*); neuper@37906: (*@@@@@begin@@@@@ neuper@37906: 1 neuper@37906: neuper@37906: 1 neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: Pbl neuper@37906: neuper@37906: neuper@37906: neuper@37906: Simplify (1 + 2) WORKS !!!!! neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: @@@@@end@@@@@*) neuper@37906: getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false; neuper@37906: (*[[from sml: > @@@@@begin@@@@@ neuper@37906: [[from sml: 1 neuper@37906: [[from sml: neuper@37906: [[from sml: 1 neuper@37906: [[from sml: error in getFormulaeFromTo neuper@37906: [[from sml: neuper@37906: [[from sml: @@@@@end@@@@@*) neuper@37906: (*step into getFormulaeFromTo --- bug corrected...*) Walther@60571: -----------------------------------------------------------------------------------------------*) neuper@42423: walther@59909: "--------- build fun check_for' ------------------------------"; walther@59909: "--------- build fun check_for' ------------------------------"; walther@59909: "--------- build fun check_for' ------------------------------"; Walther@60565: val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst; neuper@42423: val rls = norm_Rational walther@60230: val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c"; Walther@60565: val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4"); Walther@60565: val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "1 / 2"); neuper@42423: walther@60230: val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) Walther@60509: rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; neuper@42423: if rewritten then NONE else SOME "e_errpatID"; neuper@42423: Walther@60500: val norm_res = case rewrite_set_ ctxt false rls res' of neuper@42423: NONE => res' neuper@42423: | SOME (norm_res, _) => norm_res neuper@42423: Walther@60500: val norm_inf = case rewrite_set_ ctxt false rls inf of neuper@42423: NONE => inf neuper@42423: | SOME (norm_inf, _) => norm_inf; neuper@42423: neuper@42423: res' = inf; neuper@42423: norm_res = norm_inf; neuper@42423: walther@60230: val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b"; Walther@60565: val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/2", TermC.parse_test @{context} "3"); Walther@60523: if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" neuper@42423: then () else error "error patt example1 changed"; neuper@42423: walther@60230: val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c"; Walther@60565: val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(2 + 4)", TermC.parse_test @{context} "3 / 4"); Walther@60523: if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" neuper@42423: then () else error "error patt example2 changed"; neuper@42423: walther@60230: val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c"; Walther@60565: val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4"); Walther@60523: if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" neuper@42423: then () else error "error patt example3 changed"; neuper@42423: Walther@60565: val inf = TermC.parse_test @{context} "1 / 2"; Walther@60523: if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID" neuper@42423: then () else error "error patt example3 changed"; neuper@42423: walther@59909: "--------- build fun check_for' ?bdv -------------------------"; walther@59909: "--------- build fun check_for' ?bdv -------------------------"; walther@59909: "--------- build fun check_for' ?bdv -------------------------"; Walther@60500: val ctxt = Proof_Context.init_global @{theory} Walther@60565: val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst; Walther@60565: val t = TermC.parse_test @{context} "d_d x (x \ 2 + sin (x \ 4))"; Walther@60500: val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t; walther@60242: if UnparseC.term t = "2 * x + cos (x \ 4) * 4 * x \ 3" then () walther@59909: else error "build fun check_for' ?bdv changed 1"; neuper@42423: neuper@42426: val rls = norm_diff walther@60230: val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; Walther@60565: val (res, inf) = (TermC.parse_test @{context} "2 * x + d_d x (sin (x \ 4))", TermC.parse_test @{context} "2 * x + cos (4 * x \ 3)"); neuper@42426: walther@60230: val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*) Walther@60509: rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res; walther@60242: if UnparseC.term res' = "2 * x + cos (d_d x (x \ 4))" andalso rewritten then () walther@59909: else error "build fun check_for' ?bdv changed 2"; neuper@42426: Walther@60500: val norm_res = case rewrite_set_inst_ ctxt false subst rls res' of neuper@42426: NONE => res' neuper@42426: | SOME (norm_res, _) => norm_res; walther@60242: if UnparseC.term norm_res = "2 * x + cos (4 * x \ 3)" then () walther@59909: else error "build fun check_for' ?bdv changed 3"; neuper@42426: Walther@60500: val norm_inf = case rewrite_set_inst_ ctxt false subst rls inf of neuper@42426: NONE => inf neuper@42426: | SOME (norm_inf, _) => norm_inf; walther@60242: if UnparseC.term norm_inf = "2 * x + cos (4 * x \ 3)" then () walther@59909: else error "build fun check_for' ?bdv changed 4"; neuper@42426: neuper@42426: res' = inf; neuper@42426: if norm_res = norm_inf then () walther@59909: else error "build fun check_for' ?bdv changed 5"; neuper@42426: Walther@60523: if Error_Pattern.check_for' ctxt (res, inf) (subst: subst) ("errpatID": Error_Pattern.id, pat) rls = SOME "errpatID" neuper@42426: then () else error "error patt example1 changed"; neuper@42426: walther@59909: "--------- build fun check_for ------------------------"; walther@59909: "--------- build fun check_for ------------------------"; walther@59909: "--------- build fun check_for ------------------------"; neuper@42428: val (res, inf) = Walther@60565: (TermC.parse_test @{context} "d_d x (x \ 2) + d_d x (sin (x \ 4))", Walther@60565: TermC.parse_test @{context} "d_d x (x \ 2) + cos (4 * x \ 3)"); Walther@60586: val {errpats, rew_rls = rls, program = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"] neuper@42426: Walther@60565: val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")]; neuper@42428: val errpats = walther@59971: [Error_Pattern.empty, (*generalised for testing*) neuper@42428: ("chain-rule-diff-both", walther@60230: [TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", walther@60230: TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", walther@60242: TermC.parse_patt @{theory} "d_d ?bdv (?u \ ?n) = ?n * ?u \ (?n - 1)", walther@60230: TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u", walther@60230: TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"], neuper@42428: [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, walther@59921: @{thm diff_ln_chain}, @{thm diff_exp_chain}])]; Walther@60523: case Error_Pattern.check_for ctxt (res, inf) (prog, env) (errpats, rls) of SOME _ => () walther@59844: | NONE => error "Error_Pattern.check_for broken"; wneuper@59252: DEconstrCalcTree 1; neuper@42428: walther@59909: "--------- embed fun check_for ------------------------"; walther@59909: "--------- embed fun check_for ------------------------"; walther@59909: "--------- embed fun check_for ------------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} walther@60242: [(["functionTerm (x \ 2 + sin (x \ 4))", "differentiateFor x", "derivative f_f'"], walther@59997: ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))]; neuper@42428: Iterator 1; neuper@42428: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; walther@59747: autoCalculate 1 (Steps 1); walther@60242: autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \ 2) + d_d x (sin (x \ 4))*) walther@60242: (*autoCalculate 1 (Steps 1);([2], Res), d_d x (x \ 2) + cos (x \ 4) * d_d x (x \ \ 4)*) neuper@42428: walther@60242: "~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x \ 2) + cos (4 * x \ 3)"); walther@59868: "~~~~~ fun appendFormula' , args:"; val (cI, (ifo: TermC.as_string)) = (cI, ifo); Walther@60549: val cs = States.get_calc cI Walther@60549: val pos = States.get_pos cI 1; walther@59844: (*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1"; walther@59798: val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*); walther@59798: (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*) walther@59981: "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr) wneuper@59562: = (cs', (encode ifo)); wneuper@59562: val ctxt = get_ctxt pt pos (*see TODO.thy*) Walther@60424: val SOME f_in = (*case*) TermC.parseNEW ctxt istr (*of*); wneuper@59562: val pos_pred = lev_back' pos wneuper@59562: val f_pred = Ctree.get_curr_formula (pt, pos_pred); wneuper@59562: (*if*) f_pred = f_in; (*else*) walther@59982: val NONE = (*case*) CAS_Cmd.input f_in (*of*); walther@59795: (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p) Walther@60586: (*old*)val {program = prog, ...} = MethodC.from_store ctxt metID walther@59807: (*old*)val istate = get_istate_LI pt pos walther@59795: (*old*)val ctxt = get_ctxt pt pos walther@59795: ( *old*) walther@59795: val LI.Not_Derivable = walther@59795: (*case*) LI.locate_input_term (pt, pos) f_in (*of*); Walther@60631: val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p) Walther@60631: val (errpats, rew_rls, prog) = case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of Walther@60586: {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog) Walther@60559: | _ => error "inform: uncovered case of MethodC.from_store ctxt" wneuper@59562: ; Walther@60648: (*+*)if Error_Pattern.s_to_string ctxt errpats = "[(\"chain-rule-diff-both\",\n[d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u), d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u), d_d ?bdv (?u \ ?n) = ?n * ?u \ (?n - 1)],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \ ?n) = ?n * ?u \ (?n - 1) * d_d ?bdv ?u\"]]" walther@59844: (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3"; neuper@42428: walther@59807: val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate wneuper@59562: ; walther@60242: (*+*)if UnparseC.term f_pred = "d_d x (x \ 2) + d_d x (sin (x \ 4))" andalso walther@60242: (*+*) UnparseC.term f_in = "d_d x (x \ 2) + cos (4 * x \ 3)" walther@59844: (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2"; neuper@42428: Walther@60586: val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for ctxt (f_pred, f_in) (prog, env) (errpats, rew_rls) (*of*); neuper@42428: neuper@42428: "--- final check:"; walther@59798: (*+*)val (_, _, ptp') = cs'; walther@59798: case Step_Solve.by_term ptp' (encode ifo) of neuper@42428: ("error pattern #chain-rule-diff-both#", calcstate') => () walther@59844: | _ => error "inform with (positive) Error_Pattern.check_for broken" neuper@42428: neuper@48895: Walther@60631: "----------- re-build: fill_from_store without thy-hierarchy -----------------------------------"; Walther@60631: "----------- re-build: fill_from_store without thy-hierarchy -----------------------------------"; Walther@60631: "----------- re-build: fill_from_store without thy-hierarchy -----------------------------------"; Walther@60631: open Error_Pattern Walther@60631: val c = []: int list Walther@60631: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} Walther@60631: [(["functionTerm (x \ 2 + sin (x \ 4))", "differentiateFor x", "derivative f_f'"], Walther@60631: ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))]; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["diff", "differentiate_on_R"]*) Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))*) Walther@60631: val ([1], Frm) = p; Walther@60631: val "d_d x (x \ 2 + sin (x \ 4))" = f2str f; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))*) Walther@60631: val ([1], Res) = p; Walther@60631: val "d_d x (x \ 2) + d_d x (sin (x \ 4))" = f2str f Walther@60631: Walther@60631: val return_of_me = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_pow", "d_d ?bdv (?bdv \ ?n) = ?n * ?bdv \ (?n - 1)"))*) Walther@60631: val ([1], Res) = p Walther@60631: val "d_d x (x \ 2) + d_d x (sin (x \ 4))" = f2str f; Walther@60631: (* "d_d x (x \ 2) + cos (x \ 4)" .. wrong user input within next step *) Walther@60631: (*//------------------ step into find_fill_patterns ----------------------------------------\\*) Walther@60631: (* INSTEAD OF STEPPING INTO me WE DO SO FOR Kernel.findFillpatterns cI errpatID = Walther@60631: let Walther@60631: val ((pt, _), _) = States.get_calc cI Walther@60631: val pos = States.get_pos cI 1; Walther@60631: val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID Walther@60631: *) Walther@60631: "~~~~~ fun findFillpatterns , args:"; val (pt, p, errpatID) = (pt, p, "chain-rule-diff-both"); Walther@60631: "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), id) = ((pt, p), errpatID); Walther@60631: (*old-------\* ) Walther@60631: val f_curr = Ctree.get_curr_formula (pt, pos); Walther@60631: val pp = Ctree.par_pblobj pt p Walther@60631: val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of Walther@60631: {errpats, program = Rule.Prog prog, ...} => (errpats, prog) Walther@60631: | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt" Walther@60631: ( *new-------\*) Walther@60631: val ctxt = Ctree.get_ctxt pt pos Walther@60631: val f_curr = Ctree.get_curr_formula (pt, pos) Walther@60631: val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p) Walther@60631: val (errpats, prog) = case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of Walther@60631: {errpats, program = Rule.Prog prog, ...} => (errpats, prog) Walther@60631: | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt" Walther@60631: (*new-------/*) Walther@60631: Walther@60631: (*+*)val 1 = length errpats(*ONLY WITH from_store' @{theory (*!!!*)Build_Thydata}*) Walther@60631: val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate Walther@60631: val subst = Subst.for_bdv ctxt prog env Walther@60631: val errpatthms = errpats Walther@60631: |> filter ((curry op = errpatID) o (#1: Error_Pattern.T -> Error_Pattern.id)) Walther@60631: |> map (#3: Error_Pattern.T -> thm list) Walther@60631: |> flat; Walther@60631: Walther@60631: (*+*)val 3 = length errpatthms; Walther@60631: (*+*)val 5 = length (get_fill_ins @{theory} "diff_sin_chain"); Walther@60631: Walther@60631: (*case*) map ( Walther@60631: fill_from_store ctxt subst f_curr errpatID) errpatthms |> flat (*of*); Walther@60631: "~~~~~ fun fill_from_store , args:"; val (ctxt, subst, form, (*id*)errpat_id, thm) = Walther@60631: (ctxt, subst, f_curr, errpatID, hd errpatthms); Walther@60631: val thm_id_long = Thm.get_name_hint thm Walther@60631: Walther@60631: (*+*)val "Diff.diff_sin_chain" = thm_id_long; Walther@60631: (*+*)val "diff_sin_chain" = ThmC.cut_id thm_id_long; Walther@60631: Walther@60631: val thm_id = ThmC.cut_id thm_id_long Walther@60631: val fill_ins = Walther@60631: Walther@60631: Error_Pattern.get_fill_ins (Proof_Context.theory_of ctxt) thm_id; Walther@60631: "~~~~~ fun get_fill_ins , args:"; val (thy, thm_id) = Walther@60631: ((Proof_Context.theory_of ctxt), thm_id); Walther@60631: (*case*) AList.lookup (op =) (get_fill_inss thy) thm_id (*of*); Walther@60631: val ERROR "fill_ins for thm \"diff_sin_chain\" missing in theory \"Isac_Knowledge\" (and ancestors)\nTODO exception hierarchy needs to be established." = Walther@60631: ERROR ("fill_ins for thm \"" ^ thm_id ^ "\" missing in theory \"" ^ Walther@60631: (thy |> ThyC.id_of) ^ "\" (and ancestors)" ^ Walther@60631: "\nTODO exception hierarchy needs to be established."); Walther@60631: Walther@60631: (*return to fill_from_store..*) Walther@60631: val some = map (fill_form ctxt subst (thm, form) errpat_id) fill_ins; Walther@60631: val return_fill_from_store = some |> filter is_some |> map the; Walther@60631: Walther@60631: (* final test ... ----------------------------------------------------------------------------*) Walther@60631: (*+*)if length return_fill_from_store = 5 then Walther@60631: (*+*) case return_fill_from_store of Walther@60631: (*+*) ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm = Walther@60631: (*+*) "d_d x (x \ 2) + d_d x (sin (x \ 4)) =\nd_d x (x \ 2) + cos (x \ 4) * d_d x ?_dummy_1" Walther@60631: (*+*) then () else error "find_fill_patterns changed 2a" Walther@60631: (*+*) | _ => error "find_fill_patterns changed 2b" Walther@60631: (*+*)else error "find_fill_patterns changed 2c"; Walther@60631: (*-------------------- stop step into find_fill_patterns -------------------------------------*) Walther@60631: (*\\------------------ step into find_fill_patterns ----------------------------------------//*) Walther@60631: Walther@60631: val (p,_,f,nxt,_,pt) = return_of_me Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_pow", "d_d ?bdv (?bdv \ ?n) = ?n * ?bdv \ (?n - 1)"))*) Walther@60631: val ([3], Res) = p Walther@60631: val "d_d x (x \ 2) + cos (x \ 4) * (4 * x \ (4 - 1))" = f2str f; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Check_Postcond ["derivative_of", "function"]*) Walther@60631: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60631: val ([], Res) = p; Walther@60631: val "2 * x + cos (x \ 4) * 4 * x \ 3" = f2str f Walther@60631: val End_Proof' = nxt; Walther@60631: Walther@60631: walther@59909: "--------- embed fun find_fill_patterns ---------------------------"; walther@59909: "--------- embed fun find_fill_patterns ---------------------------"; walther@59909: "--------- embed fun find_fill_patterns ---------------------------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} walther@60242: [(["functionTerm (x \ 2 + sin (x \ 4))", "differentiateFor x", "derivative f_f'"], walther@59997: ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))]; neuper@42430: Iterator 1; neuper@42430: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; walther@59747: autoCalculate 1 (Steps 1); walther@60242: autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \ 2) + d_d x (sin (x \ 4))*) Walther@60631: appendFormula 1 "d_d x (x \ 2) + cos (4 * x \ 3)"; neuper@42430: (* error pattern #chain-rule-diff-both# *) neuper@42432: (*or neuper@42432: no derivation found *) neuper@42433: "~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both"); Walther@60549: val ((pt, _), _) = States.get_calc cI Walther@60549: val pos = States.get_pos cI 1; neuper@42430: Walther@60631: val return_from_find_fill_patterns = find_fill_patterns (pt, pos) errpatID; Walther@60631: DEconstrCalcTree 1; neuper@42430: Walther@60631: (* final test ... ----------------------------------------------------------------------------*) Walther@60631: val 6 = length return_from_find_fill_patterns Walther@60631: val (fill_in_id, term, thm, subst) :: _ = return_from_find_fill_patterns neuper@42430: Walther@60631: val "fill-d_d-arg" = fill_in_id Walther@60631: val "d_d x (x \ 2) + d_d x (sin (x \ 4)) =\nd_d x (x \ 2) + cos (x \ 4) * d_d x ?_dummy_1" = Walther@60631: UnparseC.term_in_ctxt @{context} term Walther@60631: val "Diff.diff_sin_chain" = Thm.get_name_hint thm Walther@60631: val "[(''bdv'', x)]" = subst |> the |> Subst.string_of_input; neuper@42430: neuper@42450: neuper@42437: "--------- build fun is_exactly_equal, inputFillFormula ----------"; neuper@42437: "--------- build fun is_exactly_equal, inputFillFormula ----------"; neuper@42437: "--------- build fun is_exactly_equal, inputFillFormula ----------"; Walther@60549: States.reset (); Walther@60571: CalcTree @{context} walther@60242: [(["functionTerm (x \ 2 + sin (x \ 4))", "differentiateFor x", "derivative f_f'"], walther@59997: ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))]; neuper@42437: Iterator 1; neuper@42437: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; walther@59747: autoCalculate 1 (Steps 1); walther@60242: autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \ 2) + d_d x (sin (x \ 4))*) walther@60242: appendFormula 1 "d_d x (x \ 2) + cos (4 * x \ 3)" (*|> Future.join*); (*<<<<<<<=========================*) Walther@60586: (* the check for errpat is maximally liberal (whole term modulo "rew_rls" from "type met"), walther@60242: would recognize "cos (4 * x \ (4 - 1)) + 2 * x" as well. neuper@42437: results in error pattern #chain-rule-diff-both# neuper@42437: instead of no derivation found *) Walther@60549: val ((pt,pos), _) = States.get_calc 1; Walther@60549: val p = States.get_pos 1 1; Walther@60577: val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p); neuper@42437: walther@60242: if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \ 2) + d_d x (sin (x \ 4))" then wneuper@59497: case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], wneuper@59253: ("diff_sum", thm)) => walther@59868: if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then () walther@59909: else error "embed fun fill_form changed 11" walther@59909: | _ => error "embed fun fill_form changed 12" walther@59909: else error "embed fun fill_form changed 13"; neuper@42437: neuper@42437: findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*) walther@60242: (* fill patterns #fill-d_d-arg#d_d x (x \ 2) + d_d x (sin (x \ 4)) = walther@60242: d_d x (x \ 2) + cos (x \ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *) Walther@60549: val ((pt,pos),_) = States.get_calc 1; Walther@60549: val p = States.get_pos 1 1; neuper@42437: Walther@60577: val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p); walther@60242: if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \ 2) + d_d x (sin (x \ 4))" then wneuper@59497: case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], wneuper@59253: ("diff_sum", thm)) => walther@59868: if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then () walther@59909: else error "embed fun fill_form changed 21" walther@59909: | _ => error "embed fun fill_form changed 22" walther@59909: else error "embed fun fill_form changed 23"; neuper@42437: neuper@42437: requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*) neuper@42437: (* ([1], Res) ([2], Res) ([2], Res) *) Walther@60549: val ((pt,pos),_) = States.get_calc 1; Walther@60549: val p = States.get_pos 1 1; Walther@60577: val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p); wneuper@59253: if p = ([1], Res) andalso existpt [2] pt walther@60242: andalso UnparseC.term f = "d_d x (x \ 2) + d_d x (sin (x \ 4))" wneuper@59497: then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], wneuper@59253: ("diff_sum", thm)) => walther@59868: if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then () walther@59909: else error "embed fun fill_form changed 31" walther@59909: | _ => error "embed fun fill_form changed 32" walther@59909: else error "embed fun fill_form changed 33"; neuper@42437: neuper@42437: (* input a formula which exactly fills the gaps in a "fillformula" neuper@42437: presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)": neuper@42437: errpatID: lhs of the respective thm = lhs of fillformula with fillpatID. neuper@42437: the respective thm is in the ctree ................ neuper@42437: *) neuper@42437: "~~~~~ fun inputFillFormula, args:"; val (cI, ifo) = walther@60242: (1, "d_d x (x \ 2) + cos (x \ 4) * d_d x (x \ 4)"); Walther@60549: val ((pt, _), _) = States.get_calc cI Walther@60549: val pos = States.get_pos cI 1; neuper@42437: neuper@42437: "~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo); walther@60360: val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr neuper@42437: val p' = lev_on p; neuper@42437: val tac = get_obj g_tac pt p'; wneuper@59497: val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac; walther@59868: if (UnparseC.term o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then () wneuper@59252: else error "inputFillFormula changed 10"; walther@59921: val Applicable.Yes rew = Step.check tac (pt, pos); neuper@42437: val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew; neuper@42437: neuper@42437: "~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac); walther@59804: val ("ok", (_, c, ptp as (_,p'))) = Step.by_tactic tac (pt, pos); Walther@60549: States.upd_calc cI (ptp, []); Walther@60549: States.upd_ipos cI 1 p'; neuper@42437: autocalculateOK2xml cI pos (if null c then p' else last_elem c) p'; neuper@42437: neuper@42437: "~~~~~ final check:"; Walther@60549: val ((pt, _),_) = States.get_calc 1; Walther@60549: val p = States.get_pos 1 1; Walther@60577: val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p); walther@60242: if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \ 2) + cos (x \ 4) * d_d x (x \ 4)" wneuper@59497: then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], wneuper@59253: ("diff_sin_chain", thm)) => walther@59868: if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then () wneuper@59253: else error "inputFillFormula changed 111" wneuper@59253: | _ => error "inputFillFormula changed 112" wneuper@59253: else error "inputFillFormula changed 113"; neuper@42437: wneuper@59262: "--------- fun appl_adds -----------------------------------------"; wneuper@59262: "--------- fun appl_adds -----------------------------------------"; wneuper@59262: "--------- fun appl_adds -----------------------------------------"; Walther@60586: (* val (dI, oris, model, pbt, selct::ss) = Walther@60586: (dI, pors, probl, model, map itms2fstr probl); wneuper@59262: ...vvv wneuper@59262: *) Walther@60586: (* val (dI, oris, model, pbt, (selct::ss))= Walther@60494: (#1 (References.select_input ospec spec), oris, []:I_Model.T, Walther@60586: ((#model o Problem.from_store) (#2 (References.select_input ospec spec))),(imodel2fstr imodel)); Walther@60586: val iii = appl_adds dI oris model pbt (selct::ss); walther@59942: tracing(I_Model.to_string thy iii); wneuper@59262: Walther@60586: val itm = add_single' dI oris model pbt selct; Walther@60586: val model = I_Model.add itm model; wneuper@59262: wneuper@59262: val _::selct::ss = (selct::ss); Walther@60586: val itm = add_single' dI oris model pbt selct; Walther@60586: val model = I_Model.add itm model; wneuper@59262: wneuper@59262: val _::selct::ss = (selct::ss); Walther@60586: val itm = add_single' dI oris model pbt selct; Walther@60586: val model = I_Model.add itm model; Walther@60586: tracing(I_Model.to_string thy model); wneuper@59262: wneuper@59262: val _::selct::ss = (selct::ss); Walther@60586: val itm = add_single' dI oris model pbt selct; Walther@60586: val model = I_Model.add itm model; wneuper@59262: *) wneuper@59264: "--------- fun concat_deriv --------------------------------------"; wneuper@59264: "--------- fun concat_deriv --------------------------------------"; wneuper@59264: "--------- fun concat_deriv --------------------------------------"; wneuper@59264: (* Walther@60586: val ({rew_ord, asm_rls, rules,...}, fo, ifo) = Walther@60565: (Rule_Set.rep Test_simplify, TermC.parse_test @{context} "x+1+ - 1*2=0", TermC.parse_test @{context} "-2*1+(x+1)=0"); walther@59906: (tracing o Derive.trtas2str) fod'; wneuper@59264: > [" walther@60324: (x + 1 + - 1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (x + 1) = 0, []))", " walther@60324: (- 1 * 2 + (x + 1) = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (1 + x) = 0, []))", " walther@60324: (- 1 * 2 + (1 + x) = 0, Thm ("radd_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (- 1 * 2 + x) = 0, []))", " walther@60324: (1 + (- 1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))", "- 1 * 2 = -2"), (1 + (-2 + x) = 0, []))"] wneuper@59264: val it = () : unit walther@59906: (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod'); wneuper@59264: > [" walther@59997: (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))", "-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))", " walther@59997: (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))", " walther@59997: (-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute", "?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"] wneuper@59264: val it = () : unit wneuper@59264: *) wneuper@59264: "--------- handle an input formula -------------------------------"; wneuper@59264: "--------- handle an input formula -------------------------------"; wneuper@59264: "--------- handle an input formula -------------------------------"; wneuper@59264: (* wneuper@59264: Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler: wneuper@59264: Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden, wneuper@59264: wenn Abteilungen nur auf gleichem Level gesucht werden ? wneuper@59264: WN.040216 wneuper@59264: wneuper@59264: Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml wneuper@59264: wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)"; wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: 1. "5 * x / (x - 2) - x / (x + 2) = 4" wneuper@59264: ... walther@60242: 4. "12 * x + 4 * x \ 2 = 4 * (-4 + x \ 2)",Subproblem["normalise", "poly".. wneuper@59264: ... wneuper@59264: 4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate".. wneuper@59264: ... wneuper@59264: 4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions" wneuper@59264: ... wneuper@59264: "[x = -4 / 3]" wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n] wneuper@59264: wneuper@59264: (4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n] wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: wneuper@59264: wneuper@59264: ------------------------------------------------------------------------------ walther@60242: "Schalk I s.87 Bsp 55b (x/(x \ 2 - 6*x+9) - 1/(x \ 2 - 3*x) =1/x)"; wneuper@59264: ------------------------------------------------------------------------------ walther@60242: 1. "x / (x \ 2 - 6 * x + 9) - 1 / (x \ 2 - 3 * x) = 1 / x" wneuper@59264: ... walther@60324: 4. "(3 + (- 1 * x + x \ 2)) * x = 1 * (9 * x + (x \ 3 + -6 * x \ 2))" wneuper@59367: Subproblem["normalise", "polynomial", "univariate".. wneuper@59264: ... walther@60242: 4.4. "-6 * x + 5 * x \ 2 = 0", Subproblem["bdv_only", "degree_2", "poly".. wneuper@59264: ... wneuper@59264: 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" wneuper@59264: 4.4.5. "[x = 0, x = 6 / 5]" wneuper@59264: ... wneuper@59264: 5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" wneuper@59264: "[x = 6 / 5]" wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: (1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x] wneuper@59264: wneuper@59264: (4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.] wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: wneuper@59264: wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))"; wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: 1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)" wneuper@59264: ... wneuper@59264: 6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x" wneuper@59489: Subproblem["sq", "rootX", "univariate", "equation"] wneuper@59264: ... walther@60242: 6.6. "144 + 288 * x + 144 * x \ 2 = 144 + x \ 2 + 288 * x + 143 * x \ 2" wneuper@59367: Subproblem["normalise", "polynomial", "univariate", "equation"] walther@60242: ...6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"] wneuper@59264: ... Or_to_List wneuper@59264: 6.6.3.2 "UniversalList" wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n] wneuper@59264: wneuper@59264: (6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n] wneuper@59264: ------------------------------------------------------------------------------ wneuper@59264: *) wneuper@59264: (*sh. comments auf 498*) wneuper@59264: "--------- fun dropwhile' ----------------------------------------"; wneuper@59264: "--------- fun dropwhile' ----------------------------------------"; wneuper@59264: "--------- fun dropwhile' ----------------------------------------"; wneuper@59264: (* wneuper@59264: fun equal a b = a=b; wneuper@59264: val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5]; wneuper@59264: val r_foder = rev foder; val r_ifoder = rev ifoder; wneuper@59264: dropwhile' equal r_foder r_ifoder; wneuper@59264: > vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list wneuper@59264: wneuper@59264: val foder = [3,4,5]; val ifoder = [11,12,3,4,5]; wneuper@59264: val r_foder = rev foder; val r_ifoder = rev ifoder; wneuper@59264: dropwhile' equal r_foder r_ifoder; wneuper@59264: > val it = ([3], [3, 12, 11]) : int list * int list wneuper@59264: wneuper@59264: val foder = [5]; val ifoder = [11,12,3,4,5]; wneuper@59264: val r_foder = rev foder; val r_ifoder = rev ifoder; wneuper@59264: dropwhile' equal r_foder r_ifoder; wneuper@59264: > val it = ([5], [5, 4, 3, 12, 11]) : int list * int list wneuper@59264: wneuper@59264: val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5]; wneuper@59264: val r_foder = rev foder; val r_ifoder = rev ifoder; wneuper@59264: dropwhile' equal r_foder r_ifoder; wneuper@59264: > *** dropwhile': did not start with equal elements*)