1 theory DiophantEq imports Atools Equation begin
4 Solve'_lineq'_equation :: "[bool, int, bool ]
6 ("((Script Diophant'_equation (_ _ =))//(_))" 9)
9 int_isolate_add: "(bdv + a = b) = (bdv = b - (a::int))"
13 val ctxt = ProofContext.init_global thy;
14 fun parseNEW ctxt str = numbers_to_string (Syntax.read_term ctxt str);
15 parseNEW ctxt "x = (1::int)"; (*TODO omit ::int*)
20 (prep_pbt thy "pbl_equ_dio" [] e_pblID
21 (["diophantine","equation"],
22 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
25 ("#Find" ,["boolTestFind s_s"])
27 e_rls, SOME "solve (e_e::bool, v_v::int)",
28 [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
30 get_pbt ["diophantine","equation"];
34 val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];
35 val t = parseNEW ctxt "x + 1 = (2::int)";
39 tracing "\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>\<equiv>";
40 rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;
46 prop_of (@{thm "int_isolate_add"});
47 writeln "-----------";