2 use"systest/tacis.sml";
5 "=================================================================";
6 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
7 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
8 "=================================================================";
12 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
13 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
14 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
16 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
17 ("Test", ["sqroot-test", "univariate", "equation", "test"],
18 ["Test", "squ-equ-test-subpbl1"]))];
19 Iterator 1; moveActiveRoot 1;
20 autoCalculate 1 CompleteCalcHead;
21 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 = 2*);
23 fetchProposedTactic 1 (*'Rewrite_Set norm_equation' in tacis*);
24 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
26 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
27 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
28 val ((pt,_),_) = States.get_calc 1;
29 val str = pr_ctree ctxt pr_short pt;
32 fetchProposedTactic 1 (*'Subproblem ...' in tacis*);
33 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*solve (-1 + x = 0,x)*);
35 fetchProposedTactic 1 (*'Model_Problem' in tacis*);
36 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*equality ///*);
37 (*----- WN060222 since complete_mod_ case cas of SOME headline -----
38 fetchProposedTactic 1 (*'Add_Given equality (-1 + x = 0)' in tacis*);
39 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*equality (-1 + x =0)*);
40 ---------------------------------------------------------------------*)
42 fetchProposedTactic 1 (*'Add_Given solveFor x' in tacis*);
43 (*----- WN060222 since complete_mod_ case cas of SOME headline:
44 (*Specify_Theory Test.thy*)
45 ---------------------------------------------------------------------*)
46 autoCalculate 1 CompleteCalcHead; refFormula 1 (States.get_pos 1 1) (*OK*);
47 (*###########################################autoCalculate 1 (Steps 1);*)
48 fetchProposedTactic 1 (*'Apply_Method Test solve_linear' in tacis*);
49 (* there was the only error \<up> \<up> \<up> in step/begin_end_prog ..Apply_Method..
50 val (str', (tacis', (pt',p'))) = Step.do_next ip (ptp, tacis);
51 writeln (State_Steps.to_string tacis');
52 ######################################################################*)
53 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
55 fetchProposedTactic 1 (*'Rewrite_Set_Inst isolate_bdv' in tacis*);
56 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 0 + -1 * -1*);
58 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
59 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 1*);
60 val ((pt,_),_) = States.get_calc 1;
61 val str = pr_ctree ctxt pr_short pt;
64 fetchProposedTactic 1 (*'Check_Postcond linear...' in tacis*);
65 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
67 fetchProposedTactic 1 (*'Check_elementwise Assumptions' in tacis*);
68 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
70 fetchProposedTactic 1 (*'Check_Postcond sqroot-test...' in tacis*);
71 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
73 fetchProposedTactic 1 (*'' in tacis*);
74 val ((pt,p),tacis) = States.get_calc 1;
75 val ip = States.get_pos 1 1;
76 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
77 if UnparseC.term @{context} f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else
78 error "tacis.sml: diff.behav. in fetchProposedTactic autoCalculate";
82 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
83 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
84 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
86 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
87 ("Test", ["sqroot-test", "univariate", "equation", "test"],
88 ["Test", "squ-equ-test-subpbl1"]))];
89 Iterator 1; moveActiveRoot 1;
90 autoCalculate 1 CompleteCalcHead;
91 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 = 2*);
93 setNextTactic 1 (Rewrite_Set "norm_equation");
94 val (_, tacis) = States.get_calc 1;
95 case tacis of [(Rewrite_Set "norm_equation",_,(([1], Res), _))] => () | _ =>
96 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (1)";
97 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
99 setNextTactic 1 (Rewrite_Set "Test_simplify");
100 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
101 val ((pt,_),_) = States.get_calc 1;
102 val str = pr_ctree ctxt pr_short pt;
105 setNextTactic 1 (Subproblem ("Test",["LINEAR", "univariate",
106 "equation", "test"]));
107 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*solve (-1 + x = 0, x)*);
108 val ((pt,_),_) = States.get_calc 1;
109 val str = pr_ctree ctxt pr_short pt;
112 setNextTactic 1 (Model_Problem (*["LINEAR", "univariate", "equation", "test"]*));
113 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*equality ///*);
115 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
116 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*equality (-1 + x = 0)*);
118 setNextTactic 1 (Add_Given "solveFor x");
119 autoCalculate 1 CompleteCalcHead; refFormula 1 (States.get_pos 1 1) (*OK*);
121 setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
122 val (_, tacis) = States.get_calc 1;
124 [((Apply_Method ["Test", "solve_linear"],_,(([3,1], Frm), _)))] =>() | _ =>
125 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (2)";
126 (*#######################################################################*)
127 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
129 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
130 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 0 + -1 * -1*);
132 setNextTactic 1 (Rewrite_Set "Test_simplify");
133 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 1*);
135 setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
136 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
138 setNextTactic 1 (Check_elementwise "Assumptions");
139 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
140 val ((pt,_),_) = States.get_calc 1;
141 val str = pr_ctree ctxt pr_short pt;
144 setNextTactic 1 (Check_Postcond
145 ["sqroot-test", "univariate", "equation", "test"]);
146 val (_, tacis) = States.get_calc 1;
148 (*case tacis of 040609 suddenly ???!
149 [((Check_Postcond _, _,(([], Res), _)))] =>() | _ =>
150 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (3)";
151 #######################################################################*)
152 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
154 val ((pt,p),tacis) = States.get_calc 1;
155 val ip = States.get_pos 1 1;
156 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
157 if UnparseC.term @{context} f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else
158 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (4)";