equal
deleted
inserted
replaced
1100 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1100 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1101 " d1_polyeq_simplify True)) @@ " ^ |
1101 " d1_polyeq_simplify True)) @@ " ^ |
1102 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1102 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1103 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1103 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1104 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1104 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1105 " in Check_elementwise L_L {(v_v::real). Assumptions} )" |
1105 " in Check_elementwise L_LL {(v_v::real). Assumptions} )" |
1106 )); |
1106 )); |
1107 *} |
1107 *} |
1108 ML{* |
1108 ML{* |
1109 store_met |
1109 store_met |
1110 (prep_met thy "met_polyeq_d22" [] e_metID |
1110 (prep_met thy "met_polyeq_d22" [] e_metID |
1127 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1127 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1128 " d1_polyeq_simplify True)) @@ " ^ |
1128 " d1_polyeq_simplify True)) @@ " ^ |
1129 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1129 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1130 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1130 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1131 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1131 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1132 " in Check_elementwise L_L {(v_v::real). Assumptions} )" |
1132 " in Check_elementwise L_LL {(v_v::real). Assumptions} )" |
1133 )); |
1133 )); |
1134 *} |
1134 *} |
1135 ML{* |
1135 ML{* |
1136 store_met |
1136 store_met |
1137 (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID |
1137 (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID |
1154 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1154 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1155 " d1_polyeq_simplify True)) @@ " ^ |
1155 " d1_polyeq_simplify True)) @@ " ^ |
1156 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1156 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1157 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1157 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1158 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1158 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1159 " in Check_elementwise L_L {(v_v::real). Assumptions} )" |
1159 " in Check_elementwise L_LL {(v_v::real). Assumptions} )" |
1160 )); |
1160 )); |
1161 *} |
1161 *} |
1162 ML{* |
1162 ML{* |
1163 store_met |
1163 store_met |
1164 (prep_met thy "met_polyeq_d2_sqonly" [] e_metID |
1164 (prep_met thy "met_polyeq_d2_sqonly" [] e_metID |
1178 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1178 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1179 " d2_polyeq_sq_only_simplify True)) @@ " ^ |
1179 " d2_polyeq_sq_only_simplify True)) @@ " ^ |
1180 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1180 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1181 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^ |
1181 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^ |
1182 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1182 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1183 " in Check_elementwise L_L {(v_v::real). Assumptions} )" |
1183 " in Check_elementwise L_LL {(v_v::real). Assumptions} )" |
1184 )); |
1184 )); |
1185 *} |
1185 *} |
1186 ML{* |
1186 ML{* |
1187 store_met |
1187 store_met |
1188 (prep_met thy "met_polyeq_d2_pq" [] e_metID |
1188 (prep_met thy "met_polyeq_d2_pq" [] e_metID |
1202 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1202 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1203 " d2_polyeq_pqFormula_simplify True)) @@ " ^ |
1203 " d2_polyeq_pqFormula_simplify True)) @@ " ^ |
1204 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1204 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1205 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1205 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1206 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1206 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1207 " in Check_elementwise L_L {(v_v::real). Assumptions} )" |
1207 " in Check_elementwise L_LL {(v_v::real). Assumptions} )" |
1208 )); |
1208 )); |
1209 *} |
1209 *} |
1210 ML{* |
1210 ML{* |
1211 store_met |
1211 store_met |
1212 (prep_met thy "met_polyeq_d2_abc" [] e_metID |
1212 (prep_met thy "met_polyeq_d2_abc" [] e_metID |
1226 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1226 " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1227 " d2_polyeq_abcFormula_simplify True)) @@ " ^ |
1227 " d2_polyeq_abcFormula_simplify True)) @@ " ^ |
1228 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1228 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1229 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1229 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1230 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1230 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1231 " in Check_elementwise L_L {(v_v::real). Assumptions} )" |
1231 " in Check_elementwise L_LL {(v_v::real). Assumptions} )" |
1232 )); |
1232 )); |
1233 *} |
1233 *} |
1234 ML{* |
1234 ML{* |
1235 store_met |
1235 store_met |
1236 (prep_met thy "met_polyeq_d3" [] e_metID |
1236 (prep_met thy "met_polyeq_d3" [] e_metID |
1256 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1256 " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^ |
1257 " d1_polyeq_simplify True)) @@ " ^ |
1257 " d1_polyeq_simplify True)) @@ " ^ |
1258 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1258 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^ |
1259 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1259 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^ |
1260 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1260 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^ |
1261 " in Check_elementwise L_L {(v_v::real). Assumptions} )" |
1261 " in Check_elementwise L_LL {(v_v::real). Assumptions} )" |
1262 )); |
1262 )); |
1263 *} |
1263 *} |
1264 ML{* |
1264 ML{* |
1265 (*.solves all expanded (ie. normalized) terms of degree 2.*) |
1265 (*.solves all expanded (ie. normalized) terms of degree 2.*) |
1266 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values |
1266 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values |