(* use"../systest/details.sml";

   use"systest/details.sml";

   use"details.sml";

########################################################

is NOT dependent on Test, but on other thys:

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

uses from Rational.ML: Rrls cancel_p, Rrls cancel

which in turn

uses from Poly.ML: Rls make_polynomial, Rls expand_binom 

######################################################## 

*)

"-------- cancel, without detail ------------------------------";

"-------- cancel, detail rev-rew (cancel) afterwards ----------";

"-------------- cancel_p, without detail ------------------------------";

"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

store_pbt

 (prep_pbt Test.thy

 (["test"],

  [],

  e_rls, None, []));

store_pbt

 (prep_pbt Test.thy

 (["detail","test"],

  [("#Given" ,["realTestGiven t_"]),

   ("#Find"  ,["realTestFind s_"])

   ],

  e_rls, None, [("Test.thy","test_detail")]));

methods:= overwritel (!methods,

[

 prep_met

 (("Test.thy","test_detail_binom"):metID,

  [("#Given" ,["realTestGiven t_"]),

   ("#Find"  ,["realTestFind s_"])

   ],

  {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls,

   asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]},

 "Script Testterm (g_::real) =   \

 \(((Rewrite_Set expand_binoms False) @@\

 \  (Rewrite_Set cancel False)) g_)"

 ),

 prep_met

 (("Test.thy","test_detail_poly"):metID,

  [("#Given" ,["realTestGiven t_"]),

   ("#Find"  ,["realTestFind s_"])

   ],

  {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,

   asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]},

 "Script Testterm (g_::real) =   \

 \(((Rewrite_Set make_polynomial False) @@\

 \  (Rewrite_Set cancel_p False)) g_)"

 )]);

(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)

"-------- cancel, without detail ------------------------------";

"-------- cancel, without detail ------------------------------";

"-------- cancel, without detail ------------------------------";

val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",

	   "realTestFind s"];

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

  ("Test.thy",["detail","test"],("Test.thy","test_detail_binom"));

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 [] pt;

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

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

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

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

(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

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

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

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

(*"(3 + -1 * x) / (3 + x)"*)

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

else raise error "details.sml, changed behaviour in: without detail";

"-------- cancel, detail rev-rew (cancel) afterwards ----------";

"-------- cancel, detail rev-rew (cancel) afterwards ----------";

"-------- cancel, detail rev-rew (cancel) afterwards ----------";

 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 [] pt;

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

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

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

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

 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

 val nxt = ("Detail",Detail);"----------------------";

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

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

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

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

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

 (*val nxt = ("End_Detail",End_Detail)*)

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

 val nxt = ("Detail",Detail);"----------------------";

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

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

(*15.10.02*)

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

(*

rewrite "Rationals.thy" "tless_true""e_rls"true("sym_real_plus_minus_binom","")

	"3 ^^^ 2 - x ^^^ 2";

*)

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

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

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

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

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

if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))

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

else raise error "new behaviour in details.sml, \

		 \cancel, rev-rew (cancel) afterwards";

(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)

"-------------- cancel_p, without detail ------------------------------";

"-------------- cancel_p, without detail ------------------------------";

"-------------- cancel_p, without detail ------------------------------";

val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",

	   "realTestFind s"];

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

  ("Test.thy",["detail","test"],("Test.thy","test_detail_poly"));

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 [] pt;

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

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

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

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

(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)

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

"(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";

 (*14.3.03*)

 val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";

 val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

 "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)";

 val Some (t,_) = rewrite_set_ thy false cancel_p t; term2str t;

 cancel_p_ thy t;

 val t = str2term "(3 + x) * (3 + -1 * x)";

 val Some (t,_) = rewrite_set_ thy false expand_poly t; term2str t;

 "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";

 val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;

 "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";

 val Some (t,_) = rewrite_set_ thy false simplify_power t; term2str t;

 "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";

 val Some (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;

 "9 + (0 * x + -1 * x ^^^ 2)";

 val Some (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;

 "9 + - (x ^^^ 2)"; 

 (*14.3.03*)

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

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

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

(*"(3 + -1 * x) / (3 + x)"*)

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

else raise error "details.sml, changed behaviour in: cancel_p, without detail";

"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";

 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 [] pt;

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

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

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

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

 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

(*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:

  fun make_deriv ...  Rls_ not yet impl. (| Thm | Calc) 

  Rls_ needed for make_polynomial ----------------------

 val nxt = ("Detail",Detail);"----------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 if nxt = ("End_Detail",End_Detail) then ()

 else raise error "details.sml: new behav. in Detail make_polynomial";

----------------------------------------------------------------------*)

(*---------------

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

 val nxt = ("Detail",Detail);"----------------------";

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

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

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

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

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

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

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

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

if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))

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

else raise error "new behaviour in details.sml, cancel_p afterwards";

----------------*)

val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",

	   "realTestFind s"];

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

  ("Test.thy",["detail","test"],("Test.thy","test_detail_poly"));

 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 [] pt;

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

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

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

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

 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)

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

(*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------

 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)

 val nxt = ("Detail",Detail);"----------------------";

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

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

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

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

-------------------------------------------------------------------------*)