1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Mar 14 16:50:44 2011 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Mar 17 10:11:18 2011 +0100
     1.3 @@ -1,20 +1,24 @@
     1.4 -theory DiophantEq imports Atools Equation begin
     1.5 +(* Title:  Knowledge/DiophantEq.thy
     1.6 +   Author: Mathias Lehnfeld 2011
     1.7 +   (c) due to copyright terms
     1.8 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
     1.9 +        10        20        30        40        50        60        70        80
    1.10 +*)
    1.11 +
    1.12 +theory DiophantEq imports Atools Equation Test
    1.13 +begin
    1.14  
    1.15  consts
    1.16 -   Solve'_lineq'_equation :: "[bool, int, bool ] 
    1.17 +  Diophant'_equation :: "[bool, int, bool ] 
    1.18                                         => bool "
    1.19                      ("((Script Diophant'_equation (_ _ =))//(_))" 9)
    1.20  axioms
    1.21  
    1.22 -  int_isolate_add: "(bdv + a = b) = (bdv = b - (a::int))"
    1.23 +  int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
    1.24  
    1.25 -ML {*
    1.26 -val thy = @{theory};
    1.27 -val ctxt = ProofContext.init_global thy;
    1.28 -fun parseNEW ctxt str = numbers_to_string (Syntax.read_term ctxt str);
    1.29 -parseNEW ctxt "x = (1::int)"; (*TODO omit ::int*)
    1.30 -*}
    1.31 +ML {*val thy = @{theory}*}
    1.32  
    1.33 +text {*problemclass for the usecase*}
    1.34  ML {*
    1.35  store_pbt
    1.36   (prep_pbt thy "pbl_equ_dio" [] e_pblID
    1.37 @@ -30,21 +34,24 @@
    1.38  get_pbt ["diophantine","equation"];
    1.39  *}
    1.40  
    1.41 +text {*method solving the usecase*}
    1.42  ML {*
    1.43 -val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];
    1.44 -val t = parseNEW ctxt "x + 1 = (2::int)";
    1.45 -*} 
    1.46 -
    1.47 -ML {*
    1.48 -rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;
    1.49 -
    1.50 - 
    1.51 -*}
    1.52 -
    1.53 -ML {*
    1.54 -prop_of (@{thm "int_isolate_add"});
    1.55 -writeln "-----------";
    1.56 -t;
    1.57 +store_met
    1.58 +(prep_met thy "met_test_diophant" [] e_metID
    1.59 + (["Test","solve_diophant"]:metID,
    1.60 +  [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.61 +  (*                                      TODO: drop ^^^^^*)
    1.62 +   ("#Where" ,[]),
    1.63 +   ("#Find"  ,["boolTestFind s_s"]) 
    1.64 +  ],
    1.65 +   {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
    1.66 +    prls = e_rls, calc = [], crls = tval_rls, nrls = Test_simplify},
    1.67 + "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
    1.68 + "(Repeat                                                          " ^
    1.69 + "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
    1.70 + "     (Try (Calculate PLUS)) @@  " ^
    1.71 + "     (Try (Calculate TIMES))) e_e::bool)"
    1.72 + ))
    1.73  *}
    1.74  
    1.75  end
    1.76 \ No newline at end of file