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

   use"ifthenelse.sml";

   use"tests/rationals2.sml";

   *)

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

val thy = (theory "Isac_Knowledge");

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

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

val t = (Thm.term_of o the o (TermC.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 = (Thm.term_of o the o (TermC.parse thy)) "x";

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

scan t v;

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

scan t v;

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

scan t v;

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

scan t v;

---*)

val t = (Thm.term_of o the o (TermC.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 = (Thm.term_of o the o (TermC.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 = (Thm.term_of o the o (TermC.parse Test.thy)) 

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

TermC.atom_trace_detail @{context} t;

val t = (Thm.term_of o the o (TermC.parse (theory "Isac_Knowledge"))) 

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

TermC.atom_trace_detail @{context} t;

(*

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

*)

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

rewrite_set "Isac_Knowledge" true 

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

rewrite_set "Test" true 

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

(*WN:  \<up> --- bitte nimm vorerst immer (theory "Isac_Knowledge"), damit wird richtig gematcht, 

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

Know_Store.add_pbls

  [Problem.prep_input (*Test.thy*) (theory "Isac_Knowledge")

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

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

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

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

        Rule_Set.append_rules Rule_Set.empty [Eval ("Test.is_rootequation_in", eval_is_rootequation_in "")],

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

  thy;

M_Match.by_formalise ["equality (sqrt(x)=1)", "solveFor x", "solutions L"] (Problem.from_store ["rootX", "univariate", "equation", "test"]); 

Know_Store.add_pbls

  [Problem.prep_input (theory "Isac_Knowledge")

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

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

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

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

        Rule_Set.append_rules Rule_Set.empty [Eval ("Prog_Expr.TermC.matches",eval_matches "#matches_")], [])]

  thy;

methods:= overwritel (!methods,

[

 MethodC.prep_input

 (("Isac_Knowledge", "solve_univar_err"):metID,

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

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

    ],

   {rew_ord="tless_true",rls'="tval_rls",asm_rls=Rule_Set.empty,where_rls=Rule_Set.empty,calc=[],

    asm_rls=[],asm_thm=[]},

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

 \ (if (is_rootequation_in e_e v_v)\

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

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

 \  else ((SubProblem (IsacX,[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_Knowledge",["approximate", "univariate", "equation", "test"],

   ("Isac_Knowledge", "solve_univar_err"));

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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_Knowledge", "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' (Test_Out.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_Knowledge",["approximate", "univariate", "equation", "test"],

   ("Isac_Knowledge", "solve_univar_err"));

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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_Knowledge", "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' (Test_Out.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";