1.1 --- a/test/Tools/isac/Interpret/inform.sml Sat Jul 26 13:39:00 2014 +0200
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Sat Jul 26 14:10:05 2014 +0200
1.3 @@ -1252,8 +1252,8 @@
1.4 val SOME ifo = parseNEW (assoc_thy "Isac" |> thy2ctxt) istr
1.5 val p' = lev_on p;
1.6 val tac = get_obj g_tac pt p';
1.7 - if tac = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) then ()
1.8 - else error "inputFillFormula changed 10";
1.9 +if tac = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
1.10 +then () else error "inputFillFormula changed 10";
1.11 val Appl rew = applicable_in pos pt tac;
1.12 val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
1.13
1.14 @@ -1269,6 +1269,7 @@
1.15 val (Form f, _, asms) = pt_extract (pt, p);
1.16 if p = ([2], Res) andalso
1.17 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
1.18 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
1.19 + get_obj g_tac pt (fst p) =
1.20 + Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
1.21 then () else error "inputFillFormula changed 11";
1.22
2.1 --- a/test/Tools/isac/Interpret/mathengine.sml Sat Jul 26 13:39:00 2014 +0200
2.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Sat Jul 26 14:10:05 2014 +0200
2.3 @@ -21,6 +21,7 @@
2.4 "----------- fun autoCalculate..CompleteCalc ------------";
2.5 "----------- search for Or_to_List ----------------------";
2.6 "----------- check thy in CalcTreeTEST ------------------";
2.7 +"----------- identified error in fun getTactic, string_of_thmI ---------------";
2.8 "--------------------------------------------------------";
2.9 "--------------------------------------------------------";
2.10 "--------------------------------------------------------";
2.11 @@ -559,3 +560,120 @@
2.12 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
2.13 val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
2.14
2.15 +"----------- identified error in fun getTactic, string_of_thmI ---------------";
2.16 +"----------- identified error in fun getTactic, string_of_thmI ---------------";
2.17 +"----------- identified error in fun getTactic, string_of_thmI ---------------";
2.18 +reset_states ();
2.19 +CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
2.20 + ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
2.21 +moveActiveRoot 1;
2.22 +autoCalculate' 1 CompleteCalcHead;
2.23 +autoCalculate' 1 (Step 1);
2.24 +autoCalculate' 1 (Step 1);
2.25 +autoCalculate' 1 (Step 1);
2.26 +getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
2.27 +interSteps 1 ([1],Res);
2.28 +"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
2.29 +val ((pt,p), tacis) = get_calc cI;
2.30 +(not o is_interpos) ip = false;
2.31 +val ip' = lev_pred' pt ip;
2.32 +"~~~~~ fun detailstep, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
2.33 +(* ^^^^^^^^^ not in test/../ *)
2.34 + val nd = get_nd pt p
2.35 + val cn = children nd;
2.36 +null cn = false;
2.37 +(is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true;
2.38 +"~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos);
2.39 +(* ^^^^^^^^^ only once in test/../solve.sml*)
2.40 + val t = get_obj g_form pt p
2.41 + val tac = get_obj g_tac pt p
2.42 + val rls = (assoc_rls o rls_of) tac
2.43 + val ctxt = get_ctxt pt pos
2.44 +(*rls = Rls {calc = [], erls = ...*)
2.45 + val is = init_istate tac t
2.46 + (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
2.47 + is wrong for simpl, but working ?!? *)
2.48 + val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
2.49 + val pos' = ((lev_on o lev_dn) p, Frm)
2.50 + val thy = assoc_thy "Isac"
2.51 + val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt;
2.52 + (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
2.53 + (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
2.54 + (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
2.55 + ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
2.56 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ptree * pos')) =
2.57 + (CompleteSubpbl, [], (pt',pos'));
2.58 +p = ([], Res) = false;
2.59 +member op = [Pbl,Met] p_ = false;
2.60 +val (_, c', ptp') = nxt_solve_ ptp;
2.61 +(* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
2.62 + ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
2.63 +"~~~~~ fun nxt_solve_, args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
2.64 +e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
2.65 + val thy' = get_obj g_domID pt (par_pblobj pt p);
2.66 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
2.67 + val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
2.68 +(*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
2.69 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
2.70 + (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
2.71 +l = [] = false;
2.72 +nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
2.73 + BUT WE FIND IN THE CODE ABOVE IN next_tac:*)
2.74 +;
2.75 +(*----------------------------------------------------------------------------------------------*)
2.76 +if string_of_thmI @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
2.77 +then () else error "string_of_thmI changed";
2.78 +if string_of_thm @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
2.79 +then () else error "string_of_thm changed";
2.80 +(*----------------------------------------------------------------------------------------------*)
2.81 +;
2.82 +(*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*)
2.83 +"~~~~~ fun nxt_solv, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
2.84 + val pos =
2.85 + case pos of
2.86 + (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
2.87 + | (p, Res) => (lev_on p,Res) (*somewhere in script*)
2.88 + | _ => pos;
2.89 +generate1 (assoc_thy "Isac") tac_ is pos pt;
2.90 +(* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
2.91 + ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
2.92 +"~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
2.93 + (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt);
2.94 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
2.95 + (Rewrite thm') (f',asm) Complete;
2.96 +(* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
2.97 + ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
2.98 +"~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
2.99 + (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
2.100 +existpt p pt andalso get_obj g_tac pt p=Empty_Tac = false;
2.101 +apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
2.102 +apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
2.103 +(append_atomic p ist_res f r f' s) : ptree -> ptree;
2.104 +;
2.105 +(* HERE THE ERROR OCCURED IN THE FIRST APPROACH
2.106 + getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*)
2.107 +"~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));
2.108 +val ((pt,_),_) = get_calc cI
2.109 +val (form, tac, asms) = pt_extract (pt, p)
2.110 +val SOME ta = tac;
2.111 +"~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
2.112 +"~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
2.113 +"~~~~~ fun thm'2xml, args:"; val (j, ((ID, form):thm')) = ((j+i), thm');
2.114 +ID = "rnorm_equation_add";
2.115 +@{thm rnorm_equation_add};
2.116 +form = "Test.rnorm_equation_add"
2.117 + (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
2.118 +(*thmstr2xml (j+i) form;
2.119 +ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
2.120 +;
2.121 +show_pt pt;
2.122 +(*[
2.123 +(([], Frm), solve (x + 1 = 2, x)),
2.124 +(([1], Frm), x + 1 = 2),
2.125 +(([1,1], Frm), x + 1 = 2),
2.126 +(([1,1], Res), x + 1 + -1 * 2 = 0),
2.127 +(([1], Res), x + 1 + -1 * 2 = 0),
2.128 +(([2], Res), -1 + x = 0)]
2.129 +
2.130 +pt; --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*)
2.131 +
3.1 --- a/test/Tools/isac/Test_Some.thy Sat Jul 26 13:39:00 2014 +0200
3.2 +++ b/test/Tools/isac/Test_Some.thy Sat Jul 26 14:10:05 2014 +0200
3.3 @@ -1,10 +1,10 @@
3.4 -theory Test_Some imports Build_Thydata begin
3.5 +theory Test_Some imports Build_Thydata begin
3.6 +ML {* fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
3.7 +
3.8 ML_file "Interpret/mathengine.sml" (*ERROR here, OK in Test_Isac.thy*)
3.9
3.10 section {* code for copy & paste ===============================================================*}
3.11 ML {*
3.12 - fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join
3.13 - ;
3.14 "~~~~~ fun , args:"; val () = ();
3.15 "~~~~~ and , args:"; val () = ();
3.16
3.17 @@ -27,317 +27,10 @@
3.18 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
3.19 *}
3.20
3.21 -section {* mini-subpbl with ERROR in <tactic applied> =========================================*}
3.22 -(* postponed due to parallelisation questions *)
3.23 +section {* ===================================================================================*}
3.24 ML {*
3.25 -reset_states ();
3.26 -CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
3.27 - ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
3.28 -moveActiveRoot 1;
3.29 -autoCalculate' 1 CompleteCalcHead;
3.30 -autoCalculate' 1 (Step 1);
3.31 -autoCalculate' 1 (Step 1);
3.32 -autoCalculate' 1 (Step 1);
3.33 -getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
3.34 -interSteps 1 ([1],Res);
3.35 *} ML {*
3.36 -"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
3.37 -val ((pt,p), tacis) = get_calc cI;
3.38 -(not o is_interpos) ip = false;
3.39 -val ip' = lev_pred' pt ip;
3.40 -"~~~~~ fun detailstep, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
3.41 -(* ^^^^^^^^^ not in test/../ *)
3.42 - val nd = get_nd pt p
3.43 - val cn = children nd;
3.44 -null cn = false;
3.45 -(is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true;
3.46 -"~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos);
3.47 -(* ^^^^^^^^^ only once in test/../solve.sml*)
3.48 - val t = get_obj g_form pt p
3.49 - val tac = get_obj g_tac pt p
3.50 - val rls = (assoc_rls o rls_of) tac
3.51 - val ctxt = get_ctxt pt pos
3.52 -(*rls = Rls {calc = [], erls = ...*)
3.53 - val is = init_istate tac t
3.54 - (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
3.55 - is wrong for simpl, but working ?!? *)
3.56 - val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
3.57 - val pos' = ((lev_on o lev_dn) p, Frm)
3.58 - val thy = assoc_thy "Isac"
3.59 *} ML {*
3.60 - val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt
3.61 -*} ML {*
3.62 - val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
3.63 - (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
3.64 - (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
3.65 - ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.66 -*} ML {*
3.67 -"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ptree * pos')) =
3.68 - (CompleteSubpbl, [], (pt',pos'));
3.69 -*} ML {*
3.70 -p = ([], Res) = false;
3.71 -*} ML {*
3.72 -member op = [Pbl,Met] p_ = false
3.73 -*} ML {*
3.74 -val (_, c', ptp') = nxt_solve_ ptp;
3.75 -(* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
3.76 - ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.77 -*} ML {*
3.78 -"~~~~~ fun nxt_solve_, args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
3.79 -*} ML {*
3.80 -e_metID = get_obj g_metID pt (par_pblobj pt p) = false
3.81 -*} ML {*
3.82 - val thy' = get_obj g_domID pt (par_pblobj pt p);
3.83 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
3.84 -*} ML {*
3.85 - val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
3.86 -*} ML {*
3.87 -"~~~~~ fun nxt_solv, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
3.88 -*} ML {*
3.89 - val pos =
3.90 - case pos of
3.91 - (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
3.92 - | (p, Res) => (lev_on p,Res) (*somewhere in script*)
3.93 - | _ => pos
3.94 -*} ML {*
3.95 -generate1 (assoc_thy "Isac") tac_ is pos pt;
3.96 -(* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
3.97 - ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.98 -*} ML {*
3.99 -tac_
3.100 -*} ML {*
3.101 -"~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
3.102 - (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt);
3.103 -*} ML {*
3.104 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
3.105 - (Rewrite thm') (f',asm) Complete
3.106 -(* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
3.107 - ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.108 -*} ML {*
3.109 -"~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) = (pt, p, (is, insert_assumptions asm ctxt), f,
3.110 - (Rewrite thm'), (f',asm), Complete);
3.111 -*} ML {*
3.112 -existpt p pt andalso get_obj g_tac pt p=Empty_Tac = false
3.113 -*} ML {*
3.114 -apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
3.115 -*} ML {*
3.116 -apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
3.117 -*} ML {*
3.118 -(append_atomic p ist_res f r f' s) : ptree -> ptree
3.119 -*} ML {*
3.120 -(cut_tree pt (p,Frm)) : ptree * pos' list
3.121 -*} ML {*
3.122 -"~~~~~ fun , args:"; val () = ();
3.123 -*} ML {*
3.124 -*} ML {*
3.125 -*} ML {*
3.126 -*} ML {*
3.127 -*} ML {*
3.128 -*} ML {*
3.129 -*} ML {*
3.130 -*} ML {*
3.131 -*} ML {*
3.132 -*} ML {*
3.133 -*} ML {*
3.134 -*} ML {*
3.135 -*} ML {*
3.136 -*} text {*
3.137 -val ptp' = (Nd (PblObj {branch = TransitiveB, cell = NONE, ctxt = <context>, env = NONE, fmz =
3.138 - (["equality (x+1=(2::real))", "solveFor x", "solutions L"], ("Test", ["sqroot-test", "univariate", "equation", "test"], ["Test", "squ-equ-test-subpbl1"])), loc =
3.139 - (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false), <context>), NONE), meth =
3.140 - [(1, [1], true, "#Given",
3.141 - Cor ((Const ("Descript.equality", "bool \<Rightarrow> una"),
3.142 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]),
3.143 - (Free ("e_e", "bool"),
3.144 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]))),
3.145 - (2, [1], true, "#Given", Cor ((Const ("Descript.solveFor", "real \<Rightarrow> una"), [Free ("x", "real")]), (Free ("v_v", "real"), [Free ("x", "real")]))),
3.146 - (3, [1], true, "#Find", Cor ((Const ("Descript.solutions", "bool list \<Rightarrow> toreall"), [Free ("L", "bool list")]), (Free ("v_v'i'", "bool list"), [Free ("L", "bool list")])))],
3.147 - origin = ([(1, [1], "#Given", Const ("Descript.equality", "bool \<Rightarrow> una"),
3.148 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]),
3.149 - (2, [1], "#Given", Const ("Descript.solveFor", "real \<Rightarrow> una"), [Free ("x", "real")]),
3.150 - (3, [1], "#Find", Const ("Descript.solutions", "bool list \<Rightarrow> toreall"), [Free ("L", "bool list")])],
3.151 - ("Test", ["sqroot-test", "univariate", "equation", "test"], ["Test", "squ-equ-test-subpbl1"]),
3.152 - Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $
3.153 - (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $
3.154 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")) $
3.155 - Free ("x", "real"))),
3.156 - ostate = Incomplete, probl =
3.157 - [(1, [1], true, "#Given",
3.158 - Cor ((Const ("Descript.equality", "bool \<Rightarrow> una"),
3.159 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]),
3.160 - (Free ("e_e", "bool"),
3.161 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]))),
3.162 - (2, [1], true, "#Given", Cor ((Const ("Descript.solveFor", "real \<Rightarrow> una"), [Free ("x", "real")]), (Free ("v_v", "real"), [Free ("x", "real")]))),
3.163 - (3, [1], true, "#Find", Cor ((Const ("Descript.solutions", "bool list \<Rightarrow> toreall"), [Free ("L", "bool list")]), (Free ("v_v'i'", "bool list"), [Free ("L", "bool list")])))],
3.164 - result = (Const ("empty", "'a"), []), spec = ("Test", ["sqroot-test", "univariate", "equation", "test"], ["Test", "squ-equ-test-subpbl1"])},
3.165 - [Nd (PrfObj {branch = TransitiveB, cell = NONE, form =
3.166 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real"), loc =
3.167 - (SOME (ScrState ([(Free ("e_e", "bool"),
3.168 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")),
3.169 - (Free ("v_v", "real"), Free ("x", "real"))],
3.170 - [], NONE, Const ("empty", "'a"), Safe, true),
3.171 - <context>),
3.172 - NONE),
3.173 - ostate = Incomplete, result = (Const ("empty", "'a"), []), tac = Rewrite_Set "norm_equation"},
3.174 - [Nd (PrfObj {branch = TransitiveB, cell = NONE, form =
3.175 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real"), loc =
3.176 - (SOME (ScrState ([(Free ("t_t", "'z"),
3.177 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.178 - Free ("2", "real"))],
3.179 - [], NONE, Const ("empty", "'a"), Sundef, true),
3.180 - <context>),
3.181 - SOME (ScrState ([(Free ("t_t", "'z"),
3.182 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.183 - Free ("2", "real"))],
3.184 - [R, R, L, R, R], SOME (Const ("empty", "'a")),
3.185 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.186 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.187 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("2", "real"))) $
3.188 - Free ("0", "real"),
3.189 - Sundef, false),
3.190 - <context>)),
3.191 - ostate = Complete, result =
3.192 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.193 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.194 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("2", "real"))) $
3.195 - Free ("0", "real"),
3.196 - []),
3.197 - tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
3.198 - [])])]),
3.199 - ([1, 1], Res)):
3.200 - ptree * pos'
3.201 -*} ML {*
3.202 -*} ML {*
3.203 -*} text {* ------------------- outcommented for quick evaluation above --------------------------
3.204 -getTactic 1 ([1,1],Frm); (*<ERROR> syserror in getTactic </ERROR>*)
3.205 - val ((pt,_),_) = get_calc 1;
3.206 - val ip = get_pos 1 1;
3.207 - val (Form f, tac, asms) = pt_extract (pt, ip);
3.208 - if term2str f = "-1 + x = 0" andalso ip = ([2], Res) then ()
3.209 - else error "xxxxx - why is output window shifted right ?";
3.210 -"~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));
3.211 -val ((pt,_),_) = get_calc cI
3.212 -val (form, tac, asms) = pt_extract (pt, p)
3.213 -val SOME ta = tac;
3.214 -"~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
3.215 -"~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
3.216 -"~~~~~ fun thm'2xml, args:"; val (j, ((ID, form):thm')) = ((j+i), thm');
3.217 -ID = "rnorm_equation_add";
3.218 -@{thm rnorm_equation_add};
3.219 -form = "Test.rnorm_equation_add" (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
3.220 -(*thmstr2xml (j+i) form;
3.221 -ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
3.222 -*} text {*
3.223 -show_pt pt;
3.224 -(*[
3.225 -(([], Frm), solve (x + 1 = 2, x)),
3.226 -(([1], Frm), x + 1 = 2),
3.227 -(([1,1], Frm), x + 1 = 2),
3.228 -(([1,1], Res), x + 1 + -1 * 2 = 0),
3.229 -(([1], Res), x + 1 + -1 * 2 = 0),
3.230 -(([2], Res), -1 + x = 0)] *)
3.231 -print_depth 99;
3.232 -pt;
3.233 -print_depth 99;
3.234 -*} text {*
3.235 -val it = (): unit
3.236 -val it = Nd (PblObj {branch = TransitiveB, cell = NONE, ctxt = <context>, env = NONE, fmz =
3.237 - (["equality (x+1=(2::real))", "solveFor x", "solutions L"], ("Test", ["sqroot-test", "univariate", "equation", "test"], ["Test", "squ-equ-test-subpbl1"])), loc =
3.238 - (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false), <context>), NONE), meth =
3.239 - [(1, [1], true, "#Given",
3.240 - Cor ((Const ("Descript.equality", "bool \<Rightarrow> una"),
3.241 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]),
3.242 - (Free ("e_e", "bool"),
3.243 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]))),
3.244 - (2, [1], true, "#Given", Cor ((Const ("Descript.solveFor", "real \<Rightarrow> una"), [Free ("x", "real")]), (Free ("v_v", "real"), [Free ("x", "real")]))),
3.245 - (3, [1], true, "#Find", Cor ((Const ("Descript.solutions", "bool list \<Rightarrow> toreall"), [Free ("L", "bool list")]), (Free ("v_v'i'", "bool list"), [Free ("L", "bool list")])))],
3.246 - origin = ([(1, [1], "#Given", Const ("Descript.equality", "bool \<Rightarrow> una"),
3.247 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]),
3.248 - (2, [1], "#Given", Const ("Descript.solveFor", "real \<Rightarrow> una"), [Free ("x", "real")]),
3.249 - (3, [1], "#Find", Const ("Descript.solutions", "bool list \<Rightarrow> toreall"), [Free ("L", "bool list")])],
3.250 - ("Test", ["sqroot-test", "univariate", "equation", "test"], ["Test", "squ-equ-test-subpbl1"]),
3.251 - Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $
3.252 - (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $
3.253 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")) $
3.254 - Free ("x", "real"))),
3.255 - ostate = Incomplete, probl =
3.256 - [(1, [1], true, "#Given",
3.257 - Cor ((Const ("Descript.equality", "bool \<Rightarrow> una"),
3.258 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]),
3.259 - (Free ("e_e", "bool"),
3.260 - [Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")]))),
3.261 - (2, [1], true, "#Given", Cor ((Const ("Descript.solveFor", "real \<Rightarrow> una"), [Free ("x", "real")]), (Free ("v_v", "real"), [Free ("x", "real")]))),
3.262 - (3, [1], true, "#Find", Cor ((Const ("Descript.solutions", "bool list \<Rightarrow> toreall"), [Free ("L", "bool list")]), (Free ("v_v'i'", "bool list"), [Free ("L", "bool list")])))],
3.263 - result = (Const ("empty", "'a"), []), spec = ("Test", ["sqroot-test", "univariate", "equation", "test"], ["Test", "squ-equ-test-subpbl1"])},
3.264 - [Nd (PrfObj {branch = TransitiveB, cell = NONE, form =
3.265 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real"), loc =
3.266 - (SOME (ScrState ([(Free ("e_e", "bool"),
3.267 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")),
3.268 - (Free ("v_v", "real"), Free ("x", "real"))],
3.269 - [], NONE, Const ("empty", "'a"), Safe, true),
3.270 - <context>),
3.271 - SOME (ScrState ([(Free ("e_e", "bool"),
3.272 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real")),
3.273 - (Free ("v_v", "real"), Free ("x", "real"))],
3.274 - [R, L, R, L, L, R, R], SOME (Free ("e_e", "bool")),
3.275 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.276 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.277 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("2", "real"))) $
3.278 - Free ("0", "real"),
3.279 - Sundef, false),
3.280 - <context>)),
3.281 - ostate = Complete, result =
3.282 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.283 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.284 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("2", "real"))) $
3.285 - Free ("0", "real"),
3.286 - []),
3.287 - tac = Rewrite_Set "norm_equation"},
3.288 - [Nd (PrfObj {branch = TransitiveB, cell = NONE, form =
3.289 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $ Free ("2", "real"), loc =
3.290 - (SOME (ScrState ([(Free ("t_t", "'z"),
3.291 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.292 - Free ("2", "real"))],
3.293 - [], NONE, Const ("empty", "'a"), Sundef, true),
3.294 - <context>),
3.295 - SOME (ScrState ([(Free ("t_t", "'z"),
3.296 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.297 - Free ("2", "real"))],
3.298 - [R, R, L, R, R], SOME (Const ("empty", "'a")),
3.299 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.300 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.301 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("2", "real"))) $
3.302 - Free ("0", "real"),
3.303 - Sundef, false),
3.304 - <context>)),
3.305 - ostate = Complete, result =
3.306 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.307 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.308 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("2", "real"))) $
3.309 - Free ("0", "real"),
3.310 - []),
3.311 - tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
3.312 - [])]),
3.313 - Nd (PrfObj {branch = TransitiveB, cell = NONE, form =
3.314 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.315 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.316 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("2", "real"))) $
3.317 - Free ("0", "real"),
3.318 - loc = (NONE, SOME (ScrState ([(Free ("e_e", "bool"),
3.319 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $ Free ("1", "real")) $
3.320 - Free ("2", "real")),
3.321 - (Free ("v_v", "real"), Free ("x", "real"))],
3.322 - [R, L, R, L, R, R], SOME (Free ("e_e", "bool")),
3.323 - Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("x", "real")) $
3.324 - Free ("0", "real"),
3.325 - Sundef, false),
3.326 - <context>)),
3.327 - ostate = Complete, result =
3.328 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("-1", "real") $ Free ("x", "real")) $ Free ("0", "real"), []), tac =
3.329 - Rewrite_Set "Test_simplify"},
3.330 - [])]):
3.331 - ptree
3.332 -val it = (): unit
3.333 *} ML {*
3.334 *}
3.335