1.1 --- a/src/sml/IsacKnowledge/EqSystem.ML Sat Sep 16 21:29:08 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/EqSystem.ML Sat Sep 16 23:07:37 2006 +0200
1.3 @@ -643,31 +643,25 @@
1.4 ("#Find" ,["solution ss___"])
1.5 ],
1.6 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
1.7 - srls = append_rls "srls_top_down_4x4" e_rls
1.8 - [Thm ("hd_thm",num_str hd_thm),
1.9 - Thm ("tl_Cons",num_str tl_Cons),
1.10 - Thm ("tl_Nil",num_str tl_Nil)
1.11 - ],
1.12 + srls = append_rls "srls_top_down_4x4" srls [],
1.13 prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.14 [Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.15 crls = Erls, nrls = Erls},
1.16 -(*GOON met ["EqSystem","top_down_substitution","4x4"]@@@@@@@@@@@@@@@@@@@@@*)
1.17 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.18 -\ (let e1__ = Take (hd es_); \
1.19 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.20 -\ isolate_bdvs False)) @@ \
1.21 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.22 -\ simplify_System False))) e1__; \
1.23 -\ e2__ = Take (hd (tl es_)); \
1.24 -\ e2__ = ((Substitute [e1__]) @@ \
1.25 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.26 -\ simplify_System_parenthesized False)) @@ \
1.27 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.28 -\ isolate_bdvs False)) @@ \
1.29 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.30 -\ simplify_System False))) e2__; \
1.31 -\ es__ = Take [e1__, e2__] \
1.32 -\ in (Try (Rewrite_Set order_system False)) es__)"
1.33 +(*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
1.34 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.35 +\ (let e1_ = nth_ 1 es_; \
1.36 +\ e2_ = Take (nth_ 2 es_); \
1.37 +\ e2_ = ((Substitute [e1_]) @@ \
1.38 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.39 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.40 +\ simplify_System_parenthesized False)) @@ \
1.41 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.42 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.43 +\ isolate_bdvs False)) @@ \
1.44 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.45 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.46 +\ norm_Rational False))) e2_ \
1.47 +\ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
1.48 ));
1.49
1.50 (* show_mets();
2.1 --- a/src/smltest/IsacKnowledge/eqsystem.sml Sat Sep 16 21:29:08 2006 +0200
2.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml Sat Sep 16 23:07:37 2006 +0200
2.3 @@ -1144,7 +1144,153 @@
2.4 then () else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
2.5
2.6 "----- 7.70 with met top_down_: ";
2.7 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
2.8 +"--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
2.9 +(*---vvv-this script failed with if ?!?-------------------------------------*)
2.10 +val str =
2.11 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.12 +\ (let e1_ = hd es_; \
2.13 +\ v1_ = hd vs_; \
2.14 +\ xxx = if lhs e1_ =!= v1_ \
2.15 +\ then 0=0 \
2.16 +\ else let e1_ = Take e1_; \
2.17 +\ e1_ = (Rewrite_Set_Inst [(bdv_1, hd vs_), \
2.18 +\ (bdv_2, hd (tl vs_))] \
2.19 +\ isolate_bdvs False) e1_; \
2.20 +\ e2_ = Take (hd (tl es_)); \
2.21 +\ e2_ = (Substitute [e1__]) e2_ \
2.22 +\ in [e1_, e2_])";
2.23 +(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
2.24 +val str =
2.25 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.26 +\ (let e1_ = hd es_; \
2.27 +\ v1_ = hd vs_; \
2.28 +\ e2_ = Take (hd (tl es_)); \
2.29 +\ e2_ = (Substitute [e1__]) e2_ \
2.30 +\ in [e1_, e2_])";
2.31 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.32 +(*---^^^-OK-----------------------------------------------------------------*)
2.33 +(*---vvv-NOT ok-------------------------------------------------------------*)
2.34 +val str =
2.35 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.36 +\ (let e1_ = hd es_; \
2.37 +\ v1_ = hd vs_; \
2.38 +\ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
2.39 +\ e2_ = Take (hd (tl es_)); \
2.40 +\ e2_ = (Substitute [e1__]) e2_ \
2.41 +\ in [e1_, e2_])";
2.42 +(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
2.43 +val str = "if lhs e1_ =!= v1_ then 1 else 2";
2.44 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.45 +
2.46 +val str = "let xxx = (if lhs e1_ =!= v1_ then 1 else 2) in xxx";
2.47 +(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
2.48 +atomty sc; term2str sc;
2.49 +
2.50 +"--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
2.51 +val str =
2.52 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.53 +\ (let e2__ = Take (hd (tl es_)); \
2.54 +\ e2__ = ((Substitute [e1__]) @@ \
2.55 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
2.56 +\ simplify_System_parenthesized False)) @@ \
2.57 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
2.58 +\ isolate_bdvs False)) @@ \
2.59 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
2.60 +\ simplify_System False))) e2__;\
2.61 +\ es__ = Take [e1__, e2__] \
2.62 +\ in (Try (Rewrite_Set order_system False)) es__)"
2.63 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.64 +val str =
2.65 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.66 +\ (let e2__ = Take (nth_ 2 es_); \
2.67 +\ e2__ = ((Substitute [e1__]) @@ \
2.68 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
2.69 +\ simplify_System_parenthesized False)) @@ \
2.70 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
2.71 +\ isolate_bdvs False)) @@ \
2.72 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
2.73 +\ simplify_System False))) e2__;\
2.74 +\ es__ = Take [e1__, e2__] \
2.75 +\ in (Try (Rewrite_Set order_system False)) es__)"
2.76 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.77 +val str =
2.78 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.79 +\ (let e2__ = Take (nth_ 2 es_); \
2.80 +\ e2__ = ((Substitute [e1__]) @@ \
2.81 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
2.82 +\ simplify_System_parenthesized False)) @@ \
2.83 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
2.84 +\ isolate_bdvs False)) @@ \
2.85 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
2.86 +\ simplify_System False))) e2__;\
2.87 +\ es__ = Take [e1__, e2__] \
2.88 +\ in (Try (Rewrite_Set order_system False)) es__)"
2.89 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.90 +val str =
2.91 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.92 +\ (let e2__ = Take (nth_ 2 es_); \
2.93 +\ e2__ = ((Substitute [e1__]) @@ \
2.94 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
2.95 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
2.96 +\ simplify_System_parenthesized False)) @@ \
2.97 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
2.98 +\ isolate_bdvs False)) @@ \
2.99 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
2.100 +\ norm_Rational False))) e2__; \
2.101 +\ es__ = Take [e1__, e2__] \
2.102 +\ in [])"
2.103 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.104 +val str =
2.105 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.106 +\ (let e2_ = Take (nth_ 2 es_); \
2.107 +\ e2_ = ((Substitute [e1_]) @@ \
2.108 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
2.109 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
2.110 +\ simplify_System_parenthesized False)) @@ \
2.111 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
2.112 +\ isolate_bdvs False)) @@ \
2.113 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
2.114 +\ norm_Rational False))) e2_; \
2.115 +\ es_ = Take [e1_, e2_] \
2.116 +\ in [e1_, e2_,e3_, e4_])"
2.117 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.118 +val str =
2.119 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.120 +\ (let e2_ = Take (nth_ 2 es_); \
2.121 +\ e2_ = ((Substitute [e1_]) @@ \
2.122 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
2.123 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
2.124 +\ simplify_System_parenthesized False)) @@ \
2.125 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
2.126 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
2.127 +\ isolate_bdvs False)) @@ \
2.128 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
2.129 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
2.130 +\ norm_Rational False))) e2_; \
2.131 +\ es_ = Take [e1_, e2_] \
2.132 +\ in [e1_, e2_,e3_, e4_])"
2.133 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.134 +(*---^^^-OK-----------------------------------------------------------------*)
2.135 +val str =
2.136 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
2.137 +\ (let e2_ = Take (nth_ 2 es_); \
2.138 +\ e2_ = ((Substitute [e1_]) @@ \
2.139 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
2.140 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
2.141 +\ simplify_System_parenthesized False)) @@ \
2.142 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
2.143 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
2.144 +\ isolate_bdvs False)) @@ \
2.145 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
2.146 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
2.147 +\ norm_Rational False))) e2_ \
2.148 +\ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
2.149 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.150 +(*---vvv-NOT ok-------------------------------------------------------------*)
2.151 +atomty sc; term2str sc;
2.152 +
2.153 +
2.154 +"----- 7.70 with met top_down_: me";
2.155 val fmz = ["equalities \
2.156 \[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]",
2.157 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
2.158 @@ -1158,30 +1304,15 @@
2.159 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.160 case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
2.161 | _ => raise error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
2.162 -
2.163 -
2.164 -print_depth 7; nxt; print_depth 3;
2.165 -
2.166 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.167 -
2.168 -
2.169 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
2.170 -(*
2.171 -
2.172 -
2.173 -
2.174 -states:=[];
2.175 -CalcTree [(["equalities \
2.176 - \[L * q_0 = c, \
2.177 - \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2,\
2.178 - \ 0 = c_4, \
2.179 - \ 0 = c_3]",
2.180 - "solveForVars [c, c_2, c_3, c_4]", "solution L"],
2.181 - ("Biegelinie.thy",["normalize", "4x4", "linear", "system"],
2.182 - ["EqSystem","normalize","4x4"]))];
2.183 -moveActiveRoot 1;
2.184 -autoCalculate 1 CompleteCalc;
2.185 -*)
2.186 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.187 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.188 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.189 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.190 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.191 +if nxt = ("End_Proof'", End_Proof') andalso
2.192 + f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
2.193 +then () else raise error "eqsystem.sml: 7.70 with met top_down_: me";
2.194
2.195
2.196 "------- Bsp 7.71";