walther@60330
|
1 |
(*
|
walther@60330
|
2 |
|
neuper@37906
|
3 |
|
neuper@37906
|
4 |
method "sqrt-equ-test", _NOT_ "square-equation"
|
neuper@37906
|
5 |
*)
|
neuper@37906
|
6 |
|
neuper@37906
|
7 |
" ================= equation with x =(-12)/5, but L ={} ======= ";
|
neuper@37906
|
8 |
" _________________ rewrite _________________ ";
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
|
neuper@37906
|
11 |
" ================= equation with result={4} ================== ";
|
neuper@37906
|
12 |
" -------------- model, specify ------------ ";
|
neuper@37906
|
13 |
" ________________ rewrite _________________";
|
neuper@37906
|
14 |
" _________________ rewrite_ x=4_________________ ";
|
neuper@37906
|
15 |
" _________________ rewrite + cappend _________________ ";
|
neuper@37906
|
16 |
" _________________ me Free_Solve _________________ ";
|
neuper@37906
|
17 |
" _________________ me + tacs input _________________ ";
|
neuper@37906
|
18 |
(*" _______________ me + nxt_step from script _________---> scriptnew.sml*)
|
neuper@37906
|
19 |
(*" _________________ me + nxt_step from script (check_elementwise..)______
|
neuper@37906
|
20 |
... L_a = Tac subproblem_equation_dummy; ";*)
|
neuper@37906
|
21 |
(*" _______________ me + root-equ: 1.norm_equation ___---> scriptnew.sml*)
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
val c = [];
|
neuper@37906
|
24 |
|
neuper@37906
|
25 |
|
neuper@37906
|
26 |
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
(*
|
walther@60340
|
29 |
> val t = (Thm.term_of o the o (TermC.parse thy)) "#2 \<up> #3";
|
walther@59686
|
30 |
> val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
|
neuper@37926
|
31 |
> val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
|
walther@60360
|
32 |
> Syntax.string_of_term (Proof_Context.init_global thy) t';
|
neuper@37906
|
33 |
*)
|
neuper@37906
|
34 |
(******************************************************************)
|
neuper@37906
|
35 |
(* ------------------------------------- *)
|
neuper@37906
|
36 |
" _________________ equation with x =(-12)/5, but L ={} ------- ";
|
neuper@37906
|
37 |
(* ------------------------------------- *)
|
neuper@37906
|
38 |
" _________________ rewrite _________________ ";
|
neuper@38058
|
39 |
val thy' = "Test";
|
neuper@37906
|
40 |
val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
|
walther@59997
|
41 |
val thm = ("square_equation_left", "");
|
neuper@37926
|
42 |
val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
|
walther@60242
|
43 |
(*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) \<up> 2"*)
|
neuper@37906
|
44 |
val rls = ("Test_simplify");
|
neuper@37906
|
45 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
46 |
(*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x \<up> 2 + -3 * x))"*)
|
neuper@37906
|
47 |
val rls = ("rearrange_assoc");
|
neuper@37906
|
48 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
49 |
(*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x \<up> 2 + -3 * x)"*)
|
neuper@37906
|
50 |
val rls = ("isolate_root");
|
neuper@37906
|
51 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
52 |
(*"sqrt (x \<up> 2 + -3 * x) =
|
neuper@37906
|
53 |
(-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*)
|
neuper@37906
|
54 |
val rls = ("Test_simplify");
|
neuper@37906
|
55 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
56 |
(*"sqrt (x \<up> 2 + -3 * x) = 6 + x"*)
|
walther@59997
|
57 |
val thm = ("square_equation_left", "");
|
neuper@37906
|
58 |
val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
neuper@37906
|
59 |
val asm = asm union asm';
|
walther@60242
|
60 |
(*"x \<up> 2 + -3 * x = (6 + x) \<up> 2"*)
|
neuper@37906
|
61 |
val rls = ("Test_simplify");
|
neuper@37906
|
62 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
63 |
(*"x \<up> 2 + -3 * x = 36 + (x \<up> 2 + 12 * x)"*)
|
neuper@37906
|
64 |
val rls = ("norm_equation");
|
neuper@37906
|
65 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
66 |
(*"x \<up> 2 + -3 * x + -1 * (36 + (x \<up> 2 + 12 * x)) = 0"*)
|
neuper@37906
|
67 |
val rls = ("Test_simplify");
|
neuper@37906
|
68 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
neuper@37906
|
69 |
(*"-36 + -15 * x = 0"*)
|
neuper@37906
|
70 |
val rls = ("isolate_bdv");
|
neuper@37906
|
71 |
val (ct,_) = the (rewrite_set_inst thy' false
|
walther@59997
|
72 |
[("bdv", "x::real")] rls ct);
|
neuper@37906
|
73 |
(*"x = (0 + -1 * -36) // -15"*)
|
neuper@37906
|
74 |
val rls = ("Test_simplify");
|
neuper@37906
|
75 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
neuper@38031
|
76 |
if ct<>"x = -12 / 5"then error "new behaviour in testexample"else ();
|
neuper@37906
|
77 |
|
neuper@37906
|
78 |
(*
|
walther@59865
|
79 |
val ct = "x = (-12) / 5" : TermC.as_string
|
neuper@37906
|
80 |
> asm;
|
neuper@37906
|
81 |
val it =
|
walther@59997
|
82 |
["(+0) <= sqrt x + sqrt ((-3) + x) ", "(+0) <= 9 + 4 * x",
|
walther@60242
|
83 |
"(+0) <= (-3) * x + x \<up> 2", "(+0) <= 6 + x"] : TermC.as_string list
|
neuper@37906
|
84 |
*)
|
neuper@37906
|
85 |
|
neuper@37906
|
86 |
|
neuper@37906
|
87 |
|
neuper@37906
|
88 |
|
neuper@37906
|
89 |
|
neuper@37906
|
90 |
" ================== equation with result={4} ================== ";
|
neuper@37906
|
91 |
" ================== equation with result={4} ================== ";
|
neuper@37906
|
92 |
" ================== equation with result={4} ================== ";
|
neuper@37906
|
93 |
|
neuper@37906
|
94 |
" -------------- model, specify ------------ ";
|
neuper@37906
|
95 |
" -------------- model, specify ------------ ";
|
neuper@37906
|
96 |
" -------------- model, specify ------------ ";
|
neuper@37906
|
97 |
" --- subproblem 1: linear-equation --- ";
|
neuper@37906
|
98 |
val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
|
walther@59997
|
99 |
"bound_variable x", "error_bound 0"(*,
|
neuper@37906
|
100 |
"solutions L::real set" ,
|
neuper@37906
|
101 |
"L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
|
wneuper@59592
|
102 |
val thy = (theory "Isac_Knowledge");
|
walther@60230
|
103 |
val formals = map (the o (TermC.parse thy)) origin;
|
neuper@37906
|
104 |
|
neuper@37906
|
105 |
val given = ["equation (l=(r::real))",
|
neuper@37906
|
106 |
"bound_variable bdv", (* TODO type *)
|
neuper@37906
|
107 |
"error_bound eps"];
|
neuper@37906
|
108 |
val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.yy*)
|
neuper@37906
|
109 |
"bdv is_var",
|
neuper@37906
|
110 |
"eps is_const_expr"];
|
neuper@37906
|
111 |
val find = ["solutions (L::bool list)"];
|
neuper@37906
|
112 |
val with_ = [(* parseold ...
|
neuper@37906
|
113 |
"L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
|
walther@60230
|
114 |
val chkpbl = map (the o (TermC.parse thy)) (given @ where_ @ find @ with_);
|
walther@60230
|
115 |
val givens = map (the o (TermC.parse thy)) given;
|
neuper@37906
|
116 |
parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
" --- subproblem 2: linear-equation --- ";
|
walther@59997
|
119 |
val origin = ["x + 4 = (0::real)", "x::real"];
|
walther@60230
|
120 |
val formals = map (the o (TermC.parse thy)) origin;
|
neuper@37906
|
121 |
|
neuper@37906
|
122 |
val given = ["equation (l=(0::real))",
|
neuper@37906
|
123 |
"bound_variable bdv"];
|
walther@60387
|
124 |
val where_ = ["l is_linear_in bdv", "bdv is_atom"];
|
neuper@37906
|
125 |
val find = ["l::real"];
|
neuper@37906
|
126 |
val with_ = ["l = (%x. l) bdv"];
|
neuper@37906
|
127 |
val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
|
walther@60230
|
128 |
val givens = map (the o (TermC.parse thy)) given;
|
neuper@37906
|
129 |
|
neuper@37906
|
130 |
|
neuper@37906
|
131 |
" _________________ rewrite_ x+4_________________ ";
|
neuper@37906
|
132 |
" _________________ rewrite_ x+4_________________ ";
|
neuper@37906
|
133 |
" _________________ rewrite_ x+4_________________ ";
|
walther@60340
|
134 |
val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
|
walther@59871
|
135 |
val thm = ThmC.numerals_to_Free @{thm square_equation_left};
|
neuper@37906
|
136 |
val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
|
neuper@37906
|
137 |
val rls = Test_simplify;
|
neuper@37906
|
138 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
neuper@37906
|
139 |
val rls = rearrange_assoc;
|
neuper@37906
|
140 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
neuper@37906
|
141 |
val rls = isolate_root;
|
neuper@37906
|
142 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
neuper@37906
|
143 |
|
neuper@37906
|
144 |
val rls = Test_simplify;
|
neuper@37906
|
145 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
neuper@37906
|
146 |
(*
|
walther@60242
|
147 |
sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
148 |
(5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
|
neuper@37906
|
149 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
neuper@37906
|
150 |
### trying thm 'rdistr_div_right'
|
walther@60242
|
151 |
### rewrites to: sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
152 |
(5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
|
walther@60242
|
153 |
### rewrites to: sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
154 |
(5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
|
walther@60242
|
155 |
### rewrites to: sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
156 |
5 / (-1 * 2) + 2 * x / (-1 * 2) +
|
neuper@37906
|
157 |
(-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
|
neuper@37906
|
158 |
|
neuper@37906
|
159 |
### trying thm 'radd_left_commute'
|
walther@60242
|
160 |
### rewrites to: sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
161 |
-1 * 9 / (-1 * 2) +
|
neuper@37906
|
162 |
(5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
|
neuper@37906
|
163 |
### trying thm 'radd_assoc'
|
walther@60242
|
164 |
### rewrites to: sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
165 |
-1 * 9 / (-1 * 2) +
|
neuper@37906
|
166 |
(5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
|
neuper@37906
|
167 |
|
neuper@37906
|
168 |
### trying thm 'radd_real_const_eq'
|
walther@60242
|
169 |
### rewrites to: sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
170 |
-1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
|
walther@60242
|
171 |
### rewrites to: sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
172 |
-1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
|
walther@60242
|
173 |
### rewrites to: sqrt (x \<up> 2 + 5 * x) =
|
neuper@37906
|
174 |
(-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)
|
neuper@37906
|
175 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
neuper@37906
|
176 |
|
neuper@37906
|
177 |
28.8.02: ruleset besser zusammenstellen !!!
|
neuper@37906
|
178 |
*)
|
walther@59871
|
179 |
val thm = ThmC.numerals_to_Free @{thm square_equation_left};
|
neuper@37906
|
180 |
val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
|
neuper@37906
|
181 |
val asm = asm union asm';
|
neuper@37906
|
182 |
val rls = Test_simplify;
|
neuper@37906
|
183 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
neuper@37906
|
184 |
val rls = norm_equation;
|
neuper@37906
|
185 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
neuper@37906
|
186 |
val rls = Test_simplify;
|
neuper@37906
|
187 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
neuper@37906
|
188 |
val rls = isolate_bdv;
|
walther@60230
|
189 |
val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
|
neuper@37906
|
190 |
val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
|
neuper@37906
|
191 |
val rls = Test_simplify;
|
neuper@37906
|
192 |
val (t,_) = the (rewrite_set_ thy false rls t);
|
walther@59868
|
193 |
val t' = UnparseC.term t;
|
neuper@37906
|
194 |
if t' = "x = 4" then ()
|
neuper@38031
|
195 |
else error "root-equ.sml: new behav. in rewrite_ x+4";
|
neuper@37906
|
196 |
|
neuper@37906
|
197 |
" _________________ rewrite x=4_________________ ";
|
neuper@37906
|
198 |
" _________________ rewrite x=4_________________ ";
|
neuper@37906
|
199 |
" _________________ rewrite x=4_________________ ";
|
neuper@37906
|
200 |
(*
|
walther@59871
|
201 |
rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
|
walther@60230
|
202 |
TermC.atomty (Thm.prop_of (!tthm));
|
walther@60230
|
203 |
TermC.atomty (Thm.term_of (!tct));
|
neuper@37906
|
204 |
*)
|
neuper@38058
|
205 |
val thy' = "Test";
|
neuper@37906
|
206 |
val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
|
walther@59997
|
207 |
(*1*)val thm = ("square_equation_left", "");
|
neuper@37906
|
208 |
val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
walther@60242
|
209 |
"9 + 4 * x = (sqrt x + sqrt (5 + x)) \<up> 2";
|
neuper@37906
|
210 |
(*2*)val rls = "Test_simplify";
|
neuper@37906
|
211 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
212 |
"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x \<up> 2 + 5 * x))";
|
neuper@37906
|
213 |
(*3*)val rls = "rearrange_assoc";
|
neuper@37906
|
214 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
215 |
"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)";
|
neuper@37906
|
216 |
(*4*)val rls = "isolate_root";
|
neuper@37906
|
217 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
218 |
"sqrt (x \<up> 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
|
neuper@37906
|
219 |
(*5*)val rls = "Test_simplify";
|
neuper@37906
|
220 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
221 |
"sqrt (x \<up> 2 + 5 * x) = 2 + x";
|
walther@59997
|
222 |
(*6*)val thm = ("square_equation_left", "");
|
neuper@37906
|
223 |
val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
neuper@37906
|
224 |
val asm = asm union asm';
|
walther@60242
|
225 |
"x \<up> 2 + 5 * x = (2 + x) \<up> 2";
|
neuper@37906
|
226 |
(*7*)val rls = "Test_simplify";
|
neuper@37906
|
227 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
228 |
"x \<up> 2 + 5 * x = 4 + (x \<up> 2 + 4 * x)";
|
neuper@37906
|
229 |
(*8*)val rls = "norm_equation";
|
neuper@37906
|
230 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60242
|
231 |
"x \<up> 2 + 5 * x + -1 * (4 + (x \<up> 2 + 4 * x)) = 0";
|
neuper@37906
|
232 |
(*9*)val rls = "Test_simplify";
|
neuper@37906
|
233 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
neuper@37906
|
234 |
"-4 + x = 0";
|
neuper@37906
|
235 |
(*10*)val rls = "isolate_bdv";
|
neuper@37906
|
236 |
val (ct,_) = the (rewrite_set_inst thy' false
|
walther@59997
|
237 |
[("bdv", "x")] rls ct);
|
neuper@37906
|
238 |
"x = 0 + -1 * -4";
|
neuper@37906
|
239 |
(*11*)val rls = "Test_simplify";
|
neuper@37906
|
240 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
neuper@38031
|
241 |
if ct="x = 4" then () else error "new behaviour in test-example";
|
neuper@37906
|
242 |
|
neuper@37906
|
243 |
|
neuper@37906
|
244 |
|
neuper@37906
|
245 |
|
neuper@37906
|
246 |
" _________________ rewrite + cappend _________________ ";
|
neuper@37906
|
247 |
" _________________ rewrite + cappend _________________ ";
|
neuper@37906
|
248 |
" _________________ rewrite + cappend _________________ ";
|
neuper@38058
|
249 |
val thy' = "Test";
|
walther@60230
|
250 |
val ct = TermC.str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
|
walther@59997
|
251 |
val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
|
Walther@60469
|
252 |
val oris = O_Model.init thy ctl
|
walther@59970
|
253 |
((#ppc o Problem.from_store)
|
walther@59997
|
254 |
["sqroot-test", "univariate", "equation", "test"]);
|
walther@59846
|
255 |
val loc = Istate.empty;
|
wneuper@59279
|
256 |
val (pt,pos) = (e_ctree,[]);
|
walther@59941
|
257 |
val (pt,_) = cappend_problem pt pos loc Formalise.empty (oris,empty_spec,TermC.empty, ContextC.empty)
|
neuper@37906
|
258 |
val pt = update_branch pt [] TransitiveB;
|
neuper@37906
|
259 |
(*
|
neuper@37906
|
260 |
val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
|
neuper@37906
|
261 |
*)
|
neuper@37906
|
262 |
(*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)
|
neuper@37906
|
263 |
val pt = update_domID pt [] "Test";
|
neuper@37906
|
264 |
val pt = update_pblID pt [] ["Test",
|
walther@59997
|
265 |
"equations", "univariate", "square-root"];
|
walther@59997
|
266 |
val pt = update_metID pt [] ["Test", "sqrt-equ-test"];
|
neuper@37906
|
267 |
val pt = update_pbl pt [] [];
|
neuper@37906
|
268 |
val pt = update_met pt [] [];
|
neuper@37906
|
269 |
(*
|
neuper@37906
|
270 |
> get_obj g_spec pt [];
|
Walther@60428
|
271 |
val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec
|
neuper@37906
|
272 |
> val pt = update_domID pt [] "RatArith";
|
neuper@37906
|
273 |
> get_obj g_spec pt [];
|
Walther@60428
|
274 |
val it = ("RatArith",Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec
|
neuper@37906
|
275 |
> val pt = update_pblID pt [] ["RatArith",
|
walther@59997
|
276 |
"equations", "univariate", "square-root"];
|
neuper@37906
|
277 |
> get_obj g_spec pt [];
|
walther@59997
|
278 |
("RatArith",["RatArith", "equations", "univariate", "square-root"],
|
Walther@60428
|
279 |
(ThyC.id_empty, MethodC.id_empty)) : spec
|
walther@59997
|
280 |
> val pt = update_metID pt [] ("RatArith", "sqrt-equ-test");
|
neuper@37906
|
281 |
> get_obj g_spec pt [];
|
walther@59997
|
282 |
("RatArith",["RatArith", "equations", "univariate", "square-root"],
|
walther@59997
|
283 |
("RatArith", "sqrt-equ-test")) : spec
|
neuper@37906
|
284 |
*)
|
neuper@37906
|
285 |
|
neuper@37906
|
286 |
|
neuper@37906
|
287 |
val pos = [1]:pos;
|
neuper@37906
|
288 |
val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;
|
neuper@37906
|
289 |
|
neuper@37906
|
290 |
val pos = (lev_on o lev_dn) pos;
|
walther@59997
|
291 |
val thm = ("square_equation_left", ""); val ctold = ct;
|
walther@59868
|
292 |
val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
|
walther@60230
|
293 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.str2term ct,[])Complete;
|
neuper@37906
|
294 |
(*val pt = union_asm pt [] (map (rpair []) asm);*)
|
neuper@37906
|
295 |
|
neuper@37906
|
296 |
val pos = lev_on pos;
|
walther@60230
|
297 |
val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
|
neuper@37906
|
298 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60230
|
299 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
300 |
|
neuper@37906
|
301 |
val pos = lev_on pos;
|
walther@60230
|
302 |
val rls = ("rearrange_assoc"); val ctold = TermC.str2term ct;
|
neuper@37906
|
303 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60230
|
304 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
305 |
|
neuper@37906
|
306 |
val pos = lev_on pos;
|
walther@60230
|
307 |
val rls = ("isolate_root"); val ctold = TermC.str2term ct;
|
neuper@37906
|
308 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60230
|
309 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
310 |
|
neuper@37906
|
311 |
val pos = lev_on pos;
|
walther@60230
|
312 |
val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
|
neuper@37906
|
313 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60230
|
314 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
315 |
|
neuper@37906
|
316 |
val pos = lev_on pos;
|
walther@60230
|
317 |
val thm = ("square_equation_left", ""); val ctold = TermC.str2term ct;
|
neuper@37906
|
318 |
val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
|
walther@60230
|
319 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
320 |
(*val pt = union_asm pt [] (map (rpair []) asm);*)
|
neuper@37906
|
321 |
|
neuper@37906
|
322 |
val pos = lev_up pos;
|
walther@60230
|
323 |
val (pt,_) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
324 |
|
neuper@37906
|
325 |
val pos = lev_on pos;
|
walther@60230
|
326 |
val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
|
neuper@37906
|
327 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60230
|
328 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
329 |
|
neuper@37906
|
330 |
val pos = lev_on pos;
|
walther@60230
|
331 |
val rls = ("norm_equation"); val ctold = TermC.str2term ct;
|
neuper@37906
|
332 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60230
|
333 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
334 |
|
neuper@37906
|
335 |
val pos = lev_on pos;
|
walther@60230
|
336 |
val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
|
neuper@37906
|
337 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60230
|
338 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
339 |
|
neuper@37906
|
340 |
(* --- see comments in interface_ME_ISA/instantiate''
|
walther@59997
|
341 |
val rlsdat' = instantiate_rls' thy' [("bdv", "x")] ("isolate_bdv");
|
neuper@37906
|
342 |
val (ct,_) = the (rewrite_set thy' false
|
neuper@37906
|
343 |
("#isolate_bdv",rlsdat') ct); *)
|
neuper@37906
|
344 |
val pos = lev_on pos;
|
walther@60230
|
345 |
val rls = ("isolate_bdv"); val ctold = TermC.str2term ct;
|
neuper@37906
|
346 |
val (ct,_) = the (rewrite_set_inst thy' false
|
walther@59997
|
347 |
[("bdv", "x")] rls ct);
|
walther@60230
|
348 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
349 |
|
neuper@37906
|
350 |
val pos = lev_on pos;
|
walther@60230
|
351 |
val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
|
neuper@37906
|
352 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
walther@60230
|
353 |
val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
|
neuper@37906
|
354 |
|
neuper@37906
|
355 |
val pos = lev_up pos;
|
walther@60230
|
356 |
val (pt,pos) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
|
walther@59844
|
357 |
Ctree.get_assumptions pt ([],Res);
|
neuper@37906
|
358 |
|
wneuper@59279
|
359 |
writeln (pr_ctree pr_short pt);
|
neuper@37906
|
360 |
(* aus src.24-11-99:
|
neuper@37906
|
361 |
. sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
|
neuper@37906
|
362 |
1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
|
neuper@37906
|
363 |
1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
|
walther@60242
|
364 |
1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) \<up> 2
|
walther@60242
|
365 |
1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x \<up> 2) )
|
walther@60242
|
366 |
1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x \<up> 2)
|
walther@60242
|
367 |
1.5. sqrt (5 * x + x \<up> 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
|
walther@60242
|
368 |
1.6. sqrt (5 * x + x \<up> 2) = (+2) + x
|
walther@60242
|
369 |
2. 5 * x + x \<up> 2 = ((+2) + x) \<up> 2
|
walther@60242
|
370 |
3. 5 * x + x \<up> 2 = 4 + (4 * x + x \<up> 2) ###12.12.99: indent 2.1. !?!
|
walther@60242
|
371 |
4. 5 * x + x \<up> 2 + (-1) * (4 + (4 * x + x \<up> 2)) = (+0)
|
neuper@37906
|
372 |
5. (-4) + x = (+0)
|
neuper@37906
|
373 |
6. x = (+0) + (-1) * (-4)
|
neuper@37906
|
374 |
*)
|
neuper@37906
|
375 |
|
neuper@37906
|
376 |
(*
|
walther@60340
|
377 |
val t = (Thm.term_of o the o (TermC.parse thy)) "solutions (L::real set)";
|
walther@60230
|
378 |
TermC.atomty t;
|
neuper@37906
|
379 |
*)
|
neuper@37906
|
380 |
|
neuper@37906
|
381 |
|
neuper@37906
|
382 |
(*- 20.9.02: Free_Solve would need the erls (for conditions of rules)
|
neuper@37906
|
383 |
from thy ???, i.e. together with the *_simplify ?!!!? ----------
|
neuper@37906
|
384 |
" _________________ me Free_Solve _________________ ";
|
neuper@37906
|
385 |
" _________________ me Free_Solve _________________ ";
|
neuper@37906
|
386 |
" _________________ me Free_Solve _________________ ";
|
neuper@37906
|
387 |
val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
|
walther@59997
|
388 |
"solveFor x", "errorBound (eps=0)",
|
neuper@37906
|
389 |
"solutions L"(*,
|
neuper@37906
|
390 |
"L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
|
neuper@37906
|
391 |
val (dI',pI',mI') =
|
walther@59997
|
392 |
("Test",["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
393 |
("Test", "sqrt-equ-test"));
|
walther@59926
|
394 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
395 |
(*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*)
|
neuper@37906
|
396 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
397 |
(* val nxt = ("Add_Given",Add_Given "bound_variable x");*)
|
neuper@37906
|
398 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
399 |
(* val nxt = ("Add_Given",Add_Given "error_bound #0");*)
|
neuper@37906
|
400 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
401 |
(* val nxt = ("Add_Find",Add_Find "solutions L"); *)
|
neuper@37906
|
402 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
Walther@60458
|
403 |
(* val nxt = ("Specify_Theory",Specify_Theory "Diff_Appl");
|
neuper@37906
|
404 |
> get_obj g_spec pt (fst p);
|
Walther@60428
|
405 |
val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec*)
|
neuper@37906
|
406 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
407 |
(*val nxt = ("Specify_Problem", Specify_Problem *)
|
neuper@37906
|
408 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
Walther@60458
|
409 |
(*val nxt = ("Specify_Method",Specify_Method ("Diff_Appl", "sqrt-equ-test"));*)
|
neuper@37906
|
410 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
Walther@60458
|
411 |
(*val nxt = ("Apply_Method",Apply_Method ("Diff_Appl", "sqrt-equ-test"));*)
|
neuper@37906
|
412 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
413 |
val nxt = ("Free_Solve",Free_Solve);
|
neuper@37906
|
414 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
415 |
get_obj g_spec pt [];
|
neuper@37906
|
416 |
|
neuper@37906
|
417 |
"--- -2 ---";
|
neuper@37906
|
418 |
get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt;
|
neuper@37906
|
419 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
420 |
me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt;
|
neuper@37906
|
421 |
(* 15.4.
|
neuper@37906
|
422 |
"--- -1 ---";
|
neuper@37906
|
423 |
get_form ("Begin_Trans",Begin_Trans) p pt;
|
neuper@37906
|
424 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
425 |
me ("Begin_Trans",Begin_Trans) p [4] pt; *)
|
neuper@37906
|
426 |
|
neuper@37906
|
427 |
"--- 1 ---";
|
walther@59997
|
428 |
get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
|
neuper@37906
|
429 |
val (p,_,f,nxt,_,pt)=
|
walther@59997
|
430 |
me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p [5] pt;
|
neuper@37906
|
431 |
"--- 2 ---";
|
neuper@37906
|
432 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;
|
neuper@37906
|
433 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
434 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt;
|
neuper@37906
|
435 |
"--- 3 ---";
|
neuper@37906
|
436 |
get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt;
|
neuper@37906
|
437 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
438 |
me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt;
|
neuper@37906
|
439 |
"--- 4 ---";
|
neuper@37906
|
440 |
get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt;
|
neuper@37906
|
441 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
442 |
me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt;
|
neuper@37906
|
443 |
"--- 5 ---";
|
neuper@37906
|
444 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
|
neuper@37906
|
445 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
446 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;
|
neuper@37906
|
447 |
"--- 6 ---";
|
walther@59997
|
448 |
get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
|
neuper@37906
|
449 |
val (p,_,f,nxt,_,pt)=
|
walther@59997
|
450 |
me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p [10] pt;
|
neuper@37906
|
451 |
(* 15.4.
|
neuper@37906
|
452 |
"--- ---";
|
neuper@37906
|
453 |
get_form ("End_Trans",End_Trans) p pt;
|
neuper@37906
|
454 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
455 |
me ("End_Trans",End_Trans) p [11] pt; *)
|
neuper@37906
|
456 |
"--- 7 ---";
|
neuper@37906
|
457 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
|
neuper@37906
|
458 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
459 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt;
|
neuper@37906
|
460 |
"--- 8 ---";
|
neuper@37906
|
461 |
get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt;
|
neuper@37906
|
462 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
463 |
me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt;
|
neuper@37906
|
464 |
"--- 9 ---";
|
neuper@37906
|
465 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
|
neuper@37906
|
466 |
val (p,_,f,nxt,_,pt)=
|
neuper@37906
|
467 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt;
|
neuper@37906
|
468 |
"--- 10 ---.";
|
wneuper@59497
|
469 |
get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p pt;
|
neuper@37906
|
470 |
val (p,_,f,nxt,_,pt)=
|
wneuper@59497
|
471 |
me ("Rewrite_Set",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p [15] pt;
|
neuper@37906
|
472 |
"--- 11 ---";
|
neuper@37906
|
473 |
get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
|
neuper@37906
|
474 |
val ((p,p_),_,f,nxt,_,pt)=
|
neuper@37906
|
475 |
me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
|
neuper@37906
|
476 |
(* 5.4.00.: ---
|
walther@59997
|
477 |
get_form ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) pt;
|
neuper@37906
|
478 |
val (p,_,f,nxt,_,pt)=
|
walther@59997
|
479 |
me ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) [17] pt;
|
neuper@37906
|
480 |
--- *)
|
wneuper@59279
|
481 |
writeln (pr_ctree pr_short pt);
|
neuper@37906
|
482 |
writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
|
neuper@37906
|
483 |
*)
|
neuper@37906
|
484 |
|
neuper@37906
|
485 |
|
neuper@37906
|
486 |
" _________________ me + tacs input _________________ ";
|
neuper@37906
|
487 |
" _________________ me + tacs input _________________ ";
|
neuper@37906
|
488 |
" _________________ me + tacs input _________________ ";
|
neuper@37906
|
489 |
val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
|
walther@59997
|
490 |
"solveFor x", "errorBound (eps=0)",
|
neuper@37906
|
491 |
"solutions L"];
|
neuper@37906
|
492 |
val (dI',pI',mI') =
|
walther@59997
|
493 |
("Test",["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
494 |
["Test", "sqrt-equ-test"]);
|
neuper@37906
|
495 |
"--- s1 ---";
|
neuper@37906
|
496 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
497 |
"--- s1b ---";
|
neuper@37906
|
498 |
val nxt = ("Model_Problem",
|
walther@59997
|
499 |
Model_Problem(*["sqroot-test", "univariate", "equation", "test"]*));
|
neuper@37906
|
500 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
501 |
"--- s2 ---";
|
neuper@37906
|
502 |
val nxt = ("Add_Given",
|
neuper@37906
|
503 |
Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
|
neuper@37906
|
504 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
505 |
"--- s3 ---";
|
neuper@37906
|
506 |
val nxt = ("Add_Given",Add_Given "solveFor x");
|
neuper@37906
|
507 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
508 |
(*"--- s4 ---";
|
neuper@37906
|
509 |
val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
|
neuper@37906
|
510 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
|
neuper@37906
|
511 |
"--- s5 ---";
|
neuper@37906
|
512 |
val nxt = ("Add_Find",Add_Find "solutions L");
|
neuper@37906
|
513 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
514 |
"--- s6 ---";
|
neuper@38058
|
515 |
val nxt = ("Specify_Theory",Specify_Theory "Test");
|
neuper@37906
|
516 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
517 |
"--- s7 ---";
|
neuper@37906
|
518 |
val nxt = ("Specify_Problem",
|
walther@59997
|
519 |
Specify_Problem ["sqroot-test", "univariate", "equation", "test"]);
|
neuper@37906
|
520 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
521 |
"--- s8 ---";
|
walther@59997
|
522 |
val nxt = ("Specify_Method",Specify_Method ["Test", "sqrt-equ-test"]);
|
neuper@37906
|
523 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
524 |
"--- s9 ---";
|
walther@59997
|
525 |
val nxt = ("Apply_Method",Apply_Method ["Test", "sqrt-equ-test"]);
|
neuper@37906
|
526 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
527 |
"--- 1 ---";
|
walther@59997
|
528 |
val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
|
neuper@37906
|
529 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
530 |
|
neuper@37906
|
531 |
(*.9.6.03
|
walther@60230
|
532 |
val t = TermC.str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
|
neuper@37926
|
533 |
val SOME (t',asm) = rewrite_set_ thy false rls t;
|
walther@59868
|
534 |
UnparseC.term t';
|
walther@60330
|
535 |
Rewrite.trace_on:=false; (*true false*)
|
neuper@37906
|
536 |
*)
|
neuper@37906
|
537 |
|
neuper@37906
|
538 |
(*me------------
|
neuper@37906
|
539 |
val (mI,m) = nxt; val pos' as (p,p_) = p;
|
neuper@37906
|
540 |
|
walther@59922
|
541 |
val Applicable.Yes m = Step.check m (pt, (p,p_));
|
neuper@37906
|
542 |
(*solve*)
|
neuper@37906
|
543 |
val pp = par_pblobj pt p;
|
neuper@37906
|
544 |
val metID = get_obj g_metID pt pp;
|
Walther@60558
|
545 |
val sc = (#scr o MethodC.from_store_PIDE ctxt) metID;
|
walther@59807
|
546 |
val is = get_istate_LI pt (p,p_);
|
neuper@37906
|
547 |
val thy' = get_obj g_domID pt pp;
|
walther@59881
|
548 |
val thy = ThyC.get_theory thy';
|
walther@59852
|
549 |
val d = Rule_Set.empty;
|
neuper@37906
|
550 |
val Steps [(m',f',pt',p',c',s')] =
|
wneuper@59559
|
551 |
locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
|
walther@59807
|
552 |
val is' = get_istate_LI pt' p';
|
walther@59791
|
553 |
LI.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
|
neuper@37906
|
554 |
|
neuper@37906
|
555 |
|
neuper@37906
|
556 |
|
neuper@37906
|
557 |
|
walther@60230
|
558 |
val ttt = (Thm.term_of o the o (TermC.parse Test.thy))
|
neuper@37981
|
559 |
"Let (((While contains_root e_e Do\
|
walther@59637
|
560 |
\Rewrite square_equation_left #>\
|
walther@59637
|
561 |
\Try (Rewrite_Set Test_simplify) #>\
|
walther@59637
|
562 |
\Try (Rewrite_Set rearrange_assoc) #>\
|
walther@59637
|
563 |
\Try (Rewrite_Set Test_simplify)) #>\
|
walther@59637
|
564 |
\Try (Rewrite_Set norm_equation) #>\
|
walther@59637
|
565 |
\Try (Rewrite_Set Test_simplify) #>\
|
walther@59637
|
566 |
\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv #>\
|
walther@59635
|
567 |
\Try (Rewrite_Set Test_simplify))\
|
neuper@37906
|
568 |
\e_)";
|
neuper@37906
|
569 |
|
neuper@37906
|
570 |
-------------------------*)
|
neuper@37906
|
571 |
|
neuper@37906
|
572 |
|
neuper@37906
|
573 |
"--- 2 ---";
|
neuper@37906
|
574 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
neuper@37906
|
575 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
576 |
"--- 3 ---";
|
neuper@37906
|
577 |
val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
|
neuper@37906
|
578 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
579 |
"--- 4 ---";
|
neuper@37906
|
580 |
val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");
|
neuper@37906
|
581 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
582 |
"--- 5 ---";
|
neuper@37906
|
583 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
neuper@37906
|
584 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
585 |
"--- 6 ---";
|
walther@59997
|
586 |
val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
|
neuper@37906
|
587 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
588 |
"--- 7 ---";
|
neuper@37906
|
589 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
neuper@37906
|
590 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
591 |
"--- 8<> ---";
|
neuper@37906
|
592 |
val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
|
neuper@37906
|
593 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
594 |
"--- 9<> ---";
|
neuper@37906
|
595 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
neuper@37906
|
596 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
597 |
"--- 10<> ---";
|
neuper@37906
|
598 |
val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
|
neuper@37906
|
599 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
600 |
"--- 11<> ---.";
|
neuper@37906
|
601 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
neuper@37906
|
602 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
603 |
"--- 12<> ---";
|
wneuper@59497
|
604 |
val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv"));
|
neuper@37906
|
605 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
606 |
"--- 13<> ---";
|
neuper@37906
|
607 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
neuper@37906
|
608 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
609 |
"--- 1<> ---";
|
walther@59997
|
610 |
val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test", "univariate", "equation", "test"]);
|
neuper@37906
|
611 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
612 |
(* val nxt = ("End_Proof'",End_Proof');*)
|
walther@59959
|
613 |
if f <> (Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
|
neuper@38031
|
614 |
then error "root-equ.sml: diff.behav. in me + tacs input"
|
neuper@37906
|
615 |
else ();
|
neuper@37906
|
616 |
|
wneuper@59279
|
617 |
writeln (pr_ctree pr_short pt);
|
walther@59868
|
618 |
writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^
|
neuper@37906
|
619 |
"\n==============================================================");
|
neuper@37906
|
620 |
|