akargl@42181
|
1 |
(* Title: test for rewtools.sml
|
neuper@37906
|
2 |
authors: Walther Neuper 2000, 2006
|
neuper@37906
|
3 |
*)
|
neuper@37906
|
4 |
|
neuper@38061
|
5 |
"--------------------------------------------------------";
|
neuper@38061
|
6 |
"--------------------------------------------------------";
|
neuper@38061
|
7 |
"table of contents --------------------------------------";
|
neuper@38061
|
8 |
"--------------------------------------------------------";
|
neuper@48895
|
9 |
(*============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! =================
|
neuper@42399
|
10 |
"----------- fun make_isab ------------------------------";
|
neuper@38061
|
11 |
"----------- fun collect_isab_thys ----------------------";
|
neuper@48895
|
12 |
============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ===============*)
|
neuper@38061
|
13 |
"----------- fun thy_containing_rls ---------------------";
|
neuper@38061
|
14 |
"----------- fun thy_containing_cal ---------------------";
|
neuper@42407
|
15 |
(*============ inhibit exn WN120321 ==============================================
|
neuper@38061
|
16 |
"----------- initContext Thy_ Integration-demo ----------";
|
neuper@38061
|
17 |
"----------- initContext..Thy_, fun context_thm ---------";
|
neuper@38061
|
18 |
"----------- initContext..Thy_, fun context_rls ---------";
|
neuper@38061
|
19 |
"----------- checkContext..Thy_, fun context_thy --------";
|
neuper@38061
|
20 |
"----------- checkContext..Thy_, fun context_rls --------";
|
neuper@38061
|
21 |
"----------- checkContext..Thy_ on last formula ---------";
|
neuper@38061
|
22 |
"----------- fun guh2theID ------------------------------";
|
neuper@38061
|
23 |
"----------- debugging on Tests/solve_linear_as_rootpbl -";
|
neuper@38061
|
24 |
"--------------------------------------------------------";
|
neuper@38061
|
25 |
"----------- fun string_of_thmI for_[.]_) ---------------";
|
neuper@38061
|
26 |
"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
|
neuper@38061
|
27 |
"--------------------------------------------------------";
|
neuper@38061
|
28 |
"----------- fun filter_appl_rews -----------------------";
|
neuper@38061
|
29 |
"----------- fun is_contained_in ------------------------";
|
neuper@42407
|
30 |
============ inhibit exn WN120321 ==============================================*)
|
neuper@42433
|
31 |
"-------- build fun get_bdv_subst --------------------------------";
|
neuper@38061
|
32 |
"--------------------------------------------------------";
|
neuper@38061
|
33 |
"--------------------------------------------------------";
|
neuper@37906
|
34 |
|
neuper@42399
|
35 |
"----------- fun make_isab ------------------------------";
|
neuper@42399
|
36 |
"----------- fun make_isab ------------------------------";
|
neuper@42407
|
37 |
(*============ inhibit exn WN120321 ==============================================
|
neuper@42399
|
38 |
"----------- fun make_isab ------------------------------";
|
neuper@42399
|
39 |
(* rlsthmsNOTisac: contains thms in rls requested from Isabelle ---" *)
|
neuper@42400
|
40 |
map #1 (rlsthmsNOTisac : (string * term) list) = (*WN101011, Isabelle2009-2*)
|
neuper@38061
|
41 |
["refl", "o_apply", "del_base", "del_rec", "LENGTH_CONS", "LENGTH_NIL",
|
neuper@38061
|
42 |
"list_diff_def", "take_Nil", "take_Cons", "if_True", "if_False",
|
neuper@52062
|
43 |
"sym_real_mult_minus1", "distrib_right", "distrib_left",
|
neuper@38061
|
44 |
"sym_realpow_twoI", "sym_realpow_addI", "mult_1_right",
|
neuper@38061
|
45 |
"sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right",
|
neuper@48763
|
46 |
"add_0_left", "add_0_right", "divide_zero_left", "sym_mult_assoc",
|
neuper@48764
|
47 |
"order_refl", "minus_minus", "mult_commute", "mult_assoc",
|
neuper@38061
|
48 |
"add_commute", "add_left_commute", "add_assoc", "minus_mult_left",
|
neuper@38061
|
49 |
"right_minus", "sym_add_assoc", "left_diff_distrib",
|
neuper@38061
|
50 |
"right_diff_distrib", "minus_divide_left", "times_divide_eq_right",
|
neuper@38061
|
51 |
"times_divide_eq_left", "divide_divide_eq_left",
|
neuper@38061
|
52 |
"divide_divide_eq_right", "divide_1", "add_divide_distrib",
|
neuper@38061
|
53 |
"sym_rmult_assoc"];
|
neuper@42399
|
54 |
if length rlsthmsNOTisac > 34 then ()
|
neuper@38061
|
55 |
else error "rewtools.sml: some rlsthmsNOTisac dropped";
|
neuper@37906
|
56 |
|
neuper@42399
|
57 |
"----- FIXME.WN11xxxx: rlsthmsNOTisac DOES contain thms from isac ---";
|
neuper@42400
|
58 |
map (thmID_of_derivation_name o #1) rlsthmsNOTisac;
|
neuper@42399
|
59 |
"----- FIXME.WN11xxxx: sym_* in rlsthmsNOTisac DOES contain thms from isac ---";
|
neuper@38062
|
60 |
val symthms = [("real_mult_minus1", @{thm real_mult_minus1}),
|
neuper@38062
|
61 |
("realpow_twoI", @{thm realpow_twoI}),
|
neuper@38062
|
62 |
("realpow_addI", @{thm realpow_addI}),
|
neuper@38062
|
63 |
("real_mult_2", @{thm real_mult_2}),
|
neuper@48763
|
64 |
("mult_assoc", @{thm mult_assoc}),
|
neuper@38062
|
65 |
("add_assoc", @{thm add_assoc}),
|
neuper@38062
|
66 |
("rmult_assoc", @{thm rmult_assoc})];
|
neuper@38062
|
67 |
map (Thm.derivation_name o #2) symthms;
|
neuper@37906
|
68 |
|
neuper@38061
|
69 |
"----------- fun collect_isab_thys ----------------------";
|
neuper@38061
|
70 |
"----------- fun collect_isab_thys ----------------------";
|
neuper@38061
|
71 |
"----------- fun collect_isab_thys ----------------------";
|
akargl@42108
|
72 |
val ancestors = Theory.ancestors_of @{theory "Complex_Main"};
|
neuper@38061
|
73 |
val isabthms = (flat o (map Theory.axioms_of)) ancestors;
|
neuper@38061
|
74 |
|
neuper@52156
|
75 |
val isacrules = (flat o (map (thms_of_rls o #2 o #2)))
|
s1210629013@55359
|
76 |
(Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
|
neuper@37906
|
77 |
(*thms from rulesets*)
|
akargl@42181
|
78 |
(*=== inhibit exn AK110725 =============================================================
|
neuper@37906
|
79 |
val isacrlsthms = ((map rep_thm_G') o flat o
|
neuper@52156
|
80 |
(map (PureThy.all_thms_of_rls o #2 o #2)))
|
s1210629013@55359
|
81 |
(Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
|
neuper@37906
|
82 |
length isacrlsthms;
|
neuper@37906
|
83 |
(*takes a few seconds...
|
neuper@37906
|
84 |
val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
|
neuper@37906
|
85 |
length isacrlsthms;
|
neuper@37906
|
86 |
"----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv";
|
neuper@37906
|
87 |
print_depth 99; map #1 isacrlsthms; print_depth 3;
|
neuper@37906
|
88 |
"----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";
|
neuper@37906
|
89 |
...*)
|
neuper@37906
|
90 |
|
akargl@42181
|
91 |
|
neuper@37906
|
92 |
(!theory');
|
neuper@37906
|
93 |
map #2 (!theory');
|
neuper@37936
|
94 |
map (PureThy.all_thms_of o #2) (!theory');
|
neuper@37936
|
95 |
val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');
|
neuper@37906
|
96 |
(*takes a few seconds...
|
neuper@37906
|
97 |
val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
|
neuper@37906
|
98 |
length rlsthmsNOTisac;
|
neuper@37906
|
99 |
"----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv";
|
neuper@37906
|
100 |
print_depth 99; map #1 rlsthmsNOTisac; print_depth 3;
|
neuper@37906
|
101 |
"----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^";
|
neuper@37906
|
102 |
...*)
|
neuper@37906
|
103 |
|
neuper@37906
|
104 |
"----- for 'fun make_isab_thm_thy'";
|
neuper@37936
|
105 |
inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors));
|
neuper@37936
|
106 |
inter eq_thmI;
|
neuper@37936
|
107 |
(inter eq_thmI);
|
neuper@37936
|
108 |
(inter eq_thmI) isacrlsthms;
|
neuper@37906
|
109 |
(*takes a few seconds...
|
neuper@37936
|
110 |
curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors));
|
neuper@37906
|
111 |
|
neuper@37906
|
112 |
val thy = (nth 52 ancestors);
|
neuper@37936
|
113 |
val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors);
|
neuper@37936
|
114 |
length (PureThy.all_thms_of (nth 9 ancestors));
|
neuper@37906
|
115 |
length sec;
|
neuper@37906
|
116 |
...*)
|
neuper@37906
|
117 |
(*takes 1 minute...
|
neuper@37906
|
118 |
print_depth 99;
|
neuper@37936
|
119 |
map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;
|
neuper@37906
|
120 |
print_depth 3;
|
neuper@37906
|
121 |
*)
|
neuper@37906
|
122 |
|
neuper@37906
|
123 |
(*takes some seconds...
|
neuper@37906
|
124 |
val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac)))
|
neuper@37906
|
125 |
((#ancestors o rep_theory) first_isac_thy);
|
neuper@37906
|
126 |
print_depth 99; isab_thm_thy; print_depth 3;
|
neuper@37906
|
127 |
*)
|
akargl@42181
|
128 |
=== inhibit exn AK110725 =============================================================*)
|
neuper@42407
|
129 |
============ inhibit exn WN120321 ==============================================*)
|
neuper@37906
|
130 |
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
|
neuper@38061
|
133 |
"----------- fun thy_containing_rls ---------------------";
|
neuper@38061
|
134 |
"----------- fun thy_containing_rls ---------------------";
|
neuper@38061
|
135 |
"----------- fun thy_containing_rls ---------------------";
|
neuper@42407
|
136 |
infix mem; (*from Isabelle2002*)
|
neuper@42407
|
137 |
fun x mem [] = false
|
neuper@42407
|
138 |
| x mem (y :: ys) = x = y orelse x mem ys;
|
neuper@42407
|
139 |
|
neuper@38058
|
140 |
val thy' = "Biegelinie";
|
neuper@42407
|
141 |
val dropthys =
|
neuper@42407
|
142 |
takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
|
neuper@42407
|
143 |
(rev (!theory'));
|
neuper@42407
|
144 |
|
neuper@48891
|
145 |
(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
|
neuper@37906
|
146 |
if length (!theory') <> length dropthys then ()
|
neuper@42407
|
147 |
else error "thy_containing_rls changed 1";
|
neuper@37906
|
148 |
|
neuper@42407
|
149 |
val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;
|
neuper@38061
|
150 |
|
neuper@42407
|
151 |
if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"](*, "Biegelinie",..,"Test",.*)
|
neuper@42407
|
152 |
then () else error "thy_containing_rls changed ancestors_rls";
|
neuper@42407
|
153 |
|
neuper@42407
|
154 |
"Isac" mem dropthys';
|
neuper@42407
|
155 |
op mem ("Isac", dropthys');
|
neuper@37906
|
156 |
(op mem) o swap;
|
neuper@42407
|
157 |
((op mem) o swap) (dropthys', "Isac");
|
neuper@37906
|
158 |
curry ((op mem) o swap);
|
neuper@42407
|
159 |
curry ((op mem) o swap) dropthys' "Isac";
|
neuper@42407
|
160 |
val ancestors_rls =
|
neuper@42407
|
161 |
filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
|
s1210629013@55359
|
162 |
(rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
|
neuper@37906
|
163 |
|
neuper@42407
|
164 |
take (10, map #1 ancestors_rls) =
|
neuper@42407
|
165 |
["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation",
|
neuper@42407
|
166 |
"matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)
|
neuper@42407
|
167 |
|
neuper@42433
|
168 |
(* WN120523 popped up again ?!?!?
|
s1210629013@55359
|
169 |
if length (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then ()
|
neuper@42407
|
170 |
else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";
|
neuper@42433
|
171 |
*)
|
akargl@42181
|
172 |
|
neuper@37906
|
173 |
val rls' = "norm_Poly";
|
neuper@42407
|
174 |
case assoc (ancestors_rls, rls') of
|
neuper@37926
|
175 |
SOME (thy', _) => thyID2theory' thy'
|
neuper@42407
|
176 |
| _ => error ("thy_containing_rls : rls '" ^ rls' ^
|
neuper@42407
|
177 |
"' not in !rulset' und thy '" ^ thy' ^ "'");
|
neuper@37906
|
178 |
|
neuper@38058
|
179 |
if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly") then ()
|
neuper@42407
|
180 |
else error "thy_containing_rls 3: changed with (Biegelinie, norm_Poly)";
|
neuper@42407
|
181 |
|
neuper@42407
|
182 |
"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie" ,"norm_Poly");
|
neuper@42407
|
183 |
val rls' = strip_thy rls'
|
neuper@42407
|
184 |
val thy' = thyID2theory' thy'
|
neuper@42407
|
185 |
val dropthys =
|
neuper@42407
|
186 |
takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
|
neuper@42407
|
187 |
(rev (!theory'));
|
neuper@42407
|
188 |
|
neuper@42407
|
189 |
map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"]; (*= true WN120410*)
|
neuper@42407
|
190 |
|
neuper@42407
|
191 |
val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
|
neuper@42407
|
192 |
val ancestors_rls =
|
neuper@42407
|
193 |
filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
|
s1210629013@55359
|
194 |
(rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));
|
neuper@42407
|
195 |
|
neuper@42407
|
196 |
case assoc (ancestors_rls, rls') of
|
neuper@42407
|
197 |
SOME ("Poly", Seq {id = "norm_Poly", ...}) => ()
|
neuper@42407
|
198 |
| _ => error "thy_containing_rls changed 2";
|
neuper@48891
|
199 |
============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
|
neuper@37906
|
200 |
|
neuper@37906
|
201 |
|
neuper@38061
|
202 |
"----------- fun thy_containing_cal ---------------------";
|
neuper@38061
|
203 |
"----------- fun thy_containing_cal ---------------------";
|
neuper@38061
|
204 |
"----------- fun thy_containing_cal ---------------------";
|
neuper@38058
|
205 |
val thy' = "Atools";
|
neuper@42407
|
206 |
val dropthys =
|
neuper@42407
|
207 |
takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
|
neuper@42407
|
208 |
(rev (!theory'));
|
neuper@42407
|
209 |
|
neuper@37906
|
210 |
length dropthys <> length (!theory');
|
neuper@42407
|
211 |
|
neuper@42407
|
212 |
val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;
|
neuper@42407
|
213 |
|
neuper@48891
|
214 |
(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
|
neuper@42407
|
215 |
if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie",
|
neuper@42407
|
216 |
"Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate",
|
neuper@42407
|
217 |
"Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq",
|
neuper@42407
|
218 |
"LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*)
|
neuper@42407
|
219 |
then () else error "thy_containing_cal changed ancestors_rls for Atools";
|
neuper@37906
|
220 |
|
s1210629013@55359
|
221 |
Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev;
|
s1210629013@55359
|
222 |
Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map #1;
|
s1210629013@55359
|
223 |
Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string);
|
neuper@37906
|
224 |
|
neuper@42407
|
225 |
val ancestors_cal =
|
neuper@42407
|
226 |
filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
|
s1210629013@55359
|
227 |
(Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev);
|
neuper@42407
|
228 |
|
neuper@42409
|
229 |
if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "plus")
|
neuper@42409
|
230 |
(*WN120410: SHOULD BE = ("IsacKnowledge", "Atools")*)
|
neuper@42409
|
231 |
then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed";
|
neuper@48891
|
232 |
============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
|
neuper@42407
|
233 |
|
neuper@38061
|
234 |
"----------- initContext Thy_ Integration-demo ----------";
|
neuper@38061
|
235 |
"----------- initContext Thy_ Integration-demo ----------";
|
neuper@38061
|
236 |
"----------- initContext Thy_ Integration-demo ----------";
|
neuper@37906
|
237 |
states:=[];
|
neuper@37906
|
238 |
CalcTree
|
neuper@37906
|
239 |
[(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
|
neuper@38058
|
240 |
("Integrate",["integrate","function"],
|
neuper@37906
|
241 |
["diff","integration"]))];
|
neuper@37906
|
242 |
Iterator 1;
|
neuper@37906
|
243 |
moveActiveRoot 1;
|
neuper@37906
|
244 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
245 |
interSteps 1 ([1],Res);
|
neuper@37906
|
246 |
interSteps 1 ([1,1],Res);
|
neuper@37906
|
247 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
248 |
if existpt' ([1,1,1], Frm) pt then ()
|
neuper@38031
|
249 |
else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
|
neuper@37906
|
250 |
initContext 1 Thy_ ([1,1,1], Frm);
|
neuper@37906
|
251 |
|
neuper@38061
|
252 |
"----------- initContext..Thy_, fun context_thm ---------";
|
neuper@38061
|
253 |
"----------- initContext..Thy_, fun context_thm ---------";
|
neuper@38061
|
254 |
"----------- initContext..Thy_, fun context_thm ---------";
|
neuper@41970
|
255 |
states:=[]; (*start of calculation, return No.1*)
|
neuper@41970
|
256 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
257 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
258 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
259 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
260 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
261 |
|
neuper@37906
|
262 |
"----- no thy-context at result -----";
|
neuper@37906
|
263 |
val p = ([], Res);
|
neuper@37906
|
264 |
initContext 1 Thy_ p;
|
neuper@37906
|
265 |
|
neuper@37906
|
266 |
interSteps 1 ([2], Res);
|
neuper@37906
|
267 |
interSteps 1 ([3,1], Res);
|
neuper@37906
|
268 |
val ((pt,_),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
269 |
|
neuper@37906
|
270 |
val p = ([2,4], Res);
|
neuper@37906
|
271 |
val tac = Rewrite ("radd_left_commute","");
|
neuper@48892
|
272 |
(*============ inhibit exn WN120321 ==============================================
|
neuper@37906
|
273 |
initContext 1 Thy_ p;
|
neuper@37906
|
274 |
(*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
|
neuper@37906
|
275 |
--- in initContext..Thy_ ---*)
|
neuper@37906
|
276 |
val ContThm {thm,result,...} = context_thy (pt,p) tac;
|
neuper@48892
|
277 |
(*WN130621: thm = "thy_isac_WN120320: AT Isa2009-2-->11 BROKEN": guh !!!!!!!!!!!!!!!!!!!!!!!!!*)
|
neuper@37906
|
278 |
if thm = "thy_isac_Test-thm-radd_left_commute"
|
neuper@37906
|
279 |
andalso term2str result = "-2 + (1 + x) = 0" then ()
|
neuper@38031
|
280 |
else error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";
|
neuper@37906
|
281 |
|
akargl@42108
|
282 |
|
neuper@37906
|
283 |
val p = ([3,1,1], Frm);
|
neuper@37906
|
284 |
val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));
|
neuper@37906
|
285 |
initContext 1 Thy_ p;
|
neuper@37906
|
286 |
(*Frm->Res, Rewrite_Inst "risolate_bdv_add" -1 + x = 0 -> x = 0 + -1 * -1
|
neuper@37906
|
287 |
--- in initContext..Thy_ ---*)
|
neuper@37906
|
288 |
val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
|
neuper@37906
|
289 |
if thm = "thy_isac_Test-thm-risolate_bdv_add"
|
neuper@37906
|
290 |
andalso term2str result = "x = 0 + -1 * -1" then ()
|
neuper@38031
|
291 |
else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
|
neuper@37906
|
292 |
|
neuper@37906
|
293 |
initContext 1 Thy_ ([2,5], Res);
|
neuper@37906
|
294 |
(*Res->Res, Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
|
neuper@37906
|
295 |
--- in initContext..Thy_ ---*)
|
neuper@37906
|
296 |
|
neuper@37906
|
297 |
|
neuper@38061
|
298 |
"----------- initContext..Thy_, fun context_rls ---------";
|
neuper@38061
|
299 |
"----------- initContext..Thy_, fun context_rls ---------";
|
neuper@38061
|
300 |
"----------- initContext..Thy_, fun context_rls ---------";
|
neuper@37906
|
301 |
(*using pt from above*)
|
neuper@37906
|
302 |
val p = ([1], Res);
|
neuper@37906
|
303 |
val tac = Rewrite_Set "Test_simplify";
|
neuper@37906
|
304 |
initContext 1 Thy_ p;
|
neuper@37906
|
305 |
(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
|
neuper@37906
|
306 |
--- in initContext..Thy_ ---*)
|
neuper@37906
|
307 |
val ContRls {rls,result,...} = context_thy (pt,p) tac;
|
neuper@37906
|
308 |
if rls = "thy_isac_Test-rls-Test_simplify"
|
neuper@37906
|
309 |
andalso term2str result = "-1 + x = 0" then ()
|
neuper@38031
|
310 |
else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
|
neuper@37906
|
311 |
|
neuper@37906
|
312 |
val p = ([3,1], Frm);
|
neuper@37906
|
313 |
val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
|
neuper@37906
|
314 |
initContext 1 Thy_ p;
|
neuper@37906
|
315 |
(*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
|
neuper@37906
|
316 |
--- in initContext..Thy_ ---*)
|
neuper@37906
|
317 |
val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
|
neuper@37906
|
318 |
if rls = "thy_isac_Test-rls-isolate_bdv"
|
neuper@37906
|
319 |
andalso term2str result = "x = 0 + -1 * -1" then ()
|
neuper@38031
|
320 |
else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
|
neuper@37906
|
321 |
|
neuper@38061
|
322 |
"----------- checkContext..Thy_, fun context_thy --------";
|
neuper@38061
|
323 |
"----------- checkContext..Thy_, fun context_thy --------";
|
neuper@38061
|
324 |
"----------- checkContext..Thy_, fun context_thy --------";
|
neuper@37906
|
325 |
(*using pt from above*)
|
neuper@37906
|
326 |
|
neuper@37906
|
327 |
val p = ([2,4], Res);
|
neuper@37906
|
328 |
val tac = Rewrite ("radd_left_commute","");
|
neuper@37906
|
329 |
checkContext 1 p "thy_Test-thm-radd_left_commute";
|
neuper@37906
|
330 |
(* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
|
neuper@37906
|
331 |
--- in checkContext..Thy_ ---*)
|
neuper@37906
|
332 |
val ContThm {thm,result,...} = context_thy (pt,p) tac;
|
neuper@37906
|
333 |
if thm = "thy_isac_Test-thm-radd_left_commute"
|
neuper@37906
|
334 |
andalso term2str result = "-2 + (1 + x) = 0" then ()
|
neuper@38031
|
335 |
else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
|
neuper@37906
|
336 |
|
neuper@37906
|
337 |
val p = ([3,1,1], Frm);
|
neuper@37906
|
338 |
val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));
|
neuper@37906
|
339 |
checkContext 1 p "thy_Test-thm-risolate_bdv_add";
|
neuper@37906
|
340 |
(* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
|
neuper@37906
|
341 |
--- in checkContext..Thy_ ---*)
|
neuper@37906
|
342 |
val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
|
neuper@37906
|
343 |
if thm = "thy_isac_Test-thm-risolate_bdv_add"
|
neuper@37906
|
344 |
andalso term2str result = "x = 0 + -1 * -1" then ()
|
neuper@38031
|
345 |
else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
|
neuper@37906
|
346 |
|
neuper@37906
|
347 |
val p = ([2,5], Res);
|
neuper@37906
|
348 |
val tac = Calculate "plus";
|
neuper@37906
|
349 |
(*checkContext..Thy_ 1 ([2,5], Res);*)
|
neuper@37906
|
350 |
(*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
|
neuper@37906
|
351 |
checkContext 1 p ;
|
neuper@37906
|
352 |
(* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
|
neuper@37906
|
353 |
--- in checkContext..Thy_ ---*)
|
neuper@37906
|
354 |
|
neuper@38061
|
355 |
"----------- checkContext..Thy_, fun context_rls --------";
|
neuper@38061
|
356 |
"----------- checkContext..Thy_, fun context_rls --------";
|
neuper@38061
|
357 |
"----------- checkContext..Thy_, fun context_rls --------";
|
neuper@37906
|
358 |
(*using pt from above*)
|
neuper@37906
|
359 |
show_pt pt;
|
neuper@37906
|
360 |
|
neuper@37906
|
361 |
val p = ([1], Res);
|
neuper@37906
|
362 |
val tac = Rewrite_Set "Test_simplify";
|
neuper@37906
|
363 |
checkContext 1 p "thy_isac_Test-rls-Test_simplify";
|
neuper@37906
|
364 |
(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
|
neuper@37906
|
365 |
--- in checkContext..Thy_ ---*)
|
neuper@37906
|
366 |
val ContRls {rls,result,...} = context_thy (pt,p) tac;
|
neuper@37906
|
367 |
if rls = "thy_isac_Test-rls-Test_simplify"
|
neuper@37906
|
368 |
andalso term2str result = "-1 + x = 0" then ()
|
neuper@38031
|
369 |
else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
|
neuper@37906
|
370 |
|
neuper@37906
|
371 |
val p = ([3,1], Frm);
|
neuper@37906
|
372 |
val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
|
neuper@37906
|
373 |
checkContext 1 p "thy_Test-rls-isolate_bdv";
|
neuper@37906
|
374 |
val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
|
neuper@37906
|
375 |
if rls = "thy_isac_Test-rls-isolate_bdv"
|
neuper@37906
|
376 |
andalso term2str result = "x = 0 + -1 * -1" then ()
|
neuper@38031
|
377 |
else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
|
neuper@37906
|
378 |
|
neuper@38061
|
379 |
"----------- checkContext..Thy_ on last formula ---------";
|
neuper@38061
|
380 |
"----------- checkContext..Thy_ on last formula ---------";
|
neuper@38061
|
381 |
"----------- checkContext..Thy_ on last formula ---------";
|
neuper@41970
|
382 |
states:=[]; (*start of calculation, return No.1*)
|
neuper@41970
|
383 |
CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
|
neuper@41970
|
384 |
("Test", ["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
385 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
386 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
387 |
|
neuper@37906
|
388 |
autoCalculate 1 CompleteCalcHead;
|
neuper@37906
|
389 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
390 |
val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
|
neuper@37906
|
391 |
initContext 1 Thy_ ([1], Frm);
|
neuper@37906
|
392 |
checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
|
neuper@37906
|
393 |
|
neuper@37906
|
394 |
autoCalculate 1 (Step 1);
|
neuper@37906
|
395 |
val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
|
neuper@37906
|
396 |
initContext 1 Thy_ ([1], Res);
|
neuper@37906
|
397 |
checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
|
neuper@37906
|
398 |
|
neuper@48892
|
399 |
============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
|
neuper@48892
|
400 |
|
neuper@37906
|
401 |
|
neuper@38061
|
402 |
"----------- fun guh2theID ------------------------------";
|
neuper@38061
|
403 |
"----------- fun guh2theID ------------------------------";
|
neuper@38061
|
404 |
"----------- fun guh2theID ------------------------------";
|
akargl@42181
|
405 |
|
neuper@37906
|
406 |
val guh = "thy_scri_ListG-thm-zip_Nil";
|
neuper@52101
|
407 |
print_depth 3; (*999*)
|
akargl@42181
|
408 |
take_fromto 1 4 (Symbol.explode guh);
|
akargl@42181
|
409 |
take_fromto 5 9 (Symbol.explode guh);
|
akargl@42181
|
410 |
val rest = takerest (9,(Symbol.explode guh));
|
neuper@37906
|
411 |
|
neuper@37906
|
412 |
separate "-" rest;
|
neuper@37906
|
413 |
space_implode "-" rest;
|
neuper@37906
|
414 |
commas rest;
|
neuper@37906
|
415 |
|
neuper@37906
|
416 |
val delim = "-";
|
neuper@37906
|
417 |
val thyID = takewhile [] (not o (curry op= delim)) rest;
|
neuper@37906
|
418 |
val rest' = dropuntil (curry op= delim) rest;
|
neuper@37906
|
419 |
val setc = take_fromto 1 5 rest';
|
neuper@37906
|
420 |
val xstr = takerest (5, rest');
|
neuper@37906
|
421 |
|
neuper@37906
|
422 |
if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
|
neuper@38031
|
423 |
else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
|
neuper@37906
|
424 |
|
neuper@37906
|
425 |
|
neuper@38061
|
426 |
"----------- debugging on Tests/solve_linear_as_rootpbl -";
|
neuper@38061
|
427 |
"----------- debugging on Tests/solve_linear_as_rootpbl -";
|
neuper@38061
|
428 |
"----------- debugging on Tests/solve_linear_as_rootpbl -";
|
akargl@42108
|
429 |
"----- initContext -----";
|
neuper@37906
|
430 |
states:=[];
|
neuper@37906
|
431 |
CalcTree
|
neuper@42124
|
432 |
[(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
|
neuper@38058
|
433 |
("Test",
|
neuper@55279
|
434 |
["LINEAR","univariate","equation","test"],
|
neuper@37906
|
435 |
["Test","solve_linear"]))];
|
neuper@37906
|
436 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
437 |
autoCalculate 1 CompleteCalcHead;
|
neuper@37906
|
438 |
|
neuper@37906
|
439 |
autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
|
neuper@37906
|
440 |
if is_curr_endof_calc pt ([1],Frm) then ()
|
neuper@38031
|
441 |
else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
|
neuper@37906
|
442 |
|
neuper@37906
|
443 |
autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
|
akargl@42125
|
444 |
|
neuper@37906
|
445 |
if not (is_curr_endof_calc pt ([1],Frm)) then ()
|
neuper@38031
|
446 |
else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
|
neuper@37906
|
447 |
if is_curr_endof_calc pt ([1],Res) then ()
|
neuper@38031
|
448 |
else error "rewtools.sml is_curr_endof_calc ([1],Res)";
|
neuper@37906
|
449 |
|
neuper@37906
|
450 |
initContext 1 Thy_ ([1],Res);
|
neuper@37906
|
451 |
|
neuper@37906
|
452 |
"----- checkContext -----";
|
neuper@37906
|
453 |
states:=[];
|
neuper@37906
|
454 |
CalcTree
|
neuper@42124
|
455 |
[(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
|
neuper@38058
|
456 |
("Test",
|
neuper@55279
|
457 |
["LINEAR","univariate","equation","test"],
|
neuper@37906
|
458 |
["Test","solve_linear"]))];
|
neuper@37906
|
459 |
Iterator 1; moveActiveRoot 1;
|
neuper@37906
|
460 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
461 |
interSteps 1 ([1],Res);
|
akargl@42108
|
462 |
|
neuper@37906
|
463 |
val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
|
neuper@37906
|
464 |
checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
|
neuper@37906
|
465 |
|
neuper@37906
|
466 |
interSteps 1 ([2],Res);
|
neuper@37906
|
467 |
val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
|
neuper@37906
|
468 |
|
neuper@37906
|
469 |
checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
|
neuper@37906
|
470 |
checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
|
neuper@37906
|
471 |
|
akargl@42125
|
472 |
|
neuper@38061
|
473 |
"----------- fun string_of_thmI for_[.]_) ---------------";
|
neuper@38061
|
474 |
"----------- fun string_of_thmI for_[.]_) ---------------";
|
neuper@38061
|
475 |
"----------- fun string_of_thmI for_[.]_) ---------------";
|
neuper@37906
|
476 |
"----- these work ?!?";
|
akargl@42181
|
477 |
(*========== inhibit exn 110718 ================================================
|
akargl@42181
|
478 |
(* ERROR: constructor real_minus_eq_cancel has not been declared *)
|
neuper@37906
|
479 |
val th = sym_thm real_minus_eq_cancel;
|
neuper@37906
|
480 |
val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
|
akargl@42181
|
481 |
val th'= mk_thm ( @{theory "Isac"} ) ((de_quote o string_of_thm) real_minus_eq_cancel);
|
akargl@42181
|
482 |
val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm) real_minus_eq_cancel);
|
neuper@37906
|
483 |
|
neuper@37906
|
484 |
"----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
|
neuper@37906
|
485 |
val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
|
neuper@37906
|
486 |
val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
|
neuper@37906
|
487 |
applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
|
neuper@37906
|
488 |
"- compose stac as done in | appy (*leaf*) by handle_leaf";
|
akargl@42108
|
489 |
|
neuper@37906
|
490 |
val (th, sr, E, a, v, t) =
|
neuper@38058
|
491 |
("Biegelinie",
|
neuper@37906
|
492 |
(#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],
|
neuper@37906
|
493 |
[(str2term "q__::bool", str2term "q x = q_0")],
|
neuper@37926
|
494 |
SOME (str2term "q x = q_0"),
|
neuper@37906
|
495 |
str2term "q__::bool",
|
neuper@37906
|
496 |
str2term "(Rewrite sym_real_minus_eq_cancel False) (q__::bool)");
|
neuper@37906
|
497 |
val (a', STac stac) = handle_leaf "next " th sr E a v t;
|
neuper@37906
|
498 |
term2str stac;
|
neuper@37906
|
499 |
"--- but this \"m\" is already corrupted";
|
neuper@37906
|
500 |
val (m,_) = stac2tac_ EmptyPtree (assoc_thy th) stac;
|
neuper@37906
|
501 |
"- because in assoc_thm'...";
|
neuper@37906
|
502 |
val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));
|
neuper@37906
|
503 |
val "s"::"y"::"m"::"_"::id = explode thmid;
|
neuper@37969
|
504 |
((num_str o (get_thm thy)) (implode id)) RS sym;
|
neuper@37906
|
505 |
((get_thm thy) (implode id)) RS sym;
|
neuper@37906
|
506 |
"... this creates [.]";
|
neuper@37906
|
507 |
((get_thm thy) (implode id));
|
neuper@37906
|
508 |
"... while this has _NO_ [.]";
|
neuper@37906
|
509 |
|
neuper@37906
|
510 |
"----- thus we repair the [.] in string_of_thmI...";
|
neuper@37969
|
511 |
val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;
|
neuper@37906
|
512 |
if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
|
neuper@38031
|
513 |
else error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
|
neuper@37906
|
514 |
" = " ^ string_of_thmI thm);
|
akargl@42108
|
515 |
========== inhibit exn 110718 ================================================*)
|
neuper@37906
|
516 |
|
neuper@38061
|
517 |
"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
|
neuper@38061
|
518 |
"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
|
neuper@38061
|
519 |
"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
|
neuper@37906
|
520 |
states:=[];
|
neuper@37906
|
521 |
CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
|
neuper@37906
|
522 |
"RandbedingungenBiegung [y 0 = 0, y L = 0]",
|
neuper@37906
|
523 |
"RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
|
neuper@37906
|
524 |
"FunktionsVariable x"],
|
neuper@38058
|
525 |
("Biegelinie",
|
neuper@37906
|
526 |
["MomentBestimmte","Biegelinien"],
|
neuper@37906
|
527 |
["IntegrierenUndKonstanteBestimmen"]))];
|
neuper@37906
|
528 |
moveActiveRoot 1;
|
neuper@37906
|
529 |
autoCalculate 1 CompleteCalcHead;
|
neuper@37906
|
530 |
autoCalculate 1 (Step 1) (*Apply_Method*);
|
neuper@37906
|
531 |
autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
|
akargl@42108
|
532 |
(*========== inhibit exn 110718 ================================================
|
akargl@42108
|
533 |
|
neuper@37906
|
534 |
"--- this was corrupted before 'fun string_of_thmI'";
|
neuper@37906
|
535 |
val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
|
neuper@37906
|
536 |
if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel",
|
neuper@37906
|
537 |
"(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()
|
neuper@38031
|
538 |
else error "rewtools.sml: string_of_thmI ?!?";
|
neuper@37906
|
539 |
|
neuper@37906
|
540 |
getTactic 1 ([1],Frm);
|
neuper@38061
|
541 |
"----------- fun filter_appl_rews -----------------------";
|
neuper@38061
|
542 |
"----------- fun filter_appl_rews -----------------------";
|
neuper@38061
|
543 |
"----------- fun filter_appl_rews -----------------------";
|
neuper@37906
|
544 |
val f = str2term "a + z + 2*a + 3*z + 5 + 6";
|
neuper@38050
|
545 |
val thy = assoc_thy "Isac";
|
neuper@37906
|
546 |
val subst = [(*TODO.WN071231 test Rewrite_Inst*)];
|
neuper@37906
|
547 |
val rls = Test_simplify;
|
neuper@37906
|
548 |
(* val rls = rls_p_33; filter_appl_rews ---> length 2
|
neuper@37906
|
549 |
val rls = norm_Poly; filter_appl_rews ---> length 1
|
neuper@37906
|
550 |
*)
|
neuper@37906
|
551 |
if filter_appl_rews thy subst f rls =
|
neuper@37906
|
552 |
[Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
|
neuper@37906
|
553 |
Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
|
neuper@37906
|
554 |
Calculate "plus"] then ()
|
neuper@38031
|
555 |
else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
|
akargl@42108
|
556 |
============ inhibit exn 110718 ==============================================*)
|
neuper@37906
|
557 |
|
neuper@37906
|
558 |
|
neuper@38061
|
559 |
"----------- fun is_contained_in ------------------------";
|
neuper@38061
|
560 |
"----------- fun is_contained_in ------------------------";
|
neuper@38061
|
561 |
"----------- fun is_contained_in ------------------------";
|
neuper@37969
|
562 |
val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus});
|
neuper@37906
|
563 |
if contains_rule r1 Test_simplify then ()
|
neuper@38031
|
564 |
else error "rewtools.sml contains_rule Thm";
|
neuper@37906
|
565 |
|
neuper@38014
|
566 |
val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");
|
neuper@37906
|
567 |
if contains_rule r1 Test_simplify then ()
|
neuper@38031
|
568 |
else error "rewtools.sml contains_rule Calc";
|
neuper@37906
|
569 |
|
neuper@38014
|
570 |
val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
|
neuper@37906
|
571 |
if not (contains_rule r1 Test_simplify) then ()
|
neuper@38031
|
572 |
else error "rewtools.sml contains_rule Calc";
|
neuper@42400
|
573 |
|
neuper@42400
|
574 |
|
neuper@42433
|
575 |
"-------- build fun get_bdv_subst --------------------------------";
|
neuper@42433
|
576 |
"-------- build fun get_bdv_subst --------------------------------";
|
neuper@42433
|
577 |
"-------- build fun get_bdv_subst --------------------------------";
|
neuper@48790
|
578 |
val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
|
neuper@42433
|
579 |
val env = [(str2term "v_v", str2term "x")];
|
neuper@42433
|
580 |
subst2str env = "[\"\n(v_v, x)\"]";
|
neuper@42433
|
581 |
|
neuper@42433
|
582 |
"~~~~~ fun get_bdv_subst, args:"; val (prog, env) = (prog, env);
|
neuper@42433
|
583 |
fun scan (Const _) = NONE
|
neuper@42433
|
584 |
| scan (Free _) = NONE
|
neuper@42433
|
585 |
| scan (Var _) = NONE
|
neuper@42433
|
586 |
| scan (Bound _) = NONE
|
neuper@42433
|
587 |
| scan (t as Const ("List.list.Cons", _) $
|
neuper@42433
|
588 |
(Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =
|
neuper@42433
|
589 |
if is_bdv_subst t then SOME t else NONE
|
neuper@42433
|
590 |
| scan (Abs (_, _, body)) = scan body
|
neuper@42433
|
591 |
| scan (t1 $ t2) =
|
neuper@42433
|
592 |
case scan t1 of
|
neuper@42433
|
593 |
NONE => scan t2
|
neuper@42433
|
594 |
| SOME subst => SOME subst
|
neuper@42433
|
595 |
|
neuper@42433
|
596 |
val SOME tm = scan prog;
|
neuper@42433
|
597 |
val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair: subst;
|
neuper@42433
|
598 |
if term2str tm = "[(bdv, v_v)]" then () else error "get_bdv_subst changed 1";
|
neuper@42433
|
599 |
|
neuper@42433
|
600 |
if subst2subs subst = ["(bdv, x)"] then () else error "get_bdv_subst changed 2";
|
neuper@42433
|
601 |
|
neuper@42433
|
602 |
case get_bdv_subst prog env of
|
neuper@42433
|
603 |
(SOME ["(bdv, x)"], [(Free ("bdv", _), Free ("x", _))]: subst) => ()
|
neuper@42433
|
604 |
| _ => error "get_bdv_subst changed 3";
|
neuper@42433
|
605 |
|
neuper@42433
|
606 |
val (SOME subs, _) = get_bdv_subst prog env;
|
neuper@42433
|
607 |
Rewrite_Inst (subs, ("diff_sin_chain","")) (*<<<----- this is the intended usage*)
|
neuper@42433
|
608 |
|