|
1 (* use"test-FE-KE.sml"; |
|
2 W.N.16.4.00 |
|
3 *) |
|
4 |
|
5 Compiler.Control.Print.printDepth:=4; (*4 default*) |
|
6 |
|
7 (*#########################################################*) |
|
8 " _________________ stdin: tutor active_________________ "; |
|
9 proofs:=[]; dials:=([],[],[]); |
|
10 (*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*) |
|
11 |
|
12 StdinSML 0 0 0 0 New_User; |
|
13 StdinSML 1 0 0 0 New_Proof; |
|
14 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
15 "solveFor x","errorBound (eps=0)", |
|
16 "solutions L"]; |
|
17 val (dI',pI',mI') = |
|
18 ("Script.thy",["sqroot-test","univariate","equation"], |
|
19 ("Script.thy","sqrt-equ-test")); |
|
20 "--- s1 ---"; |
|
21 val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1 (*@@@@@begin !!!!!*) |
|
22 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
23 "--- s2 ---"; |
|
24 StdinSML 1 1 ~1 ~1 (Command Accept); |
|
25 (*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*) |
|
26 "--- s3 ---"; |
|
27 StdinSML 1 1 ~2 ~2 (Command Accept); |
|
28 (*RuleFK (Add_Given "solveFor x")*) |
|
29 "--- s4 ---"; |
|
30 StdinSML 1 1 ~3 ~3 (Command Accept); |
|
31 (*RuleFK (Add_Given "errorBound (eps = #0)")*) |
|
32 "--- s5 ---"; |
|
33 StdinSML 1 1 ~4 ~4 (Command Accept); |
|
34 (*RuleFK (Add_Find "solutions L")*) |
|
35 "--- s6 ---"; |
|
36 StdinSML 1 1 ~5 ~5 (Command Accept); |
|
37 (*RuleFK (Specify_Domain "Script.thy")*) |
|
38 "--- s7 ---"; |
|
39 StdinSML 1 1 ~6 ~6 (Command Accept); |
|
40 (*RuleFK (Specify_Problem ["sqroot-test","univariate","equation"])*) |
|
41 "--- s8 ---"; |
|
42 StdinSML 1 1 ~7 ~7 (Command Accept); |
|
43 (*RuleFK (Specify_Method ("Script.thy","sqrt-equ-test"))*) |
|
44 "--- s9 ---"; |
|
45 StdinSML 1 1 ~8 ~8 (Command Accept); |
|
46 (*RuleFK (Apply_Method ("Script.thy","sqrt-equ-test"))*) |
|
47 "--- 1 ---"; |
|
48 StdinSML 1 1 ~9 ~9 (Command Accept); |
|
49 (*RuleFK (Rewrite ("square_equation_left",""))*) |
|
50 "--- 2 ---"; |
|
51 StdinSML 1 1 ~10 ~10 (Command Accept); |
|
52 (*RuleFK (Rewrite_Set "SqRoot_simplify")*) |
|
53 "--- 3 ---"; |
|
54 StdinSML 1 1 ~11 ~11 (Command Accept); |
|
55 (*RuleFK (Rewrite_Set "rearrange_assoc")*) |
|
56 "--- 4 ---"; |
|
57 StdinSML 1 1 ~12 ~12 (Command Accept); |
|
58 (*RuleFK (Rewrite_Set "isolate_root")*) |
|
59 "--- 5 ---"; |
|
60 StdinSML 1 1 ~13 ~13 (Command Accept); |
|
61 (*RuleFK (Rewrite_Set "SqRoot_simplify")*) |
|
62 "--- 6 ---"; |
|
63 StdinSML 1 1 ~14 ~14 (Command Accept); |
|
64 (*RuleFK (Rewrite ("square_equation_left",""))*) |
|
65 "--- 7 ---"; |
|
66 StdinSML 1 1 ~15 ~15 (Command Accept); |
|
67 (*RuleFK (Rewrite_Set "SqRoot_simplify")*) |
|
68 "--- 8 ---"; |
|
69 StdinSML 1 1 ~16 ~16 (Command Accept); |
|
70 (*RuleFK (Rewrite_Set "norm_equation")*) |
|
71 "--- 9 ---"; |
|
72 StdinSML 1 1 ~17 ~17 (Command Accept); |
|
73 (*RuleFK (Rewrite_Set "SqRoot_simplify")*) |
|
74 "--- 10 ---"; |
|
75 StdinSML 1 1 ~18 ~18 (Command Accept); |
|
76 (*RuleFK (Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv"))*) |
|
77 "--- 11 ---"; |
|
78 StdinSML 1 1 ~19 ~19 (Command Accept); |
|
79 (*RuleFK (Rewrite_Set "SqRoot_simplify")*) |
|
80 "--- 12 ---"; |
|
81 val (begin,uI,pI,acI,cI,dats,eend) = |
|
82 StdinSML 1 1 ~20 ~20 (Command Accept); |
|
83 (*RuleFK (Check_Postcond ("Script.thy","sqrt-equ-test"))*) |
|
84 |
|
85 if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]")) |
|
86 then raise error "do_ + msteps input: not finished correctly" |
|
87 else "roo-equation, do_ + msteps input: OK"; |
|
88 |
|
89 "=========================================================="; |
|
90 writeln (get_history 1 1); |
|
91 "=========================================================="; |
|
92 |
|
93 |
|
94 |
|
95 (*#########################################################*) |
|
96 " _________________ stdin: student active_________________ "; |
|
97 proofs:=[]; dials:=([],[],[]); |
|
98 (*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*) |
|
99 |
|
100 StdinSML 0 0 0 0 New_User; |
|
101 StdinSML 1 0 0 0 New_Proof; |
|
102 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
103 "solveFor x","errorBound (eps=0)", |
|
104 "solutions L"]; |
|
105 val (dI',pI',mI') = |
|
106 ("Script.thy",["sqroot-test","univariate","equation"], |
|
107 ("Script.thy","sqrt-equ-test")); |
|
108 "--- s1 ---"; |
|
109 val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1 |
|
110 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
111 "--- s2 ---"; |
|
112 StdinSML 1 1 ~1 2 (RuleFK |
|
113 (Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))")); |
|
114 "--- s3 ---"; |
|
115 StdinSML 1 1 ~2 3 (RuleFK (Add_Given "solveFor x")); |
|
116 "--- s4 ---"; |
|
117 StdinSML 1 1 ~3 4 (RuleFK (Add_Given "errorBound (eps = 0)")); |
|
118 "--- s5 ---"; |
|
119 StdinSML 1 1 ~4 5 (RuleFK (Add_Find "solutions L")); |
|
120 "--- s6 ---"; |
|
121 StdinSML 1 1 ~5 6 (RuleFK (Specify_Domain "Script.thy")); |
|
122 "--- s7 ---"; |
|
123 StdinSML 1 1 ~6 7 (RuleFK |
|
124 (Specify_Problem ["sqroot-test","univariate","equation"])); |
|
125 "--- s8 ---"; |
|
126 StdinSML 1 1 ~7 8 (RuleFK (Specify_Method ("Script.thy","sqrt-equ-test"))); |
|
127 "--- s9 ---"; |
|
128 StdinSML 1 1 ~8 9 (RuleFK (Apply_Method ("Script.thy","sqrt-equ-test"))); |
|
129 "--- 1 ---"; |
|
130 StdinSML 1 1 ~9 10 (RuleFK |
|
131 (Rewrite ("square_equation_left",""))); |
|
132 "--- 2 ---"; |
|
133 StdinSML 1 1 ~10 11 (RuleFK (Rewrite_Set "SqRoot_simplify")); |
|
134 "--- 3 ---"; |
|
135 StdinSML 1 1 ~11 12 (RuleFK (Rewrite_Set "rearrange_assoc")); |
|
136 "--- 4 ---"; |
|
137 StdinSML 1 1 ~12 13 (RuleFK (Rewrite_Set "isolate_root")); |
|
138 "--- 5 ---"; |
|
139 StdinSML 1 1 ~13 14 (RuleFK (Rewrite_Set "SqRoot_simplify")); |
|
140 "--- 6 ---"; |
|
141 StdinSML 1 1 ~14 15 (RuleFK |
|
142 (Rewrite ("square_equation_left",""))); |
|
143 "--- 7 ---"; |
|
144 StdinSML 1 1 ~15 16 (RuleFK (Rewrite_Set "SqRoot_simplify")); |
|
145 "--- 8 ---"; |
|
146 StdinSML 1 1 ~16 17 (RuleFK (Rewrite_Set "norm_equation")); |
|
147 "--- 9 ---"; |
|
148 StdinSML 1 1 ~17 18 (RuleFK (Rewrite_Set "SqRoot_simplify")); |
|
149 "--- 10 ---"; |
|
150 StdinSML 1 1 ~18 19 (RuleFK |
|
151 (Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv"))); |
|
152 "--- 11 ---"; |
|
153 StdinSML 1 1 ~19 20 (RuleFK (Rewrite_Set "SqRoot_simplify")); |
|
154 "--- 12 ---"; |
|
155 val (begin,uI,pI,acI,cI,dats,eend) = |
|
156 StdinSML 1 1 ~20 21 (RuleFK |
|
157 (Check_Postcond ("Script.thy","sqrt-equ-test"))); |
|
158 |
|
159 if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]")) |
|
160 then raise error "do_ + msteps input: not finished correctly" |
|
161 else "roo-equation, do_ + msteps input: OK"; |
|
162 |
|
163 "=========================================================="; |
|
164 writeln (get_history 1 1); |
|
165 "=========================================================="; |
|
166 |
|
167 |
|
168 (*=========27.4.01===============================================*) |
|
169 proofs:= []; dials:=([],[],[]); |
|
170 " _________________ exampel [x=4]: Rules 4.2.01a________________ "; |
|
171 val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User; |
|
172 val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof; |
|
173 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
174 "solveFor x","errorBound (eps=0)", |
|
175 "solutions L"]; |
|
176 val (dI',pI',mI') = |
|
177 ("SqRoot.thy",["sqroot-test","univariate","equation"], |
|
178 ("SqRoot.thy","squ-equ-test2")); |
|
179 StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
180 |
|
181 StdinSML uI pI ~1 ~1 (Command Accept); |
|
182 |
|
183 StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "norm_equation")); |