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 {*

 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