18 val ctxt = Proof_Context.init_global thy; |
18 val ctxt = Proof_Context.init_global thy; |
19 |
19 |
20 "------------ pbl: rational, univariate, equation ----------------"; |
20 "------------ pbl: rational, univariate, equation ----------------"; |
21 "------------ pbl: rational, univariate, equation ----------------"; |
21 "------------ pbl: rational, univariate, equation ----------------"; |
22 "------------ pbl: rational, univariate, equation ----------------"; |
22 "------------ pbl: rational, univariate, equation ----------------"; |
23 val t = TermC.parseNEW' ctxt "(1/b+1/x=1) is_ratequation_in x"; |
23 val t = ParseC.parse_test ctxt "(1/b+1/x=1) is_ratequation_in x"; |
24 val SOME (t_, _) = rewrite_set_ ctxt false RatEq_prls t; |
24 val SOME (t_, _) = rewrite_set_ ctxt false RatEq_prls t; |
25 val result = UnparseC.term t_; |
25 val result = UnparseC.term t_; |
26 if result <> "True" then error "rateq.sml: new behaviour 1:" else (); |
26 if result <> "True" then error "rateq.sml: new behaviour 1:" else (); |
27 |
27 |
28 val t = TermC.parseNEW' ctxt "(sqrt(x)=1) is_ratequation_in x"; |
28 val t = ParseC.parse_test ctxt "(sqrt(x)=1) is_ratequation_in x"; |
29 val SOME (t_, _) = rewrite_set_ ctxt false RatEq_prls t; |
29 val SOME (t_, _) = rewrite_set_ ctxt false RatEq_prls t; |
30 val result = UnparseC.term t_; |
30 val result = UnparseC.term t_; |
31 if result <> "False" then error "rateq.sml: new behaviour 2:" else (); |
31 if result <> "False" then error "rateq.sml: new behaviour 2:" else (); |
32 |
32 |
33 val t = TermC.parseNEW' ctxt "(x=- 1) is_ratequation_in x"; |
33 val t = ParseC.parse_test ctxt "(x=- 1) is_ratequation_in x"; |
34 val SOME (t_,_) = rewrite_set_ ctxt false RatEq_prls t; |
34 val SOME (t_,_) = rewrite_set_ ctxt false RatEq_prls t; |
35 val result = UnparseC.term t_; |
35 val result = UnparseC.term t_; |
36 if result <> "False" then error "rateq.sml: new behaviour 3:" else (); |
36 if result <> "False" then error "rateq.sml: new behaviour 3:" else (); |
37 |
37 |
38 val t = TermC.parseNEW' ctxt "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x"; |
38 val t = ParseC.parse_test ctxt "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x"; |
39 val SOME (t_,_) = rewrite_set_ ctxt false RatEq_prls t; |
39 val SOME (t_,_) = rewrite_set_ ctxt false RatEq_prls t; |
40 val result = UnparseC.term t_; |
40 val result = UnparseC.term t_; |
41 if result <> "True" then error "rateq.sml: new behaviour 4:" else (); |
41 if result <> "True" then error "rateq.sml: new behaviour 4:" else (); |
42 |
42 |
43 val result = M_Match.match_pbl ["equality (x=(1::real))", "solveFor x", "solutions L"] |
43 val result = M_Match.match_pbl ["equality (x=(1::real))", "solveFor x", "solutions L"] |
143 val metID = (get_obj g_metID pt pp) |
143 val metID = (get_obj g_metID pt pp) |
144 val {crls,...} = MethodC.from_store ctxt metID |
144 val {crls,...} = MethodC.from_store ctxt metID |
145 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , []) |
145 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , []) |
146 | Res => get_obj g_result pt p; |
146 | Res => get_obj g_result pt p; |
147 UnparseC.term f = "[x = 1 / 5]"; (*the current formula*) |
147 UnparseC.term f = "[x = 1 / 5]"; (*the current formula*) |
148 val vp = (Proof_Context.init_global thy, pred) |-> parseNEW |> the |> mk_set thy pt p f; |
148 val vp = (Proof_Context.init_global thy, pred) |-> ParseC.term_opt |> the |> mk_set thy pt p f; |
149 val (bdv, asms) = vp; |
149 val (bdv, asms) = vp; |
150 |
150 |
151 UnparseC.term bdv = "x"; |
151 UnparseC.term bdv = "x"; |
152 UnparseC.terms asms = (* asms from rewriting are missing : vvv *) |
152 UnparseC.terms asms = (* asms from rewriting are missing : vvv *) |
153 ("[\"~ (matches (?a = 0) (1 = 5 * x)) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^ |
153 ("[\"~ (matches (?a = 0) (1 = 5 * x)) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^ |