theory DiophantEq imports Atools Equation begin

consts

   Solve'_lineq'_equation :: "[bool, int, bool ] 

                                       => bool "

                    ("((Script Diophant'_equation (_ _ =))//(_))" 9)

axioms

  int_isolate_add: "(bdv + a = b) = (bdv = b - (a::int))"

ML {*

val thy = @{theory};

val ctxt = ProofContext.init_global thy;

fun parseNEW ctxt str = numbers_to_string (Syntax.read_term ctxt str);

parseNEW ctxt "x = (1::int)"; (*TODO omit ::int*)

*}

ML {*

store_pbt

 (prep_pbt thy "pbl_equ_dio" [] e_pblID

 (["diophantine","equation"],

  [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),

  (*                                      TODO: drop ^^^^^*)

   ("#Where" ,[]),

   ("#Find"  ,["boolTestFind s_s"]) 

  ],

  e_rls, SOME "solve (e_e::bool, v_v::int)",

  [["LinEq","solve_lineq_equation"]])); (*-----TODO*)

show_ptyps();

get_pbt ["diophantine","equation"];

*}

ML {*

val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];

val t = parseNEW ctxt "x + 1 = (2::int)";

*}

ML {*

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>";

rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;

*}

ML {*

prop_of (@{thm "int_isolate_add"});

writeln "-----------";

t;

*}

end