1.1 --- a/src/sml/IsacKnowledge/EqSystem.ML Thu Sep 14 16:18:55 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/EqSystem.ML Sat Sep 16 12:57:11 2006 +0200
1.3 @@ -279,7 +279,7 @@
1.4 rules = [Thm ("commute_0_equality",
1.5 num_str commute_0_equality),
1.6 Thm ("separate_bdvs_add1", num_str separate_bdvs_add1),
1.7 - (*GOON*)
1.8 + (*GOON rls isolate_bdvs_4x4 @@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.9 Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)(*,
1.10 Thm ("", num_str ),
1.11 Thm ("", num_str ),
1.12 @@ -458,23 +458,6 @@
1.13 (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_tri" [] e_pblID
1.14 (["triangular", "4x4", "linear", "system"],
1.15 [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.16 - ("#Where" , (*analoguous to 2x2*)
1.17 - ["(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
1.18 - " (tl (tl vs_)) from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))",
1.19 - " (tl vs_) from_ vs_ occur_exactly_in (nth_ 3 (es_::bool list))",
1.20 - " vs_ from_ vs_ occur_exactly_in (nth_ 4 (es_::bool list))"
1.21 - ]),
1.22 - ("#Find" ,["solution ss___"])
1.23 - ],
1.24 - prls_triangular,
1.25 - Some "solveSystem es_ vs_",
1.26 - [(*["EqSystem","triangular","4x4"]*)]));
1.27 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ pbl @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.28 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ pbl @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
1.29 -store_pbt
1.30 - (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_tri" [] e_pblID
1.31 - (["triangular", "4x4", "linear", "system"],
1.32 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.33 ("#Where" , (*accepts missing variables up to diagional form*)
1.34 ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.35 "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.36 @@ -483,10 +466,11 @@
1.37 ]),
1.38 ("#Find" ,["solution ss___"])
1.39 ],
1.40 - prls_triangular,
1.41 + append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.42 + [Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.43 Some "solveSystem es_ vs_",
1.44 - [(*["EqSystem","triangular","4x4"]*)]));
1.45 -@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ pbl @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.46 + [["EqSystem","top_down_substitution","4x4"]]));
1.47 +
1.48 store_pbt
1.49 (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_norm" [] e_pblID
1.50 (["normalize", "4x4", "linear", "system"],
1.51 @@ -630,6 +614,7 @@
1.52 Thm ("tl_Nil",num_str tl_Nil)
1.53 ],
1.54 prls = Erls, crls = Erls, nrls = Erls},
1.55 +(*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.56 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.57 \ (let es__ = \
1.58 \ ((Try (Rewrite_Set norm_Rational False)) @@ \
1.59 @@ -647,23 +632,27 @@
1.60 \ [bool_list_ es__, real_list_ vs_]))"
1.61 ));
1.62 store_met
1.63 - (prep_met EqSystem.thy "met_eqsys_topdown_4x4" [] e_metID
1.64 - (["EqSystem","top_down_substitution","4x4"],
1.65 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.66 - ("#Where" ,
1.67 - ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
1.68 - " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]),
1.69 - ("#Find" ,["solution ss___"])
1.70 - ],
1.71 - {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
1.72 - srls = append_rls "srls_top_down_4x4" e_rls
1.73 - [Thm ("hd_thm",num_str hd_thm),
1.74 - Thm ("tl_Cons",num_str tl_Cons),
1.75 - Thm ("tl_Nil",num_str tl_Nil)
1.76 - ],
1.77 - prls = prls_triangular, crls = Erls, nrls = Erls},
1.78 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ met @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.79 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ met @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.80 +(prep_met EqSystem.thy "met_eqsys_topdown_4x4" [] e_metID
1.81 + (["EqSystem","top_down_substitution","4x4"],
1.82 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.83 + ("#Where" , (*accepts missing variables up to diagional form*)
1.84 + ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.85 + "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.86 + "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
1.87 + "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))"
1.88 + ]),
1.89 + ("#Find" ,["solution ss___"])
1.90 + ],
1.91 + {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
1.92 + srls = append_rls "srls_top_down_4x4" e_rls
1.93 + [Thm ("hd_thm",num_str hd_thm),
1.94 + Thm ("tl_Cons",num_str tl_Cons),
1.95 + Thm ("tl_Nil",num_str tl_Nil)
1.96 + ],
1.97 + prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.98 + [Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.99 + crls = Erls, nrls = Erls},
1.100 +(*GOON met ["EqSystem","top_down_substitution","4x4"]@@@@@@@@@@@@@@@@@@@@@*)
1.101 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.102 \ (let e1__ = Take (hd es_); \
1.103 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
2.1 --- a/src/sml/ME/ptyps.sml Thu Sep 14 16:18:55 2006 +0200
2.2 +++ b/src/sml/ME/ptyps.sml Sat Sep 16 12:57:11 2006 +0200
2.3 @@ -333,11 +333,16 @@
2.4 in (map flattup' ivfds):ori list end; 10.3.00---*)
2.5 (* val fmz = ctl; val pI=["sqroot-test","univariate","equation"];
2.6 val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');
2.7 + val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));
2.8 *)
2.9 fun prep_ori [] _ _ = []
2.10 | prep_ori fmz thy pbt =
2.11 let
2.12 - val dts = map ((split_dts thy) o term_of o the o (parse thy)) fmz;
2.13 + val ctopts = map (parse thy) fmz
2.14 + val _= (*FIXME.WN060916 improve error report*)
2.15 + if null (filter is_none ctopts) then ()
2.16 + else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
2.17 + val dts = map ((split_dts thy) o term_of o the) ctopts
2.18 val ori = map (add_field thy pbt) dts;
2.19 (* val ori = map (flat3 o (pair "#undef")) dts; *)
2.20 val ori' = add_variants ori;
2.21 @@ -369,7 +374,7 @@
2.22 erls : rls, (*the eval_rls for cond. in rules FIXME "rls'
2.23 instead erls in "fun prep_met" *)
2.24 srls : rls, (*for evaluating list expressions in scr *)
2.25 - prls : rls, (*for evaluating predicates in ppc/pre *)
2.26 + prls : rls, (*for evaluating predicates in modelpattern *)
2.27 crls : rls, (*for check_elementwise, ie. formulae in calc.*)
2.28 nrls : rls, (*canonical simplifier specific for this met *)
2.29 calc : calc list, (*040207: <--- calclist' in fun prep_met *)
3.1 --- a/src/sml/Scripts/term_G.sml Thu Sep 14 16:18:55 2006 +0200
3.2 +++ b/src/sml/Scripts/term_G.sml Sat Sep 16 12:57:11 2006 +0200
3.3 @@ -1075,6 +1075,9 @@
3.4 val it = "fixed_values [(R::RealDef.real) = R]" : cterm
3.5 *)
3.6
3.7 +(*TODO.WN0609: parse should return a term or a string
3.8 + (or even more comprehensive datastructure for error-messages)
3.9 + i.e. in wrapping with Some term or None the latter is not sufficient*)
3.10 fun parseold thy str =
3.11 (let
3.12 val sgn = sign_of thy;
4.1 --- a/src/smltest/IsacKnowledge/eqsystem.sml Thu Sep 14 16:18:55 2006 +0200
4.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml Sat Sep 16 12:57:11 2006 +0200
4.3 @@ -244,7 +244,7 @@
4.4 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
4.5 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
4.6 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
4.7 -(*GOON: revise... from before 0609*)
4.8 +(*GOON??: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)
4.9 val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\
4.10 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\
4.11 \c + c_2 + c_3 + c_4 = 0,\
4.12 @@ -732,18 +732,36 @@
4.13 "----- relaxed preconditions for triangular system";
4.14 val fmz = ["equalities [L * q_0 = c, \
4.15 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
4.16 - \ 0 = c_4 + 0 / (-1 * EI), \
4.17 - \ 0 = c_3 + 0 / (-1 * EI)]",
4.18 + \ 0 = c_4, \
4.19 + \ 0 = c_3]",
4.20 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
4.21 -(*
4.22 val matches = refine fmz ["linear","system"];
4.23 -val t =str2term"(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))";
4.24 -val t =str2term"(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_))";
4.25 -val t =str2term"(nth_ 2 (vs_)) occurs_in (nth_ 2 (es_))";
4.26 -atomty t;
4.27 -*)
4.28 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
4.29 +(* trace_rewrite := true;
4.30 + trace_rewrite := false;
4.31 + *)
4.32 +(*print_depth 6; matches; print_depth 3;*)
4.33 +case matches of
4.34 + [Matches (["linear", "system"], _),
4.35 + NoMatch (["2x2", "linear", "system"], _),
4.36 + NoMatch (["3x3", "linear", "system"], _),
4.37 + Matches (["4x4", "linear", "system"], _),
4.38 + NoMatch (["triangular", "4x4", "linear", "system"], _),
4.39 + Matches (["normalize", "4x4", "linear", "system"], _)] => ()
4.40 + | _ => raise error "eqsystem.sml: refine relaxed triangular sys NoMatch";
4.41 +(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
4.42
4.43 +val fmz = ["equalities [L * q_0 = c, \
4.44 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
4.45 + \ 0 = c_3, \
4.46 + \ 0 = c_4]",
4.47 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
4.48 +val matches = refine fmz ["triangular", "4x4", "linear","system"];
4.49 +(* print_depth 11; matches; print_depth 3;
4.50 + *)
4.51 +case matches of
4.52 + [Matches (["triangular", "4x4", "linear", "system"], _)] => ()
4.53 + | _ => raise error "eqsystem.sml: refine relaxed triangular sys Matches";
4.54 +val matches = refine fmz ["linear","system"];
4.55
4.56
4.57 "----------- refine [2x2,linear,system] search error--------------";
4.58 @@ -1066,7 +1084,7 @@
4.59 c |
4.60 c c_2 |1:c -> 2:c_2
4.61 c_3 |
4.62 - c_4 | @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
4.63 + c_4 | GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
4.64
4.65 "----- go through the rewrites in met_eqsys_norm_4x4";
4.66 val t = str2term"[L * q_0 = c, \
4.67 @@ -1099,6 +1117,51 @@
4.68 trace_rewrite := true;
4.69 trace_rewrite := false;
4.70
4.71 +"----- 7.70 solving pbl with met";
4.72 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
4.73 +val fmz = ["equalities \
4.74 + \[L * q_0 = c, \
4.75 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
4.76 + \ 0 = c_4, \
4.77 + \ 0 = c_3]",
4.78 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
4.79 +val (dI',pI',mI') =
4.80 + ("Biegelinie.thy",["linear", "system"],["no_met"]);
4.81 +val p = e_pos'; val c = [];
4.82 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.83 +
4.84 +
4.85 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
4.86 +map ((split_dts thy) o term_of o the o (parse thy)) fmz;
4.87 +map ((parse thy)) fmz;
4.88 +
4.89 +parse thy "[L * q_0 = c, \
4.90 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
4.91 + \ 0 = c_4, \
4.92 + \ 0 = c_3]";
4.93 +
4.94 +(*
4.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.98 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.99 +case nxt of ("Specify_Method",_) => ()
4.100 + | _ => raise error "eqsystem.sml [EqSystem,normalize,2x2] specify";
4.101 +
4.102 +
4.103 +
4.104 +states:=[];
4.105 +CalcTree [(["equalities \
4.106 + \[L * q_0 = c, \
4.107 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2,\
4.108 + \ 0 = c_4, \
4.109 + \ 0 = c_3]",
4.110 + "solveForVars [c, c_2, c_3, c_4]", "solution L"],
4.111 + ("Biegelinie.thy",["normalize", "4x4", "linear", "system"],
4.112 + ["EqSystem","normalize","4x4"]))];
4.113 +moveActiveRoot 1;
4.114 +autoCalculate 1 CompleteCalc;
4.115 +*)
4.116
4.117
4.118 "------- Bsp 7.71";
4.119 @@ -1172,6 +1235,7 @@
4.120 "----------- 4x4 systems from Biegelinie -------------------------";
4.121 "----------- 4x4 systems from Biegelinie -------------------------";
4.122 "----------- 4x4 systems from Biegelinie -------------------------";
4.123 +(*GOON replace this test with 7.70 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@2*)
4.124 "----- Bsp 7.27";
4.125 val fmz = ["equalities \
4.126 \[0 = c_4, \
4.127 @@ -1210,7 +1274,6 @@
4.128 \ c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 4 / (-24 * EI)) + -1 * (4 * L ^^^ 3 * c / (-24 * EI)) + -1 * (12 * L ^^^ 2 * c_2 / (-24 * EI)) + -1 * (L * c_3),\
4.129 \ c_2 = 0, \
4.130 \ c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2) + -1 * (L * c)]";
4.131 -(*GOON ^^^^^*)
4.132 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.133
4.134
5.1 --- a/src/smltest/ME/inform.sml Thu Sep 14 16:18:55 2006 +0200
5.2 +++ b/src/smltest/ME/inform.sml Sat Sep 16 12:57:11 2006 +0200
5.3 @@ -399,7 +399,7 @@
5.4 Relate ["relations [A=a*b, a/2=r*sin alpha, \
5.5 \b/2=r*cos alpha]"]], Pbl, e_spec);
5.6 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl;
5.7 - if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing GOON !!!*)
5.8 + if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
5.9
5.10 (*this input is complete in variant 1 (variant 3 does not work yet)*)
5.11 val (b,pt''''',ocalhd) =
6.1 --- a/src/smltest/ME/solve.sml Thu Sep 14 16:18:55 2006 +0200
6.2 +++ b/src/smltest/ME/solve.sml Sat Sep 16 12:57:11 2006 +0200
6.3 @@ -485,7 +485,7 @@
6.4 autoCalculate 1 (Step 1);
6.5
6.6 fetchProposedTactic 1 (*DG decides to do this tactic in detail*);
6.7 - (*GOON ############################################*)
6.8 + (*TODO ...*)
6.9 setNextTactic 1 (Detail_Set "Test_simplify");
6.10
6.11