wneuper/isa: comparison src/Tools/isac/Knowledge/Test.thy

equal deleted inserted replaced

-:3147f2c1525c
+:f57ddfd09474
 store_pbt
 (prep_pbt thy "pbl_test_equ" [] e_pblID
 (["equation","test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["matches (?a = ?b) e_e"]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 assoc_rls "matches",
 SOME "solve (e_e::bool, v_v)", []));
 store_pbt
 (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
 (["linear","univariate","equation","test"],
 [("#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_v'i'"])
 ],
 assoc_rls "matches",
 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
 (*25.8.01 ------
 store_met
 (prep_met thy "met_test_solvelin" [] e_metID
 (["Test","solve_linear"]:metID,
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["matches (?a = ?b) e_e"]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
 prls = assoc_rls "matches", calc = [], crls = tval_rls,
 nrls = Test_simplify},
 "Script Solve_linear (e_e::bool) (v_v::real)=                     " ^
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
 	       "(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_v'i'"])
 ],
 assoc_rls "matches",
 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
 (*
 val e_e = (term_of o the o (parse thy)) "e_e::bool";
 store_pbt
 (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
 (["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_v'i'"])
 ],
 e_rls, SOME "solve (e_e::bool, v_v)", []));
 store_pbt
 (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_v'i'"])
 ],
 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
 store_pbt
 (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_v'i'"])
 ],
 e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
 store_pbt
 (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_v'i'"])
 ],
 e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
 *}
 ML {*
 store_pbt
 (prep_pbt thy "pbl_test_uni_root" [] e_pblID
 (["squareroot","univariate","equation","test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,["contains_root (e_e::bool)"]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
 			  eval_contains_root "#contains_root_")],
 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]]));
 store_pbt
 (prep_pbt thy "pbl_test_uni_norm" [] e_pblID
 (["normalize","univariate","equation","test"],
 [("#Given" ,["equality e_e","solveFor v_v"]),
 ("#Where" ,[]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
 store_pbt
 (prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
 (["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_v'i'"])
 ],
 e_rls, SOME "solve (e_e::bool, v_v)", []));
 (*
 (#ppc o get_pbt) ["sqroot-test","univariate","equation"];
 (prep_met thy  "met_test_sqrt" [] e_metID
 (*root-equation, version for tests before 8.01.01*)
 (["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_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls =append_rls "srls_contains_root" e_rls
 		    [Calc ("Test.contains'_root",eval_contains_root "")],
 prls =append_rls "prls_contains_root" e_rls
 store_met
 (prep_met thy  "met_test_sqrt2" [] e_metID
 (*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_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls = append_rls "srls_contains_root" e_rls
 		     [Calc ("Test.contains'_root",eval_contains_root"")],
 prls=e_rls,calc=[],
 store_met
 (prep_met thy "met_test_squ_sub" [] e_metID
 (*tests subproblem fixed linear*)
 (["Test","squ-equ-test-subpbl1"]:metID,
 [("#Given" ,["equality e_e","solveFor v_v"]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
 crls=tval_rls, nrls=Test_simplify},
 "Script Solve_root_equation (e_e::bool) (v_v::real) =                " ^
 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@            " ^
 store_met
 (prep_met thy "met_test_squ_sub2" [] e_metID
 (*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_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
 crls=tval_rls, nrls=e_rls(*,
 asm_rls=[],asm_thm=[("square_equation_left",""),
 	    ("square_equation_right","")]*)},
 store_met
 (prep_met thy "met_test_squ_nonterm" [] e_metID
 (*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_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls = append_rls "srls_contains_root" e_rls
 		     [Calc ("Test.contains'_root",eval_contains_root"")],
 prls=e_rls,calc=[],
 store_met
 (prep_met thy  "met_test_eq1" [] e_metID
 (*root-equation1:*)
 (["Test","square_equation1"]:metID,
 [("#Given" ,["equality e_e","solveFor v_v"]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls = append_rls "srls_contains_root" e_rls
 		     [Calc ("Test.contains'_root",eval_contains_root"")],
 prls=e_rls,calc=[],
 store_met
 (prep_met thy "met_test_squ2" [] e_metID
 (*root-equation2*)
 (["Test","square_equation2"]:metID,
 [("#Given" ,["equality e_e","solveFor v_v"]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls = append_rls "srls_contains_root" e_rls
 		     [Calc ("Test.contains'_root",eval_contains_root"")],
 prls=e_rls,calc=[],
 store_met
 (prep_met thy "met_test_squeq" [] e_metID
 (*root-equation*)
 (["Test","square_equation"]:metID,
 [("#Given" ,["equality e_e","solveFor v_v"]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,
 srls = append_rls "srls_contains_root" e_rls
 		     [Calc ("Test.contains'_root",eval_contains_root"")],
 prls=e_rls,calc=[],
 [("#Given",["equality e_e","solveFor v_v"]),
 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
 	       "(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_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
 prls = assoc_rls "matches",
 crls=tval_rls, nrls=e_rls(*,
 asm_rls=[],asm_thm=[]*)},
 store_met
 (prep_met thy "met_test_norm_univ" [] e_metID
 (["Test","norm_univar_equation"]:metID,
 [("#Given",["equality e_e","solveFor v_v"]),
 ("#Where" ,[]),
-("#Find"  ,["solutions v'i'"])
+("#Find"  ,["solutions v_v'i'"])
 ],
 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
 calc=[],
 crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},
 "Script Norm_univar_equation (e_e::bool) (v_v::real) =      " ^

branch	isac-update-Isa09-2
changeset 38012	f57ddfd09474
parent 38011	3147f2c1525c
child 38014	3e11e3c2dc42