1.1 --- a/src/Tools/isac/Build_Isac.thy Tue Sep 14 12:12:42 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Sep 14 15:46:56 2010 +0200
1.3 @@ -82,13 +82,11 @@
1.4 use_thy "Knowledge/EqSystem"
1.5 use_thy "Knowledge/Biegelinie"
1.6 use_thy "Knowledge/AlgEin"
1.7 - use_thy "Knowledge/Test"
1.8 *)
1.9 + use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*)
1.10 use_thy "Knowledge/Isac"
1.11 ML {* check_guhs_unique := false; *}
1.12 ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
1.13
1.14 -use "../../../test/Tools/isac/Interpret/calchead.sml"
1.15 -
1.16 end
1.17
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Tue Sep 14 12:12:42 2010 +0200
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Tue Sep 14 15:46:56 2010 +0200
2.3 @@ -931,37 +931,23 @@
2.4 of a SubProblem ? see ME/ptyps.sml 'type met '.*)
2.5 fun is_copy_named_idstr str =
2.6 case (rev o explode) str of
2.7 - (*"_"::_ ::"_"::_ => true*)
2.8 - "'"::"'"::"'"::_ => true
2.9 - | _ => false;
2.10 -(*> is_copy_named_idstr "v_i'''";
2.11 -val it = true : bool
2.12 - > is_copy_named_idstr "e_";
2.13 -val it = false : bool
2.14 - > is_copy_named_idstr "L___";
2.15 -val it = true : bool
2.16 -*)
2.17 + (*"_":: _ ::"_"::_ => true*)
2.18 + "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode)) str ^ " T");
2.19 + true)
2.20 + | _ => (tracing ((strs2str o (rev o explode)) str ^ " F"); false);
2.21 +fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
2.22 +
2.23 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
2.24 fun is_copy_named_generating_idstr str =
2.25 if is_copy_named_idstr str
2.26 then case (rev o explode) str of
2.27 - "_"::"_"::"_"::_ => false
2.28 + (*"_"::"_"::"_"::_ => false*)
2.29 + "'"::"'"::"'"::_ => false
2.30 | _ => true
2.31 else false;
2.32 -(*> is_copy_named_generating_idstr "v_i'''";
2.33 -val it = true : bool
2.34 - > is_copy_named_generating_idstr "L___";
2.35 -val it = false : bool
2.36 -*)
2.37 -
2.38 -(*.can this formal argument (of a model-pattern) be omitted in the arg-list
2.39 - of a SubProblem ? see ME/ptyps.sml 'type met '.*)
2.40 -fun is_copy_named (_,(_,t)) = (is_copy_named_idstr o free2str) t;
2.41 -(*.should this formal argument (of a model-pattern) create a new identifier?.*)
2.42 -fun is_copy_named_generating (_,(_,t)) =
2.43 +fun is_copy_named_generating (_, (_, t)) =
2.44 (is_copy_named_generating_idstr o free2str) t;
2.45
2.46 -
2.47 (*.split type-wrapper from scr-arg and build part of an ori;
2.48 an type-error is reported immediately, raises an exn,
2.49 subsequent handling of exn provides 2nd part of error message.*)
3.1 --- a/src/Tools/isac/Knowledge/Equation.thy Tue Sep 14 12:12:42 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Tue Sep 14 15:46:56 2010 +0200
3.3 @@ -44,7 +44,7 @@
3.4 (["equation"],
3.5 [("#Given" ,["equality e_e","solveFor v_v"]),
3.6 ("#Where" ,["matches (?a = ?b) e_e"]),
3.7 - ("#Find" ,["solutions v_i'''"])
3.8 + ("#Find" ,["solutions v'i'"])
3.9 ],
3.10 append_rls "equation_prls" e_rls
3.11 [Calc ("Tools.matches",eval_matches "")],
3.12 @@ -56,7 +56,7 @@
3.13 (["univariate","equation"],
3.14 [("#Given" ,["equality e_e","solveFor v_v"]),
3.15 ("#Where" ,["matches (?a = ?b) e_e"]),
3.16 - ("#Find" ,["solutions v_i'''"])
3.17 + ("#Find" ,["solutions v'i'"])
3.18 ],
3.19 univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
3.20
4.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 14 12:12:42 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 14 15:46:56 2010 +0200
4.3 @@ -134,7 +134,7 @@
4.4 "Not( (rhs e_e) is_polyrat_in v_v)",
4.5 "((lhs e_e) has_degree_in v_v)=1",
4.6 "((rhs e_e) has_degree_in v_v)=1"]),
4.7 - ("#Find" ,["solutions v_i'''"])
4.8 + ("#Find" ,["solutions v'i'"])
4.9 ],
4.10 LinEq_prls, SOME "solve (e_e::bool, v_v)",
4.11 [["LinEq","solve_lineq_equation"]]));
4.12 @@ -155,7 +155,7 @@
4.13 [("#Given", ["equality e_e", "solveFor v_v"]),
4.14 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)",
4.15 "((lhs e_e) has_degree_in v_v) = 1"]),
4.16 - ("#Find", ["solutions v_i'''"])
4.17 + ("#Find", ["solutions v'i'"])
4.18 ],
4.19 {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
4.20 calc=[], crls=LinEq_crls, nrls=norm_Poly},
5.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Tue Sep 14 12:12:42 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Tue Sep 14 15:46:56 2010 +0200
5.3 @@ -33,9 +33,9 @@
5.4 (["logarithmic","univariate","equation"],
5.5 [("#Given",["equality e_e","solveFor v_v"]),
5.6 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
5.7 - ("#Find" ,["solutions v_i'''"]),
5.8 - ("#With" ,["||(lhs (Subst (v_i''', v_v) e_e) - " ^
5.9 - " (rhs (Subst (v_i''', v_v) e_e) || < eps)"])
5.10 + ("#Find" ,["solutions v'i'"]),
5.11 + ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
5.12 + " (rhs (Subst (v'i', v_v) e_e) || < eps)"])
5.13 ],
5.14 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
5.15 [["Equation","solve_log"]]));
5.16 @@ -47,7 +47,7 @@
5.17 (["Equation","solve_log"],
5.18 [("#Given" ,["equality e_e","solveFor v_v"]),
5.19 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
5.20 - ("#Find" ,["solutions v_i'''"])
5.21 + ("#Find" ,["solutions v'i'"])
5.22 ],
5.23 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
5.24 calc=[],crls=PolyEq_crls, nrls=norm_Rational},
6.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 14 12:12:42 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 14 15:46:56 2010 +0200
6.3 @@ -849,7 +849,7 @@
6.4 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
6.5 "~((lhs e_e) is_rootTerm_in (v_v::real))",
6.6 "~((rhs e_e) is_rootTerm_in (v_v::real))"]),
6.7 - ("#Find" ,["solutions v_i'''"])
6.8 + ("#Find" ,["solutions v'i'"])
6.9 ],
6.10 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.11 []));
6.12 @@ -862,7 +862,7 @@
6.13 "(lhs e_e) is_poly_in v_v",
6.14 "((lhs e_e) has_degree_in v_v ) = 0"
6.15 ]),
6.16 - ("#Find" ,["solutions v_i'''"])
6.17 + ("#Find" ,["solutions v'i'"])
6.18 ],
6.19 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.20 [["PolyEq","solve_d0_polyeq_equation"]]));
6.21 @@ -876,7 +876,7 @@
6.22 "(lhs e_e) is_poly_in v_v",
6.23 "((lhs e_e) has_degree_in v_v ) = 1"
6.24 ]),
6.25 - ("#Find" ,["solutions v_i'''"])
6.26 + ("#Find" ,["solutions v'i'"])
6.27 ],
6.28 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.29 [["PolyEq","solve_d1_polyeq_equation"]]));
6.30 @@ -890,7 +890,7 @@
6.31 ("#Where" ,["matches (?a = 0) e_e",
6.32 "(lhs e_e) is_poly_in v_v ",
6.33 "((lhs e_e) has_degree_in v_v ) = 2"]),
6.34 - ("#Find" ,["solutions v_i'''"])
6.35 + ("#Find" ,["solutions v'i'"])
6.36 ],
6.37 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.38 [["PolyEq","solve_d2_polyeq_equation"]]));
6.39 @@ -911,7 +911,7 @@
6.40 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
6.41 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
6.42 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),
6.43 - ("#Find" ,["solutions v_i'''"])
6.44 + ("#Find" ,["solutions v'i'"])
6.45 ],
6.46 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.47 [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
6.48 @@ -926,7 +926,7 @@
6.49 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^
6.50 "matches ( ?v_^^^2 = 0) e_e | " ^
6.51 "matches ( ?b*?v_^^^2 = 0) e_e "]),
6.52 - ("#Find" ,["solutions v_i'''"])
6.53 + ("#Find" ,["solutions v'i'"])
6.54 ],
6.55 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.56 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
6.57 @@ -937,7 +937,7 @@
6.58 [("#Given" ,["equality e_e","solveFor v_v"]),
6.59 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
6.60 "matches (?a + ?v_^^^2 = 0) e_e"]),
6.61 - ("#Find" ,["solutions v_i'''"])
6.62 + ("#Find" ,["solutions v'i'"])
6.63 ],
6.64 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.65 [["PolyEq","solve_d2_polyeq_pq_equation"]]));
6.66 @@ -948,7 +948,7 @@
6.67 [("#Given" ,["equality e_e","solveFor v_v"]),
6.68 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^
6.69 "matches (?a + ?b*?v_^^^2 = 0) e_e"]),
6.70 - ("#Find" ,["solutions v_i'''"])
6.71 + ("#Find" ,["solutions v'i'"])
6.72 ],
6.73 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.74 [["PolyEq","solve_d2_polyeq_abc_equation"]]));
6.75 @@ -962,7 +962,7 @@
6.76 ("#Where" ,["matches (?a = 0) e_e",
6.77 "(lhs e_e) is_poly_in v_v ",
6.78 "((lhs e_e) has_degree_in v_v) = 3"]),
6.79 - ("#Find" ,["solutions v_i'''"])
6.80 + ("#Find" ,["solutions v'i'"])
6.81 ],
6.82 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.83 [["PolyEq","solve_d3_polyeq_equation"]]));
6.84 @@ -975,7 +975,7 @@
6.85 ("#Where" ,["matches (?a = 0) e_e",
6.86 "(lhs e_e) is_poly_in v_v ",
6.87 "((lhs e_e) has_degree_in v_v) = 4"]),
6.88 - ("#Find" ,["solutions v_i'''"])
6.89 + ("#Find" ,["solutions v'i'"])
6.90 ],
6.91 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.92 [(*["PolyEq","solve_d4_polyeq_equation"]*)]));
6.93 @@ -987,7 +987,7 @@
6.94 [("#Given" ,["equality e_e","solveFor v_v"]),
6.95 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
6.96 "(Not(((lhs e_e) is_poly_in v_v)))"]),
6.97 - ("#Find" ,["solutions v_i'''"])
6.98 + ("#Find" ,["solutions v'i'"])
6.99 ],
6.100 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.101 [["PolyEq","normalize_poly"]]));
6.102 @@ -998,7 +998,7 @@
6.103 [("#Given" ,["equality e_e","solveFor v_v"]),
6.104 ("#Where" ,["matches (?a = 0) e_e",
6.105 "(lhs e_e) is_expanded_in v_v "]),
6.106 - ("#Find" ,["solutions v_i'''"])
6.107 + ("#Find" ,["solutions v'i'"])
6.108 ],
6.109 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.110 []));
6.111 @@ -1009,7 +1009,7 @@
6.112 (["degree_2","expanded","univariate","equation"],
6.113 [("#Given" ,["equality e_e","solveFor v_v"]),
6.114 ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]),
6.115 - ("#Find" ,["solutions v_i'''"])
6.116 + ("#Find" ,["solutions v'i'"])
6.117 ],
6.118 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
6.119 [["PolyEq","complete_square"]]));
6.120 @@ -1043,7 +1043,7 @@
6.121 [("#Given" ,["equality e_e","solveFor v_v"]),
6.122 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
6.123 "(Not(((lhs e_e) is_poly_in v_v)))"]),
6.124 - ("#Find" ,["solutions v_i'''"])
6.125 + ("#Find" ,["solutions v'i'"])
6.126 ],
6.127 {rew_ord'="termlessI",
6.128 rls'=PolyEq_erls,
6.129 @@ -1070,7 +1070,7 @@
6.130 [("#Given" ,["equality e_e","solveFor v_v"]),
6.131 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
6.132 "((lhs e_e) has_degree_in v_v) = 0"]),
6.133 - ("#Find" ,["solutions v_i'''"])
6.134 + ("#Find" ,["solutions v'i'"])
6.135 ],
6.136 {rew_ord'="termlessI",
6.137 rls'=PolyEq_erls,
6.138 @@ -1091,7 +1091,7 @@
6.139 [("#Given" ,["equality e_e","solveFor v_v"]),
6.140 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
6.141 "((lhs e_e) has_degree_in v_v) = 1"]),
6.142 - ("#Find" ,["solutions v_i'''"])
6.143 + ("#Find" ,["solutions v'i'"])
6.144 ],
6.145 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
6.146 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
6.147 @@ -1112,7 +1112,7 @@
6.148 [("#Given" ,["equality e_e","solveFor v_v"]),
6.149 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
6.150 "((lhs e_e) has_degree_in v_v) = 2"]),
6.151 - ("#Find" ,["solutions v_i'''"])
6.152 + ("#Find" ,["solutions v'i'"])
6.153 ],
6.154 {rew_ord'="termlessI",
6.155 rls'=PolyEq_erls,
6.156 @@ -1139,7 +1139,7 @@
6.157 [("#Given" ,["equality e_e","solveFor v_v"]),
6.158 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
6.159 "((lhs e_e) has_degree_in v_v) = 2"]),
6.160 - ("#Find" ,["solutions v_i'''"])
6.161 + ("#Find" ,["solutions v'i'"])
6.162 ],
6.163 {rew_ord'="termlessI",
6.164 rls'=PolyEq_erls,
6.165 @@ -1166,7 +1166,7 @@
6.166 [("#Given" ,["equality e_e","solveFor v_v"]),
6.167 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
6.168 "((lhs e_e) has_degree_in v_v) = 2"]),
6.169 - ("#Find" ,["solutions v_i'''"])
6.170 + ("#Find" ,["solutions v'i'"])
6.171 ],
6.172 {rew_ord'="termlessI",
6.173 rls'=PolyEq_erls,
6.174 @@ -1190,7 +1190,7 @@
6.175 [("#Given" ,["equality e_e","solveFor v_v"]),
6.176 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
6.177 "((lhs e_e) has_degree_in v_v) = 2"]),
6.178 - ("#Find" ,["solutions v_i'''"])
6.179 + ("#Find" ,["solutions v'i'"])
6.180 ],
6.181 {rew_ord'="termlessI",
6.182 rls'=PolyEq_erls,
6.183 @@ -1214,7 +1214,7 @@
6.184 [("#Given" ,["equality e_e","solveFor v_v"]),
6.185 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
6.186 "((lhs e_e) has_degree_in v_v) = 2"]),
6.187 - ("#Find" ,["solutions v_i'''"])
6.188 + ("#Find" ,["solutions v'i'"])
6.189 ],
6.190 {rew_ord'="termlessI",
6.191 rls'=PolyEq_erls,
6.192 @@ -1238,7 +1238,7 @@
6.193 [("#Given" ,["equality e_e","solveFor v_v"]),
6.194 ("#Where" ,["(lhs e_e) is_poly_in v_v ",
6.195 "((lhs e_e) has_degree_in v_v) = 3"]),
6.196 - ("#Find" ,["solutions v_i'''"])
6.197 + ("#Find" ,["solutions v'i'"])
6.198 ],
6.199 {rew_ord'="termlessI",
6.200 rls'=PolyEq_erls,
6.201 @@ -1271,7 +1271,7 @@
6.202 [("#Given" ,["equality e_e","solveFor v_v"]),
6.203 ("#Where" ,["matches (?a = 0) e_e",
6.204 "((lhs e_e) has_degree_in v_v) = 2"]),
6.205 - ("#Find" ,["solutions v_i'''"])
6.206 + ("#Find" ,["solutions v'i'"])
6.207 ],
6.208 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
6.209 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
7.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Tue Sep 14 12:12:42 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Sep 14 15:46:56 2010 +0200
7.3 @@ -175,7 +175,7 @@
7.4 (["rational","univariate","equation"],
7.5 [("#Given" ,["equality e_e","solveFor v_v"]),
7.6 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
7.7 - ("#Find" ,["solutions v_i'''"])
7.8 + ("#Find" ,["solutions v'i'"])
7.9 ],
7.10
7.11 RatEq_prls, SOME "solve (e_e::bool, v_v)",
7.12 @@ -199,7 +199,7 @@
7.13 (["RatEq","solve_rat_equation"],
7.14 [("#Given" ,["equality e_e","solveFor v_v"]),
7.15 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
7.16 - ("#Find" ,["solutions v_i'''"])
7.17 + ("#Find" ,["solutions v'i'"])
7.18 ],
7.19 {rew_ord'="termlessI",
7.20 rls'=rateq_erls,
8.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 14 12:12:42 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 14 15:46:56 2010 +0200
8.3 @@ -482,7 +482,7 @@
8.4 [("#Given" ,["equality e_e","solveFor v_v"]),
8.5 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
8.6 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
8.7 - ("#Find" ,["solutions v_i'''"])
8.8 + ("#Find" ,["solutions v'i'"])
8.9 ],
8.10 RootEq_prls, SOME "solve (e_e::bool, v_v)",
8.11 []));
8.12 @@ -495,7 +495,7 @@
8.13 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
8.14 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
8.15 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
8.16 - ("#Find" ,["solutions v_i'''"])
8.17 + ("#Find" ,["solutions v'i'"])
8.18 ],
8.19 RootEq_prls, SOME "solve (e_e::bool, v_v)",
8.20 [["RootEq","solve_sq_root_equation"]]));
8.21 @@ -508,7 +508,7 @@
8.22 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
8.23 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
8.24 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
8.25 - ("#Find" ,["solutions v_i'''"])
8.26 + ("#Find" ,["solutions v'i'"])
8.27 ],
8.28 RootEq_prls, SOME "solve (e_e::bool, v_v)",
8.29 [["RootEq","norm_sq_root_equation"]]));
8.30 @@ -532,7 +532,7 @@
8.31 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
8.32 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
8.33 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
8.34 - ("#Find" ,["solutions v_i'''"])
8.35 + ("#Find" ,["solutions v'i'"])
8.36 ],
8.37 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
8.38 calc=[], crls=RootEq_crls, nrls=norm_Poly},
8.39 @@ -558,7 +558,7 @@
8.40 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
8.41 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
8.42 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
8.43 - ("#Find" ,["solutions v_i'''"])
8.44 + ("#Find" ,["solutions v'i'"])
8.45 ],
8.46 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
8.47 prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
8.48 @@ -586,7 +586,7 @@
8.49 (["RootEq","solve_right_sq_root_equation"],
8.50 [("#Given" ,["equality e_e","solveFor v_v"]),
8.51 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
8.52 - ("#Find" ,["solutions v_i'''"])
8.53 + ("#Find" ,["solutions v'i'"])
8.54 ],
8.55 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls,
8.56 prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
8.57 @@ -611,7 +611,7 @@
8.58 (["RootEq","solve_left_sq_root_equation"],
8.59 [("#Given" ,["equality e_e","solveFor v_v"]),
8.60 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
8.61 - ("#Find" ,["solutions v_i'''"])
8.62 + ("#Find" ,["solutions v'i'"])
8.63 ],
8.64 {rew_ord'="termlessI",
8.65 rls'=RootEq_erls,
9.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Sep 14 12:12:42 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Sep 14 15:46:56 2010 +0200
9.3 @@ -7,7 +7,7 @@
9.4 (c) by Richard Lang, 2003
9.5 *)
9.6
9.7 -theory RootRatEq imports RootEq RatEq RootRat begin
9.8 +theory RootRatEq imports LinEq RootEq RatEq RootRat begin
9.9
9.10 consts
9.11
9.12 @@ -144,7 +144,7 @@
9.13 [("#Given" ,["equality e_e","solveFor v_v"]),
9.14 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
9.15 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
9.16 - ("#Find" ,["solutions v_i'''"])
9.17 + ("#Find" ,["solutions v'i'"])
9.18 ],
9.19 RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
9.20 [["RootRatEq","elim_rootrat_equation"]]));
9.21 @@ -164,7 +164,7 @@
9.22 [("#Given" ,["equality e_e","solveFor v_v"]),
9.23 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
9.24 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
9.25 - ("#Find" ,["solutions v_i'''"])
9.26 + ("#Find" ,["solutions v'i'"])
9.27 ],
9.28 {rew_ord'="termlessI",
9.29 rls'=RooRatEq_erls,
10.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Sep 14 12:12:42 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Sep 14 15:46:56 2010 +0200
10.3 @@ -522,7 +522,7 @@
10.4 (["equation","test"],
10.5 [("#Given" ,["equality e_e","solveFor v_v"]),
10.6 ("#Where" ,["matches (?a = ?b) e_e"]),
10.7 - ("#Find" ,["solutions v_i'''"])
10.8 + ("#Find" ,["solutions v'i'"])
10.9 ],
10.10 assoc_rls "matches",
10.11 SOME "solve (e_e::bool, v_v)", []));
10.12 @@ -532,7 +532,7 @@
10.13 (["univariate","equation","test"],
10.14 [("#Given" ,["equality e_e","solveFor v_v"]),
10.15 ("#Where" ,["matches (?a = ?b) e_e"]),
10.16 - ("#Find" ,["solutions v_i'''"])
10.17 + ("#Find" ,["solutions v'i'"])
10.18 ],
10.19 assoc_rls "matches",
10.20 SOME "solve (e_e::bool, v_v)", []));
10.21 @@ -543,7 +543,7 @@
10.22 [("#Given" ,["equality e_e","solveFor v_v"]),
10.23 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
10.24 "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
10.25 - ("#Find" ,["solutions v_i'''"])
10.26 + ("#Find" ,["solutions v'i'"])
10.27 ],
10.28 assoc_rls "matches",
10.29 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
10.30 @@ -595,7 +595,7 @@
10.31 (["Test","solve_linear"]:metID,
10.32 [("#Given" ,["equality e_e","solveFor v_v"]),
10.33 ("#Where" ,["matches (?a = ?b) e_e"]),
10.34 - ("#Find" ,["solutions v_i'''"])
10.35 + ("#Find" ,["solutions v'i'"])
10.36 ],
10.37 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
10.38 prls = assoc_rls "matches", calc = [], crls = tval_rls,
10.39 @@ -783,7 +783,7 @@
10.40 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
10.41 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
10.42 "(matches ( v_v ^^^2 = 0) e_e)"]),
10.43 - ("#Find" ,["solutions v_i'''"])
10.44 + ("#Find" ,["solutions v'i'"])
10.45 ],
10.46 assoc_rls "matches",
10.47 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
10.48 @@ -817,7 +817,7 @@
10.49 (["polynomial","univariate","equation","test"],
10.50 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
10.51 ("#Where" ,["False"]),
10.52 - ("#Find" ,["solutions v_i'''"])
10.53 + ("#Find" ,["solutions v'i'"])
10.54 ],
10.55 e_rls, SOME "solve (e_e::bool, v_v)", []));
10.56
10.57 @@ -825,7 +825,7 @@
10.58 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
10.59 (["degree_two","polynomial","univariate","equation","test"],
10.60 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
10.61 - ("#Find" ,["solutions v_i'''"])
10.62 + ("#Find" ,["solutions v'i'"])
10.63 ],
10.64 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
10.65
10.66 @@ -833,7 +833,7 @@
10.67 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
10.68 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
10.69 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
10.70 - ("#Find" ,["solutions v_i'''"])
10.71 + ("#Find" ,["solutions v'i'"])
10.72 ],
10.73 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
10.74
10.75 @@ -841,7 +841,7 @@
10.76 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
10.77 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
10.78 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
10.79 - ("#Find" ,["solutions v_i'''"])
10.80 + ("#Find" ,["solutions v'i'"])
10.81 ],
10.82 e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
10.83
10.84 @@ -852,7 +852,7 @@
10.85 (["squareroot","univariate","equation","test"],
10.86 [("#Given" ,["equality e_e","solveFor v_v"]),
10.87 ("#Where" ,["contains_root (e_e::bool)"]),
10.88 - ("#Find" ,["solutions v_i'''"])
10.89 + ("#Find" ,["solutions v'i'"])
10.90 ],
10.91 append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
10.92 eval_contains_root "#contains_root_")],
10.93 @@ -863,7 +863,7 @@
10.94 (["normalize","univariate","equation","test"],
10.95 [("#Given" ,["equality e_e","solveFor v_v"]),
10.96 ("#Where" ,[]),
10.97 - ("#Find" ,["solutions v_i'''"])
10.98 + ("#Find" ,["solutions v'i'"])
10.99 ],
10.100 e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
10.101
10.102 @@ -872,7 +872,7 @@
10.103 (["sqroot-test","univariate","equation","test"],
10.104 [("#Given" ,["equality e_e","solveFor v_v"]),
10.105 (*("#Where" ,["contains_root (e_e::bool)"]),*)
10.106 - ("#Find" ,["solutions v_i'''"])
10.107 + ("#Find" ,["solutions v'i'"])
10.108 ],
10.109 e_rls, SOME "solve (e_e::bool, v_v)", []));
10.110
10.111 @@ -889,7 +889,7 @@
10.112 (["Test","sqrt-equ-test"]:metID,
10.113 [("#Given" ,["equality e_e","solveFor v_v"]),
10.114 ("#Where" ,["contains_root (e_e::bool)"]),
10.115 - ("#Find" ,["solutions v_i'''"])
10.116 + ("#Find" ,["solutions v'i'"])
10.117 ],
10.118 {rew_ord'="e_rew_ord",rls'=tval_rls,
10.119 srls =append_rls "srls_contains_root" e_rls
10.120 @@ -923,7 +923,7 @@
10.121 (*root-equation ... for test-*.sml until 8.01*)
10.122 (["Test","squ-equ-test2"]:metID,
10.123 [("#Given" ,["equality e_e","solveFor v_v"]),
10.124 - ("#Find" ,["solutions v_i'''"])
10.125 + ("#Find" ,["solutions v'i'"])
10.126 ],
10.127 {rew_ord'="e_rew_ord",rls'=tval_rls,
10.128 srls = append_rls "srls_contains_root" e_rls
10.129 @@ -957,7 +957,7 @@
10.130 (*tests subproblem fixed linear*)
10.131 (["Test","squ-equ-test-subpbl1"]:metID,
10.132 [("#Given" ,["equality e_e","solveFor v_v"]),
10.133 - ("#Find" ,["solutions v_i'''"])
10.134 + ("#Find" ,["solutions v'i'"])
10.135 ],
10.136 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
10.137 crls=tval_rls, nrls=Test_simplify},
10.138 @@ -978,7 +978,7 @@
10.139 (*tests subproblem fixed degree 2*)
10.140 (["Test","squ-equ-test-subpbl2"]:metID,
10.141 [("#Given" ,["equality e_e","solveFor v_v"]),
10.142 - ("#Find" ,["solutions v_i'''"])
10.143 + ("#Find" ,["solutions v'i'"])
10.144 ],
10.145 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
10.146 crls=tval_rls, nrls=e_rls(*,
10.147 @@ -998,7 +998,7 @@
10.148 (*root-equation: see foils..., but notTerminating*)
10.149 (["Test","square_equation...notTerminating"]:metID,
10.150 [("#Given" ,["equality e_e","solveFor v_v"]),
10.151 - ("#Find" ,["solutions v_i'''"])
10.152 + ("#Find" ,["solutions v'i'"])
10.153 ],
10.154 {rew_ord'="e_rew_ord",rls'=tval_rls,
10.155 srls = append_rls "srls_contains_root" e_rls
10.156 @@ -1031,7 +1031,7 @@
10.157 (*root-equation1:*)
10.158 (["Test","square_equation1"]:metID,
10.159 [("#Given" ,["equality e_e","solveFor v_v"]),
10.160 - ("#Find" ,["solutions v_i'''"])
10.161 + ("#Find" ,["solutions v'i'"])
10.162 ],
10.163 {rew_ord'="e_rew_ord",rls'=tval_rls,
10.164 srls = append_rls "srls_contains_root" e_rls
10.165 @@ -1063,7 +1063,7 @@
10.166 (*root-equation2*)
10.167 (["Test","square_equation2"]:metID,
10.168 [("#Given" ,["equality e_e","solveFor v_v"]),
10.169 - ("#Find" ,["solutions v_i'''"])
10.170 + ("#Find" ,["solutions v'i'"])
10.171 ],
10.172 {rew_ord'="e_rew_ord",rls'=tval_rls,
10.173 srls = append_rls "srls_contains_root" e_rls
10.174 @@ -1096,7 +1096,7 @@
10.175 (*root-equation*)
10.176 (["Test","square_equation"]:metID,
10.177 [("#Given" ,["equality e_e","solveFor v_v"]),
10.178 - ("#Find" ,["solutions v_i'''"])
10.179 + ("#Find" ,["solutions v'i'"])
10.180 ],
10.181 {rew_ord'="e_rew_ord",rls'=tval_rls,
10.182 srls = append_rls "srls_contains_root" e_rls
10.183 @@ -1133,7 +1133,7 @@
10.184 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
10.185 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
10.186 "(matches ( v_v ^^^2 = 0) e_e)"]),
10.187 - ("#Find" ,["solutions v_i'''"])
10.188 + ("#Find" ,["solutions v'i'"])
10.189 ],
10.190 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
10.191 prls = assoc_rls "matches",
10.192 @@ -1155,7 +1155,7 @@
10.193 (["Test","norm_univar_equation"]:metID,
10.194 [("#Given",["equality e_e","solveFor v_v"]),
10.195 ("#Where" ,[]),
10.196 - ("#Find" ,["solutions v_i'''"])
10.197 + ("#Find" ,["solutions v'i'"])
10.198 ],
10.199 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
10.200 calc=[],
11.1 --- a/src/Tools/isac/ROOT.ML Tue Sep 14 12:12:42 2010 +0200
11.2 +++ b/src/Tools/isac/ROOT.ML Tue Sep 14 15:46:56 2010 +0200
11.3 @@ -1,7 +1,7 @@
11.4 (*
11.5 $ cd /usr/local/Isabelle2009-1/src/Tools/isac
11.6 $ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
11.7 -
11.8 +$ ls -l /home/neuper/.isabelle/heaps/polyml-5.3.0_x86-linux/Isac
11.9 *)
11.10
11.11 use_thys ["Build_Isac"];
12.1 --- a/test/Tools/isac/Interpret/calchead.sml Tue Sep 14 12:12:42 2010 +0200
12.2 +++ b/test/Tools/isac/Interpret/calchead.sml Tue Sep 14 15:46:56 2010 +0200
12.3 @@ -7,36 +7,18 @@
12.4 use"calchead.sml";
12.5 *)
12.6
12.7 -"-----------------------------------------------------------------";
12.8 -"table of contents -----------------------------------------------";
12.9 -"-----------------------------------------------------------------";
12.10 -"--------- regression test fun is_copy_named ---------------------";
12.11 -"--------- get_interval after replace} other 2 -------------------";
12.12 -"--------- maximum example with 'specify' ------------------------";
12.13 -"--------- maximum example with 'specify', fmz <> [] -------------";
12.14 -"--------- maximum example with 'specify', fmz = [] --------------";
12.15 -"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";
12.16 -"-----------------------------------------------------------------";
12.17 -"-----------------------------------------------------------------";
12.18 -"-----------------------------------------------------------------";
12.19 -
12.20 -
12.21 -"--------- regression test fun is_copy_named ---------------------";
12.22 -"--------- regression test fun is_copy_named ---------------------";
12.23 -"--------- regression test fun is_copy_named ---------------------";
12.24 -val trm = (1, (2, @{term "v_i'''"}));
12.25 -if is_copy_named trm then () else raise error "regr. is_copy_named";
12.26 -val trm = (1, (2, @{term "e_e"}));
12.27 -if is_copy_named trm then raise error "regr. is_copy_named" else ();
12.28 -val trm = (1, (2, @{term "L'''"}));
12.29 -if is_copy_named trm then () else raise error "regr. is_copy_named";
12.30 -
12.31 -(* out-comment 'structure CalcHead'...
12.32 -val trm = (1, (2, @{term "v_i'''"}));
12.33 -if is_copy_named_generating trm then () else raise error "regr. is_copy_named";
12.34 -val trm = (1, (2, @{term "L'''"}));
12.35 -if is_copy_named_generating trm then raise error "regr. is_copy_named" else ();
12.36 -*)
12.37 +"--------------------------------------------------------";
12.38 +"table of contents --------------------------------------";
12.39 +"--------------------------------------------------------";
12.40 +"--------- get_interval after replace} other 2 ----------";
12.41 +"--------- maximum example with 'specify' ---------------";
12.42 +"--------- maximum example with 'specify', fmz <> [] ----";
12.43 +"--------- maximum example with 'specify', fmz = [] -----";
12.44 +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
12.45 +"--------- regression test fun is_copy_named ------------";
12.46 +"--------------------------------------------------------";
12.47 +"--------------------------------------------------------";
12.48 +"--------------------------------------------------------";
12.49
12.50 (*==========================================================================
12.51 "--------- get_interval after replace} other 2 -------------------";
12.52 @@ -432,3 +414,20 @@
12.53 | _ => raise error "calchead.sml match_ags [univariate,equation,test]--";
12.54
12.55 ==========================================================================*)
12.56 +
12.57 +"--------- regression test fun is_copy_named ------------";
12.58 +"--------- regression test fun is_copy_named ------------";
12.59 +"--------- regression test fun is_copy_named ------------";
12.60 +val trm = (1, (2, @{term "v'i'"}));
12.61 +if is_copy_named trm then () else raise error "regr. is_copy_named 1";
12.62 +val trm = (1, (2, @{term "e_e"}));
12.63 +if is_copy_named trm then raise error "regr. is_copy_named 2" else ();
12.64 +val trm = (1, (2, @{term "L'''"}));
12.65 +if is_copy_named trm then () else raise error "regr. is_copy_named 3";
12.66 +
12.67 +(* out-comment 'structure CalcHead'...
12.68 +val trm = (1, (2, @{term "v'i'"}));
12.69 +if is_copy_named_generating trm then () else raise error "regr. is_copy_named";
12.70 +val trm = (1, (2, @{term "L'''"}));
12.71 +if is_copy_named_generating trm then raise error "regr. is_copy_named" else ();
12.72 +*)
13.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue Sep 14 12:12:42 2010 +0200
13.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Sep 14 15:46:56 2010 +0200
13.3 @@ -6,7 +6,7 @@
13.4 use"../smltest/IsacKnowledge/integrate.sml";
13.5 use"integrate.sml";
13.6 *)
13.7 -val thy = Integrate.thy;
13.8 +val thy = theory "Integrate";
13.9
13.10 "-----------------------------------------------------------------";
13.11 "table of contents -----------------------------------------------";
14.1 --- a/test/Tools/isac/Test_Isac.thy Tue Sep 14 12:12:42 2010 +0200
14.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Sep 14 15:46:56 2010 +0200
14.3 @@ -1,13 +1,15 @@
14.4 (* Title Run_Tests on isac
14.5 $ cd /usr/local/isabisac/test/Tools/isac
14.6 -$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy &
14.7 +$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
14.8
14.9 +RESTART emacs after having created a new Isac heap.
14.10 was sml/RTEST-root.sml in isac-2002
14.11 *)
14.12
14.13 theory Test_Isac imports Isac begin
14.14
14.15 ML{* writeln "**** run the tests **************************************" *};
14.16 +ML {* Toplevel.debug := true; *}
14.17 (*
14.18 cd "systest";
14.19 (*+ check kbtest/diffapp.sml for additional items in met-model*)
14.20 @@ -60,7 +62,9 @@
14.21 use"complex.sml";
14.22 use"diff.sml";
14.23 use"diffapp.sml";
14.24 - use"integrate.sml";
14.25 +*)
14.26 +use"Knowledge/integrate.sml";
14.27 +(*
14.28 use"equation.sml";
14.29 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
14.30 use"logexp.sml";