1.1 --- a/test/Tools/isac/Knowledge/algein.sml Thu Jul 21 12:01:56 2011 +0200
1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Fri Jul 22 14:01:09 2011 +0200
1.3 @@ -17,8 +17,7 @@
1.4 "-----------------------------------------------------------------";
1.5 "-----------------------------------------------------------------";
1.6
1.7 -(*=== inhibit exn ?=============================================================
1.8 -val thy = AlgEin.thy;
1.9 +val thy = @{theory "AlgEin"};
1.10
1.11
1.12 (* use"../smltest/IsacKnowledge/algein.sml";
1.13 @@ -33,8 +32,10 @@
1.14 \ (let t_ = (l_ = 1)\
1.15 \ in t_)"
1.16 ;
1.17 +(*=== inhibit exn 110722=============================================================
1.18 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.19 -(*---^^^-OK-----------------------------------------------------------------*)
1.20 +=== inhibit exn 110722=============================================================*)
1.21 +
1.22 val str =
1.23 "Script RechnenSymbolScript (k_::bool) (q__::bool) \
1.24 \(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
1.25 @@ -46,14 +47,12 @@
1.26 \ t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
1.27 \ in t_)"
1.28 ;
1.29 +(*=== inhibit exn 110722=============================================================
1.30 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.31 -(*---vvv-NOTok--------------------------------------------------------------*)
1.32 -
1.33 -
1.34
1.35 atomty sc;
1.36 atomt sc;
1.37 -
1.38 +=== inhibit exn 110722=============================================================*)
1.39
1.40 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.41 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
1.42 @@ -68,6 +67,7 @@
1.43 ("Isac",["numerischSymbolische", "Berechnung"],
1.44 ["Berechnung","erstNumerisch"]);
1.45 val p = e_pos'; val c = [];
1.46 +(*=== inhibit exn 110722=============================================================
1.47 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
1.48 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
1.49 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
1.50 @@ -97,12 +97,12 @@
1.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.52 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
1.53 else error "algein.sml diff.behav. in erstSymbolisch 99";
1.54 -
1.55 + DEconstrCalcTree 1;
1.56 +=== inhibit exn 110722=============================================================*)
1.57
1.58 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.59 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.60 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
1.61 -states:=[];
1.62 CalcTree
1.63 [(["KantenLaenge (k=10)","Querschnitt (q=1)",
1.64 "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
1.65 @@ -115,9 +115,10 @@
1.66 moveActiveRoot 1;
1.67 autoCalculate 1 CompleteCalc;
1.68 val ((pt,p),_) = get_calc 1; show_pt pt;
1.69 +(*=== inhibit exn 110722=============================================================
1.70 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
1.71 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
1.72 -
1.73 +===== inhibit exn 110722===========================================================*)
1.74 (*
1.75 show_pt pt;
1.76 trace_rewrite:=true;
1.77 @@ -125,14 +126,13 @@
1.78 trace_script:=true;
1.79 trace_script:=false;
1.80 *)
1.81 -
1.82 "----------- Widerspruch 3 = 777 ---------------------------------";
1.83 "----------- Widerspruch 3 = 777 ---------------------------------";
1.84 "----------- Widerspruch 3 = 777 ---------------------------------";
1.85 -val thy = (theory "Isac");
1.86 +val thy = @{theory "Isac"};
1.87 val rew_ord = dummy_ord;
1.88 val erls = Erls;
1.89 -
1.90 +(*===== inhibit exn 110722===========================================================
1.91 val thm = assoc_thm' thy ("sym_real_mult_0_right","");
1.92 val t = str2term "0 = 0";
1.93 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
1.94 @@ -148,6 +148,7 @@
1.95 val t'' = subst_atomic subst t';
1.96 term2str t'';
1.97 (********"0 = 3 * 0"*)
1.98 +===== inhibit exn 110722===========================================================*)
1.99
1.100 val thm = assoc_thm' thy ("sym","");
1.101 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
1.102 @@ -157,4 +158,3 @@
1.103 (* use"../smltest/IsacKnowledge/algein.sml";
1.104 *)
1.105
1.106 -===== inhibit exn ?===========================================================*)
2.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Thu Jul 21 12:01:56 2011 +0200
2.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Fri Jul 22 14:01:09 2011 +0200
2.3 @@ -25,8 +25,8 @@
2.4 "-----------------------------------------------------------------";
2.5 "-----------------------------------------------------------------";
2.6
2.7 -(*=== inhibit exn ?=============================================================
2.8 -val thy = Biegelinie.thy;
2.9 +val thy = @{theory "Biegelinie"};
2.10 +(*=== inhibit exn 110722=============================================================
2.11
2.12 "----------- the rules -------------------------------------------";
2.13 "----------- the rules -------------------------------------------";
2.14 @@ -48,7 +48,7 @@
2.15 term2s t;
2.16 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
2.17 else error "biegelinie.sml: Moment_Neigung";
2.18 -
2.19 +=== inhibit exn 110722=============================================================*)
2.20
2.21 "----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
2.22 "----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
2.23 @@ -114,11 +114,12 @@
2.24 \ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \
2.25 \ in B__)"
2.26 ;
2.27 +(*=== inhibit exn 110722=============================================================
2.28 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.29 -(*---^^^-OK-----------------------------------------------------------------*)
2.30 -(*---vvv-NOTok--------------------------------------------------------------*)
2.31 +
2.32 atomty sc;
2.33 atomt sc;
2.34 +=== inhibit exn 110722=============================================================*)
2.35
2.36 (* use"../smltest/IsacKnowledge/biegelinie.sml";
2.37 *)
2.38 @@ -127,6 +128,7 @@
2.39 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
2.40 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
2.41 val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
2.42 +(*=== inhibit exn 110722=============================================================
2.43 val t = rewrit Moment_Neigung t; term2s t;
2.44 (*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
2.45 ### before declaring "y''" as a constant *)
2.46 @@ -155,9 +157,11 @@
2.47 eval_argument_in "Atools.argument'_in")
2.48 ],
2.49 scr = EmptyScr};
2.50 +=== inhibit exn 110722=============================================================*)
2.51 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
2.52 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
2.53 -val SOME (e1__,_) =
2.54 +(*=== inhibit exn 110722=============================================================
2.55 +val SOME (e1__l,_) =
2.56 rewrite_set_ thy false srls
2.57 (str2term"(nth_::[real,bool list]=>bool) 1 " $ rm_);
2.58 if term2str e1__ = "M_b 0 = 0" then ()
2.59 @@ -168,12 +172,12 @@
2.60 (str2term"argument_in (lhs (M_b 0 = 0))");
2.61 if term2str x1__ = "0" then ()
2.62 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
2.63 +=== inhibit exn 110722=============================================================*)
2.64
2.65 trace_rewrite:=true;
2.66 trace_rewrite:=false;
2.67
2.68
2.69 -
2.70 "----------- Bsp 7.27 me -----------------------------------------";
2.71 "----------- Bsp 7.27 me -----------------------------------------";
2.72 "----------- Bsp 7.27 me -----------------------------------------";
2.73 @@ -207,6 +211,7 @@
2.74 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
2.75 | _ => error "biegelinie.sml: Bsp 7.27 #4b";
2.76
2.77 +(*=== inhibit exn 110722=============================================================
2.78 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.79 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
2.80 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
2.81 @@ -401,6 +406,7 @@
2.82 else error "biegelinie.sml: Bsp 7.27 #24 f";
2.83 case nxt of ("End_Proof'", End_Proof') => ()
2.84 | _ => error "biegelinie.sml: Bsp 7.27 #24";
2.85 +=== inhibit exn 110722=============================================================*)
2.86
2.87 (* use"../smltest/IsacKnowledge/biegelinie.sml";
2.88 *)
2.89 @@ -474,10 +480,12 @@
2.90
2.91 autoCalculate 1 CompleteCalc;
2.92 val ((pt,p),_) = get_calc 1;
2.93 +(*=== inhibit exn 110722=============================================================
2.94 if p = ([], Res) andalso length (children pt) = 23 andalso
2.95 term2str (get_obj g_res pt (fst p)) =
2.96 "y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
2.97 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
2.98 +=== inhibit exn 110722=============================================================*)
2.99
2.100 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
2.101 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
2.102 @@ -511,6 +519,7 @@
2.103 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.104 if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
2.105 then () else error "biegelinie.sml met2 b";
2.106 +(*=== inhibit exn 110722=============================================================
2.107
2.108 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
2.109 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
2.110 @@ -570,6 +579,7 @@
2.111 if nxt = ("End_Proof'", End_Proof') andalso f2str f =
2.112 "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]" then ()
2.113 else error "biegelinie.sml met2 e";
2.114 +=== inhibit exn 110722=============================================================*)
2.115
2.116
2.117
2.118 @@ -580,6 +590,7 @@
2.119 "Script Function2Equality (fun_::bool) (sub_::bool) =\
2.120 \(equ___::bool)"
2.121 ;
2.122 +(*=== inhibit exn 110722=============================================================
2.123 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.124 val str =
2.125 "Script Function2Equality (fun_::bool) (sub_::bool) =\
2.126 @@ -601,7 +612,8 @@
2.127 \ in (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False) equ_)"
2.128 ;
2.129 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.130 -(*---^^^-OK-----------------------------------------------------------------*)
2.131 +=== inhibit exn 110722=============================================================*)
2.132 +
2.133 val str =
2.134 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
2.135 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
2.136 @@ -612,8 +624,8 @@
2.137 \ equ_ = (Substitute [sub_]) fun_\
2.138 \ in (Rewrite_Set_Inst [(bdv_, v_v)] make_ratpoly_in False) equ_)"
2.139 ;
2.140 +(*=== inhibit exn 110722=============================================================
2.141 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.142 -(*---vvv-NOTok--------------------------------------------------------------*)
2.143 atomty sc;
2.144
2.145 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
2.146 @@ -641,6 +653,7 @@
2.147 CHANGE NOT considered, already on leave*)
2.148 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
2.149 then () else error "biegelinie.sml: SubProblem (_,[setzeRandbed";
2.150 +=== inhibit exn 110722=============================================================*)
2.151
2.152
2.153 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
2.154 @@ -652,6 +665,7 @@
2.155 \ (let b1 = Take (nth_ 1 beds_)\
2.156 \ in (equs_::bool list))"
2.157 ;
2.158 +(*=== inhibit exn 110722=============================================================
2.159 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.160 val str =
2.161 "Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
2.162 @@ -705,8 +719,7 @@
2.163 \ in [e1_,e1_])"
2.164 ;
2.165 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.166 -(*---vvv-NOTok--------------------------------------------------------------*)
2.167 -(*---^^^-OK-----------------------------------------------------------------*)
2.168 +
2.169 atomty sc;
2.170
2.171 "----- execute script by manual rewriting";
2.172 @@ -756,6 +769,7 @@
2.173 (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),
2.174 BOOL (y 0 = 0)]*)
2.175 show_types := false;
2.176 +=== inhibit exn 110722=============================================================*)
2.177
2.178
2.179 "----- execute script by interpreter: setzeRandbedingungenEin";
2.180 @@ -768,6 +782,7 @@
2.181 val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"],
2.182 ["Biegelinien","setzeRandbedingungenEin"]);
2.183 val p = e_pos'; val c = [];
2.184 +(*=== inhibit exn 110722=============================================================
2.185 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.186 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.187 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.188 @@ -860,6 +875,7 @@
2.189 (* "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" *)
2.190 "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /\n (-1 * EI * 24),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"
2.191 then () else error "biegelinie.sml met2 oo";
2.192 +=== inhibit exn 110722=============================================================*)
2.193
2.194 (*
2.195 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.196 @@ -870,8 +886,6 @@
2.197 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
2.198 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
2.199 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
2.200 -(*---^^^-OK-----------------------------------------------------------------*)
2.201 -(*---vvv-NOTok--------------------------------------------------------------*)
2.202 val str =
2.203 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
2.204 \ (let b1_ = nth_ 1 rb_; \
2.205 @@ -882,8 +896,8 @@
2.206 \ [BOOL (hd fs_), BOOL b1_]) \
2.207 \ in [e1_,e2_,e3_,e4_])"
2.208 ;
2.209 +(*=== inhibit exn 110722=============================================================
2.210 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.211 -(*---vvv-NOTok--------------------------------------------------------------*)
2.212 val str =
2.213 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
2.214 \ (let b1_ = nth_ 1 rb_; \
2.215 @@ -913,6 +927,7 @@
2.216 \ in [e1_,e2_,e3_,e4_])"
2.217 ;
2.218 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.219 +=== inhibit exn 110722=============================================================*)
2.220
2.221
2.222
2.223 @@ -946,10 +961,8 @@
2.224 \ [REAL (rhs N__), REAL v_v, real_REAL y]) \
2.225 \ in [Q__, M__, N__, B__])"
2.226 ;
2.227 +(*=== inhibit exn 110722=============================================================
2.228 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.229 -(*---^^^-OK-----------------------------------------------------------------*)
2.230 -(*---vvv-NOTok--------------------------------------------------------------*)
2.231 -
2.232
2.233 "----- Bsp 7.70 with me";
2.234 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
2.235 @@ -982,11 +995,11 @@
2.236 ##########################################################################
2.237 BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
2.238 ##########################################################################*)
2.239 +=== inhibit exn 110722=============================================================*)
2.240 "further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------\
2.241 \ ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
2.242 -
2.243 +DEconstrCalcTree 1;
2.244 "----- Bsp 7.70 with autoCalculate";
2.245 -states:=[];
2.246 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
2.247 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
2.248 "FunktionsVariable x"],
2.249 @@ -995,9 +1008,11 @@
2.250 moveActiveRoot 1;
2.251 autoCalculate 1 CompleteCalc;
2.252 val ((pt,p),_) = get_calc 1; show_pt pt;
2.253 +(*=== inhibit exn 110722=============================================================
2.254 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
2.255 "y x =\n-6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 +\n4 * L * q_0 / (-24 * EI) * x ^^^ 3 +\n-1 * q_0 / (-24 * EI) * x ^^^ 4" then ()
2.256 else error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
2.257 +===== inhibit exn 110722===========================================================*)
2.258
2.259 val is = get_istate pt ([],Res); writeln (istate2str is);
2.260 val t = str2term " last \
2.261 @@ -1027,7 +1042,6 @@
2.262 trace_script := true;
2.263 trace_script := false;
2.264
2.265 -
2.266 "----------- investigate normalforms in biegelinien --------------";
2.267 "----------- investigate normalforms in biegelinien --------------";
2.268 "----------- investigate normalforms in biegelinien --------------";
2.269 @@ -1040,4 +1054,4 @@
2.270
2.271 "----- functions comming from:";
2.272
2.273 -===== inhibit exn ?===========================================================*)
2.274 +
3.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Jul 21 12:01:56 2011 +0200
3.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Fri Jul 22 14:01:09 2011 +0200
3.3 @@ -20,7 +20,7 @@
3.4 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
3.5
3.6
3.7 -(*=== inhibit exn ?=============================================================
3.8 +(*=== inhibit exn 110722=============================================================
3.9
3.10
3.11
3.12 @@ -112,6 +112,7 @@
3.13 "additionalRels [(a/2)^^^2 + (b/2)^^^2 = r^^^2]"];
3.14 map (the o (parseold thy)) fmz1;
3.15
3.16 +=== inhibit exn 110722=============================================================*)
3.17
3.18
3.19 "-------------------- ptree of {(a,b). is-max ... --------------------------";
3.20 @@ -271,6 +272,7 @@
3.21 ["DiffApp","max_by_calculus"]);
3.22
3.23 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.24 +(*=== inhibit exn 110722=============================================================
3.25 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.26 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.27 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.28 @@ -294,6 +296,7 @@
3.29 case nxt of (_,Apply_Method ["DiffApp","max_by_calculus"] ) => ()
3.30 | _ => error "diffapp.sml: max-exp me, nxt = Apply_Method";
3.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.32 +=== inhibit exn 110722=============================================================*)
3.33
3.34 (*since 0508 Apply_Method does the 1st step, if NONE init_form -------------
3.35 (*val nxt = ("Subproblem",Subproblem ("DiffApp",["make","function"]))*)
3.36 @@ -305,21 +308,25 @@
3.37 case nxt of (_, Model_Problem(*["by_explicit", "make", "function"]*)) => ()
3.38 | _ => error "diffapp.sml: max-exp me, nxt = Model_Problem";
3.39
3.40 +(*=== inhibit exn 110722=============================================================
3.41 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.42 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.43 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.44 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.45 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.46 +=== inhibit exn 110722=============================================================*)
3.47
3.48 val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
3.49 val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
3.50
3.51 +(*=== inhibit exn 110722=============================================================
3.52 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.53 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.54 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.55 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.56 case nxt of (_, Apply_Method ["DiffApp", "make_fun_by_explicit"]) => ()
3.57 | _ => error "diffapp.sml: max-exp Apply_Method ([1], Met) ";
3.58 +=== inhibit exn 110722=============================================================*)
3.59
3.60 (*----since WN050901 (ie. corr. mathengine#nxt_specify_ ..nxt_spec Pbl->p_
3.61 we get at ...
3.62 @@ -372,9 +379,11 @@
3.63 Error' (Error_ "Refine_Tacitly [\"univariate\",\"equation\"] not applicable")*)
3.64
3.65
3.66 -(*----postponed.15.5.03 run scripts for maximum-example: univariate equation
3.67 +(*----postponed.15.5.03 run scripts for maximum-example: univariate equation*)
3.68 +(*=== inhibit exn 110722=============================================================
3.69
3.70 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
3.71 +=== inhibit exn 110722=============================================================*)
3.72
3.73 val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
3.74
3.75 @@ -384,11 +393,13 @@
3.76 val mits = get_obj g_met pt (fst p);writeln(itms2str_ ctxt mits);
3.77 val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits);
3.78
3.79 +(*=== inhibit exn 110722=============================================================
3.80 itms2args thy ["DiffApp","max_by_calculus"] mits;
3.81
3.82 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.83 +=== inhibit exn 110722=============================================================*)
3.84
3.85 ----*)
3.86 +(*---*)
3.87
3.88 "--------- autoCalc .. scripts for maximum-example ---------------";
3.89 "--------- autoCalc .. scripts for maximum-example ---------------";
3.90 @@ -439,6 +450,7 @@
3.91 *)
3.92
3.93
3.94 +(*=== inhibit exn 110722=============================================================
3.95
3.96 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
3.97 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
3.98 @@ -749,6 +761,4 @@
3.99
3.100
3.101
3.102 -
3.103 -
3.104 -===== inhibit exn ?===========================================================*)
3.105 +===== inhibit exn 110722===========================================================*)
4.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Thu Jul 21 12:01:56 2011 +0200
4.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Fri Jul 22 14:01:09 2011 +0200
4.3 @@ -53,14 +53,12 @@
4.4 ["Test", "solve_diophant"]));
4.5 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
4.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.7 -(*========== inhibit exn WN110318 ==============================================
4.8 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.14 -============ inhibit exn WN110318 ============================================*)
4.15
4.16 "----------- rewriting for usecase2 ---------------------";
4.17 "----------- rewriting for usecase2 ---------------------";
4.18 @@ -100,5 +98,4 @@
4.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.20 (*nxt = ("Empty_Tac", ...) #############################*)
4.21 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.22 -(*========== inhibit exn WN110318 ==============================================
4.23 -============ inhibit exn WN110318 ============================================*)
4.24 +
5.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Thu Jul 21 12:01:56 2011 +0200
5.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Fri Jul 22 14:01:09 2011 +0200
5.3 @@ -30,8 +30,7 @@
5.4 "-----------------------------------------------------------------";
5.5 "-----------------------------------------------------------------";
5.6
5.7 -(*=== inhibit exn ?=============================================================
5.8 -val thy = EqSystem.thy;
5.9 +val thy = @{theory "EqSystem"};
5.10
5.11 "----------- occur_exactly_in ------------------------------------";
5.12 "----------- occur_exactly_in ------------------------------------";
5.13 @@ -48,6 +47,7 @@
5.14 if not (occur_exactly_in [str2term"c_2"] all t)
5.15 then () else error "eqsystem.sml occur_exactly_in 3";
5.16
5.17 +(*=== inhibit exn 110722=============================================================
5.18
5.19 val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \
5.20 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
5.21 @@ -120,6 +120,7 @@
5.22 ]) t;
5.23 if t = HOLogic.true_const then ()
5.24 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
5.25 +=== inhibit exn 110722=============================================================*)
5.26
5.27
5.28 "----------- rewrite-order ord_simplify_System -------------------";
5.29 @@ -180,7 +181,7 @@
5.30 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
5.31 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
5.32 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
5.33 -val thy = (theory "Isac") (*because of Undeclared constant "Biegelinie.EI*);
5.34 +val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
5.35 val t =
5.36 str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
5.37 \ -1 * q_0 / 24 * 0 ^^^ 4),\
5.38 @@ -280,6 +281,7 @@
5.39 \ c + (c_2 + (c_3 + c_4)) = 0]"
5.40 then () else error "eqsystem.sml rewrite in 4x4 order_system";
5.41
5.42 +(*=== inhibit exn 110722=============================================================
5.43
5.44 "----------- script [EqSystem,normalize,2x2] ---------------------";
5.45 "----------- script [EqSystem,normalize,2x2] ---------------------";
5.46 @@ -380,9 +382,6 @@
5.47 \ [BOOL_LIST es__, REAL_LIST v_s]))"
5.48 ;
5.49 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.50 -(*---^^^-OK-----------------------------------------------------------------*)
5.51 -(*---vvv-NOT ok-------------------------------------------------------------*)
5.52 -
5.53
5.54 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
5.55 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
5.56 @@ -392,6 +391,7 @@
5.57 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.58 \ simplify_System_parenthesized False) es_ \
5.59 \ in ([]))";
5.60 +
5.61 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.62 val str =
5.63 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.64 @@ -416,12 +416,10 @@
5.65 \ e1__ = ((Rewrite_Set order_system False)) e1__\
5.66 \ in ([]))";
5.67 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.68 -(*--------------------------------------------------------------------------*)
5.69 val str =
5.70 "(Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.71 \ isolate_bdvs False) (e1__::bool)";
5.72 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.73 -(*--------------------------------------------------------------------------*)
5.74 val str =
5.75 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.76 \ (let e1__ = Take (hd es_); \
5.77 @@ -514,7 +512,8 @@
5.78 \ in [e1__, e2__])"
5.79 ;
5.80 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.81 -(*---^^^-OK-----------------------------------------------------------------*)
5.82 +=== inhibit exn 110722=============================================================*)
5.83 +
5.84 val str =
5.85 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.86 \ (let e1__ = Take (hd es_); \
5.87 @@ -533,19 +532,22 @@
5.88 \ es__ = Take [e1__, e2__]\
5.89 \ in (Try (Rewrite_Set order_system False)) es__)"
5.90 ;
5.91 +(*=== inhibit exn 110722=============================================================
5.92 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.93 -(*---vvv-NOT ok-------------------------------------------------------------*)
5.94 +
5.95 atomty sc;
5.96 +=== inhibit exn 110722=============================================================*)
5.97
5.98 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
5.99 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
5.100 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
5.101 val str =
5.102 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.103 -\ (let es__ = Take es_; \
5.104 -\ e1__ = hd es__\
5.105 +"Script SolveSystemScript (es_s::bool list) (v_s::real list) = \
5.106 +\ (let es__s = Take es_s; \
5.107 +\ e1__1 = hd es__e\
5.108 \ in ([]))"
5.109 ;
5.110 +(*=== inhibit exn 110722=============================================================
5.111 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.112 val str =
5.113 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.114 @@ -641,7 +643,8 @@
5.115 \ simplify_System False))) es__)"
5.116 ;
5.117 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.118 -(*---^^^-OK-----------------------------------------------------------------*)
5.119 +=== inhibit exn 110722=============================================================*)
5.120 +
5.121 val str =
5.122 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
5.123 \ (let es__ = Take es_; \
5.124 @@ -657,9 +660,11 @@
5.125 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
5.126 \ simplify_System False))) es__)"
5.127 ;
5.128 +(*=== inhibit exn 110722=============================================================
5.129 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.130 -(*---vvv-NOT ok-------------------------------------------------------------*)
5.131 +
5.132 atomty sc;
5.133 +=== inhibit exn 110722=============================================================*)
5.134
5.135
5.136 "----------- refine [linear,system]-------------------------------";
5.137 @@ -668,6 +673,7 @@
5.138 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
5.139 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
5.140 "solveForVars [c, c_2]", "solution L"];
5.141 +(*=== inhibit exn 110722=============================================================
5.142 val matches = refine fmz ["linear","system"];
5.143 case matches of [_,_,_,
5.144 Matches (["normalize", "2x2", "linear", "system"],
5.145 @@ -682,8 +688,10 @@
5.146 | _ => error "eqsystem.sml refine ['normalize','2x2'...]";
5.147
5.148
5.149 +=== inhibit exn 110722=============================================================*)
5.150 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
5.151 "solveForVars [c, c_2]", "solution L"];
5.152 +(*=== inhibit exn 110722=============================================================
5.153 val matches = refine fmz ["linear","system"];
5.154 case matches of [_,_,
5.155 Matches
5.156 @@ -701,6 +709,8 @@
5.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]"],
5.158 Relate = []})] => ()
5.159 | _ => error "eqsystem.sml refine ['triangular','2x2'...]";
5.160 +=== inhibit exn 110722=============================================================*)
5.161 +(*=== inhibit exn 110722=============================================================
5.162
5.163
5.164 (*WN051014----------------------------------------------------------------
5.165 @@ -728,7 +738,7 @@
5.166
5.167 ... i.e Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
5.168 trace_rewrite:=false;
5.169 -(*WN051014------------------------------------------------------------------*)
5.170 +
5.171
5.172 "----- relaxed preconditions for triangular system";
5.173 val fmz = ["equalities [L * q_0 = c, \
5.174 @@ -1444,4 +1454,4 @@
5.175 use"../smltest/IsacKnowledge/eqsystem.sml";
5.176 use"eqsystem.sml";
5.177 *)
5.178 -===== inhibit exn ?===========================================================*)
5.179 +===== inhibit exn 110722===========================================================*)
6.1 --- a/test/Tools/isac/Knowledge/isac.sml Thu Jul 21 12:01:56 2011 +0200
6.2 +++ b/test/Tools/isac/Knowledge/isac.sml Fri Jul 22 14:01:09 2011 +0200
6.3 @@ -27,7 +27,7 @@
6.4 "--------------------------------------------------------";
6.5 map Context.theory_name allthys;
6.6 map Context.theory_name isabthys;
6.7 -(*========== inhibit exn 110314 ================================================
6.8 +(*========== inhibit exn 110722 ================================================
6.9 if map Context.theory_name isacthys =
6.10 ["Isac", "Test", "AlgEin", "Biegelinie", "DiffApp", "Vect", "PolyMinus",
6.11 "EqSystem", "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq",
6.12 @@ -36,6 +36,7 @@
6.13 "Language", "Script", "Tools", "ListC"] then ()
6.14 else error "isac.sml: names of isac theories changed";
6.15 "--------------------------------------------------------";
6.16 +========== inhibit exn 110722 ================================================*)
6.17 (* val _ = theory' :=*) (map Context.theory_name isacthys) ~~ isacthys;
6.18
6.19
6.20 @@ -46,13 +47,13 @@
6.21 : (thmID * term) list;
6.22 if length isacthms > 300 then () else error "isac.sml some isacthms dropped";
6.23 "--------------------------------------------------------";
6.24 +(*========== inhibit exn 110722 ================================================
6.25 val all_ListC_thms = PureThy.all_thms_of (@{theory "ListC"});
6.26 val all_Complex_Main_thms = PureThy.all_thms_of (@{theory "Complex_Main"});
6.27 (* delivers [] after 100 secs ...
6.28 subtract Thm.eq_thm (map #2 all_ListC_thms) (map #2 all_Complex_Main_thms);
6.29 ... because ListC contains no thms, but axioms only.*)
6.30 "----- so we cannot get isacthms as thm, only as term ---";
6.31 -
6.32 "----- but we can retain isacrlsthms as thm ---";
6.33 val isacrlsthms = ((*(map (apsnd prop_of)) o*)
6.34 (gen_distinct eq_thmI) o (map rep_thm_G') o flat o
6.35 @@ -65,10 +66,11 @@
6.36 *)
6.37 val thmID = thmID_of_derivation_name dn;
6.38 val thyID = thyID_of_derivation_name dn;
6.39 +============ inhibit exn 110722 ==============================================*)
6.40 (*
6.41 fun eq_thmI' ((thmid1, _), (thmid2, _)) =
6.42 (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
6.43 *)
6.44 val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms);
6.45
6.46 -============ inhibit exn 110314 ==============================================*)
6.47 +
7.1 --- a/test/Tools/isac/Test_Isac.thy Thu Jul 21 12:01:56 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Jul 22 14:01:09 2011 +0200
7.3 @@ -164,13 +164,13 @@
7.4 use "Knowledge/diff.sml" (*part.*)
7.5 use "Knowledge/integrate.sml" (*part. was complete 2009-2
7.6 diff.emacs--jedit*)
7.7 -(*use "Knowledge/eqsystem.sml" 2002*)
7.8 + use "Knowledge/eqsystem.sml" (*part.*)
7.9 use "Knowledge/test.sml" (*complete*)
7.10 use "Knowledge/polyminus.sml" (*part.*)
7.11 -(*use "Knowledge/vect.sml" 2002*)
7.12 -(*use "Knowledge/diffapp.sml" 2002*)
7.13 -(*use "Knowledge/biegelinie.sml" 2002*)
7.14 -(*use "Knowledge/algein.sml" 2002*)
7.15 + use "Knowledge/vect.sml" (*complete*)
7.16 + use "Knowledge/diffapp.sml" (*part.*)
7.17 + use "Knowledge/biegelinie.sml" (*part.*)
7.18 + use "Knowledge/algein.sml" (*part.*)
7.19 use "Knowledge/diophanteq.sml" (*complete*)
7.20 use "Knowledge/isac.sml" (*part.*)
7.21 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
8.1 --- a/test/Tools/isac/Test_Some.thy Thu Jul 21 12:01:56 2011 +0200
8.2 +++ b/test/Tools/isac/Test_Some.thy Fri Jul 22 14:01:09 2011 +0200
8.3 @@ -7,17 +7,19 @@
8.4
8.5 ML{* writeln "**** run the test ***************************************" *}
8.6
8.7 -use"../../../test/Tools/isac/Frontend/interface.sml"
8.8 -
8.9 +use"../../../test/Tools/isac/Knowledge/eqsystem.sml"
8.10 +
8.11 ML{*
8.12 -
8.13 +show_mets()
8.14
8.15 *}
8.16 ML{*
8.17 -
8.18 +show_ptyps();
8.19 +["logarithmic","univariate","equation","test"];
8.20 *}
8.21 ML{*
8.22
8.23 +
8.24 *}
8.25 ML{*
8.26 *}
8.27 @@ -27,8 +29,8 @@
8.28 end
8.29
8.30
8.31 -(*========== inhibit exn 110719 ================================================
8.32 -============ inhibit exn 110719 ==============================================*)
8.33 +(*========== inhibit exn 110722 ================================================
8.34 +============ inhibit exn 110722 ==============================================*)
8.35
8.36
8.37 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.