1 (* Title: Knowledge/eqsystem-1.sml |
1 (* Title: Knowledge/eqsystem-1.sml |
2 author: Walther Neuper 050826, |
2 author: Walther Neuper 050826, |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 |
5 |
6 "-----------------------------------------------------------------"; |
6 "-----------------------------------------------------------------------------------------------"; |
7 "table of contents -----------------------------------------------"; |
7 "table of contents -----------------------------------------------------------------------------"; |
8 "-----------------------------------------------------------------"; |
8 "-----------------------------------------------------------------------------------------------"; |
9 "----------- occur_exactly_in ------------------------------------"; |
9 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml"; |
10 "----------- problems --------------------------------------------"; |
10 "----------- problems -----------------------------------------------------------equsystem-1.sml"; |
11 "----------- rewrite-order ord_simplify_System -------------------"; |
11 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml"; |
12 "----------- rewrite in [EqSystem,normalise,2x2] -----------------"; |
12 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml"; |
13 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; |
13 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml"; |
14 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----"; |
14 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml"; |
15 "----------- rewrite in [EqSystem,normalise,4x4] -----------------"; |
15 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml"; |
16 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --"; |
16 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml"; |
17 "----------- refine [linear,system]-------------------------------"; |
17 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml"; |
18 "----------- refine [2x2,linear,system] search error--------------"; |
18 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml"; |
19 (*^^^--- eqsystem-1.sml #####################################################################*) |
19 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml"; |
20 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; |
20 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; |
21 (*^^^--- eqsystem-1a.sml ##################################################################### |
21 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml"; |
22 vvv--- eqsystem-2.sml #####################################################################*) |
22 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml"; |
23 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
23 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml"; |
24 "----------- all systems from Biegelinie -------------------------"; |
24 "-----------------------------------------------------------------------------------------------"; |
25 "----------- 4x4 systems from Biegelinie -------------------------"; |
25 "-----------------------------------------------------------------------------------------------"; |
26 "-----------------------------------------------------------------"; |
26 "-----------------------------------------------------------------------------------------------"; |
27 "-----------------------------------------------------------------"; |
|
28 "-----------------------------------------------------------------"; |
|
29 |
27 |
30 val thy = @{theory "EqSystem"}; |
28 val thy = @{theory "EqSystem"}; |
31 val ctxt = Proof_Context.init_global thy; |
29 val ctxt = Proof_Context.init_global thy; |
32 |
30 |
33 "----------- occur_exactly_in ------------------------------------"; |
31 "----------- occur_exactly_in ------------------------------------"; |
174 "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)"; |
172 "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)"; |
175 val SOME (t,_) = rewrite_set_ ctxt true order_system t; |
173 val SOME (t,_) = rewrite_set_ ctxt true order_system t; |
176 if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" |
174 if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" |
177 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3"; |
175 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3"; |
178 |
176 |
|
177 |
179 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; |
178 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; |
180 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; |
179 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; |
181 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; |
180 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; |
182 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*); |
181 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*); |
183 val ctxt = Proof_Context.init_global thy; |
182 val ctxt = Proof_Context.init_global thy; |
282 if UnparseC.term t = "[c_4 = 0,\ |
281 if UnparseC.term t = "[c_4 = 0,\ |
283 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\ |
282 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\ |
284 \ c_2 + (c_3 + c_4) = 0,\n\ |
283 \ c_2 + (c_3 + c_4) = 0,\n\ |
285 \ c + (c_2 + (c_3 + c_4)) = 0]" |
284 \ c + (c_2 + (c_3 + c_4)) = 0]" |
286 then () else error "eqsystem.sml rewrite in 4x4 order_system"; |
285 then () else error "eqsystem.sml rewrite in 4x4 order_system"; |
|
286 |
|
287 |
287 |
288 |
288 "----------- refine [linear,system]-------------------------------"; |
289 "----------- refine [linear,system]-------------------------------"; |
289 "----------- refine [linear,system]-------------------------------"; |
290 "----------- refine [linear,system]-------------------------------"; |
290 "----------- refine [linear,system]-------------------------------"; |
291 "----------- refine [linear,system]-------------------------------"; |
291 val fmz = |
292 val fmz = |
421 [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => () |
422 [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => () |
422 | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch"; |
423 | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch"; |
423 val TermC.matches = Refine.refine fmz ["LINEAR", "system"]; |
424 val TermC.matches = Refine.refine fmz ["LINEAR", "system"]; |
424 ============ inhibit exn WN120314 ==============================================*) |
425 ============ inhibit exn WN120314 ==============================================*) |
425 |
426 |
|
427 |
|
428 |
426 "----------- Refine.refine [2x2,linear,system] search error--------------"; |
429 "----------- Refine.refine [2x2,linear,system] search error--------------"; |
427 "----------- Refine.refine [2x2,linear,system] search error--------------"; |
430 "----------- Refine.refine [2x2,linear,system] search error--------------"; |
428 "----------- Refine.refine [2x2,linear,system] search error--------------"; |
431 "----------- Refine.refine [2x2,linear,system] search error--------------"; |
429 (*didn't go into ["2x2", "LINEAR", "system"]; |
432 (*didn't go into ["2x2", "LINEAR", "system"]; |
430 we investigated in these steps:*) |
433 we investigated in these steps:*) |
510 |
513 |
511 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM |
514 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM |
512 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
515 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
513 *) |
516 *) |
514 |
517 |
|
518 |
515 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; |
519 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; |
516 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; |
520 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; |
517 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; |
521 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; |
518 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\ |
522 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^ |
519 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]", |
523 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]", |
520 "solveForVars [c, c_2]", "solution LL"]; |
524 "solveForVars [c, c_2]", "solution LL"]; |
521 val (dI',pI',mI') = |
525 val (dI',pI',mI') = |
522 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"], |
526 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"], |
523 ["EqSystem", "normalise", "2x2"]); |
527 ["EqSystem", "normalise", "2x2"]); |
524 val p = e_pos'; val c = []; |
528 val p = e_pos'; val c = []; |
530 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => () |
534 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => () |
531 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify"; |
535 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify"; |
532 |
536 |
533 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
537 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
534 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
538 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
535 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*); |
539 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
536 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
540 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
537 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
541 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
538 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
542 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
539 case nxt of |
543 case nxt of |
540 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => () |
544 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => () |
547 case nxt of |
551 case nxt of |
548 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
552 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
549 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; |
553 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; |
550 |
554 |
551 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
555 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
552 val PblObj {probl,...} = get_obj I pt [5]; |
|
553 (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl; |
|
554 (*[ |
|
555 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])), |
|
556 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])), |
|
557 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))] |
|
558 *) |
|
559 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
556 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
560 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
557 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
561 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
558 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
562 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
559 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
563 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
560 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
567 case nxt of |
564 case nxt of |
568 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => () |
565 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => () |
569 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished"; |
566 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished"; |
570 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
567 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
571 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
568 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
569 (* final test ... ----------------------------------------------------------------------------*) |
572 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then () |
570 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then () |
573 else error "eqsystem.sml me [EqSys...2x2] finished f2str f"; |
571 else error "eqsystem.sml me [EqSys...2x2] finished f2str f"; |
|
572 |
574 case nxt of |
573 case nxt of |
575 (End_Proof') => () |
574 (End_Proof') => () |
576 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; |
575 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; |
|
576 |
|
577 Test_Tool.show_pt pt (*[ |
|
578 (([], Frm), solveSystem |
|
579 [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2], |
|
580 [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]] |
|
581 [[c], [c_2]]), |
|
582 (([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2, |
|
583 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]), |
|
584 (([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]), |
|
585 (([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]), |
|
586 (([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]), |
|
587 (([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]), |
|
588 (([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]), |
|
589 (([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2), |
|
590 (([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2), |
|
591 (([5, 2], Res), L * c = q_0 * L \<up> 2 / 2), |
|
592 (([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L), |
|
593 (([5, 4], Res), c = L * q_0 / 2), |
|
594 (([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]), |
|
595 (([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]), |
|
596 (([5], Res), [c = L * q_0 / 2, c_2 = 0]), |
|
597 (([], Res), [c = L * q_0 / 2, c_2 = 0])] |
|
598 *) |