1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Sat Mar 10 14:53:18 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Tue Mar 13 15:04:09 2012 +0100
1.3 @@ -1127,7 +1127,7 @@
1.4
1.5
1.6 (*. for math-experts .*)
1.7 -(*19.10.02FIXME: needs thy for parsing fmz*)
1.8 +(*FIXME.WN021019: needs thy for parsing fmz*)
1.9 (* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID;
1.10 val pbls = []; val ptys = !ptyps;
1.11 *)
2.1 --- a/test/Tools/isac/Interpret/ptyps.sml Sat Mar 10 14:53:18 2012 +0100
2.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Tue Mar 13 15:04:09 2012 +0100
2.3 @@ -1,11 +1,7 @@
2.4 (* Title: tests for ME/ptyps.sml
2.5 CAUTION: intermediately stores !ptyps THUS EVALUATE IN 1 GO
2.6 - uthor: Walther Neuper
2.7 - 010916,
2.8 + Author: Walther Neuper 010916
2.9 (c) due to copyright terms
2.10 -
2.11 -use"../smltest/ME/ptyps.sml";
2.12 -use"ptyps.sml";
2.13 *)
2.14
2.15 "--------------------------------------------------------";
2.16 @@ -33,74 +29,59 @@
2.17 "----------- store test-pbtyps -----------------------------------";
2.18 "----------- store test-pbtyps -----------------------------------";
2.19 ptyps:= ([]:ptyps);
2.20 -(*========== inhibit exn AK110725 ======================================================
2.21 store_pbt
2.22 (prep_pbt @{theory DiffApp} "pbl_pbla" [] e_pblID
2.23 (["pbla"],
2.24 - [("#Given", ["fixedValues a_"])], e_rls, NONE, []));
2.25 + [("#Given", ["fixedValues a_a"])], e_rls, NONE, []));
2.26 store_pbt
2.27 - (prep_pbt DiffApp.thy "pbl_pbla1" [] e_pblID
2.28 + (prep_pbt @{theory DiffApp} "pbl_pbla1" [] e_pblID
2.29 (["pbla1","pbla"],
2.30 - [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, NONE, []));
2.31 + [("#Given", ["fixedValues a_a","maximum a_1"])], e_rls, NONE, []));
2.32 store_pbt
2.33 - (prep_pbt DiffApp.thy "pbl_pbla2" [] e_pblID
2.34 + (prep_pbt @{theory DiffApp} "pbl_pbla2" [] e_pblID
2.35 (["pbla2","pbla"],
2.36 - [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, NONE, []));
2.37 + [("#Given", ["fixedValues a_a","valuesFor a_2"])], e_rls, NONE, []));
2.38 store_pbt
2.39 - (prep_pbt DiffApp.thy "pbl_pbla2x" [] e_pblID
2.40 + (prep_pbt @{theory DiffApp} "pbl_pbla2x" [] e_pblID
2.41 (["pbla2x","pbla2","pbla"],
2.42 - [("#Given", ["fixedValues a_","valuesFor a2_","functionOf a2x_"])],
2.43 + [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])],
2.44 e_rls, NONE, []));
2.45 store_pbt
2.46 - (prep_pbt DiffApp.thy "pbl_pbla2y" [] e_pblID
2.47 + (prep_pbt @{theory DiffApp} "pbl_pbla2y" [] e_pblID
2.48 (["pbla2y","pbla2","pbla"],
2.49 - [("#Given" ,["fixedValues a_","valuesFor a2_","boundVariable a2y_"])],
2.50 + [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])],
2.51 e_rls, NONE, []));
2.52 store_pbt
2.53 - (prep_pbt DiffApp.thy "pbl_pbla2z" [] e_pblID
2.54 + (prep_pbt @{theory DiffApp} "pbl_pbla2z" [] e_pblID
2.55 (["pbla2z","pbla2","pbla"],
2.56 - [("#Given" ,["fixedValues a_","valuesFor a2_","interval a2z_"])],
2.57 + [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])],
2.58 e_rls, NONE, []));
2.59 store_pbt
2.60 - (prep_pbt DiffApp.thy "pbl_pbla3" [] e_pblID
2.61 + (prep_pbt @{theory DiffApp} "pbl_pbla3" [] e_pblID
2.62 (["pbla3","pbla"],
2.63 - [("#Given" ,["fixedValues a_","relations a3_"])],
2.64 + [("#Given" ,["fixedValues a_a","relations a_3"])],
2.65 e_rls, NONE, []));
2.66
2.67 show_ptyps();
2.68 -========== inhibit exn AK110725 ======================================================*)
2.69 +val thy = @{theory "Isac"};
2.70 +val ctxt = ProofContext.init_global @{theory "Isac"};
2.71
2.72 (*case 1: no refinement *)
2.73 -val thy = (@{theory "Isac"});
2.74 -(*========== inhibit exn AK110725 ======================================================
2.75 -val (d1,ts1) = split_dts thy ((term_of o the o (parse thy)) "fixedValues [aaa=0]");
2.76 -val (d2,ts2) = split_dts thy ((term_of o the o (parse thy)) "errorBound (ddd=0)");
2.77 -
2.78 -val ori1 = [(1,[1],"#Given",d1,ts1),
2.79 - (2,[1],"#Given",d2,ts2)]:ori list;
2.80 -
2.81 +val (d1,ts1) = split_dts ((term_of o the o (parse thy)) "fixedValues [aaa = 0]");
2.82 +val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "errorBound (ddd = 0)");
2.83 +val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list;
2.84
2.85 (*case 2: refined to pbt without children *)
2.86 -val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
2.87 - "relations [aaa333]");
2.88 -val ori2 = [(1,[1],"#Given",d1,ts1),
2.89 - (2,[1],"#Given",d2,ts2)]:ori list;
2.90 -
2.91 +val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "relations [aaa333]");
2.92 +val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
2.93
2.94 (*case 3: refined to pbt with children *)
2.95 -val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
2.96 - "valuesFor [aaa222]");
2.97 -val ori3 = [(1,[1],"#Given",d1,ts1),
2.98 - (2,[1],"#Given",d2,ts2)]:ori list;
2.99 -
2.100 +val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "valuesFor [aaa222]");
2.101 +val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
2.102
2.103 (*case 4: refined to children (without child)*)
2.104 -val (d3,ts3) = split_dts thy ((term_of o the o (parse thy))
2.105 - "boundVariable aaa222yyy");
2.106 -val ori4 = [(1,[1],"#Given",d1,ts1),
2.107 - (2,[1],"#Given",d2,ts2),
2.108 - (3,[1],"#Given",d3,ts3)]:ori list;
2.109 -
2.110 +val (d3,ts3) = split_dts ((term_of o the o (parse thy)) "boundVariable aaa222yyy");
2.111 +val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list;
2.112
2.113 "----------- refin test-pbtyps -----------------------------------";
2.114 "----------- refin test-pbtyps -----------------------------------";
2.115 @@ -126,7 +107,6 @@
2.116 refin ["pbla"] ori4 ppp;
2.117 (*val it = SOME ["pbla2","pbla2y"] : pblRD option*)
2.118
2.119 -
2.120 "----------- refine_ori test-pbtyps ------------------------------";
2.121 "----------- refine_ori test-pbtyps ------------------------------";
2.122 "----------- refine_ori test-pbtyps ------------------------------";
2.123 @@ -150,8 +130,6 @@
2.124 (*case 5: start refinement somewhere in ptyps*)
2.125 refine_ori ori4 ["pbla2","pbla"];
2.126 (*val it = SOME ["pbla2y","pbla2","pbla"] : pblID option*)
2.127 -========== inhibit exn AK110725 ======================================================*)
2.128 -
2.129
2.130 "----------- refine test-pbtyps ----------------------------------";
2.131 "----------- refine test-pbtyps ----------------------------------";
2.132 @@ -162,9 +140,13 @@
2.133 val fmz4 = ["fixedValues [aaa=0]","valuesFor [aaa222]",
2.134 "boundVariable aaa222yyy"];
2.135
2.136 -(*========== inhibit exn AK110725 ======================================================
2.137 (*case 1: no refinement *)
2.138 -refine fmz1 ["pbla"];
2.139 +case refine fmz1 ["pbla"] of
2.140 + [Matches (["pbla"], _),
2.141 + NoMatch (["pbla1", "pbla"], _),
2.142 + NoMatch (["pbla2", "pbla"], _),
2.143 + NoMatch (["pbla3", "pbla"], _)] => ()
2.144 + | _ => error "--- refine test-pbtyps --- broken with case 1";
2.145 (*
2.146 *** pass ["pbla"]
2.147 *** pass ["pbla","pbla1"]
2.148 @@ -195,7 +177,12 @@
2.149
2.150
2.151 (*case 2: refined to pbt without children *)
2.152 -refine fmz2 ["pbla"];
2.153 +case refine fmz2 ["pbla"] of
2.154 + [Matches (["pbla"], _),
2.155 + NoMatch (["pbla1", "pbla"], _),
2.156 + NoMatch (["pbla2", "pbla"], _),
2.157 + Matches (["pbla3", "pbla"], _)] => ()
2.158 + | _ => error "--- refine test-pbtyps --- broken with case 2";
2.159 (*
2.160 *** pass ["pbla"]
2.161 *** pass ["pbla","pbla1"]
2.162 @@ -224,7 +211,15 @@
2.163 Relate=[],Where=[],With=[]})] : match list*)
2.164
2.165 (*case 3: refined to pbt with children *)
2.166 -refine fmz3 ["pbla"];
2.167 +case refine fmz3 ["pbla"] of
2.168 + [Matches (["pbla"], _),
2.169 + NoMatch (["pbla1", "pbla"], _),
2.170 + Matches (["pbla2", "pbla"], _),
2.171 + NoMatch (["pbla2x", "pbla2", "pbla"], _),
2.172 + NoMatch (["pbla2y", "pbla2", "pbla"], _),
2.173 + NoMatch (["pbla2z", "pbla2", "pbla"], _),
2.174 + NoMatch (["pbla3", "pbla"], _)] => ()
2.175 + | _ => error "--- refine test-pbtyps --- broken with case 3";
2.176 (*
2.177 *** pass ["pbla"]
2.178 *** pass ["pbla","pbla1"]
2.179 @@ -272,7 +267,13 @@
2.180 : match list*)
2.181
2.182 (*case 4: refined to children (without child)*)
2.183 -refine fmz4 ["pbla"];
2.184 +case refine fmz4 ["pbla"] of
2.185 + [Matches (["pbla"], _),
2.186 + NoMatch (["pbla1", "pbla"], _),
2.187 + Matches (["pbla2", "pbla"], _),
2.188 + NoMatch (["pbla2x", "pbla2", "pbla"], _),
2.189 + Matches (["pbla2y", "pbla2", "pbla"], _)] => ()
2.190 + | _ => error "--- refine test-pbtyps --- broken with case 4";
2.191 (*
2.192 *** pass ["pbla"]
2.193 *** pass ["pbla","pbla1"]
2.194 @@ -310,7 +311,11 @@
2.195 : match list*)
2.196
2.197 (*case 5: start refinement somewhere in ptyps*)
2.198 -refine fmz4 ["pbla2","pbla"];
2.199 +case refine fmz4 ["pbla2","pbla"] of
2.200 + [Matches (["pbla2", "pbla"], _),
2.201 + NoMatch (["pbla2x", "pbla2", "pbla"], _),
2.202 + Matches (["pbla2y", "pbla2", "pbla"], _)] => ()
2.203 + | _ => error "--- refine test-pbtyps --- broken with case 5";
2.204 (*
2.205 *** pass ["pbla","pbla2"]
2.206 *** pass ["pbla","pbla2","pbla2x"]
2.207 @@ -333,38 +338,44 @@
2.208 Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
2.209 Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
2.210 : match list*)
2.211 -========== inhibit exn AK110725 ======================================================*)
2.212
2.213
2.214 "###### ptyps:= intermediate_ptyps;###############################";
2.215 "###### ptyps:= intermediate_ptyps;###############################";
2.216 "###### ptyps:= intermediate_ptyps;###############################";
2.217 ptyps:= intermediate_ptyps;
2.218 +if length (! ptyps) = 12 then () else error "test setup with intermediate_ptyps broken";
2.219 show_ptyps();
2.220
2.221 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
2.222 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
2.223 "----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
2.224 -val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x",
2.225 +(*WN120313: attention: the 'nxt' in the comments are not correct!*)
2.226 +val c = [];
2.227 +val fmz = ["equality ((x+1)*(x+2)=x^^^2+(8::real))","solveFor x",
2.228 "errorBound (eps=0)","solutions L"];
2.229 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
2.230 ["Test","squ-equ-test-subpbl1"]);
2.231 -(*========== inhibit exn AK110725 ======================================================
2.232 -(* ERROR: get_pbt not found: ["sqroot-test","univariate","equation","test"] *)
2.233 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.234 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.235 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.236 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Add_Find", Add_Find "solutions L")*)
2.237
2.238 +val nxt = ("Specify_Problem", Specify_Problem ["linear","univariate","equation","test"]);
2.239 +(*=== specify a not-matching problem ------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
2.240 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.241 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.242 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.243 -(*nxt = ("Add_Find", Add_Find "solutions L")*)
2.244 -
2.245 -
2.246 -val nxt = ("Specify_Problem",(*vvvv---specify a not-matching problem*)
2.247 - Specify_Problem ["linear","univariate","equation","test"]);
2.248 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.249 +if f = Form' (PpcKF (0, EdUndef, 0, Nundef, (Problem [],
2.250 + {Find = [Incompl "solutions"], With = [],
2.251 + Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"],
2.252 + Where = [False ("matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
2.253 + "matches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
2.254 + "matches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
2.255 + "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)")],
2.256 + Relate = []}))) then ()
2.257 +else error "--- Refine_Problem broken 1";
2.258 (*ML> f;
2.259 val it = Form' (PpcKF (0,EdUndef,0,Nundef,
2.260 - (Problem ["linear","univariate","equation","test"],
2.261 + (Problem ["linear","univariate","equation","test"], <<<<<===== diff.to above WN120313
2.262 {Find=[Incompl "solutions []"],
2.263 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
2.264 Correct "solveFor x"],Relate=[],
2.265 @@ -375,12 +386,13 @@
2.266 With=[]}))) : mout
2.267 val nxt = ("Add_Find",Add_Find "solutions L") ????!!!!????*)
2.268
2.269 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
2.270 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*NEW2*);
2.271 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e*);
2.272 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.273 (*val nxt = ("Empty_Tac",Empty_Tac)
2.274 ... Refine_Problem ["linear"..] fails internally 040312: works!?!*)
2.275
2.276 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
2.277 +(*=== refine problem -----------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
2.278 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.279 (*("Specify_Problem", Specify_Problem ["normalize", "univariate", ...])*)
2.280 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.281 @@ -396,14 +408,13 @@
2.282 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.283 (*Subproblem ("Test", ["linear", "univariate", "equation", "test"]*)
2.284
2.285 -
2.286 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.287 (*nxt = Model_Problem ["linear","univariate","equation","test"]*)
2.288 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.289 (*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
2.290 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.291 (**)
2.292 -val (p,_,f,nxt,_,pt) = me nxt p c pt;2
2.293 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.294 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.295 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.296 (*nxt = Specify_Problem ["linear","univariate","equation","test"])*)
2.297 @@ -428,10 +439,9 @@
2.298 (*Check_Postcond ["normalize","univariate","equation","test"])*)
2.299 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.300 val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f;
2.301 -if (snd nxt)=End_Proof' andalso res="[x = 2]" then ()
2.302 +
2.303 +if (snd nxt) = End_Proof' andalso res = "[x = 2]" then ()
2.304 else error "new behaviour in test:refine.sml:miniscript with mini-subpb";
2.305 -========== inhibit exn AK110725 ======================================================*)
2.306 -
2.307
2.308 "----------- fun coll_guhs ---------------------------------------";
2.309 "----------- fun coll_guhs ---------------------------------------";
2.310 @@ -465,7 +475,6 @@
2.311 "----------- fun guh2kestoreID -----------------------------------";
2.312 "----------- fun guh2kestoreID -----------------------------------";
2.313 "----- we assumed the problem-hierarchy containing 3 elements on toplevel";
2.314 -(*========== inhibit exn AK110725 ======================================================
2.315 (* ERROR: Exception Bind raised *)
2.316 val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
2.317 Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (!ptyps);
2.318 @@ -486,4 +495,4 @@
2.319 nodes [] guh3 (!ptyps);
2.320 nodes [] guh21 (!ptyps);
2.321 *)
2.322 -============ inhibit exn AK110725 ====================================================*)
2.323 +
3.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Sat Mar 10 14:53:18 2012 +0100
3.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue Mar 13 15:04:09 2012 +0100
3.3 @@ -18,7 +18,6 @@
3.4 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
3.5 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
3.6 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
3.7 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
3.8 "----------- refine [linear,system]-------------------------------";
3.9 "----------- refine [2x2,linear,system] search error--------------";
3.10 "----------- me [EqSystem,normalize,2x2] -------------------------";
3.11 @@ -30,6 +29,7 @@
3.12 "-----------------------------------------------------------------";
3.13
3.14 val thy = @{theory "EqSystem"};
3.15 +val ctxt = ProofContext.init_global thy;
3.16
3.17 "----------- occur_exactly_in ------------------------------------";
3.18 "----------- occur_exactly_in ------------------------------------";
3.19 @@ -46,81 +46,76 @@
3.20 if not (occur_exactly_in [str2term"c_2"] all t)
3.21 then () else error "eqsystem.sml occur_exactly_in 3";
3.22
3.23 -(*=== inhibit exn 110722=============================================================
3.24 +val t = str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
3.25 +eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
3.26 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
3.27 +if str = "[c, c_2] from [c, c_2,\n" ^
3.28 + " c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True"
3.29 +then () else error "eval_occur_exactly_in [c, c_2]";
3.30
3.31 -val t = str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in \
3.32 - \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
3.33 +val t = str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
3.34 + "-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2");
3.35 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
3.36 -if str = "[c, c_2] from [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True" then ()
3.37 -else error "eval_occur_exactly_in [c, c_2]";
3.38 -
3.39 -val t = str2term"[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in \
3.40 - \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
3.41 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
3.42 -if str = "[c, c_2,\n c_3] from_ [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
3.43 -else error "eval_occur_exactly_in [c, c_2, c_3]";
3.44 +if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
3.45 +" c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False"
3.46 +then () else error "eval_occur_exactly_in [c, c_2, c_3]";
3.47
3.48 val t = str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
3.49 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
3.50 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
3.51 -if str = "[c_2] from_ [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
3.52 -else error "eval_occur_exactly_in [c, c_2, c_3]";
3.53 +if str = "[c_2] from [c, c_2,\n" ^
3.54 + " c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False"
3.55 +then () else error "eval_occur_exactly_in [c, c_2, c_3]";
3.56
3.57 val t = str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
3.58 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
3.59 -if str = "[] from_ [c, c_2, c_3] occur_exactly_in 0 = True" then ()
3.60 +if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
3.61 else error "eval_occur_exactly_in [c, c_2, c_3]";
3.62
3.63 val t =
3.64 str2term
3.65 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";
3.66 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
3.67 -if str = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in \
3.68 +if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
3.69 \-1 * (q_0 * L ^^^ 2) / 2 = True" then ()
3.70 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
3.71
3.72 -
3.73 "----------- problems --------------------------------------------";
3.74 "----------- problems --------------------------------------------";
3.75 "----------- problems --------------------------------------------";
3.76 val t = str2term "LENGTH [x+y=1,y=2] = 2";
3.77 atomty t;
3.78 val testrls = append_rls "testrls" e_rls
3.79 - [(Thm ("length_Nil_",num_str @{thm length_Nil_})),
3.80 - (Thm ("length_Cons_",num_str @{thm length_Cons_})),
3.81 + [(Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL})),
3.82 + (Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS})),
3.83 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
3.84 Calc ("HOL.eq",eval_equal "#equal_")
3.85 ];
3.86 val SOME (t',_) = rewrite_set_ thy false testrls t;
3.87 -if term2str t' = "HOL.True" then ()
3.88 +if term2str t' = "True" then ()
3.89 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
3.90
3.91 -val SOME t = parse EqSystem.thy "solution L";
3.92 +val SOME t = parse thy "solution L";
3.93 atomty (term_of t);
3.94 -val SOME t = parse Biegelinie.thy "solution L";
3.95 +val SOME t = parse thy "solution L";
3.96 atomty (term_of t);
3.97
3.98 val t = str2term
3.99 -"(tl (tl (tl v_s))) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))";
3.100 +"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
3.101 atomty t;
3.102 -val t = str2term
3.103 -"(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \
3.104 -\(nth_ 1 [c_4 = 1, 2=2,3=3,4=4])";
3.105 +val t = str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
3.106 + "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
3.107 val SOME (t,_) =
3.108 rewrite_set_ thy true
3.109 (append_rls "prls_" e_rls
3.110 - [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
3.111 - Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
3.112 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
3.113 - Thm ("tl_Nil",num_str @{thm tl_Nil}),
3.114 - Calc ("EqSystem.occur'_exactly'_in",
3.115 - eval_occur_exactly_in
3.116 - "#eval_occur_exactly_in_")
3.117 + [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
3.118 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
3.119 + Thm ("TL_CONS",num_str @{thm tl_Cons}),
3.120 + Thm ("TL_NIL",num_str @{thm tl_Nil}),
3.121 + Calc ("EqSystem.occur'_exactly'_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
3.122 ]) t;
3.123 if t = HOLogic.true_const then ()
3.124 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
3.125 -=== inhibit exn 110722=============================================================*)
3.126 -
3.127
3.128 "----------- rewrite-order ord_simplify_System -------------------";
3.129 "----------- rewrite-order ord_simplify_System -------------------";
3.130 @@ -280,63 +275,6 @@
3.131 \ c + (c_2 + (c_3 + c_4)) = 0]"
3.132 then () else error "eqsystem.sml rewrite in 4x4 order_system";
3.133
3.134 -
3.135 -val str =
3.136 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
3.137 -\ (let e1__ = Take (hd es_); \
3.138 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
3.139 -\ isolate_bdvs False)) @@ \
3.140 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
3.141 -\ simplify_System False))) e1__; \
3.142 -\ e2__ = Take (hd (tl es_)); \
3.143 -\ e2__ = ((Substitute [e1__]) @@ \
3.144 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
3.145 -\ simplify_System_parenthesized False)) @@ \
3.146 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
3.147 -\ isolate_bdvs False)) @@ \
3.148 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
3.149 -\ simplify_System False))) e2__; \
3.150 -\ es__ = Take [e1__, e2__]\
3.151 -\ in (Try (Rewrite_Set order_system False)) es__)"
3.152 -;
3.153 -(*=== inhibit exn 110722=============================================================
3.154 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
3.155 -
3.156 -atomty sc;
3.157 -=== inhibit exn 110722=============================================================*)
3.158 -
3.159 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
3.160 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
3.161 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
3.162 -val str =
3.163 -"Script SolveSystemScript (es_s::bool list) (v_s::real list) = \
3.164 -\ (let es__s = Take es_s; \
3.165 -\ e1__1 = hd es__e\
3.166 -\ in ([]))"
3.167 -;
3.168 -
3.169 -val str =
3.170 -"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
3.171 -\ (let es__ = Take es_; \
3.172 -\ e1__ = hd es__; \
3.173 -\ e2__ = hd (tl es__); \
3.174 -\ es__ = [e1__, Substitute [e1__] e2__] "^
3.175 -(* this ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'
3.176 - which is not yet searched for 'STac's; thus this script does not yet work*)
3.177 -" in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
3.178 -\ simplify_System_parenthesized False)) @@ \
3.179 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
3.180 -\ isolate_bdvs False)) @@ \
3.181 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
3.182 -\ simplify_System False))) es__)"
3.183 -;
3.184 -(*=== inhibit exn 110722=============================================================
3.185 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
3.186 -
3.187 -atomty sc;
3.188 -=== inhibit exn 110722=============================================================*)
3.189 -
3.190 -
3.191 "----------- refine [linear,system]-------------------------------";
3.192 "----------- refine [linear,system]-------------------------------";
3.193 "----------- refine [linear,system]-------------------------------";
3.194 @@ -380,7 +318,7 @@
3.195 Relate = []})] => ()
3.196 | _ => error "eqsystem.sml refine ['triangular','2x2'...]";
3.197 === inhibit exn 110722=============================================================*)
3.198 -(*=== inhibit exn 110722=============================================================
3.199 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.200
3.201
3.202 (*WN051014----------------------------------------------------------------
3.203 @@ -398,7 +336,7 @@
3.204 trace_rewrite:=true;
3.205 val SOME (t',_) = rewrite_set_ thy false prls_triangular t;
3.206 (*found:...
3.207 -## try thm: nth_Cons_
3.208 +## try thm: NTH_CONS
3.209 ### eval asms: 1 < 2 + - 1
3.210 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L ^^^ 2 / 2] =
3.211 nth_ (2 + - 1 + - 1) []
3.212 @@ -443,7 +381,9 @@
3.213 [Matches (["triangular", "4x4", "linear", "system"], _)] => ()
3.214 | _ => error "eqsystem.sml: refine relaxed triangular sys Matches";
3.215 val matches = refine fmz ["linear","system"];
3.216 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
3.217
3.218 +(*=== inhibit exn 110722=============================================================
3.219
3.220 "----------- refine [2x2,linear,system] search error--------------";
3.221 "----------- refine [2x2,linear,system] search error--------------";
4.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Sat Mar 10 14:53:18 2012 +0100
4.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Mar 13 15:04:09 2012 +0100
4.3 @@ -129,12 +129,11 @@
4.4 " a kleiner b ==> (b + a) = (a + b)";
4.5 str2term "aaa";
4.6 str2term "222 * aaa";
4.7 -(*
4.8 +
4.9 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of
4.10 - SOME ("12 kleiner 9 = False", _) => ()
4.11 + SOME ("123 kleiner 32 = False", _) => ()
4.12 | _ => error "polyminus.sml: 12 kleiner 9 = False";
4.13 -*)
4.14 -(*========== inhibit exn =======================================================
4.15 +
4.16 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of
4.17 SOME ("a kleiner b = True", _) => ()
4.18 | _ => error "polyminus.sml: a kleiner b = True";
4.19 @@ -159,10 +158,7 @@
4.20 SOME ("3 * a * b kleiner c = True", _) => ()
4.21 | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
4.22
4.23 -============ inhibit exn =====================================================*)
4.24 -
4.25 -
4.26 -"----- compare tausche_plus with real_num_collect";
4.27 +"======= compare tausche_plus with real_num_collect";
4.28 val od = dummy_ord;
4.29
4.30 val erls = erls_ordne_alphabetisch;
4.31 @@ -175,7 +171,7 @@
4.32 val t = str2term "2*a + 3*a";
4.33 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; term2str t;
4.34
4.35 -"----- test rewrite_, rewrite_set_";
4.36 +"======= test rewrite_, rewrite_set_";
4.37 trace_rewrite:=true;
4.38 val erls = erls_ordne_alphabetisch;
4.39 val t = str2term "b + a";
4.40 @@ -193,7 +189,7 @@
4.41 if term2str t = "a + b + c" then ()
4.42 else error "polyminus.sml: ordne_alphabetisch a + b + c";
4.43
4.44 -"----- rewrite goes into subterms";
4.45 +"======= rewrite goes into subterms";
4.46 val t = str2term "a + c + b + d";
4.47 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; term2str t;
4.48 if term2str t = "a + b + c + d" then ()
4.49 @@ -204,13 +200,13 @@
4.50 if term2str t = "a + b + c + d" then ()
4.51 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
4.52
4.53 -"----- here we see rew_sub going into subterm with cond.rew....";
4.54 +"======= here we see rew_sub going into subterm with cond.rew....";
4.55 val t = str2term "b + a + c + d";
4.56 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t;
4.57 if term2str t = "a + b + c + d" then ()
4.58 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
4.59
4.60 -"----- compile rls for the most complicated terms";
4.61 +"======= compile rls for the most complicated terms";
4.62 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
4.63 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
4.64 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
4.65 @@ -248,7 +244,6 @@
4.66 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.67 atomty sc;
4.68
4.69 -
4.70 "----------- me simplification.for_polynomials.with_minus";
4.71 "----------- me simplification.for_polynomials.with_minus";
4.72 "----------- me simplification.for_polynomials.with_minus";
4.73 @@ -274,7 +269,6 @@
4.74 if f2str f = "3 - 2 * e + 2 * f + 2 * g" andalso #1 nxt = "End_Proof'" then ()
4.75 else error "polyminus.sml: me simplification.for_polynomials.with_minus";
4.76
4.77 -
4.78 "----------- pbl polynom vereinfachen p.33 -----------------------";
4.79 "----------- pbl polynom vereinfachen p.33 -----------------------";
4.80 "----------- pbl polynom vereinfachen p.33 -----------------------";
4.81 @@ -291,7 +285,7 @@
4.82 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
4.83 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
4.84
4.85 -"----------- 140 d ---";
4.86 +"======= 140 d ---";
4.87 states:=[];
4.88 CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
4.89 "normalform N"],
4.90 @@ -304,8 +298,7 @@
4.91 term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
4.92 then () else error "polyminus.sml: Vereinfache 140 d)";
4.93
4.94 -
4.95 -"----------- 139 c ---";
4.96 +"======= 139 c ---";
4.97 states:=[];
4.98 CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
4.99 "normalform N"],
4.100 @@ -318,7 +311,7 @@
4.101 term2str (get_obj g_res pt (fst p)) = "- (3 * f)"
4.102 then () else error "polyminus.sml: Vereinfache 139 c)";
4.103
4.104 -"----------- 139 b ---";
4.105 +"======= 139 b ---";
4.106 states:=[];
4.107 CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
4.108 "normalform N"],
4.109 @@ -331,7 +324,7 @@
4.110 term2str (get_obj g_res pt (fst p)) = "-3 * u - v"
4.111 then () else error "polyminus.sml: Vereinfache 139 b)";
4.112
4.113 -"----------- 138 a ---";
4.114 +"======= 138 a ---";
4.115 states:=[];
4.116 CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)",
4.117 "normalform N"],
4.118 @@ -344,7 +337,6 @@
4.119 term2str (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
4.120 then () else error "polyminus.sml: Vereinfache 138 a)";
4.121
4.122 -
4.123 "----------- met probe fuer_polynom ------------------------------";
4.124 "----------- met probe fuer_polynom ------------------------------";
4.125 "----------- met probe fuer_polynom ------------------------------";
4.126 @@ -358,7 +350,6 @@
4.127 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.128 atomty sc;
4.129
4.130 -
4.131 "----------- pbl polynom probe -----------------------------------";
4.132 "----------- pbl polynom probe -----------------------------------";
4.133 "----------- pbl polynom probe -----------------------------------";
4.134 @@ -382,8 +373,6 @@
4.135 then () else error "polyminus.sml: Probe 11 = 11";
4.136 show_pt pt;
4.137
4.138 -
4.139 -
4.140 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
4.141 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
4.142 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
4.143 @@ -400,7 +389,7 @@
4.144 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
4.145 show_pt pt;
4.146
4.147 -"----- probe p.34 -----";
4.148 +"======= probe p.34 -----";
4.149 states:=[];
4.150 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)",
4.151 "mitWert [u = 2]",
4.152 @@ -413,8 +402,6 @@
4.153 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29"
4.154 then () else error "polyminus.sml: Probe 29 = 29";
4.155 show_pt pt;
4.156 -(*========== inhibit exn 110719 ================================================
4.157 -
4.158
4.159 "----------- try fun applyTactics --------------------------------";
4.160 "----------- try fun applyTactics --------------------------------";
4.161 @@ -471,7 +458,6 @@
4.162 val ((pt,p),_) = get_calc 1; show_pt pt;
4.163 "----- 7 ^^^";
4.164 *)
4.165 -============ inhibit exn 110719 ==============================================*)
4.166 autoCalculate 1 CompleteCalc;
4.167 val ((pt,p),_) = get_calc 1; show_pt pt;
4.168 (*independent from failure above: met_simp_poly_minus not confluent:
4.169 @@ -505,8 +491,6 @@
4.170 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g"
4.171 then () else error "polyminus.sml: tausche_vor_plus";
4.172
4.173 -(*========== inhibit exn 110719 ================================================
4.174 -
4.175 "----------- pbl binom polynom vereinfachen p.39 -----------------";
4.176 "----------- pbl binom polynom vereinfachen p.39 -----------------";
4.177 "----------- pbl binom polynom vereinfachen p.39 -----------------";
4.178 @@ -539,12 +523,7 @@
4.179 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;
4.180 *)
4.181
4.182 -
4.183 -trace_rewrite := true;
4.184 -trace_rewrite := false;
4.185 -
4.186 (*@@@@@@@*)
4.187 -============ inhibit exn 110719 ==============================================*)
4.188 states:=[];
4.189 CalcTree [(["Term ((3*a + 2) * (4*a - 1))",
4.190 "normalform N"],
4.191 @@ -557,8 +536,6 @@
4.192 term2str (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
4.193 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
4.194
4.195 -
4.196 -
4.197 "----------- pbl binom polynom vereinfachen: cube ----------------";
4.198 "----------- pbl binom polynom vereinfachen: cube ----------------";
4.199 "----------- pbl binom polynom vereinfachen: cube ----------------";
4.200 @@ -572,24 +549,18 @@
4.201 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
4.202 then () else error "pbl binom polynom vereinfachen: cube";
4.203
4.204 -(*========== inhibit exn 110719 ================================================
4.205 -
4.206 "----------- refine Vereinfache ----------------------------------";
4.207 "----------- refine Vereinfache ----------------------------------";
4.208 "----------- refine Vereinfache ----------------------------------";
4.209 -val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))",
4.210 - "normalform N"];
4.211 +val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
4.212 print_depth 11;
4.213 val matches = refine fmz ["vereinfachen"];
4.214 print_depth 3;
4.215
4.216 "----- go into details, if it seems not to work -----";
4.217 "--- does the predicate evaluate correctly ?";
4.218 -(*=== inhibit exn ==============================================================
4.219 -!!!!! no '?a' ............
4.220 val t = str2term
4.221 - "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + \
4.222 - \3 * (a - 2 * q))";
4.223 + "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
4.224 val ma = eval_matchsub "" "Tools.matchsub" t thy;
4.225 case ma of
4.226 SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
4.227 @@ -621,10 +592,8 @@
4.228 trace_rewrite := true;
4.229 val SOME (t', _) = rewrite_set_ thy false prls t;
4.230 trace_rewrite := false;
4.231 -if term2str t' = "HOL.False" then ()
4.232 +if term2str t' = "False" then ()
4.233 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
4.234 -============ inhibit exn =====================================================*)
4.235 -
4.236
4.237 "----------- *** prep_pbt: syntax error in '#Where' of [v";
4.238 "----------- *** prep_pbt: syntax error in '#Where' of [v";
4.239 @@ -635,11 +604,11 @@
4.240 " matchsub (?a + (?b - ?c)) t_t | " ^
4.241 " matchsub (?a - (?b + ?c)) t_t | " ^
4.242 " matchsub (?a + (?b - ?c)) t_t )");
4.243 -show_types := true;
4.244 +(*show_types := true;
4.245 if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
4.246 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
4.247 -show_types := false;
4.248 +show_types := false;*)
4.249 +if term2str t = "~ (matchsub (?a + (?b + ?c)) t_t |\n matchsub (?a + (?b - ?c)) t_t |\n" ^
4.250 +" matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
4.251 +then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
4.252
4.253 -
4.254 -============ inhibit exn 110719 ==============================================*)
4.255 -
5.1 --- a/test/Tools/isac/ProgLang/listC.sml Sat Mar 10 14:53:18 2012 +0100
5.2 +++ b/test/Tools/isac/ProgLang/listC.sml Tue Mar 13 15:04:09 2012 +0100
5.3 @@ -10,17 +10,17 @@
5.4 "--------------------- nth_ ----------------------------------------------";
5.5 val t = str2term "nth_ 3 [a,b,c,d,e]";
5.6 atomty t;
5.7 -val thm = (#prop o rep_thm o num_str) nth_Cons_;
5.8 +val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS};
5.9 atomty thm;
5.10 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Cons_}) t;
5.11 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_CONS}) t;
5.12 if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then ()
5.13 else error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
5.14
5.15 val t = str2term "nth_ 1 [a,b,c,d,e]";
5.16 atomty t;
5.17 -val thm = (#prop o rep_thm o num_str) nth_Nil_;
5.18 +val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};
5.19 atomty thm;
5.20 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm nth_Nil_}) t;
5.21 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{thm NTH_NIL}) t;
5.22 term2str t';
5.23 "a";
5.24
5.25 @@ -33,7 +33,7 @@
5.26 "c";
5.27
5.28 (*-------------------------------------------------------------------*)
5.29 -val SOME (Thm (_,thm)) = rls_get_thm list_rls "nth_Nil_";
5.30 +val SOME (Thm (_,thm)) = rls_get_thm list_rls "NTH_NIL";
5.31 val ttt = (#prop o rep_thm) thm;
5.32 atomty ttt;
5.33 (*Free ( 1, real) ...OK, Var ((x, 0), ?'a) OK*)
5.34 @@ -45,11 +45,11 @@
5.35 "--------------------- length_ -------------------------------------------";
5.36 val thy' = "ListG";
5.37 val ct = "length_ [1,1,1]";
5.38 -val thm = ("length_Cons_","");
5.39 +val thm = (@{thm LENGTH_CONS},"");
5.40 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
5.41 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
5.42 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
5.43 -val thm = ("length_Nil_","");
5.44 +val thm = (@{thm LENGTH_NIL},"");
5.45 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct);
5.46 if ct="1 + (1 + (1 + 0))"then()
5.47 else error ("list_rls.sml 1: behaviour of test-expl changed: "^ct);
6.1 --- a/test/Tools/isac/Test_Isac.thy Sat Mar 10 14:53:18 2012 +0100
6.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Mar 13 15:04:09 2012 +0100
6.3 @@ -123,7 +123,7 @@
6.4 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
6.5 use "Interpret/mstools.sml"
6.6 use "Interpret/ctree.sml" (*!...!see(25)*)
6.7 - use "Interpret/ptyps.sml" (*part.*)
6.8 + use "Interpret/ptyps.sml"
6.9 use "Interpret/generate.sml"
6.10 use "Interpret/calchead.sml" (*part.*)
6.11 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
6.12 @@ -155,7 +155,7 @@
6.13 (*use "Knowledge/rational.sml" part.; diff.emacs--jedit*)
6.14 (*use "Knowledge/equation.sml" 2002*)
6.15 (*use "Knowledge/root.sml" 2002*)
6.16 - use "Knowledge/lineq.sml" (*new 2011*)
6.17 + use "Knowledge/lineq.sml" (*new 2011*) (*part.*)
6.18 (*use "Knowledge/rooteq.sml" 2002*)
6.19 (*use "Knowledge/rateq.sml" 2002*)
6.20 use "Knowledge/rootrat.sml"
6.21 @@ -171,9 +171,9 @@
6.22 diff.emacs--jedit*)
6.23 use "Knowledge/eqsystem.sml" (*part.*)
6.24 use "Knowledge/test.sml"
6.25 - use "Knowledge/polyminus.sml" (*part.*)
6.26 + use "Knowledge/polyminus.sml"
6.27 use "Knowledge/vect.sml"
6.28 - use "Knowledge/diffapp.sml" (*part.*)
6.29 + use "Knowledge/diffapp.sml" (*postponed*)
6.30 use "Knowledge/biegelinie.sml"
6.31 use "Knowledge/algein.sml"
6.32 use "Knowledge/diophanteq.sml"
7.1 --- a/test/Tools/isac/Test_Some.thy Sat Mar 10 14:53:18 2012 +0100
7.2 +++ b/test/Tools/isac/Test_Some.thy Tue Mar 13 15:04:09 2012 +0100
7.3 @@ -1,10 +1,12 @@
7.4
7.5 theory Test_Some imports Isac begin
7.6
7.7 -use"../../../test/Tools/isac/Knowledge/partial_fractions.sml"
7.8 +use"../../../test/Tools/isac/Interpret/ptyps.sml"
7.9
7.10 ML {*
7.11 *}
7.12 +ML {*
7.13 +*}
7.14 ML {* (*==================*)
7.15 *}
7.16 ML {*
8.1 --- a/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Sat Mar 10 14:53:18 2012 +0100
8.2 +++ b/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Tue Mar 13 15:04:09 2012 +0100
8.3 @@ -1,4 +1,12 @@
8.4 WN110726 see ~/devel/isac/isac-10/isa2009-2/thms-replace-Isa02-Isa09-2.sml
8.5 +-----------------------------------------------------------------------------------------------------------------
8.6 +find_theorems: in emacs
8.7 +(999) name :
8.8 +(999) simp : "?a * (?b + ?c)"
8.9 +Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)"
8.10 +-----------------------------------------------------------------------------------------------------------------
8.11 +
8.12 +(1) ======================================================================= + ===========
8.13 Isabelle2002-isac Isabelle2009-2
8.14 ok
8.15 \ to be checked
8.16 @@ -73,18 +81,20 @@
8.17 ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc
8.18 ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc
8.19 : (thmID * Thm.thm) list
8.20 +
8.21 +
8.22 +(2) ===== thms in Scripts: ================================================ + ===========
8.23 "real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1
8.24 "real_minus_eq_cancel", "(- ?a = - ?b) = (?a = ?b)" Groups.group_add_class.neg_equal_iff_equal:
8.25
8.26 ------------------------------------------------------------------------------------------------------------------
8.27 -find_theorems: in emacs
8.28 -(999) name :
8.29 -(999) simp : "?a * (?b + ?c)"
8.30 -Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)"
8.31 "_ + (_ + (_::nat)) = _ + _ + _"
8.32
8.33 +(3) ===== list funs: ====================================================== + ===========
8.34 + nth_Nil_ NTH_NIL
8.35 + nth_Cons_ NTH_CONS
8.36
8.37 ------------------------------------------------------------------------------------------------------------------
8.38 -list funs:
8.39 -nth_Cons_ NTH_CONS
8.40 -nth_Nil_ NTH_NIL
8.41 + length_Nil_ LENGTH_NIL
8.42 + length_Cons_ LENGTH_CONS
8.43 +
8.44 + tl_Nil_ tl_Nil_
8.45 + tl_Cons_ tl_Cons_