1.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Thu Jul 21 12:01:56 2011 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Fri Jul 22 14:01:09 2011 +0200
1.3 @@ -30,8 +30,7 @@
1.4 "-----------------------------------------------------------------";
1.5 "-----------------------------------------------------------------";
1.6
1.7 -(*=== inhibit exn ?=============================================================
1.8 -val thy = EqSystem.thy;
1.9 +val thy = @{theory "EqSystem"};
1.10
1.11 "----------- occur_exactly_in ------------------------------------";
1.12 "----------- occur_exactly_in ------------------------------------";
1.13 @@ -48,6 +47,7 @@
1.14 if not (occur_exactly_in [str2term"c_2"] all t)
1.15 then () else error "eqsystem.sml occur_exactly_in 3";
1.16
1.17 +(*=== inhibit exn 110722=============================================================
1.18
1.19 val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \
1.20 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
1.21 @@ -120,6 +120,7 @@
1.22 ]) t;
1.23 if t = HOLogic.true_const then ()
1.24 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
1.25 +=== inhibit exn 110722=============================================================*)
1.26
1.27
1.28 "----------- rewrite-order ord_simplify_System -------------------";
1.29 @@ -180,7 +181,7 @@
1.30 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
1.31 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
1.32 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
1.33 -val thy = (theory "Isac") (*because of Undeclared constant "Biegelinie.EI*);
1.34 +val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
1.35 val t =
1.36 str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
1.37 \ -1 * q_0 / 24 * 0 ^^^ 4),\
1.38 @@ -280,6 +281,7 @@
1.39 \ c + (c_2 + (c_3 + c_4)) = 0]"
1.40 then () else error "eqsystem.sml rewrite in 4x4 order_system";
1.41
1.42 +(*=== inhibit exn 110722=============================================================
1.43
1.44 "----------- script [EqSystem,normalize,2x2] ---------------------";
1.45 "----------- script [EqSystem,normalize,2x2] ---------------------";
1.46 @@ -380,9 +382,6 @@
1.47 \ [BOOL_LIST es__, REAL_LIST v_s]))"
1.48 ;
1.49 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.50 -(*---^^^-OK-----------------------------------------------------------------*)
1.51 -(*---vvv-NOT ok-------------------------------------------------------------*)
1.52 -
1.53
1.54 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
1.55 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
1.56 @@ -392,6 +391,7 @@
1.57 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.58 \ simplify_System_parenthesized False) es_ \
1.59 \ in ([]))";
1.60 +
1.61 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.62 val str =
1.63 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.64 @@ -416,12 +416,10 @@
1.65 \ e1__ = ((Rewrite_Set order_system False)) e1__\
1.66 \ in ([]))";
1.67 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.68 -(*--------------------------------------------------------------------------*)
1.69 val str =
1.70 "(Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.71 \ isolate_bdvs False) (e1__::bool)";
1.72 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.73 -(*--------------------------------------------------------------------------*)
1.74 val str =
1.75 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.76 \ (let e1__ = Take (hd es_); \
1.77 @@ -514,7 +512,8 @@
1.78 \ in [e1__, e2__])"
1.79 ;
1.80 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.81 -(*---^^^-OK-----------------------------------------------------------------*)
1.82 +=== inhibit exn 110722=============================================================*)
1.83 +
1.84 val str =
1.85 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.86 \ (let e1__ = Take (hd es_); \
1.87 @@ -533,19 +532,22 @@
1.88 \ es__ = Take [e1__, e2__]\
1.89 \ in (Try (Rewrite_Set order_system False)) es__)"
1.90 ;
1.91 +(*=== inhibit exn 110722=============================================================
1.92 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.93 -(*---vvv-NOT ok-------------------------------------------------------------*)
1.94 +
1.95 atomty sc;
1.96 +=== inhibit exn 110722=============================================================*)
1.97
1.98 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
1.99 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
1.100 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
1.101 val str =
1.102 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.103 -\ (let es__ = Take es_; \
1.104 -\ e1__ = hd es__\
1.105 +"Script SolveSystemScript (es_s::bool list) (v_s::real list) = \
1.106 +\ (let es__s = Take es_s; \
1.107 +\ e1__1 = hd es__e\
1.108 \ in ([]))"
1.109 ;
1.110 +(*=== inhibit exn 110722=============================================================
1.111 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.112 val str =
1.113 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.114 @@ -641,7 +643,8 @@
1.115 \ simplify_System False))) es__)"
1.116 ;
1.117 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.118 -(*---^^^-OK-----------------------------------------------------------------*)
1.119 +=== inhibit exn 110722=============================================================*)
1.120 +
1.121 val str =
1.122 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.123 \ (let es__ = Take es_; \
1.124 @@ -657,9 +660,11 @@
1.125 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.126 \ simplify_System False))) es__)"
1.127 ;
1.128 +(*=== inhibit exn 110722=============================================================
1.129 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.130 -(*---vvv-NOT ok-------------------------------------------------------------*)
1.131 +
1.132 atomty sc;
1.133 +=== inhibit exn 110722=============================================================*)
1.134
1.135
1.136 "----------- refine [linear,system]-------------------------------";
1.137 @@ -668,6 +673,7 @@
1.138 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
1.139 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
1.140 "solveForVars [c, c_2]", "solution L"];
1.141 +(*=== inhibit exn 110722=============================================================
1.142 val matches = refine fmz ["linear","system"];
1.143 case matches of [_,_,_,
1.144 Matches (["normalize", "2x2", "linear", "system"],
1.145 @@ -682,8 +688,10 @@
1.146 | _ => error "eqsystem.sml refine ['normalize','2x2'...]";
1.147
1.148
1.149 +=== inhibit exn 110722=============================================================*)
1.150 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
1.151 "solveForVars [c, c_2]", "solution L"];
1.152 +(*=== inhibit exn 110722=============================================================
1.153 val matches = refine fmz ["linear","system"];
1.154 case matches of [_,_,
1.155 Matches
1.156 @@ -701,6 +709,8 @@
1.157 "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"],
1.158 Relate = []})] => ()
1.159 | _ => error "eqsystem.sml refine ['triangular','2x2'...]";
1.160 +=== inhibit exn 110722=============================================================*)
1.161 +(*=== inhibit exn 110722=============================================================
1.162
1.163
1.164 (*WN051014----------------------------------------------------------------
1.165 @@ -728,7 +738,7 @@
1.166
1.167 ... i.e Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
1.168 trace_rewrite:=false;
1.169 -(*WN051014------------------------------------------------------------------*)
1.170 +
1.171
1.172 "----- relaxed preconditions for triangular system";
1.173 val fmz = ["equalities [L * q_0 = c, \
1.174 @@ -1444,4 +1454,4 @@
1.175 use"../smltest/IsacKnowledge/eqsystem.sml";
1.176 use"eqsystem.sml";
1.177 *)
1.178 -===== inhibit exn ?===========================================================*)
1.179 +===== inhibit exn 110722===========================================================*)