1.1 --- a/src/Tools/isac/Knowledge/Descript.thy	Thu Mar 03 17:37:46 2011 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Descript.thy	Fri Mar 04 11:30:37 2011 +0100
     1.3 @@ -37,6 +37,7 @@
     1.4    unknown        :: "'a => unknow"
     1.5    valuesFor      :: "real list => toreall"
     1.6  
     1.7 +  intTestGiven   :: "int => una"
     1.8    realTestGiven  :: "real => una"
     1.9    realTestFind   :: "real => una"
    1.10    boolTestGiven  :: "bool => una"

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Fri Mar 04 11:30:37 2011 +0100
     2.3 @@ -0,0 +1,51 @@
     2.4 +theory DiophantEq imports Atools Equation begin
     2.5 +
     2.6 +consts
     2.7 +   Solve'_lineq'_equation :: "[bool, int, bool ] 
     2.8 +                                       => bool "
     2.9 +                    ("((Script Diophant'_equation (_ _ =))//(_))" 9)
    2.10 +axioms
    2.11 +
    2.12 +  int_isolate_add: "(bdv + a = b) = (bdv = b - (a::int))"
    2.13 +
    2.14 +ML {*
    2.15 +val thy = @{theory};
    2.16 +val ctxt = ProofContext.init_global thy;
    2.17 +fun parseNEW ctxt str = numbers_to_string (Syntax.read_term ctxt str);
    2.18 +parseNEW ctxt "x = (1::int)"; (*TODO omit ::int*)
    2.19 +*}
    2.20 +
    2.21 +ML {*
    2.22 +store_pbt
    2.23 + (prep_pbt thy "pbl_equ_dio" [] e_pblID
    2.24 + (["diophantine","equation"],
    2.25 +  [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    2.26 +  (*                                      TODO: drop ^^^^^*)
    2.27 +   ("#Where" ,[]),
    2.28 +   ("#Find"  ,["boolTestFind s_s"]) 
    2.29 +  ],
    2.30 +  e_rls, SOME "solve (e_e::bool, v_v::int)",
    2.31 +  [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
    2.32 +show_ptyps();
    2.33 +get_pbt ["diophantine","equation"];
    2.34 +*}
    2.35 +
    2.36 +ML {*
    2.37 +val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")];
    2.38 +val t = parseNEW ctxt "x + 1 = (2::int)";
    2.39 +*}
    2.40 +
    2.41 +ML {*
    2.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>";
    2.43 +rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;
    2.44 +
    2.45 +
    2.46 +*}
    2.47 +
    2.48 +ML {*
    2.49 +prop_of (@{thm "int_isolate_add"});
    2.50 +writeln "-----------";
    2.51 +t;
    2.52 +*}
    2.53 +
    2.54 +end
    2.55 \ No newline at end of file

     3.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Thu Mar 03 17:37:46 2011 +0100
     3.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Fri Mar 04 11:30:37 2011 +0100
     3.3 @@ -22,7 +22,9 @@
     3.4       else NONE end)
     3.5  (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
     3.6  and rew_sub thy i bdv tless rls put_asm lrd r t = 
     3.7 -  ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));*)
     3.8 +  (tracing ("@@@ rew_sub begin: t = "^(term2str t));
     3.9 +   tracing ("@@@ rew_sub begin: bdv = "^(PolyML.makestring bdv));
    3.10 +   tracing ("@@@ rew_sub begin: r = "^(term2str r));
    3.11      let                  (* copy from Pure/thm.ML: fun rewritec *)
    3.12       val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    3.13                         o Logic.strip_imp_concl) r;

     4.1 --- a/src/Tools/isac/ROOT.ML	Thu Mar 03 17:37:46 2011 +0100
     4.2 +++ b/src/Tools/isac/ROOT.ML	Fri Mar 04 11:30:37 2011 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  (*
     4.5 -$ cd /usr/local/Isabelle2009-1/src/Tools/isac
     4.6 -$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
     4.7 -$ ls -l /home/neuper/.isabelle/heaps/polyml-5.3.0_x86-linux/Isac
     4.8 +$ cd /usr/local/Isabelle/src/Tools/isac
     4.9 +$ /usr/local/Isabelle/bin/isabelle usedir -b HOL Isac
    4.10 +$ ls -l /home/neuper/.isabelle/heaps/polyml-5.4.0_x86-linux/Isac
    4.11  *)
    4.12  
    4.13  use_thys ["Build_Isac"];