1039 store_met |
1039 store_met |
1040 (prep_met thy "met_polyeq" [] e_metID |
1040 (prep_met thy "met_polyeq" [] e_metID |
1041 (["PolyEq"], |
1041 (["PolyEq"], |
1042 [], |
1042 [], |
1043 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
1043 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
1044 crls=PolyEq_crls, nrls=norm_Rational}, "empty_script")); |
1044 crls=PolyEq_crls, nrls = norm_Rational}, "empty_script")); |
1045 |
1045 |
1046 store_met |
1046 store_met |
1047 (prep_met thy "met_polyeq_norm" [] e_metID |
1047 (prep_met thy "met_polyeq_norm" [] e_metID |
1048 (["PolyEq","normalize_poly"], |
1048 (["PolyEq","normalize_poly"], |
1049 [("#Given" ,["equality e_e","solveFor v_v"]), |
1049 [("#Given" ,["equality e_e","solveFor v_v"]), |
1054 {rew_ord'="termlessI", |
1054 {rew_ord'="termlessI", |
1055 rls'=PolyEq_erls, |
1055 rls'=PolyEq_erls, |
1056 srls=e_rls, |
1056 srls=e_rls, |
1057 prls=PolyEq_prls, |
1057 prls=PolyEq_prls, |
1058 calc=[], |
1058 calc=[], |
1059 crls=PolyEq_crls, nrls=norm_Rational}, |
1059 crls=PolyEq_crls, nrls = norm_Rational}, |
1060 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^ |
1060 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^ |
1061 "(let e_e =((Try (Rewrite all_left False)) @@ " ^ |
1061 "(let e_e =((Try (Rewrite all_left False)) @@ " ^ |
1062 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^ |
1062 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^ |
1063 " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^ |
1063 " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^ |
1064 " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1064 " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1081 {rew_ord'="termlessI", |
1081 {rew_ord'="termlessI", |
1082 rls'=PolyEq_erls, |
1082 rls'=PolyEq_erls, |
1083 srls=e_rls, |
1083 srls=e_rls, |
1084 prls=PolyEq_prls, |
1084 prls=PolyEq_prls, |
1085 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1085 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1086 crls=PolyEq_crls, nrls=norm_Rational}, |
1086 crls=PolyEq_crls, nrls = norm_Rational}, |
1087 "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1087 "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1088 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1088 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1089 " d0_polyeq_simplify False))) e_e " ^ |
1089 " d0_polyeq_simplify False))) e_e " ^ |
1090 " in ((Or_to_List e_e)::bool list))" |
1090 " in ((Or_to_List e_e)::bool list))" |
1091 )); |
1091 )); |
1099 "((lhs e_e) has_degree_in v_v) = 1"]), |
1099 "((lhs e_e) has_degree_in v_v) = 1"]), |
1100 ("#Find" ,["solutions v_v'i'"]) |
1100 ("#Find" ,["solutions v_v'i'"]) |
1101 ], |
1101 ], |
1102 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, |
1102 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, |
1103 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1103 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1104 crls=PolyEq_crls, nrls=norm_Rational}, |
1104 crls=PolyEq_crls, nrls = norm_Rational}, |
1105 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1105 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1106 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1106 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1107 " d1_polyeq_simplify True)) @@ " ^ |
1107 " d1_polyeq_simplify True)) @@ " ^ |
1108 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1108 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1109 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1109 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1123 {rew_ord'="termlessI", |
1123 {rew_ord'="termlessI", |
1124 rls'=PolyEq_erls, |
1124 rls'=PolyEq_erls, |
1125 srls=e_rls, |
1125 srls=e_rls, |
1126 prls=PolyEq_prls, |
1126 prls=PolyEq_prls, |
1127 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1127 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1128 crls=PolyEq_crls, nrls=norm_Rational}, |
1128 crls=PolyEq_crls, nrls = norm_Rational}, |
1129 "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1129 "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1130 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1130 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1131 " d2_polyeq_simplify True)) @@ " ^ |
1131 " d2_polyeq_simplify True)) @@ " ^ |
1132 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1132 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1133 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1133 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1150 {rew_ord'="termlessI", |
1150 {rew_ord'="termlessI", |
1151 rls'=PolyEq_erls, |
1151 rls'=PolyEq_erls, |
1152 srls=e_rls, |
1152 srls=e_rls, |
1153 prls=PolyEq_prls, |
1153 prls=PolyEq_prls, |
1154 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1154 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1155 crls=PolyEq_crls, nrls=norm_Rational}, |
1155 crls=PolyEq_crls, nrls = norm_Rational}, |
1156 "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^ |
1156 "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^ |
1157 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1157 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1158 " d2_polyeq_bdv_only_simplify True)) @@ " ^ |
1158 " d2_polyeq_bdv_only_simplify True)) @@ " ^ |
1159 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1159 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1160 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1160 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1177 {rew_ord'="termlessI", |
1177 {rew_ord'="termlessI", |
1178 rls'=PolyEq_erls, |
1178 rls'=PolyEq_erls, |
1179 srls=e_rls, |
1179 srls=e_rls, |
1180 prls=PolyEq_prls, |
1180 prls=PolyEq_prls, |
1181 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1181 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1182 crls=PolyEq_crls, nrls=norm_Rational}, |
1182 crls=PolyEq_crls, nrls = norm_Rational}, |
1183 "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^ |
1183 "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^ |
1184 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1184 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1185 " d2_polyeq_sq_only_simplify True)) @@ " ^ |
1185 " d2_polyeq_sq_only_simplify True)) @@ " ^ |
1186 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1186 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1187 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^ |
1187 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^ |
1201 {rew_ord'="termlessI", |
1201 {rew_ord'="termlessI", |
1202 rls'=PolyEq_erls, |
1202 rls'=PolyEq_erls, |
1203 srls=e_rls, |
1203 srls=e_rls, |
1204 prls=PolyEq_prls, |
1204 prls=PolyEq_prls, |
1205 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1205 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1206 crls=PolyEq_crls, nrls=norm_Rational}, |
1206 crls=PolyEq_crls, nrls = norm_Rational}, |
1207 "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^ |
1207 "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^ |
1208 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1208 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1209 " d2_polyeq_pqFormula_simplify True)) @@ " ^ |
1209 " d2_polyeq_pqFormula_simplify True)) @@ " ^ |
1210 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1210 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1211 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1211 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1225 {rew_ord'="termlessI", |
1225 {rew_ord'="termlessI", |
1226 rls'=PolyEq_erls, |
1226 rls'=PolyEq_erls, |
1227 srls=e_rls, |
1227 srls=e_rls, |
1228 prls=PolyEq_prls, |
1228 prls=PolyEq_prls, |
1229 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1229 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1230 crls=PolyEq_crls, nrls=norm_Rational}, |
1230 crls=PolyEq_crls, nrls = norm_Rational}, |
1231 "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^ |
1231 "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^ |
1232 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1232 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1233 " d2_polyeq_abcFormula_simplify True)) @@ " ^ |
1233 " d2_polyeq_abcFormula_simplify True)) @@ " ^ |
1234 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1234 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1235 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1235 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1249 {rew_ord'="termlessI", |
1249 {rew_ord'="termlessI", |
1250 rls'=PolyEq_erls, |
1250 rls'=PolyEq_erls, |
1251 srls=e_rls, |
1251 srls=e_rls, |
1252 prls=PolyEq_prls, |
1252 prls=PolyEq_prls, |
1253 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1253 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1254 crls=PolyEq_crls, nrls=norm_Rational}, |
1254 crls=PolyEq_crls, nrls = norm_Rational}, |
1255 "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1255 "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1256 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1256 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1257 " d3_polyeq_simplify True)) @@ " ^ |
1257 " d3_polyeq_simplify True)) @@ " ^ |
1258 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1258 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1259 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1259 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1279 "((lhs e_e) has_degree_in v_v) = 2"]), |
1279 "((lhs e_e) has_degree_in v_v) = 2"]), |
1280 ("#Find" ,["solutions v_v'i'"]) |
1280 ("#Find" ,["solutions v_v'i'"]) |
1281 ], |
1281 ], |
1282 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
1282 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
1283 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1283 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1284 crls=PolyEq_crls, nrls=norm_Rational}, |
1284 crls=PolyEq_crls, nrls = norm_Rational}, |
1285 "Script Complete_square (e_e::bool) (v_v::real) = " ^ |
1285 "Script Complete_square (e_e::bool) (v_v::real) = " ^ |
1286 "(let e_e = " ^ |
1286 "(let e_e = " ^ |
1287 " ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^ |
1287 " ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^ |
1288 " @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True)) " ^ |
1288 " @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True)) " ^ |
1289 " @@ (Try (Rewrite square_explicit1 False)) " ^ |
1289 " @@ (Try (Rewrite square_explicit1 False)) " ^ |