1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Fri Mar 04 11:30:37 2011 +0100
     1.3 @@ -0,0 +1,51 @@
     1.4 +theory DiophantEq imports Atools Equation begin
     1.5 +
     1.6 +consts
     1.7 +   Solve'_lineq'_equation :: "[bool, int, bool ] 
     1.8 +                                       => bool "
     1.9 +                    ("((Script Diophant'_equation (_ _ =))//(_))" 9)
    1.10 +axioms
    1.11 +
    1.12 +  int_isolate_add: "(bdv + a = b) = (bdv = b - (a::int))"
    1.13 +
    1.14 +ML {*
    1.15 +val thy = @{theory};
    1.16 +val ctxt = ProofContext.init_global thy;
    1.17 +fun parseNEW ctxt str = numbers_to_string (Syntax.read_term ctxt str);
    1.18 +parseNEW ctxt "x = (1::int)"; (*TODO omit ::int*)
    1.19 +*}
    1.20 +
    1.21 +ML {*
    1.22 +store_pbt
    1.23 + (prep_pbt thy "pbl_equ_dio" [] e_pblID
    1.24 + (["diophantine","equation"],
    1.25 +  [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.26 +  (*                                      TODO: drop ^^^^^*)
    1.27 +   ("#Where" ,[]),
    1.28 +   ("#Find"  ,["boolTestFind s_s"]) 
    1.29 +  ],
    1.30 +  e_rls, SOME "solve (e_e::bool, v_v::int)",
    1.31 +  [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
    1.32 +show_ptyps();
    1.33 +get_pbt ["diophantine","equation"];
    1.34 +*}
    1.35 +
    1.36 +ML {*
    1.37 +val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];
    1.38 +val t = parseNEW ctxt "x + 1 = (2::int)";
    1.39 +*}
    1.40 +
    1.41 +ML {*
    1.42 +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>";
    1.43 +rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;
    1.44 +
    1.45 +
    1.46 +*}
    1.47 +
    1.48 +ML {*
    1.49 +prop_of (@{thm "int_isolate_add"});
    1.50 +writeln "-----------";
    1.51 +t;
    1.52 +*}
    1.53 +
    1.54 +end
    1.55 \ No newline at end of file