1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Fri Sep 16 12:13:23 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Mon Sep 26 10:57:53 2022 +0200
1.3 @@ -16,9 +16,10 @@
1.4 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
1.5 "----------- refine [linear,system]-------------------------------";
1.6 "----------- refine [2x2,linear,system] search error--------------";
1.7 -"----------- me [EqSystem,normalise,2x2] -------------------------";
1.8 -(*^^^--- eqsystem-1.sml #####################################################################
1.9 - vvv--- eqsystem-2.sml #####################################################################*)
1.10 +(*^^^--- eqsystem-1.sml #####################################################################*)
1.11 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.12 +(*^^^--- eqsystem-1a.sml #####################################################################
1.13 + vvv--- eqsystem-2.sml #####################################################################*)
1.14 "----------- me [linear,system] ..normalise..top_down_sub..-------";
1.15 "----------- all systems from Biegelinie -------------------------";
1.16 "----------- 4x4 systems from Biegelinie -------------------------";
1.17 @@ -158,7 +159,7 @@
1.18 \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
1.19 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
1.20 (TermC.str2term"bdv_2",TermC.str2term"c_2")];
1.21 -val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.22 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
1.23 if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
1.24 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
1.25
1.26 @@ -166,7 +167,7 @@
1.27 if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
1.28 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
1.29
1.30 -val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
1.31 +val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
1.32 if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
1.33 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
1.34
1.35 @@ -292,11 +293,11 @@
1.36 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
1.37 "solveForVars [c, c_2]", "solution LL"];
1.38
1.39 -(*WN120313 in "solution L" above "Refine.refine fmz ["LINEAR", "system"]" caused an error...*)
1.40 -"~~~~~ fun Refine.refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
1.41 -"~~~~~ fun refin', args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
1.42 +(*WN120313 in "solution L" above "Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]" caused an error...*)
1.43 +"~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
1.44 +"~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
1.45 ((rev o tl) pblID, fmz, [(*match list*)],
1.46 - ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR", "system"]], [])): Problem.T Store.node));
1.47 + ((Store.Node ("LINEAR", [Problem.from_store_PIDE ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
1.48 val {thy, ppc, where_, prls, ...} = py ;
1.49 "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
1.50 val ctxt = Proof_Context.init_global thy;
1.51 @@ -325,26 +326,23 @@
1.52 Operand: L :: real ========== L was already present in equalities ========== *)
1.53
1.54 "===== case 1 =====";
1.55 -val matches = Refine.refine fmz ["LINEAR", "system"];
1.56 +val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
1.57 case matches of
1.58 - [M_Match.Matches (["LINEAR", "system"], _),
1.59 - M_Match.Matches (["2x2", "LINEAR", "system"], _),
1.60 - M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _),
1.61 - M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],
1.62 - {Find = [Correct "solution LL"],
1.63 - With = [],
1.64 - Given =
1.65 - [Correct
1.66 - "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.67 - Correct "solveForVars [c, c_2]"],
1.68 - Where = [],
1.69 - Relate = []})] => ()
1.70 + [M_Match.Matches (["LINEAR", "system"], _), (*Matches*)
1.71 + M_Match.Matches (["2x2", "LINEAR", "system"], _), (*NoMatch ! GOON !*)
1.72 + M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
1.73 + M_Match.Matches (["normalise", "2x2", "LINEAR", "system"], (**)
1.74 + {Find = [Correct "solution LL"], With = [], (**)
1.75 + Given = [Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.76 + Correct "solveForVars [c, c_2]"],
1.77 + Where = [],
1.78 + Relate = []})] => ()
1.79 | _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
1.80
1.81 "===== case 2 =====";
1.82 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
1.83 "solveForVars [c, c_2]", "solution LL"];
1.84 -val matches = Refine.refine fmz ["LINEAR", "system"];
1.85 +val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
1.86 case matches of [_,_,
1.87 M_Match.Matches
1.88 (["triangular", "2x2", "LINEAR", "system"],
1.89 @@ -361,11 +359,11 @@
1.90 | _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
1.91
1.92 (*WN051014-----------------------------------------------------------------------------------\\
1.93 - the above 'val matches = Refine.refine fmz ["LINEAR", "system"]'
1.94 + the above 'val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]'
1.95 didn't work anymore; we investigated in these steps:*)
1.96 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
1.97 "solveForVars [c, c_2]", "solution LL"];
1.98 -val matches = Refine.refine fmz ["triangular", "2x2", "LINEAR", "system"];
1.99 +val matches = Refine.refine_PIDE @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
1.100 (*... resulted in
1.101 False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
1.102 [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
1.103 @@ -433,7 +431,7 @@
1.104 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
1.105 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.106 "solveForVars [c, c_2]", "solution LL"];
1.107 -val matches = Refine.refine fmz ["2x2", "LINEAR", "system"];
1.108 +val matches = Refine.refine_PIDE @{context} fmz ["2x2", "LINEAR", "system"];
1.109 (*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
1.110 (*brought: 'False "length_ es_ = 2"'*)
1.111
1.112 @@ -514,9 +512,9 @@
1.113 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.114 *)
1.115
1.116 -"----------- me [EqSystem,normalise,2x2] -------------------------";
1.117 -"----------- me [EqSystem,normalise,2x2] -------------------------";
1.118 -"----------- me [EqSystem,normalise,2x2] -------------------------";
1.119 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.120 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.121 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
1.122 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
1.123 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
1.124 "solveForVars [c, c_2]", "solution LL"];