(* 1.if-te-else- 8.02 f"ur Richard

   use"ifthenelse.sml";

   use"tests/rationals2.sml";

   *)

(*---------------- 25.7.02 ---------------------*)

val thy = (theory "Isac");

val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";

val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;

val t = (term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";

val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 

(*---

val v = (term_of o the o (parse thy)) "x";

val t = (term_of o the o (parse thy)) "sqrt(#3+#4*x)";

scan t v;

val t = (term_of o the o (parse thy)) "sqrt(#3+#4*a)";

scan t v;

val t = (term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";

scan t v;

val t = (term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";

scan t v;

---*)

val t = (term_of o the o (parse thy)) 

	    "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";

val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 

val t = (term_of o the o (parse thy)) 

	    "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";

val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 

val t = (term_of o the o (parse Test.thy)) 

	    "is_rootequation_in (sqrt(x)=1) x";

atomty t;

val t = (term_of o the o (parse (theory "Isac"))) 

	    "is_rootequation_in (sqrt(x)=1) x";

atomty t;

(*

val SOME(tt,_) = rewrite_set_ Test.thytrue tval_rls t;

*)

val SOME(tt,_) = rewrite_set_ (theory "Isac") true tval_rls t;

rewrite_set "Isac" true 

	    "tval_rls" "is_rootequation_in (sqrt(x)=1) x";

rewrite_set "Test" true 

	    "tval_rls" "is_rootequation_in (sqrt(x)=1) x";

(*WN: ^^^--- bitte nimm vorerst immer (theory "Isac"), damit wird richtig gematcht, 

  siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)

KEStore_Elems.add_pbts

  [prep_pbt (*Test.thy*) (theory "Isac")

      (["root'","univariate","equation","test"],

        [("#Given" ,["equality e_e","solveFor v_v"]),

          ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),

          ("#Find"  ,["solutions v_i_"])],

        append_rls e_rls [Calc ("Test.is'_rootequation'_in", eval_is_rootequation_in "")],

        [("Test","methode")])]

  thy;

match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root'","univariate","equation","test"]); 

KEStore_Elems.add_pbts

  [prep_pbt (theory "Isac")

      (["approximate","univariate","equation","test"],

        [("#Given", ["equality e_e","solveFor v_v","errorBound err_"]),

          ("#Where", ["matches (?a = ?b) e_e"]),

          ("#Find", ["solutions v_i_"])],

        append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")], [])]

  thy;

methods:= overwritel (!methods,

[

 prep_met

 (("Isac","solve_univar_err"):metID,

   [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),

    ("#Find"  ,["solutions v_i_"])

    ],

   {rew_ord'="tless_true",rls'="tval_rls",erls=e_rls,prls=e_rls,calc=[],

    asm_rls=[],asm_thm=[]},

 "Script Solve_univar_err (e_e::bool) (v_::real) (err_::bool) =  \

 \ (if (is_rootequation_in e_e v_v)\

 \  then ((SubProblem (Isac_,[squareroot,univariate,equation],\

 \         (SqRoot_,square_equation)) [BOOL e_e, REAL v_v, BOOL err_]))\

 \  else ((SubProblem (Isac_,[linear,univariate,equation],\

 \         (RatArith_,solve_linear)) [BOOL e_e, REAL v_])))"

 )]);

val fmz = ["equality (1+2*x=0)","solveFor x","errorBound (eps=0)",

	   "solutions L"];

val (dI',pI',mI') =

  ("Isac",["approximate","univariate","equation","test"],

   ("Isac","solve_univar_err"));

val p = e_pos'; val c = []; 

val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt = ("Apply_Method",Apply_Method ("Isac","solve_univar_err"))*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt = ("Apply_Method",Apply_Method ("RatArith","solve_linear"))*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]"))

   andalso nxt = ("End_Proof'",End_Proof') then ()

else error "new behaviour in testexample rationals2.sml 1+2*x=0";

(*---------------------------------*)

"-------------- is_rootequ_in - SubProblem -------------------------";

"-------------- is_rootequ_in - SubProblem -------------------------";

"-------------- is_rootequ_in - SubProblem -------------------------";

val fmz = ["equality (sqrt(x) - 1 = 0)","solveFor x","errorBound (eps=0)",

	   "solutions L"];

val (dI',pI',mI') =

  ("Isac",["approximate","univariate","equation","test"],

   ("Isac","solve_univar_err"));

val p = e_pos'; val c = []; 

val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt = ("Apply_Method",Apply_Method ("Isac","solve_univar_err"))*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

if p = ([1,1],Frm) andalso 

   f = Form' (FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso

   nxt = ("Empty_Tac",Empty_Tac) (*script ist noch 'helpless'*) then ()

else error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0";