prep. cleanup istate/ctxt in Ctree, part 6
1.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Mon Feb 24 17:51:26 2020 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Feb 25 18:36:29 2020 +0100
1.3 @@ -30,8 +30,8 @@
1.4 val cappend_problem : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context ->
1.5 Selem.fmz -> Model.ori list * Celem.spec * term -> CTbasic.ctree * CTbasic.pos' list
1.6 val append_atomic : (* for solve.sml *)
1.7 - CTbasic.pos -> Istate_Def.T * Proof.context -> term -> Tactic.input -> Selem.result ->
1.8 - CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
1.9 + CTbasic.pos -> ((Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context)) ->
1.10 + term -> Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
1.11 val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term ->
1.12 Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list
1.13 val append_result : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context ->
1.14 @@ -219,12 +219,14 @@
1.15 in (pt'', cs) end;
1.16
1.17 (* insert a complete step with term, Tactic and result into the Ctree*)
1.18 -fun append_atomic p ist_ctxt f r f' s pt =
1.19 +fun append_atomic p (ic_form, ic_res) f r f' s pt =
1.20 let
1.21 val (iss, f) =
1.22 if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
1.23 - then ((fst (get_obj g_loc pt p), SOME ist_ctxt), get_obj g_form pt p) (*after Take*)
1.24 - else ((NONE, SOME ist_ctxt), f)
1.25 + (* ^^^^^^^ ^^ has been cut before, so this ^^^^^^^^^^^^^^^^^^ might cause
1.26 + exception PTREE "get_obj: pos = ... does not exist", (!) WHICH IS NOT DETECTED BY if *)
1.27 + then ((fst (get_obj g_loc pt p), SOME ic_res), get_obj g_form pt p) (*after Take*)
1.28 + else ((ic_form, SOME ic_res), f)
1.29 in
1.30 insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = iss, branch = NoBranch,
1.31 result = f', ostate = s}) pt p
1.32 @@ -238,12 +240,11 @@
1.33 let
1.34 val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
1.35 val (pt, cs) = cut_tree pt (p, Frm)
1.36 - val pt = append_atomic p (** )ic_res( **)(Istate_Def.e_istate, ContextC.e_ctxt)(**) f r f' s pt
1.37 -(**) val pt = update_loc' pt p (SOME ic_form, SOME ic_res) (**)
1.38 + val pt = append_atomic p (SOME ic_form, ic_res) f r f' s pt
1.39 in
1.40 (pt, cs)
1.41 end
1.42 - else apfst (append_atomic p ic_res f r f' s) (cut_tree pt (p, Frm));
1.43 + else apfst (append_atomic p (NONE, ic_res) f r f' s) (cut_tree pt (p, Frm));
1.44
1.45 (* insert a SubProblem' into the Ctree;
1.46 istate and ctxt are stored different from the other append* *)
2.1 --- a/src/Tools/isac/MathEngine/solve.sml Mon Feb 24 17:51:26 2020 +0100
2.2 +++ b/src/Tools/isac/MathEngine/solve.sml Tue Feb 25 18:36:29 2020 +0100
2.3 @@ -96,7 +96,7 @@
2.4 (* aux.fun for detailrls with Rrls, reverse rewriting *)
2.5 fun rul_terms_2nds _ nds _ [] = nds
2.6 | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
2.7 - (append_atomic [] (Istate.e_istate, ContextC.e_ctxt) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
2.8 + (append_atomic [] (NONE(*guessed*), (Istate.e_istate, ContextC.e_ctxt)) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
2.9 (rul_terms_2nds thy nds t' rts);
2.10
2.11 (* detail steps done internally by Rewrite_Set* into Ctree
3.1 --- a/src/Tools/isac/TODO.thy Mon Feb 24 17:51:26 2020 +0100
3.2 +++ b/src/Tools/isac/TODO.thy Tue Feb 25 18:36:29 2020 +0100
3.3 @@ -25,6 +25,8 @@
3.4 text \<open>
3.5 \begin{itemize}
3.6 \item xxx
3.7 + \item Tactic.is_empty_tac -> Tactic.is_empty,
3.8 + \item xxx
3.9 \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
3.10 there it is Free ("Subproblem", "char list \<times> ..
3.11 instead of Const (|???.Subproblem", "char list \<times> ..
3.12 @@ -427,8 +429,18 @@
3.13 \<close>
3.14 subsection \<open>Ctree\<close>
3.15 text \<open>
3.16 +analysis
3.17 +# mixture pos' .. pos in cappend_*, append_* is confusing
3.18 +# existpt p pt andalso Tactic.is_empty_tac DIFFERENT IN append_*, cappend_* is confusing
3.19 + "exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!
3.20 + NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS is confusing
3.21 + see test/../--- Minisubpbl/800-append-on-Frm.sml ---
3.22 +# ?!? "cut branches below cannot be decided here" in append_atomic
3.23 +# sign. of functions too different ?!?canonical arg.order ?!?
3.24 \begin{itemize}
3.25 \item xxx
3.26 + \item remove update_branch, update_*? -- make branch, etc args of append_*
3.27 + \item xxx
3.28 \item close sig Ctree, contains cappen_* ?only? --- ?make parallel to ?Pide_Store?
3.29 \item xxx
3.30 \item unify args to Ctree.state (pt, p)
4.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Feb 24 17:51:26 2020 +0100
4.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Tue Feb 25 18:36:29 2020 +0100
4.3 @@ -114,10 +114,10 @@
4.4 term at the end:
4.5 \<close>
4.6 text \<open>default_print_depth 40;\<close>
4.7 -ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Math_Engine.f2str f;\<close>
4.8 -ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Math_Engine.f2str f;\<close>
4.9 -ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Math_Engine.f2str f;\<close>
4.10 -ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Math_Engine.f2str f;\<close>
4.11 +ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Test_Code.f2str f;\<close>
4.12 +ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Test_Code.f2str f;\<close>
4.13 +ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Test_Code.f2str f;\<close>
4.14 +ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Test_Code.f2str f;\<close>
4.15 text \<open>default_print_depth 3;\<close>
4.16 text\<open>And, please, note that the result of applying the 'nxt' ruleset is to be
4.17 found in the output of the next step !
4.18 @@ -128,7 +128,7 @@
4.19 perfect mathematics engine has to prove the socalled 'postcondition' of the
4.20 current problem; this is not yet implemented in the current version of ISAC.
4.21 \<close>
4.22 -ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Math_Engine.f2str f;\<close>
4.23 +ML \<open>val (p,_,f,nxt,_,pt) = Test_Code.me nxt p c pt; Test_Code.f2str f;\<close>
4.24 text\<open>Now the mathematics engine has found the end of the calculation.
4.25
4.26 With 'show_pt' the calculation can be inspected (in a more or less readable
5.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Mon Feb 24 17:51:26 2020 +0100
5.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue Feb 25 18:36:29 2020 +0100
5.3 @@ -6,14 +6,123 @@
5.4 "----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
5.5 "----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
5.6 "----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
5.7 +(*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)
5.8 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
5.9 +val (dI',pI',mI') =
5.10 + ("Test", ["sqroot-test","univariate","equation","test"],
5.11 + ["Test","squ-equ-test-subpbl1"]);
5.12 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];(*Model_Problem*)
5.13 + (*autoCalculate 1 CompleteCalcHead;*)
5.14 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "equality (x + 1 = 2)"*)
5.15 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "solveFor x"*)
5.16 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Find "solutions L"*)
5.17 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Theory "Test"*)
5.18 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
5.19 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
5.20 - (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
5.21 + (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
5.22 +
5.23 + (*autoCalculate 1 (Steps 1);*)
5.24 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
5.25 - (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
5.26 - (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
5.27 +
5.28 +(*+*)show_pt_tac pt; (*isa==REP [
5.29 +([], Frm), solve (x + 1 = 2, x)
5.30 +. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
5.31 +([1], Frm), x + 1 = 2
5.32 +. . . . . . . . . . Empty_Tac] *)
5.33 +
5.34 + (*appendFormula 1 "2+ -1 + x = 2";*)
5.35 +"~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ -1 + x = 2");
5.36 + val cs = (*get_calc cI*) ((pt, p), []) (*..continue fun me*)
5.37 + val pos = (*get_pos cI 1*) p (*..continue fun me*)
5.38 +
5.39 + val ("ok", cs' as (_, _, ptp''''')) = (*case*)
5.40 + Step.do_next pos cs (*of*);
5.41 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (pos, cs);
5.42 + val pIopt = Ctree.get_pblID (pt, ip);
5.43 + (*if*) ip = ([], Pos.Res) (*else*);
5.44 + val _ = (*case*) tacis (*of*);
5.45 + val SOME _ = (*case*) pIopt (*of*);
5.46 +
5.47 + Step.switch_specify_solve p_ (pt, ip);
5.48 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.49 + (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
5.50 +
5.51 + LI.do_next (pt, input_pos);
5.52 +"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
5.53 + (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
5.54 + val thy' = get_obj g_domID pt (par_pblobj pt p);
5.55 + val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
5.56 +
5.57 +val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
5.58 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
5.59 +
5.60 +(*+*)val ("ok", ([(Rewrite_Set "norm_equation", _, (([1], Frm), _))], _, _)) =
5.61 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
5.62 +"~~~~~ fun by_tactic , args:"; val (tac_, is, (pt, pos)) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
5.63 + val pos = next_in_prog' pos;
5.64 +
5.65 + (** )val (pos', c, _, pt) =( **)
5.66 + Generate.generate1 tac_ is (pt, pos);
5.67 +"~~~~~ fun generate1 , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
5.68 + = (tac_, is, (pt, pos));
5.69 +
5.70 + (** )val (pt, c) =( **)
5.71 + cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
5.72 + (Tactic.Rewrite_Set (Rule.id_rls rls')) (f',asm) Complete;
5.73 +"~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
5.74 + = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
5.75 + (Tactic.Rewrite_Set (Rule.id_rls rls')), (f',asm), Complete);
5.76 + (*if*) existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) (*then*);
5.77 + val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
5.78 + val (pt, cs) = cut_tree(*!*)pt (p, Frm);
5.79 + (** )val pt = ( **)
5.80 + append_atomic p (SOME ic_form, ic_res) f r f' s pt;
5.81 +"~~~~~ fun append_atomic , args:"; val (p, (ic_form, ic_res), f, r, f', s, pt)
5.82 + = (p, (SOME ic_form, ic_res), f, r, f', s, pt);
5.83 + (*if*) existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) (*else*);
5.84 + val (iss, f) =
5.85 + ((ic_form, SOME ic_res), f); (*return from if*)
5.86 +
5.87 + insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = iss, branch = NoBranch,
5.88 + result = f', ostate = s}) pt p (*return from append_atomic*); (*isa==REP*)
5.89 +"~~~~~ from fun append_atomic \<longrightarrow>funcappend_atomic , return:"; val (pt)
5.90 + = (insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = iss, branch = NoBranch,
5.91 + result = f', ostate = s}) pt p);
5.92 +
5.93 +(*/--------------------- final test ----------------------------------------------------------\\*)
5.94 + val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =
5.95 + (*case*) Step_Solve.by_term ptp (encode ifo) (*of*);
5.96 +
5.97 +val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
5.98 +;
5.99 +if
5.100 + (ctxt_frm |> get_assumptions |> terms2str) = "[\"precond_rootmet x\"]"
5.101 + andalso
5.102 + (ctxt_res |> get_assumptions |> terms2str) = "[\"precond_rootmet x\"]"
5.103 + andalso
5.104 + istate2str ist_res =
5.105 + "Pstate ([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n2 + -1 + x = 2, ORundef, false, true)"
5.106 +then () else error "/800-append-on-Frm.sml CHANGED";
5.107 +
5.108 +show_pt_tac (fst ptp''''');(*[
5.109 +([], Frm), solve (x + 1 = 2, x)
5.110 +. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
5.111 +([1], Frm), x + 1 = 2
5.112 +. . . . . . . . . . Derive Test_simplify,
5.113 +([1,1], Frm), x + 1 = 2
5.114 +. . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
5.115 +([1,1], Res), 1 + x = 2
5.116 +. . . . . . . . . . Rewrite ("#: 1 + x = -1 + (2 + x)", "1 + x = -1 + (2 + x)"),
5.117 +([1,2], Res), -1 + (2 + x) = 2
5.118 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
5.119 +([1,3], Res), -1 + (x + 2) = 2
5.120 +. . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
5.121 +([1,4], Res), x + (-1 + 2) = 2
5.122 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
5.123 +([1,5], Res), x + (2 + -1) = 2
5.124 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
5.125 +([1,6], Res), 2 + -1 + x = 2
5.126 +. . . . . . . . . . tac2str not impl. for ?!,
5.127 +([1], Res), 2 + -1 + x = 2
5.128 +. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"]]
5.129 +*)
6.1 --- a/test/Tools/isac/Test_Some.thy Mon Feb 24 17:51:26 2020 +0100
6.2 +++ b/test/Tools/isac/Test_Some.thy Tue Feb 25 18:36:29 2020 +0100
6.3 @@ -99,1817 +99,6 @@
6.4 \<close> ML \<open>
6.5 \<close>
6.6
6.7 -section \<open>===================================================================================\<close>
6.8 -ML \<open>
6.9 -\<close> ML \<open>
6.10 -\<close> ML \<open>
6.11 -\<close>
6.12 -
6.13 -section \<open>============ Build 800-append-on-Frm.sml ==========================================\<close>
6.14 -ML \<open>
6.15 -\<close> ML \<open>
6.16 -(* Title: "Minisubpbl/250-Rewrite_Set-from-method.sml"
6.17 - Author: Walther Neuper 1105
6.18 - (c) copyright due to lincense terms.
6.19 -*)
6.20 -
6.21 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
6.22 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
6.23 -"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
6.24 -(*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)
6.25 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
6.26 -val (dI',pI',mI') =
6.27 - ("Test", ["sqroot-test","univariate","equation","test"],
6.28 - ["Test","squ-equ-test-subpbl1"]);
6.29 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];(*Model_Problem*)
6.30 - (*autoCalculate 1 CompleteCalcHead;*)
6.31 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "equality (x + 1 = 2)"*)
6.32 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "solveFor x"*)
6.33 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Find "solutions L"*)
6.34 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Theory "Test"*)
6.35 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
6.36 - (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
6.37 - (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
6.38 -\<close> ML \<open>
6.39 - (*autoCalculate 1 (Steps 1);*)
6.40 - (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
6.41 -\<close> ML \<open>
6.42 -(*+*)(get_ctxt pt p |> get_assumptions |> terms2str) = "[\"precond_rootmet x\"]";(*isa==REP*)
6.43 -(*+*)val (SOME (ist, ctxt), NONE) = get_obj g_loc pt (fst p); (*isa==REP*)
6.44 -(*+*)istate2str ist = (*isa==REP*)
6.45 -"Pstate ([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)";
6.46 -(ctxt |> get_assumptions |> terms2str) = "[\"precond_rootmet x\"]"; (*isa==REP*)
6.47 -\<close> ML \<open>
6.48 -(*+*)show_pt_tac pt;(*isa==REP [
6.49 -([], Frm), solve (x + 1 = 2, x)
6.50 -. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
6.51 -([1], Frm), x + 1 = 2
6.52 -. . . . . . . . . . Empty_Tac] *)
6.53 -\<close> ML \<open>
6.54 - (*appendFormula 1 "2+ -1 + x = 2";*)
6.55 -\<close> ML \<open>
6.56 -"~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ -1 + x = 2");
6.57 -\<close> ML \<open>
6.58 - val cs = (*get_calc cI*) ((pt, p), [])
6.59 - val pos = (*get_pos cI 1*) p
6.60 -\<close> ML \<open>
6.61 - val ("ok", cs' as (_, _, ptp''''')) = (*case*)
6.62 - Step.do_next pos cs (*of*);
6.63 -\<close> ML \<open>
6.64 -snd(**) ptp''''' = ([1], Res); (*isa==REP*)
6.65 -(fst((**)snd(**) ptp''''')) = [1]; (*isa==REP*)
6.66 -\<close> ML \<open>(*isa*)
6.67 -(*+*)val (NONE , SOME _) = get_obj g_loc (fst ptp''''') (fst((**)snd(**) ptp'''''));(*isa<> *)
6.68 -\<close> text \<open>(*REP*)
6.69 -(*+*)val (SOME _, SOME _) = get_obj g_loc (fst ptp''''') (fst((**)snd(**) ptp'''''));(* <>REP*)
6.70 -\<close> ML \<open>
6.71 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (pos, cs);
6.72 -\<close> ML \<open>
6.73 - val pIopt = Ctree.get_pblID (pt, ip);
6.74 -\<close> ML \<open>
6.75 - (*if*) ip = ([], Pos.Res) (*else*);
6.76 -\<close> ML \<open>
6.77 - val _ = (*case*) tacis (*of*);
6.78 -\<close> ML \<open>
6.79 - val SOME _ = (*case*) pIopt (*of*);
6.80 -\<close> ML \<open>
6.81 - switch_specify_solve p_ (pt, ip);
6.82 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.83 -\<close> ML \<open>
6.84 - (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
6.85 -\<close> ML \<open>
6.86 - LI.do_next (pt, input_pos);
6.87 -\<close> ML \<open>
6.88 -"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
6.89 -\<close> ML \<open>
6.90 - (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
6.91 -\<close> ML \<open>
6.92 - val thy' = get_obj g_domID pt (par_pblobj pt p);
6.93 - val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
6.94 -\<close> ML \<open>
6.95 -val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
6.96 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
6.97 -\<close> ML \<open>
6.98 - by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
6.99 -\<close> ML \<open>
6.100 -"~~~~~ fun by_tactic , args:"; val (tac_, is, (pt, pos)) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
6.101 -\<close> ML \<open>
6.102 - val pos = next_in_prog' pos
6.103 -\<close> ML \<open>
6.104 - (** )val (pos', c, _, pt) =( **)
6.105 - Generate.generate1 tac_ is (pt, pos);
6.106 -\<close> ML \<open>
6.107 -"~~~~~ fun generate1 , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
6.108 - = (tac_, is, (pt, pos));
6.109 -\<close> ML \<open>
6.110 - (** )val (pt, c) =( **)
6.111 - cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
6.112 - (Tactic.Rewrite_Set (Rule.id_rls rls')) (f',asm) Complete
6.113 -\<close> ML \<open>
6.114 -"~~~~~ fun cappend_atomic , args:"; val (pt, p, ic_res, f, r, f', s)
6.115 - = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
6.116 - (Tactic.Rewrite_Set (Rule.id_rls rls')), (f',asm), Complete);
6.117 -\<close> ML \<open>
6.118 - (*if*) existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)(*then*);
6.119 -\<close> ML \<open>
6.120 - val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
6.121 - val (pt, cs) = cut_tree pt (p, Frm)
6.122 -\<close> ML \<open>
6.123 - (** )val pt = ( **)
6.124 - append_atomic p (**)ic_res(** )(Istate_Def.e_istate, ContextC.e_ctxt)( **) f r f' s pt
6.125 -\<close> ML \<open>
6.126 -"~~~~~ fun append_atomic , args:"; val (p, ist_ctxt, f, r, f', s, pt)
6.127 - = (p, (**)ic_res(** )(Istate_Def.e_istate, ContextC.e_ctxt)( **), f, r, f', s, pt);
6.128 -\<close> ML \<open>
6.129 - (*if*) existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) (*else*);
6.130 -\<close> ML \<open>
6.131 - ((NONE, SOME ist_ctxt), f) (*return from append_atomic*); (*isa*)
6.132 -\<close> ML \<open>
6.133 -(*+*)val (ist, ctxt) = ist_ctxt
6.134 -\<close> ML \<open>
6.135 -(*+isa*)istate2str ist =
6.136 - "Pstate ([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R], e_rls, SOME e_e, \nx + 1 + -1 * 2 = 0, ORundef, true, false)"
6.137 -\<close> ML \<open>
6.138 -(*+isa*)(ctxt |> get_assumptions |> terms2str) = "[\"precond_rootmet x\"]"
6.139 -\<close> ML \<open>
6.140 -\<close> ML \<open>
6.141 -\<close> ML \<open>
6.142 -\<close> ML \<open>
6.143 -\<close> ML \<open>
6.144 -\<close> ML \<open>
6.145 -\<close> ML \<open>
6.146 -\<close> ML \<open>
6.147 -\<close> ML \<open>
6.148 -\<close> ML \<open>
6.149 -\<close> ML \<open>
6.150 -\<close> ML \<open>
6.151 -\<close> ML \<open>
6.152 -\<close> ML \<open>
6.153 -\<close> ML \<open>
6.154 -\<close> ML \<open>
6.155 -\<close> text \<open>(*isa ERROR embed_deriv Frm: uncovered case get_obj*)
6.156 - val ("ok", (_(*use in DG !!!*), _, ptp''''' as (_, _))) =
6.157 - (*case*) Step_Solve.by_term ptp (encode ifo) (*of*);
6.158 -\<close> text \<open>(*isa: pt FROM ELSEWHERE <> REP..*)
6.159 -show_pt_tac (fst ptp''''');(*[
6.160 -([], Frm), solve (x + 1 = 2, x)
6.161 -. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
6.162 -([1], Frm), x + 1 = 2
6.163 -. . . . . . . . . . Derive Test_simplify,
6.164 -([1,1], Frm), x + 1 = 2
6.165 -. . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
6.166 -([1,1], Res), 1 + x = 2
6.167 -. . . . . . . . . . Rewrite ("#: 1 + x = -1 + (2 + x)", "1 + x = -1 + (2 + x)"),
6.168 -([1,2], Res), -1 + (2 + x) = 2
6.169 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
6.170 -([1,3], Res), -1 + (x + 2) = 2
6.171 -. . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
6.172 -([1,4], Res), x + (-1 + 2) = 2
6.173 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
6.174 -([1,5], Res), x + (2 + -1) = 2
6.175 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
6.176 -([1,6], Res), 2 + -1 + x = 2
6.177 -. . . . . . . . . . tac2str not impl. for ?!,
6.178 -([1], Res), 2 + -1 + x = 2
6.179 -. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"]]
6.180 -*)
6.181 -\<close> ML \<open>
6.182 -"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp''''', (encode ifo));
6.183 -\<close> ML \<open>
6.184 -(*+*)get_obj g_loc pt ((** )fst( **) p);(*NONE, SOME*)
6.185 -\<close> ML \<open>
6.186 -\<close> ML \<open>
6.187 - val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr (*of*);
6.188 -\<close> ML \<open>
6.189 - val f_in = Thm.term_of f_in
6.190 - val pos_pred = lev_back(*'*) pos
6.191 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
6.192 - val f_succ = Ctree.get_curr_formula (pt, pos);
6.193 -\<close> ML \<open>
6.194 - (*if*) f_succ = f_in (*else*);
6.195 -\<close> ML \<open>
6.196 - val NONE = (*case*) Inform.cas_input f_in (*of*);
6.197 -\<close> text \<open>(*isa ERROR embed_deriv Frm: uncovered case get_obj*)
6.198 - val LI.Found_Step cstate =
6.199 -(*case*)LI.locate_input_term (pt, pos) f_in (*of*);
6.200 -\<close> ML \<open>
6.201 -"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
6.202 -\<close> ML \<open>
6.203 - val pos_pred = Pos.lev_back' pos;
6.204 -\<close> text \<open>(*isa ERROR embed_deriv Frm: uncovered case get_obj*)
6.205 - val ("ok", (_, _, cstate)) =
6.206 - (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
6.207 -\<close> ML \<open>
6.208 -"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p,p_))), ifo)
6.209 - = (([], [], (pt, pos_pred)), tm);
6.210 -\<close> ML \<open>
6.211 - val fo =
6.212 - case p_ of
6.213 - Pos.Frm => Ctree.get_obj Ctree.g_form pt p
6.214 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
6.215 - | _ => Rule.e_term (*on PblObj is fo <> ifo*);
6.216 - val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
6.217 - val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls
6.218 -\<close> ML \<open>
6.219 -(*+*)val ("sqrt_right", _) = rew_ord; (*isa==REP*)
6.220 -(*+*)val Rls {id = "tval_rls", ...} = erls; (*isa==REP*)
6.221 -(*+*)length rules = 37; (*isa==REP*)
6.222 -(*+*)term2str fo = "x + 1 = 2"; (*isa==REP*)
6.223 -(*+*)term2str ifo = "2 + -1 + x = 2"; (*isa==REP*)
6.224 -
6.225 - val (found, der) =
6.226 - Inform.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
6.227 -\<close> ML \<open>
6.228 -(*+*)length der = 6;(*isa==REP*)
6.229 -\<close> ML \<open>
6.230 - (*if*) found (*then*);
6.231 -\<close> ML \<open>
6.232 - val tacis' = map (Inform.mk_tacis rew_ord erls) der;
6.233 -\<close> text \<open>(*isa ERROR last_elem*)
6.234 - (**)val (c', ptp''''') =(**)
6.235 - Generate.embed_deriv tacis' ptp;
6.236 -\<close> ML \<open>
6.237 -"~~~~~ fun embed_deriv , args:"; val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp);
6.238 -\<close> ML \<open>
6.239 -show_pt_tac (fst ptp''''');(*isa<>REP: [1,1]..[1,6] *)
6.240 -\<close> ML \<open>
6.241 -length tacis = 6; (*isa==REP*)
6.242 -\<close> ML \<open>
6.243 - val (res, asm) = (res_from_taci o last_elem) tacis
6.244 -\<close> text \<open> (*isa*)
6.245 -(*+*)val (NONE, SOME _) = get_obj g_loc pt p;
6.246 -\<close> ML \<open>
6.247 -(*+*)get_obj g_loc pt p;
6.248 -\<close> ML \<open>
6.249 -\<close> text \<open> (*REP*)
6.250 -(*+*)val (SOME _, SOME _) = get_obj g_loc pt p
6.251 -\<close> ML \<open>
6.252 -(*+*)p = [1]; (*isa==REP*)
6.253 -\<close> ML \<open>
6.254 -(*+*)show_pt_tac pt;(*[
6.255 -([], Frm), solve (x + 1 = 2, x)
6.256 -. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
6.257 -([1], Frm), x + 1 = 2
6.258 -. . . . . . . . . . Rewrite_Set "norm_equation",
6.259 -([1], Res), x + 1 + -1 * 2 = 0
6.260 -. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"]] *)
6.261 -\<close> ML \<open>
6.262 - val (ist, ctxt) = case get_obj g_loc pt p of
6.263 - (SOME (ist, ctxt), _) => (ist, ctxt)
6.264 - | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"
6.265 -\<close> ML \<open>
6.266 - val form = get_obj g_form pt p
6.267 -\<close> ML \<open>
6.268 - val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
6.269 - (insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
6.270 - (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
6.271 - val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
6.272 -;
6.273 - (** )val (pt, c, pos as (p, _)) =( **)
6.274 - generate (rev tacis) (pt, [], (p, Res))
6.275 -\<close> ML \<open>
6.276 -"~~~~~ fun generate , args:"; val (tacis, (pt, c: pos' list, _: pos'))
6.277 - = ((rev tacis), (pt, [], (p, Res)));
6.278 -\<close> ML \<open>
6.279 - val (tacis', (_, tac_, (p, is))) = split_last tacis
6.280 -\<close> ML \<open>
6.281 - (** )val (p',c',_,pt') =( **)
6.282 - generate1 tac_ is (pt, p);
6.283 -"~~~~~ fun generate1 , args:"; val ((Tactic.Begin_Trans' t), l, (pt, (p, Frm))) = (tac_, is, (pt, p));
6.284 -\<close> ML \<open>
6.285 - (** )val (pt, c) =( **)
6.286 - cappend_form pt p l t;
6.287 -"~~~~~ fun cappend_form , args:"; val (pt, p, loc, f) = (pt, p, l, t);
6.288 -\<close> ML \<open>
6.289 - val (pt', cs) = cut_tree pt (p, Frm)
6.290 -\<close> ML \<open>
6.291 - (** )val pt'' =( **)
6.292 - append_form p loc f pt';
6.293 -\<close> ML \<open>
6.294 -"~~~~~ fun append_form , args:"; val (p, l, f, pt) = (p, loc, f, pt');
6.295 -\<close> ML \<open>
6.296 - val (pt', cs) = cut_tree pt (p, Frm)
6.297 -\<close> ML \<open>
6.298 - insert_pt (PrfObj {cell = NONE, form = f, tac = Tactic.Empty_Tac, loc = (SOME l, NONE),
6.299 - branch = NoBranch, result = (Rule.e_term, []), ostate = Incomplete}) pt p;
6.300 - (*return from append_form*);
6.301 -\<close> ML \<open>
6.302 -"~~~~~ from fun append_form \<longrightarrow>fun cappend_form, return:"; val (pt'')
6.303 - = (insert_pt (PrfObj {cell = NONE, form = f, tac = Tactic.Empty_Tac, loc = (SOME l, NONE),
6.304 - branch = NoBranch, result = (Rule.e_term, []), ostate = Incomplete}) pt p);
6.305 -\<close> ML \<open>
6.306 - (pt'', cs); (*return from cappend_form*)
6.307 -\<close> ML \<open>
6.308 -"~~~~~ from fun cappend_form \<longrightarrow>fun generate1 , return:"; val (pt, c:pos' list) = (pt'', cs);
6.309 -\<close> ML \<open>
6.310 - val pt = update_branch pt p TransitiveB (*040312*)
6.311 - (* replace the old PrfOjb ~~~~~ *)
6.312 - val p = (lev_on o lev_dn (* starts with [...,0] *)) p
6.313 - val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)
6.314 - (*^^^^^^^^^^^^^^^^^^^^^again, skipped *)
6.315 -\<close> ML \<open>
6.316 - ((p, Frm), c @ c', FormKF (Rule.term2str t), pt) (*return from generate1*);
6.317 -\<close> ML \<open>
6.318 -"~~~~~ from fun generate1 \<longrightarrow>fun generate \<longrightarrow>fun zzz , return:"; val (p',c',_,pt')
6.319 - = ((p, Frm), c @ c', FormKF (Rule.term2str t), pt);
6.320 -\<close> ML \<open>
6.321 - generate tacis' (pt', c@c', p');
6.322 -\<close> ML \<open>
6.323 -"~~~~~ fun generate , args:"; val (tacis, (pt, c, _: pos')) = (tacis' , (pt', c@c', p'));
6.324 -\<close> ML \<open>
6.325 - val (tacis', (_, tac_, (p, is))) = split_last tacis
6.326 -\<close> ML \<open>
6.327 - (** )val (p',c',_,pt') =( **)
6.328 - generate1 tac_ is (pt, p);
6.329 -\<close> ML \<open>
6.330 -"~~~~~ fun generate1 , args:"; val ((Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))), (is, ctxt), (pt, (p, _)))
6.331 - = (tac_, is, (pt, p));
6.332 -\<close> ML \<open>
6.333 - (** )val (pt, c) =( **)
6.334 - cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Complete
6.335 -\<close> ML \<open>
6.336 -"~~~~~ fun cappend_atomic , args:"; val (pt, p, ic_res, f, r, f', s)
6.337 - = (pt, p, (is, ctxt), f, (Tactic.Rewrite thm'), (f', asm), Complete);
6.338 -\<close> ML \<open>
6.339 - (*if*) existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) (*then*);
6.340 -\<close> ML \<open>
6.341 - val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
6.342 - val (pt, cs) = cut_tree pt (p, Frm)
6.343 -\<close> ML \<open>
6.344 -(*//------------------------- ? change ? ----------------------------------------------------\\*)
6.345 - val pt = append_atomic p (** )ic_res( **)(Istate_Def.e_istate, ContextC.e_ctxt)(**) f r f' s pt
6.346 -\<close> ML \<open>
6.347 -(**) val pt = update_loc' pt p (SOME ic_form, SOME ic_res) (**)
6.348 -(*\\------------------------- ? change ? ----------------------------------------------------//*)
6.349 -\<close> ML \<open>
6.350 -\<close> ML \<open>
6.351 -\<close> ML \<open>
6.352 -\<close> ML \<open>
6.353 -\<close> ML \<open>
6.354 -\<close> ML \<open>
6.355 -\<close> ML \<open>
6.356 -\<close> ML \<open>
6.357 -\<close> ML \<open>
6.358 -\<close> ML \<open>
6.359 -\<close> ML \<open>
6.360 -\<close> ML \<open>
6.361 -\<close> ML \<open>
6.362 -\<close> ML \<open>
6.363 -\<close> ML \<open>
6.364 -\<close>
6.365 -
6.366 -section \<open>============ Check Interpret/inform.sml ===========================================\<close>
6.367 -ML \<open>
6.368 -\<close> ML \<open>
6.369 -(* Title: Interpret/inform.sml
6.370 - Author: Walther Neuper 060225,
6.371 - (c) due to copyright terms
6.372 -*)
6.373 -
6.374 -"-----------------------------------------------------------------";
6.375 -"table of contents -----------------------------------------------";
6.376 -"-----------------------------------------------------------------";
6.377 -"appendForm with miniscript with mini-subpbl:";
6.378 -"--------- appendFormula: on Res + equ_nrls ----------------------";
6.379 -"ERR--------- appendFormula: on Frm + equ_nrls ----------------------";
6.380 -"--------- appendFormula: on Res + NO deriv ----------------------";
6.381 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
6.382 -"replaceForm with miniscript with mini-subpbl:";
6.383 -"--------- replaceFormula: on Res + = ----------------------------";
6.384 -"ERR--------- replaceFormula: on Res + = 1st Nd ---------------------";
6.385 -"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
6.386 -"ERR--------- replaceFormula: cut calculation -----------------------";
6.387 -(* "--------- maximum-example, UC: Modeling / modifyCalcHead --------";*)
6.388 -"--------- syntax error ------------------------------------------";
6.389 -"--------- CAS-command on ([],Pbl) -------------------------------";
6.390 -"--------- CAS-command on ([],Pbl) FE-interface ------------------";
6.391 -"--------- inform [rational,simplification] ----------------------";
6.392 -"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
6.393 -"--------- Take as 1st tac, start from exp -----------------------";
6.394 -"--------- init_form, start with <NEW> (CAS input) ---------------";
6.395 -"--------- build fun check_err_patt ------------------------------";
6.396 -"--------- build fun check_err_patt ?bdv -------------------------";
6.397 -"--------- build fun check_error_patterns ------------------------";
6.398 -"--------- embed fun check_error_patterns ------------------------";
6.399 -"--------- build fun get_fillpats --------------------------------";
6.400 -"--------- embed fun find_fillpatterns ---------------------------";
6.401 -"--------- build fun is_exactly_equal, inputFillFormula ----------";
6.402 -"--------- fun appl_adds -----------------------------------------";
6.403 -"--------- fun concat_deriv --------------------------------------";
6.404 -"--------- handle an input formula -------------------------------";
6.405 -"--------- fun dropwhile' ----------------------------------------";
6.406 -"-----------------------------------------------------------------";
6.407 -"-----------------------------------------------------------------";
6.408 -"-----------------------------------------------------------------";
6.409 -
6.410 -
6.411 -"--------- appendFormula: on Res + equ_nrls ----------------------";
6.412 -"--------- appendFormula: on Res + equ_nrls ----------------------";
6.413 -"--------- appendFormula: on Res + equ_nrls ----------------------";
6.414 - val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
6.415 - (writeln o term2str) sc;
6.416 - val Prog sc = (#scr o get_met) ["Test","solve_linear"];
6.417 - (writeln o term2str) sc;
6.418 -
6.419 - reset_states ();
6.420 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.421 - ("Test", ["sqroot-test","univariate","equation","test"],
6.422 - ["Test","squ-equ-test-subpbl1"]))];
6.423 - Iterator 1; moveActiveRoot 1;
6.424 - autoCalculate 1 CompleteCalcHead;
6.425 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.426 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.427 -
6.428 - appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
6.429 - val ((pt,_),_) = get_calc 1;
6.430 - val str = pr_ctree pr_short pt;
6.431 -if str =
6.432 -(". ----- pblobj -----\n" ^
6.433 -"1. x + 1 = 2\n" ^
6.434 -"2. x + 1 + -1 * 2 = 0\n" ^
6.435 -"2.1. x + 1 + -1 * 2 = 0\n" ^
6.436 -"2.2. 1 + x + -1 * 2 = 0\n" ^
6.437 -"2.3. 1 + (x + -1 * 2) = 0\n" ^
6.438 -"2.4. 1 + (x + -2) = 0\n" ^
6.439 -"2.5. 1 + (x + -2 * 1) = 0\n" ^
6.440 -"2.6. 1 + x + -2 * 1 = 0\n" ) then ()
6.441 -else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
6.442 -
6.443 - moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
6.444 - moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
6.445 -
6.446 - (*the seven steps of detailed derivation*)
6.447 - moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
6.448 - moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);
6.449 - moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);
6.450 - moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res);
6.451 - moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
6.452 - moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
6.453 - moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
6.454 - val ((pt,_),_) = get_calc 1;
6.455 - if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()
6.456 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
6.457 -
6.458 - fetchProposedTactic 1; (*takes Iterator 1 _1_*)
6.459 -(* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*)
6.460 -(*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 =============
6.461 - val (_,(tac,_,_)::_) = get_calc 1;
6.462 - if tac = Rewrite_Set "Test_simplify" then ()
6.463 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
6.464 -============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
6.465 -
6.466 - autoCalculate 1 CompleteCalc;
6.467 - val ((pt,_),_) = get_calc 1;
6.468 - if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.469 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
6.470 - (* autoCalculate 1 CompleteCalc;
6.471 - val ((pt,p),_) = get_calc 1;
6.472 - (writeln o istates2str) (get_obj g_loc pt [ ]);
6.473 - (writeln o istates2str) (get_obj g_loc pt [1]);
6.474 - (writeln o istates2str) (get_obj g_loc pt [2]);
6.475 - (writeln o istates2str) (get_obj g_loc pt [3]);
6.476 - (writeln o istates2str) (get_obj g_loc pt [3,1]);
6.477 - (writeln o istates2str) (get_obj g_loc pt [3,2]);
6.478 - (writeln o istates2str) (get_obj g_loc pt [4]);
6.479 -
6.480 - *)
6.481 -"----------------------------------------------------------";
6.482 -
6.483 - val fod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
6.484 - ((#rules o rep_rls) Test_simplify)
6.485 - (sqrt_right false (@{theory "Pure"})) NONE
6.486 - (str2term "x + 1 + -1 * 2 = 0");
6.487 - (writeln o trtas2str) fod;
6.488 -
6.489 - val ifod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
6.490 - ((#rules o rep_rls) Test_simplify)
6.491 - (sqrt_right false (@{theory "Pure"})) NONE
6.492 - (str2term "-2 * 1 + (1 + x) = 0");
6.493 - (writeln o trtas2str) ifod;
6.494 - fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
6.495 - val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
6.496 - val der = fod' @ (map rev_deriv' rifod');
6.497 - (writeln o trtas2str) der;
6.498 - "----------------------------------------------------------";
6.499 -DEconstrCalcTree 1;
6.500 -
6.501 -\<close> ML \<open>
6.502 -"--------- appendFormula: on Frm + equ_nrls ----------------------";
6.503 -"--------- appendFormula: on Frm + equ_nrls ----------------------";
6.504 -"--------- appendFormula: on Frm + equ_nrls ----------------------";
6.505 - reset_states ();
6.506 -\<close> ML \<open>
6.507 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.508 - ("Test", ["sqroot-test","univariate","equation","test"],
6.509 - ["Test","squ-equ-test-subpbl1"]))];
6.510 - Iterator 1; moveActiveRoot 1;
6.511 - autoCalculate 1 CompleteCalcHead;
6.512 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
6.513 -\<close> ML \<open>
6.514 - val ((pt,_),_) = get_calc 1;
6.515 -\<close> ML \<open>
6.516 -show_pt_tac pt;(*[
6.517 -([], Frm), solve (x + 1 = 2, x)
6.518 -. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
6.519 -([1], Frm), x + 1 = 2
6.520 -. . . . . . . . . . Empty_Tac] *)
6.521 -\<close> ML \<open>
6.522 - appendFormula 1 "2+ -1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
6.523 -
6.524 -\<close> ML \<open>
6.525 - val ((pt,_),_) = get_calc 1;
6.526 -\<close> ML \<open>
6.527 -show_pt_tac pt;(*[
6.528 -([], Frm), solve (x + 1 = 2, x)
6.529 -. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
6.530 -([1], Frm), x + 1 = 2
6.531 -. . . . . . . . . . Derive Test_simplify,
6.532 -([1,1], Frm), x + 1 = 2
6.533 -. . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
6.534 -([1,1], Res), 1 + x = 2
6.535 -. . . . . . . . . . Rewrite ("#: 1 + x = -1 + (2 + x)", "1 + x = -1 + (2 + x)"),
6.536 -([1,2], Res), -1 + (2 + x) = 2
6.537 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
6.538 -([1,3], Res), -1 + (x + 2) = 2
6.539 -. . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
6.540 -([1,4], Res), x + (-1 + 2) = 2
6.541 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
6.542 -([1,5], Res), x + (2 + -1) = 2
6.543 -. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
6.544 -([1,6], Res), 2 + -1 + x = 2
6.545 -. . . . . . . . . . tac2str not impl. for ?!,
6.546 -([1], Res), 2 + -1 + x = 2
6.547 -. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"]]
6.548 -*)
6.549 -\<close> ML \<open>
6.550 - moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
6.551 -
6.552 -\<close> ML \<open>
6.553 - moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
6.554 - moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
6.555 - moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
6.556 - moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
6.557 - moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
6.558 - moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
6.559 - moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
6.560 -\<close> ML \<open>
6.561 - val ((pt,_),_) = get_calc 1;
6.562 -\<close> ML \<open>
6.563 -term2str (fst (get_obj g_result pt [1,6]))
6.564 -\<close> ML \<open>
6.565 - if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()
6.566 - else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
6.567 -\<close> ML \<open>
6.568 -
6.569 - fetchProposedTactic 1; (*takes Iterator 1 _1_*)
6.570 - val (_,(tac,_,_)::_) = get_calc 1;
6.571 - case tac of Rewrite_Set "norm_equation" => ()
6.572 - | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
6.573 - autoCalculate 1 CompleteCalc;
6.574 - val ((pt,_),_) = get_calc 1;
6.575 -\<close> ML \<open>
6.576 - if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.577 - else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
6.578 -DEconstrCalcTree 1;
6.579 -
6.580 -\<close> ML \<open>
6.581 -"--------- appendFormula: on Res + NO deriv ----------------------";
6.582 -"--------- appendFormula: on Res + NO deriv ----------------------";
6.583 -"--------- appendFormula: on Res + NO deriv ----------------------";
6.584 - reset_states ();
6.585 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.586 - ("Test", ["sqroot-test","univariate","equation","test"],
6.587 - ["Test","squ-equ-test-subpbl1"]))];
6.588 - Iterator 1; moveActiveRoot 1;
6.589 - autoCalculate 1 CompleteCalcHead;
6.590 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.591 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.592 -
6.593 - appendFormula 1 "x = 2" (*|> Future.join*);
6.594 - val ((pt,p),_) = get_calc 1;
6.595 - val str = pr_ctree pr_short pt;
6.596 - writeln str;
6.597 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
6.598 - then ()
6.599 - else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
6.600 -
6.601 - fetchProposedTactic 1;
6.602 - val (_,(tac,_,_)::_) = get_calc 1;
6.603 - case tac of Rewrite_Set "Test_simplify" => ()
6.604 - | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
6.605 - autoCalculate 1 CompleteCalc;
6.606 - val ((pt,_),_) = get_calc 1;
6.607 - if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.608 - else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
6.609 -DEconstrCalcTree 1;
6.610 -
6.611 -\<close> ML \<open>
6.612 -"--------- appendFormula: on Res + late deriv --------------------";
6.613 -"--------- appendFormula: on Res + late deriv --------------------";
6.614 -"--------- appendFormula: on Res + late deriv --------------------";
6.615 -(*cp with "fun me" to test/../lucas-interpreter.sml:
6.616 - re-build: fun locate_input_term ---------------------------------------------------";
6.617 -*)
6.618 - reset_states ();
6.619 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.620 - ("Test", ["sqroot-test","univariate","equation","test"],
6.621 - ["Test","squ-equ-test-subpbl1"]))];
6.622 - Iterator 1; moveActiveRoot 1;
6.623 - autoCalculate 1 CompleteCalcHead;
6.624 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.625 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.626 -
6.627 - appendFormula 1 "x = 1" (*|> Future.join*);
6.628 - val ((pt,p),_) = get_calc 1;
6.629 - val str = pr_ctree pr_short pt;
6.630 - writeln str;
6.631 - 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)
6.632 - then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
6.633 - else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
6.634 -
6.635 - fetchProposedTactic 1;
6.636 - val (_,(tac,_,_)::_) = get_calc 1;
6.637 - case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => ()
6.638 - | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
6.639 - autoCalculate 1 CompleteCalc;
6.640 - val ((pt,_),_) = get_calc 1;
6.641 - if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.642 - else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
6.643 -DEconstrCalcTree 1;
6.644 -
6.645 -\<close> ML \<open>
6.646 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
6.647 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
6.648 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
6.649 - reset_states ();
6.650 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.651 - ("Test", ["sqroot-test","univariate","equation","test"],
6.652 - ["Test","squ-equ-test-subpbl1"]))];
6.653 - Iterator 1; moveActiveRoot 1;
6.654 - autoCalculate 1 CompleteCalcHead;
6.655 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.656 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.657 - appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
6.658 - val ((pt,p),_) = get_calc 1;
6.659 - val str = pr_ctree pr_short pt;
6.660 - writeln str;
6.661 - 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 ()
6.662 - else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
6.663 - autoCalculate 1 CompleteCalc;
6.664 - val ((pt,p),_) = get_calc 1;
6.665 - if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.666 - (* ~~~~~~~~~~ simplify as last step in any script ?!*)
6.667 - else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
6.668 -DEconstrCalcTree 1;
6.669 -
6.670 -\<close> ML \<open>
6.671 -"--------- replaceFormula: on Res + = ----------------------------";
6.672 -"--------- replaceFormula: on Res + = ----------------------------";
6.673 -"--------- replaceFormula: on Res + = ----------------------------";
6.674 - reset_states ();
6.675 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.676 - ("Test", ["sqroot-test","univariate","equation","test"],
6.677 - ["Test","squ-equ-test-subpbl1"]))];
6.678 - Iterator 1; moveActiveRoot 1;
6.679 - autoCalculate 1 CompleteCalcHead;
6.680 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.681 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.682 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
6.683 -
6.684 - replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
6.685 - val ((pt,_),_) = get_calc 1;
6.686 - val str = pr_ctree pr_short pt;
6.687 -
6.688 -(* before AK110725 this was
6.689 -". ----- pblobj -----\n
6.690 -1. x + 1 = 2\n
6.691 -2. x + 1 + -1 * 2 = 0\n
6.692 -2.1. x + 1 + -1 * 2 = 0\n
6.693 -2.2. 1 + x + -1 * 2 = 0\n
6.694 -2.3. 1 + (x + -1 * 2) = 0\n
6.695 -2.4. 1 + (x + -2) = 0\n
6.696 -2.5. 1 + (x + -2 * 1) = 0\n
6.697 -2.6. 1 + x + -2 * 1 = 0\n";
6.698 -*)
6.699 -if str =
6.700 -". ----- pblobj -----\n"^
6.701 -"1. x + 1 = 2\n"^
6.702 -"2. x + 1 + -1 * 2 = 0\n"^
6.703 -"2.1. x + 1 + -1 * 2 = 0\n"^
6.704 -"2.2. 1 + x + -1 * 2 = 0\n"^
6.705 -"2.3. 1 + (x + -1 * 2) = 0\n"^
6.706 -"2.4. 1 + (x + -2) = 0\n"^
6.707 -"2.5. 1 + (x + -2 * 1) = 0\n"^
6.708 -"2.6. 1 + x + -2 * 1 = 0\n" then()
6.709 -else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
6.710 -
6.711 - autoCalculate 1 CompleteCalc;
6.712 - val ((pt,pos as (p,_)),_) = get_calc 1;
6.713 - if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
6.714 - else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
6.715 -DEconstrCalcTree 1;
6.716 -
6.717 -\<close> ML \<open>
6.718 -"--------- replaceFormula: on Res + = 1st Nd ---------------------";
6.719 -"--------- replaceFormula: on Res + = 1st Nd ---------------------";
6.720 -"--------- replaceFormula: on Res + = 1st Nd ---------------------";
6.721 - reset_states ();
6.722 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.723 - ("Test", ["sqroot-test","univariate","equation","test"],
6.724 - ["Test","squ-equ-test-subpbl1"]))];
6.725 - Iterator 1; moveActiveRoot 1;
6.726 - autoCalculate 1 CompleteCalcHead;
6.727 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.728 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.729 -
6.730 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
6.731 - val ((pt,_),_) = get_calc 1;
6.732 - val str = pr_ctree pr_short pt;
6.733 - writeln str;
6.734 - 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 ()
6.735 - else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
6.736 - autoCalculate 1 CompleteCalc;
6.737 - val ((pt,pos as (p,_)),_) = get_calc 1;
6.738 - if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
6.739 - else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
6.740 -DEconstrCalcTree 1;
6.741 -
6.742 -\<close> ML \<open>
6.743 -"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
6.744 -"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
6.745 -"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
6.746 - reset_states ();
6.747 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.748 - ("Test", ["sqroot-test","univariate","equation","test"],
6.749 - ["Test","squ-equ-test-subpbl1"]))];
6.750 - Iterator 1; moveActiveRoot 1;
6.751 - autoCalculate 1 CompleteCalcHead;
6.752 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.753 -
6.754 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
6.755 - val ((pt,_),_) = get_calc 1;
6.756 - val str = pr_ctree pr_short pt;
6.757 - writeln str;
6.758 - 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 ()
6.759 - else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
6.760 - autoCalculate 1 CompleteCalc;
6.761 - val ((pt,pos as (p,_)),_) = get_calc 1;
6.762 - if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
6.763 - else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
6.764 -DEconstrCalcTree 1;
6.765 -
6.766 -\<close> ML \<open>
6.767 -"--------- replaceFormula: cut calculation -----------------------";
6.768 -"--------- replaceFormula: cut calculation -----------------------";
6.769 -"--------- replaceFormula: cut calculation -----------------------";
6.770 - reset_states ();
6.771 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.772 - ("Test", ["sqroot-test","univariate","equation","test"],
6.773 - ["Test","squ-equ-test-subpbl1"]))];
6.774 - Iterator 1; moveActiveRoot 1;
6.775 - autoCalculate 1 CompleteCalc;
6.776 - moveActiveRoot 1; moveActiveDown 1;
6.777 - if get_pos 1 1 = ([1], Frm) then ()
6.778 - else error "inform.sml: diff.behav. cut calculation 1";
6.779 -
6.780 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
6.781 - val ((pt,p),_) = get_calc 1;
6.782 - val str = pr_ctree pr_short pt;
6.783 - writeln str;
6.784 - if p = ([1], Res) then ()
6.785 - else error "inform.sml: diff.behav. cut calculation 2";
6.786 -
6.787 -
6.788 -\<close> ML \<open>
6.789 -(* 040307 copied from informtest.sml; ... old version
6.790 - "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
6.791 - "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
6.792 - "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
6.793 -
6.794 - val p = ([],Pbl);
6.795 - val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
6.796 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
6.797 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
6.798 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
6.799 - (*^^^ these are the elements for the root-problem (in variants)*)
6.800 - (*vvv these are elements required for subproblems*)
6.801 - "boundVariable a","boundVariable b","boundVariable alpha",
6.802 - "interval {x::real. 0 <= x & x <= 2*r}",
6.803 - "interval {x::real. 0 <= x & x <= 2*r}",
6.804 - "interval {x::real. 0 <= x & x <= pi}",
6.805 - "errorBound (eps=(0::real))"]
6.806 - (*specifying is not interesting for this example*)
6.807 - val spec = ("DiffApp", ["maximum_of","function"],
6.808 - ["DiffApp","max_by_calculus"]);
6.809 - (*the empty model with descriptions for user-guidance by Model_Problem*)
6.810 - val empty_model = [Given ["fixedValues []"],
6.811 - Find ["maximum", "valuesFor"],
6.812 - Relate ["relations []"]];
6.813 -
6.814 -
6.815 - (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
6.816 - val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
6.817 - (*val nxt = ("Model_Problem", ...*)
6.818 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
6.819 -
6.820 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.821 - (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
6.822 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
6.823 -(*[
6.824 -(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
6.825 -(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
6.826 -(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
6.827 -(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
6.828 -
6.829 - (*the empty CalcHead is checked w.r.t the model and re-established as such*)
6.830 - val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
6.831 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
6.832 - 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(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
6.833 -
6.834 - (*there is one input to the model (could be more)*)
6.835 - val (b,pt,ocalhd) =
6.836 - input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
6.837 - Find ["maximum", "valuesFor"],
6.838 - Relate ["relations"]], Pbl, e_spec);
6.839 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
6.840 - 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(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
6.841 - else error "informtest.sml: diff.behav. max 2";
6.842 -
6.843 - (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
6.844 - val (b,pt''''',ocalhd) =
6.845 - input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
6.846 - Find ["maximum A", "valuesFor [a,b]"],
6.847 - Relate ["relations [A=a*b, a/2=r*sin alpha, \
6.848 - \b/2=r*cos alpha]"]], Pbl, e_spec);
6.849 - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
6.850 - if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
6.851 -
6.852 - (*this input is complete in variant 1 (variant 3 does not work yet)*)
6.853 - val (b,pt''''',ocalhd) =
6.854 - input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
6.855 - Find ["maximum A", "valuesFor [a,b]"],
6.856 - Relate ["relations [A=a*b, \
6.857 - \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
6.858 - Pbl, e_spec);
6.859 - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
6.860 -
6.861 - modifycalcheadOK2xml 111 (bool2str b) ocalhd;
6.862 -*)
6.863 -DEconstrCalcTree 1;
6.864 -
6.865 -\<close> ML \<open>
6.866 -"--------- syntax error ------------------------------------------";
6.867 -"--------- syntax error ------------------------------------------";
6.868 -"--------- syntax error ------------------------------------------";
6.869 - reset_states ();
6.870 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.871 - ("Test", ["sqroot-test","univariate","equation","test"],
6.872 - ["Test","squ-equ-test-subpbl1"]))];
6.873 - Iterator 1; moveActiveRoot 1;
6.874 - autoCalculate 1 CompleteCalcHead;
6.875 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.876 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.877 -
6.878 - appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
6.879 - val ((pt,_),_) = get_calc 1;
6.880 - val str = pr_ctree pr_short pt;
6.881 - writeln str;
6.882 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
6.883 - else error "inform.sml: diff.behav.appendFormula: syntax error";
6.884 -DEconstrCalcTree 1;
6.885 -
6.886 -\<close> ML \<open>
6.887 -"--------- CAS-command on ([],Pbl) -------------------------------";
6.888 -"--------- CAS-command on ([],Pbl) -------------------------------";
6.889 -"--------- CAS-command on ([],Pbl) -------------------------------";
6.890 -val (p,_,f,nxt,_,pt) =
6.891 - CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
6.892 -val ifo = "solve(x+1=2,x)";
6.893 -val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
6.894 -show_pt pt;
6.895 -val nxt = (Apply_Method ["Test","squ-equ-test-subpbl1"]);
6.896 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.897 -if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
6.898 -else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
6.899 -DEconstrCalcTree 1;
6.900 -
6.901 -\<close> ML \<open>
6.902 -"--------- CAS-command on ([],Pbl) FE-interface ------------------";
6.903 -"--------- CAS-command on ([],Pbl) FE-interface ------------------";
6.904 -"--------- CAS-command on ([],Pbl) FE-interface ------------------";
6.905 -reset_states ();
6.906 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
6.907 -Iterator 1;
6.908 -moveActiveRoot 1;
6.909 -replaceFormula 1 "solve(x+1=2,x)";
6.910 -autoCalculate 1 CompleteCalc;
6.911 -val ((pt,p),_) = get_calc 1;
6.912 -show_pt pt;
6.913 -if p = ([], Res) then ()
6.914 -else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
6.915 -DEconstrCalcTree 1;
6.916 -
6.917 -\<close> ML \<open>
6.918 -"--------- inform [rational,simplification] ----------------------";
6.919 -"--------- inform [rational,simplification] ----------------------";
6.920 -"--------- inform [rational,simplification] ----------------------";
6.921 -reset_states ();
6.922 -CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
6.923 - ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
6.924 -Iterator 1; moveActiveRoot 1;
6.925 -autoCalculate 1 CompleteCalcHead;
6.926 -
6.927 -"--- (-1) give a preview on the calculation without any input";
6.928 -(*
6.929 -autoCalculate 1 CompleteCalc;
6.930 -val ((pt, p), _) = get_calc 1;
6.931 -show_pt pt;
6.932 -[
6.933 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
6.934 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
6.935 -(([1], Res), a / b + c / d + e / f), <--- (1) input arbitrary
6.936 -(([2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.937 -(([3], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
6.938 -(([4], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)), <--- (2) input next
6.939 -(([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))] <--- (3) is also final result
6.940 - EXAMPLE NOT OPTIMAL
6.941 -*)
6.942 -"--- (0) user input as the *first* step does not work, thus impdo at least 1 step";
6.943 -autoCalculate 1 (Steps 1);
6.944 -autoCalculate 1 (Steps 1);
6.945 -val ((pt, p), _) = get_calc 1;
6.946 -(*show_pt pt;
6.947 -[
6.948 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
6.949 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
6.950 -(([1], Res), a / b + c / d + e / f)]
6.951 -*)
6.952 -"--- (1) input an arbitrary next formula";
6.953 -appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*);
6.954 -val ((pt, p), _) = get_calc 1;
6.955 -(*show_pt pt;
6.956 -[
6.957 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
6.958 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
6.959 -(([1], Res), a / b + c / d + e / f),
6.960 -(([2,1], Frm), a / b + c / d + e / f),
6.961 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.962 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
6.963 -(([2], Res), (a * d + c * b) / (b * d) + e / f)]
6.964 -*)
6.965 -val ((pt,p),_) = get_calc 1;
6.966 -if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
6.967 -else error ("inform.sml: [rational,simplification] 1");
6.968 -
6.969 -"--- (2) input the next formula that would be presented by mat-engine";
6.970 -(* generate a preview:
6.971 -autoCalculate 1 (Steps 1);
6.972 -val ((pt, p), _) = get_calc 1;
6.973 -show_pt pt;
6.974 -[
6.975 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
6.976 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
6.977 -(([1], Res), a / b + c / d + e / f),
6.978 -(([2,1], Frm), a / b + c / d + e / f),
6.979 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.980 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
6.981 -(([2], Res), (a * d + c * b) / (b * d) + e / f),
6.982 -(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this
6.983 -*)
6.984 -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
6.985 -val ((pt, p), _) = get_calc 1;
6.986 -(*show_pt pt;
6.987 -[
6.988 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
6.989 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
6.990 -(([1], Res), a / b + c / d + e / f),
6.991 -(([2,1], Frm), a / b + c / d + e / f),
6.992 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.993 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
6.994 -(([2], Res), (a * d + c * b) / (b * d) + e / f),
6.995 -(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]
6.996 -*)
6.997 -if p = ([3], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
6.998 -else error ("inform.sml: [rational,simplification] 2");
6.999 -
6.1000 -"--- (3) input the exact final result";
6.1001 -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
6.1002 -val ((pt, p), _) = get_calc 1;
6.1003 -(*show_pt pt;
6.1004 -[
6.1005 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
6.1006 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
6.1007 -(([1], Res), a / b + c / d + e / f),
6.1008 -(([2,1], Frm), a / b + c / d + e / f),
6.1009 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1010 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
6.1011 -(([2], Res), (a * d + c * b) / (b * d) + e / f),
6.1012 -(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1013 -(([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1014 -(([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
6.1015 -(([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1016 -(([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]
6.1017 -*)
6.1018 -if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
6.1019 -else error ("inform.sml: [rational,simplification] 3");
6.1020 -
6.1021 -"--- (4) finish the calculation + check the postcondition (in the future)";
6.1022 -autoCalculate 1 CompleteCalc;
6.1023 -val ((pt, p), _) = get_calc 1;
6.1024 -val (t, asm) = get_obj g_result pt [];
6.1025 -if term2str t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
6.1026 -terms2str asm = "[\"b * d * f \<noteq> 0\",\"d \<noteq> 0\",\"b \<noteq> 0\",\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"
6.1027 -then () else error "inform [rational,simplification] changed at end";
6.1028 -(*show_pt pt;
6.1029 -[
6.1030 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
6.1031 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
6.1032 -(([1], Res), a / b + c / d + e / f),
6.1033 -(([2,1], Frm), a / b + c / d + e / f),
6.1034 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1035 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
6.1036 -(([2], Res), (a * d + c * b) / (b * d) + e / f),
6.1037 -(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1038 -(([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1039 -(([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
6.1040 -(([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1041 -(([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
6.1042 -(([5], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
6.1043 -(([6], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)),
6.1044 -(([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))]
6.1045 -*)
6.1046 -DEconstrCalcTree 1;
6.1047 -
6.1048 -\<close> ML \<open>
6.1049 -"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
6.1050 -"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
6.1051 -"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
6.1052 -val t = str2term "Diff (x^^^2 + x + 1, x)";
6.1053 -case t of Const ("Diff.Diff", _) $ _ => ()
6.1054 - | _ => raise
6.1055 - error "diff.sml behav.changed for CAS Diff (..., x)";
6.1056 -atomty t;
6.1057 -"-----------------------------------------------------------------";
6.1058 -(*1>*)reset_states ();
6.1059 -(*2>*)CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
6.1060 -(*3>*)Iterator 1;moveActiveRoot 1;
6.1061 -"----- here the Headline has been finished";
6.1062 -(*4>*)moveActiveFormula 1 ([],Pbl);
6.1063 -(*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";
6.1064 -val ((pt,_),_) = get_calc 1;
6.1065 -val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
6.1066 -val NONE = env;
6.1067 -val (SOME istate, NONE) = loc;
6.1068 -(*default_print_depth 5;*)
6.1069 -writeln"-----------------------------------------------------------";
6.1070 -spec;
6.1071 -writeln (itms2str_ ctxt probl);
6.1072 -writeln (itms2str_ ctxt meth);
6.1073 -writeln (istate2str (fst istate));
6.1074 -
6.1075 -refFormula 1 ([],Pbl) (*--> correct CalcHead*);
6.1076 - (*081016 NOT necessary (but leave it in Java):*)
6.1077 -(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
6.1078 -"----- here the CalcHead has been completed --- ONCE MORE ?????";
6.1079 -
6.1080 -(***difference II***)
6.1081 -val ((pt,p),_) = get_calc 1;
6.1082 -(*val p = ([], Pbl)*)
6.1083 -val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
6.1084 -val NONE = env;
6.1085 -val (SOME istate, NONE) = loc;
6.1086 -(*default_print_depth 5;*) writeln (istate2str (fst istate)); (*default_print_depth 3;*)
6.1087 -(*Pstate ([],
6.1088 - [], NONE,
6.1089 - ??.empty, Sundef, false)*)
6.1090 -(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
6.1091 -(*("Isac_Knowledge",
6.1092 - ["derivative_of", "function"],
6.1093 - ["diff", "differentiate_on_R"]) : spec*)
6.1094 -writeln (itms2str_ ctxt probl);
6.1095 -(*[
6.1096 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
6.1097 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
6.1098 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
6.1099 -writeln (itms2str_ ctxt meth);
6.1100 -(*[
6.1101 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
6.1102 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
6.1103 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
6.1104 -writeln"-----------------------------------------------------------";
6.1105 -(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
6.1106 -(*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
6.1107 -autoCalculate 1 CompleteCalc;
6.1108 -val ((pt,p),_) = get_calc 1;
6.1109 -val Form res = (#1 o pt_extract) (pt, ([],Res));
6.1110 -show_pt pt;
6.1111 -if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
6.1112 -else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
6.1113 -DEconstrCalcTree 1;
6.1114 -
6.1115 -\<close> ML \<open>
6.1116 -"--------- Take as 1st tac, start from exp -----------------------";
6.1117 -"--------- Take as 1st tac, start from exp -----------------------";
6.1118 -"--------- Take as 1st tac, start from exp -----------------------";
6.1119 -(*the following input is copied from BridgeLog Java <==> SML,
6.1120 - omitting unnecessary inputs*)
6.1121 -(*1>*)reset_states ();
6.1122 -(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of","function"],["diff","differentiate_on_R"]))];
6.1123 -(*3>*)Iterator 1; moveActiveRoot 1;
6.1124 -
6.1125 -(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
6.1126 -(***difference II***)
6.1127 -val ((pt,_),_) = get_calc 1;
6.1128 -val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
6.1129 -val NONE = env;
6.1130 -val (SOME istate, NONE) = loc;
6.1131 -(*default_print_depth 5;*) writeln (istate2str (fst istate)); (*default_print_depth 3;*)
6.1132 -(*Pstate ([],
6.1133 - [], NONE,
6.1134 - ??.empty, Sundef, false)*)
6.1135 -(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
6.1136 -(*("Isac_Knowledge",
6.1137 - ["derivative_of", "function"],
6.1138 - ["diff", "differentiate_on_R"]) : spec*)
6.1139 -writeln (itms2str_ ctxt probl);
6.1140 -(*[
6.1141 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
6.1142 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
6.1143 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
6.1144 -writeln (itms2str_ ctxt meth);
6.1145 -(*[
6.1146 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
6.1147 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
6.1148 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
6.1149 -writeln"-----------------------------------------------------------";
6.1150 -(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
6.1151 -autoCalculate 1 (Steps 1);
6.1152 -val ((pt,p),_) = get_calc 1;
6.1153 -val Form res = (#1 o pt_extract) (pt, p);
6.1154 -if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
6.1155 -else error "diff.sml Diff (x^2 + x + 1, x) from exp";
6.1156 -DEconstrCalcTree 1;
6.1157 -
6.1158 -\<close> ML \<open>
6.1159 -"--------- init_form, start with <NEW> (CAS input) ---------------";
6.1160 -"--------- init_form, start with <NEW> (CAS input) ---------------";
6.1161 -"--------- init_form, start with <NEW> (CAS input) ---------------";
6.1162 -reset_states ();
6.1163 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
6.1164 -(*[[from sml: > @@@@@begin@@@@@
6.1165 -[[from sml: 1
6.1166 -[[from sml: <CALCTREE>
6.1167 -[[from sml: <CALCID> 1 </CALCID>
6.1168 -[[from sml: </CALCTREE>
6.1169 -[[from sml: @@@@@end@@@@@*)
6.1170 -Iterator 1;
6.1171 -(*[[from sml: > @@@@@begin@@@@@
6.1172 -[[from sml: 1
6.1173 -[[from sml: <ADDUSER>
6.1174 -[[from sml: <CALCID> 1 </CALCID>
6.1175 -[[from sml: <USERID> 1 </USERID>
6.1176 -[[from sml: </ADDUSER>
6.1177 -[[from sml: @@@@@end@@@@@*)
6.1178 -moveActiveRoot 1;
6.1179 -(*[[from sml: > @@@@@begin@@@@@
6.1180 -[[from sml: 1
6.1181 -[[from sml: <CALCITERATOR>
6.1182 -[[from sml: <CALCID> 1 </CALCID>
6.1183 -[[from sml: <POSITION>
6.1184 -[[from sml: <INTLIST>
6.1185 -[[from sml: </INTLIST>
6.1186 -[[from sml: <POS> Pbl </POS>
6.1187 -[[from sml: </POSITION>
6.1188 -[[from sml: </CALCITERATOR>
6.1189 -[[from sml: @@@@@end@@@@@*)
6.1190 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
6.1191 -(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
6.1192 -[[from sml: 1
6.1193 -[[from sml: <GETELEMENTSFROMTO>
6.1194 -[[from sml: <CALCID> 1 </CALCID>
6.1195 -[[from sml: <FORMHEADS>
6.1196 -[[from sml: <CALCFORMULA>
6.1197 -[[from sml: <POSITION>
6.1198 -[[from sml: <INTLIST>
6.1199 -[[from sml: </INTLIST>
6.1200 -[[from sml: <POS> Pbl </POS>
6.1201 -[[from sml: </POSITION>
6.1202 -[[from sml: <FORMULA>
6.1203 -[[from sml: <MATHML>
6.1204 -[[from sml: <ISA> ________________________________________________ </ISA>
6.1205 -[[from sml: </MATHML>
6.1206 -[[from sml:
6.1207 -[[from sml: </FORMULA>
6.1208 -[[from sml: </CALCFORMULA>
6.1209 -[[from sml: </FORMHEADS>
6.1210 -[[from sml: </GETELEMENTSFROMTO>
6.1211 -[[from sml: @@@@@end@@@@@*)
6.1212 -refFormula 1 ([],Pbl);
6.1213 -(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
6.1214 -[[from sml: 1
6.1215 -[[from sml: <REFFORMULA>
6.1216 -[[from sml: <CALCID> 1 </CALCID>
6.1217 -[[from sml: <CALCHEAD status = "incorrect">
6.1218 -[[from sml: <POSITION>
6.1219 -[[from sml: <INTLIST>
6.1220 -[[from sml: </INTLIST>
6.1221 -[[from sml: <POS> Pbl </POS>
6.1222 -[[from sml: </POSITION>
6.1223 -[[from sml: <HEAD>
6.1224 -[[from sml: <MATHML>
6.1225 -[[from sml: <ISA> Problem (e_domID, [e_pblID]) </ISA>
6.1226 -[[from sml: </MATHML>
6.1227 -[[from sml: </HEAD>
6.1228 -[[from sml: <MODEL>
6.1229 -[[from sml: <GIVEN> </GIVEN>
6.1230 -[[from sml: <WHERE> </WHERE>
6.1231 -[[from sml: <FIND> </FIND>
6.1232 -[[from sml: <RELATE> </RELATE>
6.1233 -[[from sml: </MODEL>
6.1234 -[[from sml: <BELONGSTO> Pbl </BELONGSTO>
6.1235 -[[from sml: <SPECIFICATION>
6.1236 -[[from sml: <THEORYID> e_domID </THEORYID>
6.1237 -[[from sml: <PROBLEMID>
6.1238 -[[from sml: <STRINGLIST>
6.1239 -[[from sml: <STRING> e_pblID </STRING>
6.1240 -[[from sml: </STRINGLIST>
6.1241 -[[from sml: </PROBLEMID>
6.1242 -[[from sml: <METHODID>
6.1243 -[[from sml: <STRINGLIST>
6.1244 -[[from sml: <STRING> e_metID </STRING>
6.1245 -[[from sml: </STRINGLIST>
6.1246 -[[from sml: </METHODID>
6.1247 -[[from sml: </SPECIFICATION>
6.1248 -[[from sml: </CALCHEAD>
6.1249 -[[from sml: </REFFORMULA>
6.1250 -[[from sml: @@@@@end@@@@@*)
6.1251 -moveActiveFormula 1 ([],Pbl);
6.1252 -(*[[from sml: > @@@@@begin@@@@@
6.1253 -[[from sml: 1
6.1254 -[[from sml: <CALCITERATOR>
6.1255 -[[from sml: <CALCID> 1 </CALCID>
6.1256 -[[from sml: <POSITION>
6.1257 -[[from sml: <INTLIST>
6.1258 -[[from sml: </INTLIST>
6.1259 -[[from sml: <POS> Pbl </POS>
6.1260 -[[from sml: </POSITION>
6.1261 -[[from sml: </CALCITERATOR>
6.1262 -[[from sml: @@@@@end@@@@@*)
6.1263 -replaceFormula 1 "Simplify (1+2)";
6.1264 -(*[[from sml: > @@@@@begin@@@@@
6.1265 -[[from sml: 1
6.1266 -[[from sml: <REPLACEFORMULA>
6.1267 -[[from sml: <CALCID> 1 </CALCID>
6.1268 -[[from sml: <CALCCHANGED>
6.1269 -[[from sml: <UNCHANGED>
6.1270 -[[from sml: <INTLIST>
6.1271 -[[from sml: </INTLIST>
6.1272 -[[from sml: <POS> Pbl </POS>
6.1273 -[[from sml: </UNCHANGED>
6.1274 -[[from sml: <DELETED>
6.1275 -[[from sml: <INTLIST>
6.1276 -[[from sml: </INTLIST>
6.1277 -[[from sml: <POS> Pbl </POS>
6.1278 -[[from sml: </DELETED>
6.1279 -[[from sml: <GENERATED>
6.1280 -[[from sml: <INTLIST>
6.1281 -[[from sml: </INTLIST>
6.1282 -[[from sml: <POS> Met </POS> DIFFERENCE: Pbl
6.1283 -[[from sml: </GENERATED>
6.1284 -[[from sml: </CALCCHANGED>
6.1285 -[[from sml: </REPLACEFORMULA>
6.1286 -[[from sml: @@@@@end@@@@@*)
6.1287 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(* DIFFERENCE: Pbl*);
6.1288 -(*@@@@@begin@@@@@
6.1289 - 1
6.1290 -<GETELEMENTSFROMTO>
6.1291 - <CALCID> 1 </CALCID>
6.1292 - <FORMHEADS>
6.1293 - <CALCFORMULA>
6.1294 - <POSITION>
6.1295 - <INTLIST>
6.1296 - </INTLIST>
6.1297 - <POS> Pbl </POS>
6.1298 - </POSITION>
6.1299 - <FORMULA>
6.1300 - <MATHML>
6.1301 - <ISA> Simplify (1 + 2) </ISA> WORKS !!!!!
6.1302 - </MATHML>
6.1303 - </FORMULA>
6.1304 - </CALCFORMULA>
6.1305 - </FORMHEADS>
6.1306 -</GETELEMENTSFROMTO>
6.1307 -@@@@@end@@@@@*)
6.1308 -getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;
6.1309 -(*[[from sml: > @@@@@begin@@@@@
6.1310 -[[from sml: 1
6.1311 -[[from sml: <SYSERROR>
6.1312 -[[from sml: <CALCID> 1 </CALCID>
6.1313 -[[from sml: <ERROR> error in getFormulaeFromTo </ERROR>
6.1314 -[[from sml: </SYSERROR>
6.1315 -[[from sml: @@@@@end@@@@@*)
6.1316 -(*step into getFormulaeFromTo --- bug corrected...*)
6.1317 -
6.1318 -\<close> ML \<open>
6.1319 -"--------- build fun check_err_patt ------------------------------";
6.1320 -"--------- build fun check_err_patt ------------------------------";
6.1321 -"--------- build fun check_err_patt ------------------------------";
6.1322 -val subst = [(str2term "bdv", str2term "x")]: subst;
6.1323 -val rls = norm_Rational
6.1324 -val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
6.1325 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
6.1326 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
6.1327 -
6.1328 -val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
6.1329 - rew_sub thy 1 [] e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) res;
6.1330 -if rewritten then NONE else SOME "e_errpatID";
6.1331 -
6.1332 -val norm_res = case rewrite_set_ (Isac()) false rls res' of
6.1333 - NONE => res'
6.1334 -| SOME (norm_res, _) => norm_res
6.1335 -
6.1336 -val norm_inf = case rewrite_set_ (Isac()) false rls inf of
6.1337 - NONE => inf
6.1338 -| SOME (norm_inf, _) => norm_inf;
6.1339 -
6.1340 -res' = inf;
6.1341 -norm_res = norm_inf;
6.1342 -
6.1343 -val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
6.1344 -val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
6.1345 -if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
6.1346 -then () else error "error patt example1 changed";
6.1347 -
6.1348 -val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
6.1349 -val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
6.1350 -if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
6.1351 -then () else error "error patt example2 changed";
6.1352 -
6.1353 -val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
6.1354 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
6.1355 -if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
6.1356 -then () else error "error patt example3 changed";
6.1357 -
6.1358 -val inf = str2term "1 / 2";
6.1359 -if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
6.1360 -then () else error "error patt example3 changed";
6.1361 -
6.1362 -"--------- build fun check_err_patt ?bdv -------------------------";
6.1363 -"--------- build fun check_err_patt ?bdv -------------------------";
6.1364 -"--------- build fun check_err_patt ?bdv -------------------------";
6.1365 -val subst = [(str2term "bdv", str2term "x")]: subst;
6.1366 -val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
6.1367 -val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
6.1368 -if term2str t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
6.1369 -else error "build fun check_err_patt ?bdv changed 1";
6.1370 -
6.1371 -val rls = norm_diff
6.1372 -val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
6.1373 -val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
6.1374 -
6.1375 -val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
6.1376 - rew_sub thy 1 subst e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) res;
6.1377 -if term2str res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
6.1378 -else error "build fun check_err_patt ?bdv changed 2";
6.1379 -
6.1380 -val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
6.1381 - NONE => res'
6.1382 -| SOME (norm_res, _) => norm_res;
6.1383 -if term2str norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()
6.1384 -else error "build fun check_err_patt ?bdv changed 3";
6.1385 -
6.1386 -val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
6.1387 - NONE => inf
6.1388 -| SOME (norm_inf, _) => norm_inf;
6.1389 -if term2str norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()
6.1390 -else error "build fun check_err_patt ?bdv changed 4";
6.1391 -
6.1392 -res' = inf;
6.1393 -if norm_res = norm_inf then ()
6.1394 -else error "build fun check_err_patt ?bdv changed 5";
6.1395 -
6.1396 -if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
6.1397 -then () else error "error patt example1 changed";
6.1398 -
6.1399 -"--------- build fun check_error_patterns ------------------------";
6.1400 -"--------- build fun check_error_patterns ------------------------";
6.1401 -"--------- build fun check_error_patterns ------------------------";
6.1402 -val (res, inf) =
6.1403 - (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
6.1404 - str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
6.1405 -val {errpats, nrls = rls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
6.1406 -
6.1407 -val env = [(str2term "v_v", str2term "x")];
6.1408 -val errpats =
6.1409 - [e_errpat, (*generalised for testing*)
6.1410 - ("chain-rule-diff-both",
6.1411 - [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
6.1412 - parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
6.1413 - parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
6.1414 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
6.1415 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
6.1416 - [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
6.1417 - @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
6.1418 -case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
6.1419 -| NONE => error "check_error_patterns broken";
6.1420 -DEconstrCalcTree 1;
6.1421 -
6.1422 -"--------- embed fun check_error_patterns ------------------------";
6.1423 -"--------- embed fun check_error_patterns ------------------------";
6.1424 -"--------- embed fun check_error_patterns ------------------------";
6.1425 -reset_states ();
6.1426 -CalcTree
6.1427 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
6.1428 - ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
6.1429 -Iterator 1;
6.1430 -moveActiveRoot 1;
6.1431 -autoCalculate 1 CompleteCalcHead;
6.1432 -autoCalculate 1 (Steps 1);
6.1433 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.1434 -(*autoCalculate 1 (Steps 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
6.1435 -
6.1436 -"~~~~~ fun appendFormula , args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
6.1437 -"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: Rule.cterm')) = (cI, ifo);
6.1438 - val cs = get_calc cI
6.1439 - val pos = get_pos cI 1;
6.1440 -(*+*)if pos = ([1], Res) then () else error "inform with (positive) check_error_patterns broken 1";
6.1441 - val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
6.1442 - (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
6.1443 -"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
6.1444 - = (cs', (encode ifo));
6.1445 - val ctxt = get_ctxt pt pos (*see TODO.thy*)
6.1446 - val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr (*of*);
6.1447 - val f_in = Thm.term_of f_in
6.1448 - val pos_pred = lev_back' pos
6.1449 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
6.1450 - (*if*) f_pred = f_in; (*else*)
6.1451 - val NONE = (*case*) Inform.cas_input f_in (*of*);
6.1452 - (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
6.1453 - (*old*)val {scr = prog, ...} = Specify.get_met metID
6.1454 - (*old*)val istate = get_istate_LI pt pos
6.1455 - (*old*)val ctxt = get_ctxt pt pos
6.1456 - ( *old*)
6.1457 - val LI.Not_Derivable =
6.1458 - (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
6.1459 - val pp = Ctree.par_pblobj pt p
6.1460 - val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
6.1461 - {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
6.1462 - | _ => error "inform: uncovered case of get_met"
6.1463 -;
6.1464 -(*+*)if errpats2str 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)\",\"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\",\"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\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\",\"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\",\"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]"
6.1465 -(*+*)then () else error "inform with (positive) check_error_patterns broken 3";
6.1466 -
6.1467 - val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
6.1468 -;
6.1469 -(*+*)if term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
6.1470 -(*+*) term2str f_in = "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)"
6.1471 -(*+*)then () else error "inform with (positive) check_error_patterns broken 2";
6.1472 -
6.1473 - val SOME "chain-rule-diff-both" = (*case*) Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
6.1474 -
6.1475 -"--- final check:";
6.1476 -(*+*)val (_, _, ptp') = cs';
6.1477 -case Step_Solve.by_term ptp' (encode ifo) of
6.1478 - ("error pattern #chain-rule-diff-both#", calcstate') => ()
6.1479 -| _ => error "inform with (positive) check_error_patterns broken"
6.1480 -
6.1481 -
6.1482 -"--------- embed fun find_fillpatterns ---------------------------";
6.1483 -"--------- embed fun find_fillpatterns ---------------------------";
6.1484 -"--------- embed fun find_fillpatterns ---------------------------";
6.1485 -reset_states ();
6.1486 -CalcTree
6.1487 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
6.1488 - ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
6.1489 -Iterator 1;
6.1490 -moveActiveRoot 1;
6.1491 -autoCalculate 1 CompleteCalcHead;
6.1492 -autoCalculate 1 (Steps 1);
6.1493 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.1494 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
6.1495 - (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
6.1496 - (*or
6.1497 - <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
6.1498 -
6.1499 -"~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
6.1500 - val ((pt, _), _) = get_calc cI
6.1501 - val pos = get_pos cI 1;
6.1502 -"~~~~~ fun find_fillpatterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
6.1503 - val f_curr = Ctree.get_curr_formula (pt, pos);
6.1504 - val pp = Ctree.par_pblobj pt p
6.1505 - val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
6.1506 - {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
6.1507 - | _ => error "find_fillpatterns: uncovered case of get_met"
6.1508 - val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
6.1509 - val subst = Rtools.get_bdv_subst prog env
6.1510 - val errpatthms = errpats
6.1511 - |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
6.1512 - |> map (#3: errpat -> thm list)
6.1513 - |> flat;
6.1514 -
6.1515 -case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of
6.1516 - ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if term2str tm =
6.1517 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
6.1518 - then () else error "find_fillpatterns changed 1a"
6.1519 -| _ => error "find_fillpatterns changed 1b"
6.1520 -
6.1521 -"~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
6.1522 - (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
6.1523 - val thmDeriv = Thm.get_name_hint thm
6.1524 - val (part, thyID) = thy_containing_thm thmDeriv
6.1525 - val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
6.1526 - val Hthm {fillpats, ...} = get_the theID
6.1527 - val some = map (get_fillform subst (thm, form) errpatID) fillpats;
6.1528 -
6.1529 -case some |> filter is_some |> map the of
6.1530 - ("fill-d_d-arg", tm, thm, subsopt) :: _ => if term2str tm =
6.1531 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
6.1532 - then () else error "find_fillpatterns changed 2a"
6.1533 -| _ => error "find_fillpatterns changed 2b"
6.1534 -
6.1535 -"~~~~~ fun get_fillform, args:";
6.1536 - val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
6.1537 - (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
6.1538 -val (form', _, _, rewritten) =
6.1539 - rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) form;
6.1540 -
6.1541 -if term2str form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
6.1542 -else error "find_fillpatterns changed 3";
6.1543 -
6.1544 -"~~~~~ to findFillpatterns return val:"; val (fillpats) =
6.1545 - (map (get_fillpats (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
6.1546 -
6.1547 -"vvv--- dropped this code WN120730";
6.1548 -val msg = "fill patterns " ^
6.1549 - ((map ((apsnd term2str) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
6.1550 -msg =
6.1551 - "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
6.1552 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
6.1553 - "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
6.1554 - " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
6.1555 - "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
6.1556 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^
6.1557 - "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
6.1558 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^
6.1559 - "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#";
6.1560 -"^^^--- dropped this code WN120730";
6.1561 -
6.1562 -if (map #1 fillpats) =
6.1563 - ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
6.1564 -then () else error "find_fillpatterns changed 4b";
6.1565 -DEconstrCalcTree 1;
6.1566 -
6.1567 -"--------- build fun is_exactly_equal, inputFillFormula ----------";
6.1568 -"--------- build fun is_exactly_equal, inputFillFormula ----------";
6.1569 -"--------- build fun is_exactly_equal, inputFillFormula ----------";
6.1570 -reset_states ();
6.1571 -CalcTree
6.1572 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
6.1573 - ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
6.1574 -Iterator 1;
6.1575 -moveActiveRoot 1;
6.1576 -autoCalculate 1 CompleteCalcHead;
6.1577 -autoCalculate 1 (Steps 1);
6.1578 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.1579 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
6.1580 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
6.1581 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
6.1582 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
6.1583 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
6.1584 - val ((pt,pos), _) = get_calc 1;
6.1585 - val p = get_pos 1 1;
6.1586 - val (Form f, _, asms) = pt_extract (pt, p);
6.1587 -
6.1588 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
6.1589 - case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.1590 - ("diff_sum", thm)) =>
6.1591 - if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
6.1592 - else error "embed fun get_fillform changed 11"
6.1593 - | _ => error "embed fun get_fillform changed 12"
6.1594 - else error "embed fun get_fillform changed 13";
6.1595 -
6.1596 -findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
6.1597 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
6.1598 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
6.1599 - val ((pt,pos),_) = get_calc 1;
6.1600 - val p = get_pos 1 1;
6.1601 -
6.1602 - val (Form f, _, asms) = pt_extract (pt, p);
6.1603 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
6.1604 - case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.1605 - ("diff_sum", thm)) =>
6.1606 - if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
6.1607 - else error "embed fun get_fillform changed 21"
6.1608 - | _ => error "embed fun get_fillform changed 22"
6.1609 - else error "embed fun get_fillform changed 23";
6.1610 -
6.1611 -requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
6.1612 - (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
6.1613 - val ((pt,pos),_) = get_calc 1;
6.1614 - val p = get_pos 1 1;
6.1615 - val (Form f, _, asms) = pt_extract (pt, p);
6.1616 - if p = ([1], Res) andalso existpt [2] pt
6.1617 - andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
6.1618 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.1619 - ("diff_sum", thm)) =>
6.1620 - if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
6.1621 - else error "embed fun get_fillform changed 31"
6.1622 - | _ => error "embed fun get_fillform changed 32"
6.1623 - else error "embed fun get_fillform changed 33";
6.1624 -
6.1625 -(* input a formula which exactly fills the gaps in a "fillformula"
6.1626 - presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
6.1627 - errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
6.1628 - the respective thm is in the ctree ................
6.1629 -*)
6.1630 -"~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
6.1631 - (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)");
6.1632 - val ((pt, _), _) = get_calc cI
6.1633 - val pos = get_pos cI 1;
6.1634 -
6.1635 -"~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
6.1636 - val SOME ifo = parseNEW (assoc_thy "Isac_Knowledge" |> thy2ctxt) istr
6.1637 - val p' = lev_on p;
6.1638 - val tac = get_obj g_tac pt p';
6.1639 -val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
6.1640 -if (term2str o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
6.1641 -else error "inputFillFormula changed 10";
6.1642 - val Appl rew = applicable_in pos pt tac;
6.1643 - val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
6.1644 -
6.1645 -"~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
6.1646 - val ("ok", (_, c, ptp as (_,p'))) = Step.by_tactic tac (pt, pos);
6.1647 - upd_calc cI (ptp, []);
6.1648 - upd_ipos cI 1 p';
6.1649 - autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
6.1650 -
6.1651 -"~~~~~ final check:";
6.1652 -val ((pt, _),_) = get_calc 1;
6.1653 -val p = get_pos 1 1;
6.1654 -val (Form f, _, asms) = pt_extract (pt, p);
6.1655 - if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"
6.1656 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
6.1657 - ("diff_sin_chain", thm)) =>
6.1658 - if (term2str o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
6.1659 - else error "inputFillFormula changed 111"
6.1660 - | _ => error "inputFillFormula changed 112"
6.1661 - else error "inputFillFormula changed 113";
6.1662 -
6.1663 -"--------- fun appl_adds -----------------------------------------";
6.1664 -"--------- fun appl_adds -----------------------------------------";
6.1665 -"--------- fun appl_adds -----------------------------------------";
6.1666 -(* val (dI, oris, ppc, pbt, selct::ss) =
6.1667 - (dI, pors, probl, ppc, map itms2fstr probl);
6.1668 - ...vvv
6.1669 - *)
6.1670 -(* val (dI, oris, ppc, pbt, (selct::ss))=
6.1671 - (#1 (some_spec ospec spec), oris, []:itm list,
6.1672 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
6.1673 - val iii = appl_adds dI oris ppc pbt (selct::ss);
6.1674 - tracing(itms2str_ thy iii);
6.1675 -
6.1676 - val itm = appl_add' dI oris ppc pbt selct;
6.1677 - val ppc = insert_ppc' itm ppc;
6.1678 -
6.1679 - val _::selct::ss = (selct::ss);
6.1680 - val itm = appl_add' dI oris ppc pbt selct;
6.1681 - val ppc = insert_ppc' itm ppc;
6.1682 -
6.1683 - val _::selct::ss = (selct::ss);
6.1684 - val itm = appl_add' dI oris ppc pbt selct;
6.1685 - val ppc = insert_ppc' itm ppc;
6.1686 - tracing(itms2str_ thy ppc);
6.1687 -
6.1688 - val _::selct::ss = (selct::ss);
6.1689 - val itm = appl_add' dI oris ppc pbt selct;
6.1690 - val ppc = insert_ppc' itm ppc;
6.1691 - *)
6.1692 -"--------- fun concat_deriv --------------------------------------";
6.1693 -"--------- fun concat_deriv --------------------------------------";
6.1694 -"--------- fun concat_deriv --------------------------------------";
6.1695 -(*
6.1696 - val ({rew_ord, erls, rules,...}, fo, ifo) =
6.1697 - (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
6.1698 - (tracing o trtas2str) fod';
6.1699 -> ["
6.1700 -(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
6.1701 -(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
6.1702 -(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
6.1703 -(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
6.1704 -val it = () : unit
6.1705 - (tracing o trtas2str) (map rev_deriv' rifod');
6.1706 -> ["
6.1707 -(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
6.1708 -(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
6.1709 -(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
6.1710 -val it = () : unit
6.1711 -*)
6.1712 -"--------- handle an input formula -------------------------------";
6.1713 -"--------- handle an input formula -------------------------------";
6.1714 -"--------- handle an input formula -------------------------------";
6.1715 -(*
6.1716 -Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
6.1717 -Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
6.1718 -wenn Abteilungen nur auf gleichem Level gesucht werden ?
6.1719 -WN.040216
6.1720 -
6.1721 -Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
6.1722 -
6.1723 -------------------------------------------------------------------------------
6.1724 -"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
6.1725 -------------------------------------------------------------------------------
6.1726 -1. "5 * x / (x - 2) - x / (x + 2) = 4"
6.1727 -...
6.1728 -4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalise", "poly"..
6.1729 -...
6.1730 -4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
6.1731 -...
6.1732 -4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
6.1733 -...
6.1734 -"[x = -4 / 3]"
6.1735 -------------------------------------------------------------------------------
6.1736 -(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
6.1737 -
6.1738 -(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
6.1739 -------------------------------------------------------------------------------
6.1740 -
6.1741 -
6.1742 -------------------------------------------------------------------------------
6.1743 -"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
6.1744 -------------------------------------------------------------------------------
6.1745 -1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
6.1746 -...
6.1747 -4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
6.1748 - Subproblem["normalise", "polynomial", "univariate"..
6.1749 -...
6.1750 -4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
6.1751 -...
6.1752 -4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
6.1753 -4.4.5. "[x = 0, x = 6 / 5]"
6.1754 -...
6.1755 -5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
6.1756 - "[x = 6 / 5]"
6.1757 -------------------------------------------------------------------------------
6.1758 -(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
6.1759 -
6.1760 -(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
6.1761 -------------------------------------------------------------------------------
6.1762 -
6.1763 -
6.1764 -------------------------------------------------------------------------------
6.1765 -"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
6.1766 -------------------------------------------------------------------------------
6.1767 -1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
6.1768 -...
6.1769 -6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
6.1770 - Subproblem["sq", "rootX", "univariate", "equation"]
6.1771 -...
6.1772 -6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
6.1773 - Subproblem["normalise", "polynomial", "univariate", "equation"]
6.1774 -...
6.1775 -6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
6.1776 -... Or_to_List
6.1777 -6.6.3.2 "UniversalList"
6.1778 -------------------------------------------------------------------------------
6.1779 -(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
6.1780 -
6.1781 -(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
6.1782 -------------------------------------------------------------------------------
6.1783 -*)
6.1784 -(*sh. comments auf 498*)
6.1785 -"--------- fun dropwhile' ----------------------------------------";
6.1786 -"--------- fun dropwhile' ----------------------------------------";
6.1787 -"--------- fun dropwhile' ----------------------------------------";
6.1788 -(*
6.1789 - fun equal a b = a=b;
6.1790 - val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
6.1791 - val r_foder = rev foder; val r_ifoder = rev ifoder;
6.1792 - dropwhile' equal r_foder r_ifoder;
6.1793 -> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
6.1794 -
6.1795 - val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
6.1796 - val r_foder = rev foder; val r_ifoder = rev ifoder;
6.1797 - dropwhile' equal r_foder r_ifoder;
6.1798 -> val it = ([3], [3, 12, 11]) : int list * int list
6.1799 -
6.1800 - val foder = [5]; val ifoder = [11,12,3,4,5];
6.1801 - val r_foder = rev foder; val r_ifoder = rev ifoder;
6.1802 - dropwhile' equal r_foder r_ifoder;
6.1803 -> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
6.1804 -
6.1805 - val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
6.1806 - val r_foder = rev foder; val r_ifoder = rev ifoder;
6.1807 - dropwhile' equal r_foder r_ifoder;
6.1808 -> *** dropwhile': did not start with equal elements*)
6.1809 -\<close> ML \<open>
6.1810 -\<close>
6.1811 -
6.1812 -section \<open>===================================================================================\<close>
6.1813 -ML \<open>
6.1814 -\<close> ML \<open>
6.1815 -\<close> ML \<open>
6.1816 -\<close>
6.1817 -
6.1818 section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>
6.1819 ML \<open>
6.1820 "~~~~~ fun xxx , args:"; val () = ();