146 val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f; |
146 val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f; |
147 val (bdv, asms) = vp; |
147 val (bdv, asms) = vp; |
148 |
148 |
149 term2str bdv = "x"; |
149 term2str bdv = "x"; |
150 terms2str asms = (* GOON: asms from rewriting are missing : vvv *) |
150 terms2str asms = (* GOON: asms from rewriting are missing : vvv *) |
151 ("[\"~ matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\"," ^ |
151 ("[\"<not> matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\"," ^ |
152 "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\"," ^ |
152 "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\"," ^ |
153 "\"1 / x = 5 is_ratequation_in x\"]"); |
153 "\"1 / x = 5 is_ratequation_in x\"]"); |
154 (* |
154 (* |
155 WN120317.TODO dropped rateq: ctxt should contain "x ~= 0 here, but it does not, see above. |
155 WN120317.TODO dropped rateq: ctxt should contain "x ~= 0 here, but it does not, see above. |
156 *) |
156 *) |
258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
259 |
259 |
260 f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*) |
260 f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*) |
261 case snd nxt of Check_elementwise "Assumptions" => () | _ => ((*not checked before*)); (*= GUI*) |
261 case snd nxt of Check_elementwise "Assumptions" => () | _ => ((*not checked before*)); (*= GUI*) |
262 if terms2str (get_assumptions_ pt p) = |
262 if terms2str (get_assumptions_ pt p) = |
263 ("[\"~ matches (?a = 0)\n" ^ |
263 ("[\"<not> matches (?a = 0)\n" ^ |
264 " ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) |\n" ^ |
264 " ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) |\n" ^ |
265 "~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n " ^ |
265 "<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n " ^ |
266 " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"," ^ |
266 " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"," ^ |
267 "\"x = 6 / 5\"," ^ |
267 "\"x = 6 / 5\"," ^ |
268 "\"x = 0\"," ^ |
268 "\"x = 0\"," ^ |
269 "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\"," ^ |
269 "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\"," ^ |
270 "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"," ^ |
270 "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"," ^ |