100 "----------- fun thy_containing_thm ------------------------------"; |
100 "----------- fun thy_containing_thm ------------------------------"; |
101 "----------- fun thy_containing_thm ------------------------------"; |
101 "----------- fun thy_containing_thm ------------------------------"; |
102 "----------- fun thy_containing_thm ------------------------------"; |
102 "----------- fun thy_containing_thm ------------------------------"; |
103 val (str, (thy', thy)) = ("real_diff_minus",("Root.thy", Root.thy)); |
103 val (str, (thy', thy)) = ("real_diff_minus",("Root.thy", Root.thy)); |
104 if thy_contains_thm str ("XXX",thy) then () |
104 if thy_contains_thm str ("XXX",thy) then () |
105 else raise error "rewtools.sml: NOT thy_contains_thm \ |
105 else error "rewtools.sml: NOT thy_contains_thm \ |
106 \(real_diff_minus,(Root.thy,."; |
106 \(real_diff_minus,(Root.thy,."; |
107 (rev (!theory')); |
107 (rev (!theory')); |
108 dropuntil (curry op= thy'); |
108 dropuntil (curry op= thy'); |
109 dropuntil ((curry op= thy') o (#1:theory' * theory -> theory')); |
109 dropuntil ((curry op= thy') o (#1:theory' * theory -> theory')); |
110 val startsearch = dropuntil ((curry op= thy') o |
110 val startsearch = dropuntil ((curry op= thy') o |
111 (#1:theory' * theory -> theory')) |
111 (#1:theory' * theory -> theory')) |
112 (rev (!theory')); |
112 (rev (!theory')); |
113 if thy_containing_thm thy' str = ("IsacKnowledge", "Root.thy") then () |
113 if thy_containing_thm thy' str = ("IsacKnowledge", "Root.thy") then () |
114 else raise error "rewtools.sml: NOT thy_containin_thm \ |
114 else error "rewtools.sml: NOT thy_containin_thm \ |
115 \(real_diff_minus,(Root.thy,."; |
115 \(real_diff_minus,(Root.thy,."; |
116 |
116 |
117 "----- search the same theorem somewhere further below in the list"; |
117 "----- search the same theorem somewhere further below in the list"; |
118 if thy_contains_thm str ("XXX",Poly.thy) then () |
118 if thy_contains_thm str ("XXX",Poly.thy) then () |
119 else raise error "rewtools.sml: NOT thy_contains_thm \ |
119 else error "rewtools.sml: NOT thy_contains_thm \ |
120 \(real_diff_minus,(Poly.thy,."; |
120 \(real_diff_minus,(Poly.thy,."; |
121 if thy_containing_thm "LinEq.thy" str = ("IsacKnowledge", "Poly.thy") then () |
121 if thy_containing_thm "LinEq.thy" str = ("IsacKnowledge", "Poly.thy") then () |
122 else raise error "rewtools.sml: NOT thy_containing_thm \ |
122 else error "rewtools.sml: NOT thy_containing_thm \ |
123 \(real_diff_minus,(Poly.thy,."; |
123 \(real_diff_minus,(Poly.thy,."; |
124 |
124 |
125 "----- second test -------------------------------"; |
125 "----- second test -------------------------------"; |
126 show_thes(); |
126 show_thes(); |
127 (*args vor thy_containing_thm...*) |
127 (*args vor thy_containing_thm...*) |
130 (#1:theory' * theory -> theory')) |
130 (#1:theory' * theory -> theory')) |
131 (rev (!theory')); |
131 (rev (!theory')); |
132 length (!theory'); |
132 length (!theory'); |
133 length startsearch; |
133 length startsearch; |
134 if thy_containing_thm thy' str = ("IsacKnowledge", "Test.thy") then () |
134 if thy_containing_thm thy' str = ("IsacKnowledge", "Test.thy") then () |
135 else raise error "rewtools.sml: diff.behav. in \ |
135 else error "rewtools.sml: diff.behav. in \ |
136 \thy_containing_thm Test radd_commute"; |
136 \thy_containing_thm Test radd_commute"; |
137 |
137 |
138 |
138 |
139 "----------- fun thy_containing_rls ------------------------------"; |
139 "----------- fun thy_containing_rls ------------------------------"; |
140 "----------- fun thy_containing_rls ------------------------------"; |
140 "----------- fun thy_containing_rls ------------------------------"; |
142 val thy' = "Biegelinie.thy"; |
142 val thy' = "Biegelinie.thy"; |
143 val dropthys = takewhile [] (not o (curry op= thy') o |
143 val dropthys = takewhile [] (not o (curry op= thy') o |
144 (#1:theory' * theory -> theory')) |
144 (#1:theory' * theory -> theory')) |
145 (rev (!theory')); |
145 (rev (!theory')); |
146 if length (!theory') <> length dropthys then () |
146 if length (!theory') <> length dropthys then () |
147 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 1"; |
147 else error "rewtools.sml: diff.behav. in thy_containing_rls 1"; |
148 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory')) |
148 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory')) |
149 dropthys; |
149 dropthys; |
150 print_depth 99; dropthy's; print_depth 3; |
150 print_depth 99; dropthy's; print_depth 3; |
151 |
151 |
152 (*WN100819======================================================== |
152 (*WN100819======================================================== |
159 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o |
159 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o |
160 ((#1 o #2) : rls' * (theory' * rls) -> theory')) |
160 ((#1 o #2) : rls' * (theory' * rls) -> theory')) |
161 (rev (!ruleset')); |
161 (rev (!ruleset')); |
162 print_depth 99; map (#1 o #2) startsearch; print_depth 3; |
162 print_depth 99; map (#1 o #2) startsearch; print_depth 3; |
163 if length (!ruleset') <> length startsearch then () |
163 if length (!ruleset') <> length startsearch then () |
164 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 2"; |
164 else error "rewtools.sml: diff.behav. in thy_containing_rls 2"; |
165 |
165 |
166 val rls' = "norm_Poly"; |
166 val rls' = "norm_Poly"; |
167 case assoc (startsearch, rls') of |
167 case assoc (startsearch, rls') of |
168 SOME (thy', _) => thyID2theory' thy' |
168 SOME (thy', _) => thyID2theory' thy' |
169 | _ => raise error ("thy_containing_rls : rls '"^str^ |
169 | _ => error ("thy_containing_rls : rls '"^str^ |
170 "' not in !rulset' und thy '"^thy'^"'"); |
170 "' not in !rulset' und thy '"^thy'^"'"); |
171 |
171 |
172 if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly.thy") then () |
172 if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly.thy") then () |
173 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 3"; |
173 else error "rewtools.sml: diff.behav. in thy_containing_rls 3"; |
174 |
174 |
175 |
175 |
176 "----------- fun thy_containing_cal ------------------------------"; |
176 "----------- fun thy_containing_cal ------------------------------"; |
177 "----------- fun thy_containing_cal ------------------------------"; |
177 "----------- fun thy_containing_cal ------------------------------"; |
178 "----------- fun thy_containing_cal ------------------------------"; |
178 "----------- fun thy_containing_cal ------------------------------"; |
205 autoCalculate 1 CompleteCalc; |
205 autoCalculate 1 CompleteCalc; |
206 interSteps 1 ([1],Res); |
206 interSteps 1 ([1],Res); |
207 interSteps 1 ([1,1],Res); |
207 interSteps 1 ([1,1],Res); |
208 val ((pt,p),_) = get_calc 1; show_pt pt; |
208 val ((pt,p),_) = get_calc 1; show_pt pt; |
209 if existpt' ([1,1,1], Frm) pt then () |
209 if existpt' ([1,1,1], Frm) pt then () |
210 else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1"; |
210 else error "integrate.sml: interSteps on Rewrite_Set_Inst 1"; |
211 |
211 |
212 initContext 1 Thy_ ([1,1,1], Frm); |
212 initContext 1 Thy_ ([1,1,1], Frm); |
213 --------------------TODO.new_c: cvs before 071227, 11:50*) |
213 --------------------TODO.new_c: cvs before 071227, 11:50*) |
214 |
214 |
215 "----------- initContext..Thy_, fun context_thm ------------------"; |
215 "----------- initContext..Thy_, fun context_thm ------------------"; |
239 (*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0 |
239 (*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0 |
240 --- in initContext..Thy_ ---*) |
240 --- in initContext..Thy_ ---*) |
241 val ContThm {thm,result,...} = context_thy (pt,p) tac; |
241 val ContThm {thm,result,...} = context_thy (pt,p) tac; |
242 if thm = "thy_isac_Test-thm-radd_left_commute" |
242 if thm = "thy_isac_Test-thm-radd_left_commute" |
243 andalso term2str result = "-2 + (1 + x) = 0" then () |
243 andalso term2str result = "-2 + (1 + x) = 0" then () |
244 else raise error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute"; |
244 else error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute"; |
245 |
245 |
246 val p = ([3,1,1], Frm); |
246 val p = ([3,1,1], Frm); |
247 val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add","")); |
247 val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add","")); |
248 initContext 1 Thy_ p; |
248 initContext 1 Thy_ p; |
249 (*Frm->Res, Rewrite_Inst "risolate_bdv_add" -1 + x = 0 -> x = 0 + -1 * -1 |
249 (*Frm->Res, Rewrite_Inst "risolate_bdv_add" -1 + x = 0 -> x = 0 + -1 * -1 |
250 --- in initContext..Thy_ ---*) |
250 --- in initContext..Thy_ ---*) |
251 val ContThmInst {thm,result,...} = context_thy (pt,p) tac; |
251 val ContThmInst {thm,result,...} = context_thy (pt,p) tac; |
252 if thm = "thy_isac_Test-thm-risolate_bdv_add" |
252 if thm = "thy_isac_Test-thm-risolate_bdv_add" |
253 andalso term2str result = "x = 0 + -1 * -1" then () |
253 andalso term2str result = "x = 0 + -1 * -1" then () |
254 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add"; |
254 else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add"; |
255 |
255 |
256 initContext 1 Thy_ ([2,5], Res); |
256 initContext 1 Thy_ ([2,5], Res); |
257 (*Res->Res, Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0 |
257 (*Res->Res, Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0 |
258 --- in initContext..Thy_ ---*) |
258 --- in initContext..Thy_ ---*) |
259 |
259 |
268 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0 |
268 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0 |
269 --- in initContext..Thy_ ---*) |
269 --- in initContext..Thy_ ---*) |
270 val ContRls {rls,result,...} = context_thy (pt,p) tac; |
270 val ContRls {rls,result,...} = context_thy (pt,p) tac; |
271 if rls = "thy_isac_Test-rls-Test_simplify" |
271 if rls = "thy_isac_Test-rls-Test_simplify" |
272 andalso term2str result = "-1 + x = 0" then () |
272 andalso term2str result = "-1 + x = 0" then () |
273 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add"; |
273 else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add"; |
274 |
274 |
275 val p = ([3,1], Frm); |
275 val p = ([3,1], Frm); |
276 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv"); |
276 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv"); |
277 initContext 1 Thy_ p; |
277 initContext 1 Thy_ p; |
278 (*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1 |
278 (*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1 |
279 --- in initContext..Thy_ ---*) |
279 --- in initContext..Thy_ ---*) |
280 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac; |
280 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac; |
281 if rls = "thy_isac_Test-rls-isolate_bdv" |
281 if rls = "thy_isac_Test-rls-isolate_bdv" |
282 andalso term2str result = "x = 0 + -1 * -1" then () |
282 andalso term2str result = "x = 0 + -1 * -1" then () |
283 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add"; |
283 else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add"; |
284 |
284 |
285 |
285 |
286 |
286 |
287 "----------- checkContext..Thy_, fun context_thy -----------------"; |
287 "----------- checkContext..Thy_, fun context_thy -----------------"; |
288 "----------- checkContext..Thy_, fun context_thy -----------------"; |
288 "----------- checkContext..Thy_, fun context_thy -----------------"; |
295 (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0 |
295 (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0 |
296 --- in checkContext..Thy_ ---*) |
296 --- in checkContext..Thy_ ---*) |
297 val ContThm {thm,result,...} = context_thy (pt,p) tac; |
297 val ContThm {thm,result,...} = context_thy (pt,p) tac; |
298 if thm = "thy_isac_Test-thm-radd_left_commute" |
298 if thm = "thy_isac_Test-thm-radd_left_commute" |
299 andalso term2str result = "-2 + (1 + x) = 0" then () |
299 andalso term2str result = "-2 + (1 + x) = 0" then () |
300 else raise error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute"; |
300 else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute"; |
301 |
301 |
302 val p = ([3,1,1], Frm); |
302 val p = ([3,1,1], Frm); |
303 val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add","")); |
303 val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add","")); |
304 checkContext 1 p "thy_Test-thm-risolate_bdv_add"; |
304 checkContext 1 p "thy_Test-thm-risolate_bdv_add"; |
305 (* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1 |
305 (* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1 |
306 --- in checkContext..Thy_ ---*) |
306 --- in checkContext..Thy_ ---*) |
307 val ContThmInst {thm,result,...} = context_thy (pt,p) tac; |
307 val ContThmInst {thm,result,...} = context_thy (pt,p) tac; |
308 if thm = "thy_isac_Test-thm-risolate_bdv_add" |
308 if thm = "thy_isac_Test-thm-risolate_bdv_add" |
309 andalso term2str result = "x = 0 + -1 * -1" then () |
309 andalso term2str result = "x = 0 + -1 * -1" then () |
310 else raise error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add"; |
310 else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add"; |
311 |
311 |
312 val p = ([2,5], Res); |
312 val p = ([2,5], Res); |
313 val tac = Calculate "plus"; |
313 val tac = Calculate "plus"; |
314 (*checkContext..Thy_ 1 ([2,5], Res);*) |
314 (*checkContext..Thy_ 1 ([2,5], Res);*) |
315 (*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*) |
315 (*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*) |
330 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0 |
330 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0 |
331 --- in checkContext..Thy_ ---*) |
331 --- in checkContext..Thy_ ---*) |
332 val ContRls {rls,result,...} = context_thy (pt,p) tac; |
332 val ContRls {rls,result,...} = context_thy (pt,p) tac; |
333 if rls = "thy_isac_Test-rls-Test_simplify" |
333 if rls = "thy_isac_Test-rls-Test_simplify" |
334 andalso term2str result = "-1 + x = 0" then () |
334 andalso term2str result = "-1 + x = 0" then () |
335 else raise error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify"; |
335 else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify"; |
336 |
336 |
337 val p = ([3,1], Frm); |
337 val p = ([3,1], Frm); |
338 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv"); |
338 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv"); |
339 checkContext 1 p "thy_Test-rls-isolate_bdv"; |
339 checkContext 1 p "thy_Test-rls-isolate_bdv"; |
340 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac; |
340 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac; |
341 if rls = "thy_isac_Test-rls-isolate_bdv" |
341 if rls = "thy_isac_Test-rls-isolate_bdv" |
342 andalso term2str result = "x = 0 + -1 * -1" then () |
342 andalso term2str result = "x = 0 + -1 * -1" then () |
343 else raise error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv"; |
343 else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv"; |
344 |
344 |
345 |
345 |
346 "----------- checkContext..Thy_ on last formula ------------------"; |
346 "----------- checkContext..Thy_ on last formula ------------------"; |
347 "----------- checkContext..Thy_ on last formula ------------------"; |
347 "----------- checkContext..Thy_ on last formula ------------------"; |
348 "----------- checkContext..Thy_ on last formula ------------------"; |
348 "----------- checkContext..Thy_ on last formula ------------------"; |
385 val rest' = dropuntil (curry op= delim) rest; |
385 val rest' = dropuntil (curry op= delim) rest; |
386 val setc = take_fromto 1 5 rest'; |
386 val setc = take_fromto 1 5 rest'; |
387 val xstr = takerest (5, rest'); |
387 val xstr = takerest (5, rest'); |
388 |
388 |
389 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then () |
389 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then () |
390 else raise error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed"; |
390 else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed"; |
391 |
391 |
392 |
392 |
393 "----------- debugging on Tests/solve_linear_as_rootpbl ----------"; |
393 "----------- debugging on Tests/solve_linear_as_rootpbl ----------"; |
394 "----------- debugging on Tests/solve_linear_as_rootpbl ----------"; |
394 "----------- debugging on Tests/solve_linear_as_rootpbl ----------"; |
395 "----------- debugging on Tests/solve_linear_as_rootpbl ----------"; |
395 "----------- debugging on Tests/solve_linear_as_rootpbl ----------"; |
403 Iterator 1; moveActiveRoot 1; |
403 Iterator 1; moveActiveRoot 1; |
404 autoCalculate 1 CompleteCalcHead; |
404 autoCalculate 1 CompleteCalcHead; |
405 |
405 |
406 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt; |
406 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt; |
407 if is_curr_endof_calc pt ([1],Frm) then () |
407 if is_curr_endof_calc pt ([1],Frm) then () |
408 else raise error "rewtools.sml is_curr_endof_calc ([1],Frm)"; |
408 else error "rewtools.sml is_curr_endof_calc ([1],Frm)"; |
409 |
409 |
410 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt; |
410 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt; |
411 if not (is_curr_endof_calc pt ([1],Frm)) then () |
411 if not (is_curr_endof_calc pt ([1],Frm)) then () |
412 else raise error "rewtools.sml is_curr_endof_calc ([1],Frm) not"; |
412 else error "rewtools.sml is_curr_endof_calc ([1],Frm) not"; |
413 if is_curr_endof_calc pt ([1],Res) then () |
413 if is_curr_endof_calc pt ([1],Res) then () |
414 else raise error "rewtools.sml is_curr_endof_calc ([1],Res)"; |
414 else error "rewtools.sml is_curr_endof_calc ([1],Res)"; |
415 |
415 |
416 initContext 1 Thy_ ([1],Res); |
416 initContext 1 Thy_ ([1],Res); |
417 |
417 |
418 "----- checkContext -----"; |
418 "----- checkContext -----"; |
419 states:=[]; |
419 states:=[]; |
471 "... while this has _NO_ [.]"; |
471 "... while this has _NO_ [.]"; |
472 |
472 |
473 "----- thus we repair the [.] in string_of_thmI..."; |
473 "----- thus we repair the [.] in string_of_thmI..."; |
474 val thm = ((num_str o (get_thm thy)) (implode id)) RS sym; |
474 val thm = ((num_str o (get_thm thy)) (implode id)) RS sym; |
475 if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then () |
475 if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then () |
476 else raise error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^ |
476 else error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^ |
477 " = " ^ string_of_thmI thm); |
477 " = " ^ string_of_thmI thm); |
478 |
478 |
479 |
479 |
480 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----"; |
480 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----"; |
481 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----"; |
481 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----"; |
494 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*); |
494 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*); |
495 "--- this was corrupted before 'fun string_of_thmI'"; |
495 "--- this was corrupted before 'fun string_of_thmI'"; |
496 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt; |
496 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt; |
497 if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel", |
497 if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel", |
498 "(?b1 = ?a1) = (- ?b1 = - ?a1)") then () |
498 "(?b1 = ?a1) = (- ?b1 = - ?a1)") then () |
499 else raise error "rewtools.sml: string_of_thmI ?!?"; |
499 else error "rewtools.sml: string_of_thmI ?!?"; |
500 |
500 |
501 getTactic 1 ([1],Frm); |
501 getTactic 1 ([1],Frm); |
502 |
502 |
503 "----------- fun filter_appl_rews --------------------------------"; |
503 "----------- fun filter_appl_rews --------------------------------"; |
504 "----------- fun filter_appl_rews --------------------------------"; |
504 "----------- fun filter_appl_rews --------------------------------"; |
512 *) |
512 *) |
513 if filter_appl_rews thy subst f rls = |
513 if filter_appl_rews thy subst f rls = |
514 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"), |
514 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"), |
515 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), |
515 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), |
516 Calculate "plus"] then () |
516 Calculate "plus"] then () |
517 else raise error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6"; |
517 else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6"; |
518 |
518 |
519 |
519 |
520 "----------- fun is_contained_in ---------------------------------"; |
520 "----------- fun is_contained_in ---------------------------------"; |
521 "----------- fun is_contained_in ---------------------------------"; |
521 "----------- fun is_contained_in ---------------------------------"; |
522 "----------- fun is_contained_in ---------------------------------"; |
522 "----------- fun is_contained_in ---------------------------------"; |
523 val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus}); |
523 val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus}); |
524 if contains_rule r1 Test_simplify then () |
524 if contains_rule r1 Test_simplify then () |
525 else raise error "rewtools.sml contains_rule Thm"; |
525 else error "rewtools.sml contains_rule Thm"; |
526 |
526 |
527 val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_"); |
527 val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_"); |
528 if contains_rule r1 Test_simplify then () |
528 if contains_rule r1 Test_simplify then () |
529 else raise error "rewtools.sml contains_rule Calc"; |
529 else error "rewtools.sml contains_rule Calc"; |
530 |
530 |
531 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_"); |
531 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_"); |
532 if not (contains_rule r1 Test_simplify) then () |
532 if not (contains_rule r1 Test_simplify) then () |
533 else raise error "rewtools.sml contains_rule Calc"; |
533 else error "rewtools.sml contains_rule Calc"; |