# HG changeset patch # User Walther Neuper # Date 1284472016 -7200 # Node ID a37a3ab989f4f1d3750f459197f8a5d63db0d78b # Parent b497233515336c9356cd7c1cf6e97c1ca045cf9a repaired copy_nam diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Build_Isac.thy Tue Sep 14 15:46:56 2010 +0200 @@ -82,13 +82,11 @@ use_thy "Knowledge/EqSystem" use_thy "Knowledge/Biegelinie" use_thy "Knowledge/AlgEin" - use_thy "Knowledge/Test" *) + use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*) use_thy "Knowledge/Isac" ML {* check_guhs_unique := false; *} ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *} -use "../../../test/Tools/isac/Interpret/calchead.sml" - end diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Interpret/calchead.sml Tue Sep 14 15:46:56 2010 +0200 @@ -931,37 +931,23 @@ of a SubProblem ? see ME/ptyps.sml 'type met '.*) fun is_copy_named_idstr str = case (rev o explode) str of - (*"_"::_ ::"_"::_ => true*) - "'"::"'"::"'"::_ => true - | _ => false; -(*> is_copy_named_idstr "v_i'''"; -val it = true : bool - > is_copy_named_idstr "e_"; -val it = false : bool - > is_copy_named_idstr "L___"; -val it = true : bool -*) + (*"_":: _ ::"_"::_ => true*) + "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode)) str ^ " T"); + true) + | _ => (tracing ((strs2str o (rev o explode)) str ^ " F"); false); +fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t; + (*.should this formal argument (of a model-pattern) create a new identifier?.*) fun is_copy_named_generating_idstr str = if is_copy_named_idstr str then case (rev o explode) str of - "_"::"_"::"_"::_ => false + (*"_"::"_"::"_"::_ => false*) + "'"::"'"::"'"::_ => false | _ => true else false; -(*> is_copy_named_generating_idstr "v_i'''"; -val it = true : bool - > is_copy_named_generating_idstr "L___"; -val it = false : bool -*) - -(*.can this formal argument (of a model-pattern) be omitted in the arg-list - of a SubProblem ? see ME/ptyps.sml 'type met '.*) -fun is_copy_named (_,(_,t)) = (is_copy_named_idstr o free2str) t; -(*.should this formal argument (of a model-pattern) create a new identifier?.*) -fun is_copy_named_generating (_,(_,t)) = +fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o free2str) t; - (*.split type-wrapper from scr-arg and build part of an ori; an type-error is reported immediately, raises an exn, subsequent handling of exn provides 2nd part of error message.*) diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/Equation.thy --- a/src/Tools/isac/Knowledge/Equation.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Knowledge/Equation.thy Tue Sep 14 15:46:56 2010 +0200 @@ -44,7 +44,7 @@ (["equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], append_rls "equation_prls" e_rls [Calc ("Tools.matches",eval_matches "")], @@ -56,7 +56,7 @@ (["univariate","equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[])); diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/LinEq.thy --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Sep 14 15:46:56 2010 +0200 @@ -134,7 +134,7 @@ "Not( (rhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v)=1", "((rhs e_e) has_degree_in v_v)=1"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq","solve_lineq_equation"]])); @@ -155,7 +155,7 @@ [("#Given", ["equality e_e", "solveFor v_v"]), ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]), - ("#Find", ["solutions v_i'''"]) + ("#Find", ["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls, calc=[], crls=LinEq_crls, nrls=norm_Poly}, diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/LogExp.thy --- a/src/Tools/isac/Knowledge/LogExp.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Knowledge/LogExp.thy Tue Sep 14 15:46:56 2010 +0200 @@ -33,9 +33,9 @@ (["logarithmic","univariate","equation"], [("#Given",["equality e_e","solveFor v_v"]), ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), - ("#Find" ,["solutions v_i'''"]), - ("#With" ,["||(lhs (Subst (v_i''', v_v) e_e) - " ^ - " (rhs (Subst (v_i''', v_v) e_e) || < eps)"]) + ("#Find" ,["solutions v'i'"]), + ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^ + " (rhs (Subst (v'i', v_v) e_e) || < eps)"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]])); @@ -47,7 +47,7 @@ (["Equation","solve_log"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, calc=[],crls=PolyEq_crls, nrls=norm_Rational}, diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/PolyEq.thy --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 14 15:46:56 2010 +0200 @@ -849,7 +849,7 @@ ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))", "~((lhs e_e) is_rootTerm_in (v_v::real))", "~((rhs e_e) is_rootTerm_in (v_v::real))"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])); @@ -862,7 +862,7 @@ "(lhs e_e) is_poly_in v_v", "((lhs e_e) has_degree_in v_v ) = 0" ]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d0_polyeq_equation"]])); @@ -876,7 +876,7 @@ "(lhs e_e) is_poly_in v_v", "((lhs e_e) has_degree_in v_v ) = 1" ]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d1_polyeq_equation"]])); @@ -890,7 +890,7 @@ ("#Where" ,["matches (?a = 0) e_e", "(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v ) = 2"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_equation"]])); @@ -911,7 +911,7 @@ "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^ "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^ "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_sqonly_equation"]])); @@ -926,7 +926,7 @@ "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^ "matches ( ?v_^^^2 = 0) e_e | " ^ "matches ( ?b*?v_^^^2 = 0) e_e "]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])); @@ -937,7 +937,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^ "matches (?a + ?v_^^^2 = 0) e_e"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_pq_equation"]])); @@ -948,7 +948,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^ "matches (?a + ?b*?v_^^^2 = 0) e_e"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_abc_equation"]])); @@ -962,7 +962,7 @@ ("#Where" ,["matches (?a = 0) e_e", "(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d3_polyeq_equation"]])); @@ -975,7 +975,7 @@ ("#Where" ,["matches (?a = 0) e_e", "(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 4"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])); @@ -987,7 +987,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^ "(Not(((lhs e_e) is_poly_in v_v)))"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalize_poly"]])); @@ -998,7 +998,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = 0) e_e", "(lhs e_e) is_expanded_in v_v "]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])); @@ -1009,7 +1009,7 @@ (["degree_2","expanded","univariate","equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","complete_square"]])); @@ -1043,7 +1043,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^ "(Not(((lhs e_e) is_poly_in v_v)))"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1070,7 +1070,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1091,7 +1091,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], @@ -1112,7 +1112,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1139,7 +1139,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1166,7 +1166,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1190,7 +1190,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1214,7 +1214,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1238,7 +1238,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=PolyEq_erls, @@ -1271,7 +1271,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/RatEq.thy --- a/src/Tools/isac/Knowledge/RatEq.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Sep 14 15:46:56 2010 +0200 @@ -175,7 +175,7 @@ (["rational","univariate","equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], RatEq_prls, SOME "solve (e_e::bool, v_v)", @@ -199,7 +199,7 @@ (["RatEq","solve_rat_equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=rateq_erls, diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/RootEq.thy --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Sep 14 15:46:56 2010 +0200 @@ -482,7 +482,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ "(rhs e_e) is_rootTerm_in (v_v::real)"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], RootEq_prls, SOME "solve (e_e::bool, v_v)", [])); @@ -495,7 +495,7 @@ " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])); @@ -508,7 +508,7 @@ " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","norm_sq_root_equation"]])); @@ -532,7 +532,7 @@ " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, calc=[], crls=RootEq_crls, nrls=norm_Poly}, @@ -558,7 +558,7 @@ " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly}, @@ -586,7 +586,7 @@ (["RootEq","solve_right_sq_root_equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly}, @@ -611,7 +611,7 @@ (["RootEq","solve_left_sq_root_equation"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=RootEq_erls, diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/RootRatEq.thy --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Sep 14 15:46:56 2010 +0200 @@ -7,7 +7,7 @@ (c) by Richard Lang, 2003 *) -theory RootRatEq imports RootEq RatEq RootRat begin +theory RootRatEq imports LinEq RootEq RatEq RootRat begin consts @@ -144,7 +144,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^ "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq","elim_rootrat_equation"]])); @@ -164,7 +164,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^ "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="termlessI", rls'=RooRatEq_erls, diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Sep 14 15:46:56 2010 +0200 @@ -522,7 +522,7 @@ (["equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], assoc_rls "matches", SOME "solve (e_e::bool, v_v)", [])); @@ -532,7 +532,7 @@ (["univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], assoc_rls "matches", SOME "solve (e_e::bool, v_v)", [])); @@ -543,7 +543,7 @@ [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^ "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], assoc_rls "matches", SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]])); @@ -595,7 +595,7 @@ (["Test","solve_linear"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches (?a = ?b) e_e"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, prls = assoc_rls "matches", calc = [], crls = tval_rls, @@ -783,7 +783,7 @@ "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ "(matches (?a + v_v ^^^2 = 0) e_e) |" ^ "(matches ( v_v ^^^2 = 0) e_e)"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], assoc_rls "matches", SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]])); @@ -817,7 +817,7 @@ (["polynomial","univariate","equation","test"], [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), ("#Where" ,["False"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], e_rls, SOME "solve (e_e::bool, v_v)", [])); @@ -825,7 +825,7 @@ (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID (["degree_two","polynomial","univariate","equation","test"], [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])); @@ -833,7 +833,7 @@ (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID (["pq_formula","degree_two","polynomial","univariate","equation","test"], [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])); @@ -841,7 +841,7 @@ (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID (["abc_formula","degree_two","polynomial","univariate","equation","test"], [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])); @@ -852,7 +852,7 @@ (["squareroot","univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["contains_root (e_e::bool)"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], append_rls "contains_root" e_rls [Calc ("Test.contains'_root", eval_contains_root "#contains_root_")], @@ -863,7 +863,7 @@ (["normalize","univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,[]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])); @@ -872,7 +872,7 @@ (["sqroot-test","univariate","equation","test"], [("#Given" ,["equality e_e","solveFor v_v"]), (*("#Where" ,["contains_root (e_e::bool)"]),*) - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], e_rls, SOME "solve (e_e::bool, v_v)", [])); @@ -889,7 +889,7 @@ (["Test","sqrt-equ-test"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["contains_root (e_e::bool)"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls =append_rls "srls_contains_root" e_rls @@ -923,7 +923,7 @@ (*root-equation ... for test-*.sml until 8.01*) (["Test","squ-equ-test2"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -957,7 +957,7 @@ (*tests subproblem fixed linear*) (["Test","squ-equ-test-subpbl1"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], crls=tval_rls, nrls=Test_simplify}, @@ -978,7 +978,7 @@ (*tests subproblem fixed degree 2*) (["Test","squ-equ-test-subpbl2"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls(*, @@ -998,7 +998,7 @@ (*root-equation: see foils..., but notTerminating*) (["Test","square_equation...notTerminating"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -1031,7 +1031,7 @@ (*root-equation1:*) (["Test","square_equation1"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -1063,7 +1063,7 @@ (*root-equation2*) (["Test","square_equation2"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -1096,7 +1096,7 @@ (*root-equation*) (["Test","square_equation"]:metID, [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls, srls = append_rls "srls_contains_root" e_rls @@ -1133,7 +1133,7 @@ "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ "(matches (?a + v_v ^^^2 = 0) e_e) |" ^ "(matches ( v_v ^^^2 = 0) e_e)"]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls, prls = assoc_rls "matches", @@ -1155,7 +1155,7 @@ (["Test","norm_univar_equation"]:metID, [("#Given",["equality e_e","solveFor v_v"]), ("#Where" ,[]), - ("#Find" ,["solutions v_i'''"]) + ("#Find" ,["solutions v'i'"]) ], {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls, calc=[], diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/ROOT.ML --- a/src/Tools/isac/ROOT.ML Tue Sep 14 12:12:42 2010 +0200 +++ b/src/Tools/isac/ROOT.ML Tue Sep 14 15:46:56 2010 +0200 @@ -1,7 +1,7 @@ (* $ cd /usr/local/Isabelle2009-1/src/Tools/isac $ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac - +$ ls -l /home/neuper/.isabelle/heaps/polyml-5.3.0_x86-linux/Isac *) use_thys ["Build_Isac"]; diff -r b49723351533 -r a37a3ab989f4 test/Tools/isac/Interpret/calchead.sml --- a/test/Tools/isac/Interpret/calchead.sml Tue Sep 14 12:12:42 2010 +0200 +++ b/test/Tools/isac/Interpret/calchead.sml Tue Sep 14 15:46:56 2010 +0200 @@ -7,36 +7,18 @@ use"calchead.sml"; *) -"-----------------------------------------------------------------"; -"table of contents -----------------------------------------------"; -"-----------------------------------------------------------------"; -"--------- regression test fun is_copy_named ---------------------"; -"--------- get_interval after replace} other 2 -------------------"; -"--------- maximum example with 'specify' ------------------------"; -"--------- maximum example with 'specify', fmz <> [] -------------"; -"--------- maximum example with 'specify', fmz = [] --------------"; -"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; - - -"--------- regression test fun is_copy_named ---------------------"; -"--------- regression test fun is_copy_named ---------------------"; -"--------- regression test fun is_copy_named ---------------------"; -val trm = (1, (2, @{term "v_i'''"})); -if is_copy_named trm then () else raise error "regr. is_copy_named"; -val trm = (1, (2, @{term "e_e"})); -if is_copy_named trm then raise error "regr. is_copy_named" else (); -val trm = (1, (2, @{term "L'''"})); -if is_copy_named trm then () else raise error "regr. is_copy_named"; - -(* out-comment 'structure CalcHead'... -val trm = (1, (2, @{term "v_i'''"})); -if is_copy_named_generating trm then () else raise error "regr. is_copy_named"; -val trm = (1, (2, @{term "L'''"})); -if is_copy_named_generating trm then raise error "regr. is_copy_named" else (); -*) +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"--------- get_interval after replace} other 2 ----------"; +"--------- maximum example with 'specify' ---------------"; +"--------- maximum example with 'specify', fmz <> [] ----"; +"--------- maximum example with 'specify', fmz = [] -----"; +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; +"--------- regression test fun is_copy_named ------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; (*========================================================================== "--------- get_interval after replace} other 2 -------------------"; @@ -432,3 +414,20 @@ | _ => raise error "calchead.sml match_ags [univariate,equation,test]--"; ==========================================================================*) + +"--------- regression test fun is_copy_named ------------"; +"--------- regression test fun is_copy_named ------------"; +"--------- regression test fun is_copy_named ------------"; +val trm = (1, (2, @{term "v'i'"})); +if is_copy_named trm then () else raise error "regr. is_copy_named 1"; +val trm = (1, (2, @{term "e_e"})); +if is_copy_named trm then raise error "regr. is_copy_named 2" else (); +val trm = (1, (2, @{term "L'''"})); +if is_copy_named trm then () else raise error "regr. is_copy_named 3"; + +(* out-comment 'structure CalcHead'... +val trm = (1, (2, @{term "v'i'"})); +if is_copy_named_generating trm then () else raise error "regr. is_copy_named"; +val trm = (1, (2, @{term "L'''"})); +if is_copy_named_generating trm then raise error "regr. is_copy_named" else (); +*) diff -r b49723351533 -r a37a3ab989f4 test/Tools/isac/Knowledge/integrate.sml --- a/test/Tools/isac/Knowledge/integrate.sml Tue Sep 14 12:12:42 2010 +0200 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Sep 14 15:46:56 2010 +0200 @@ -6,7 +6,7 @@ use"../smltest/IsacKnowledge/integrate.sml"; use"integrate.sml"; *) -val thy = Integrate.thy; +val thy = theory "Integrate"; "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; diff -r b49723351533 -r a37a3ab989f4 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Tue Sep 14 12:12:42 2010 +0200 +++ b/test/Tools/isac/Test_Isac.thy Tue Sep 14 15:46:56 2010 +0200 @@ -1,13 +1,15 @@ (* Title Run_Tests on isac $ cd /usr/local/isabisac/test/Tools/isac -$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy & +$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy & +RESTART emacs after having created a new Isac heap. was sml/RTEST-root.sml in isac-2002 *) theory Test_Isac imports Isac begin ML{* writeln "**** run the tests **************************************" *}; +ML {* Toplevel.debug := true; *} (* cd "systest"; (*+ check kbtest/diffapp.sml for additional items in met-model*) @@ -60,7 +62,9 @@ use"complex.sml"; use"diff.sml"; use"diffapp.sml"; - use"integrate.sml"; +*) +use"Knowledge/integrate.sml"; +(* use"equation.sml"; (*use"inssort.sml"; problems with recdef in Isabelle2002*) use"logexp.sml";