agriesma@338: (* use"../systest/details.sml"; agriesma@338: use"systest/details.sml"; agriesma@338: use"details.sml"; agriesma@338: agriesma@338: ######################################################## agriesma@338: is NOT dependent on Test, but on other thys: agriesma@338: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ agriesma@338: uses from Rational.ML: Rrls cancel_p, Rrls cancel agriesma@338: which in turn agriesma@338: uses from Poly.ML: Rls make_polynomial, Rls expand_binom agriesma@338: ######################################################## agriesma@338: *) agriesma@338: "-------- cancel, without detail ------------------------------"; agriesma@338: "-------- cancel, detail rev-rew (cancel) afterwards ----------"; agriesma@338: "-------------- cancel_p, without detail ------------------------------"; agriesma@338: "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; agriesma@338: agriesma@338: store_pbt agriesma@338: (prep_pbt Test.thy agriesma@338: (["test"], agriesma@338: [], agriesma@338: e_rls, None, [])); agriesma@338: store_pbt agriesma@338: (prep_pbt Test.thy agriesma@338: (["detail","test"], agriesma@338: [("#Given" ,["realTestGiven t_"]), agriesma@338: ("#Find" ,["realTestFind s_"]) agriesma@338: ], agriesma@338: e_rls, None, [("Test.thy","test_detail")])); agriesma@338: agriesma@338: methods:= overwritel (!methods, agriesma@338: [ agriesma@338: prep_met agriesma@338: (("Test.thy","test_detail_binom"):metID, agriesma@338: [("#Given" ,["realTestGiven t_"]), agriesma@338: ("#Find" ,["realTestFind s_"]) agriesma@338: ], agriesma@338: {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls, agriesma@338: asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]}, agriesma@338: "Script Testterm (g_::real) = \ agriesma@338: \(((Rewrite_Set expand_binoms False) @@\ agriesma@338: \ (Rewrite_Set cancel False)) g_)" agriesma@338: ), agriesma@338: prep_met agriesma@338: (("Test.thy","test_detail_poly"):metID, agriesma@338: [("#Given" ,["realTestGiven t_"]), agriesma@338: ("#Find" ,["realTestFind s_"]) agriesma@338: ], agriesma@338: {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls, agriesma@338: asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]}, agriesma@338: "Script Testterm (g_::real) = \ agriesma@338: \(((Rewrite_Set make_polynomial False) @@\ agriesma@338: \ (Rewrite_Set cancel_p False)) g_)" agriesma@338: )]); agriesma@338: agriesma@338: (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*) agriesma@338: agriesma@338: "-------- cancel, without detail ------------------------------"; agriesma@338: "-------- cancel, without detail ------------------------------"; agriesma@338: "-------- cancel, without detail ------------------------------"; agriesma@338: val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))", agriesma@338: "realTestFind s"]; agriesma@338: val (dI',pI',mI') = agriesma@338: ("Test.thy",["detail","test"],("Test.thy","test_detail_binom")); agriesma@338: agriesma@338: val p = e_pos'; val c = []; agriesma@338: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); agriesma@338: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*"(3 + -1 * x) / (3 + x)"*) agriesma@338: if nxt = ("End_Proof'",End_Proof') then () agriesma@338: else raise error "details.sml, changed behaviour in: without detail"; agriesma@338: agriesma@338: agriesma@338: "-------- cancel, detail rev-rew (cancel) afterwards ----------"; agriesma@338: "-------- cancel, detail rev-rew (cancel) afterwards ----------"; agriesma@338: "-------- cancel, detail rev-rew (cancel) afterwards ----------"; agriesma@338: val p = e_pos'; val c = []; agriesma@338: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); agriesma@338: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) agriesma@338: val nxt = ("Detail",Detail);"----------------------"; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*val nxt = ("End_Detail",End_Detail)*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) agriesma@338: val nxt = ("Detail",Detail);"----------------------"; agriesma@338: val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*15.10.02*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (* agriesma@338: rewrite "Rationals.thy" "tless_true""e_rls"true("sym_real_plus_minus_binom","") agriesma@338: "3 ^^^ 2 - x ^^^ 2"; agriesma@338: *) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)")) agriesma@338: andalso nxt = ("End_Proof'",End_Proof') then () agriesma@338: else raise error "new behaviour in details.sml, \ agriesma@338: \cancel, rev-rew (cancel) afterwards"; agriesma@338: agriesma@338: (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*) agriesma@338: agriesma@338: "-------------- cancel_p, without detail ------------------------------"; agriesma@338: "-------------- cancel_p, without detail ------------------------------"; agriesma@338: "-------------- cancel_p, without detail ------------------------------"; agriesma@338: val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))", agriesma@338: "realTestFind s"]; agriesma@338: val (dI',pI',mI') = agriesma@338: ("Test.thy",["detail","test"],("Test.thy","test_detail_poly")); agriesma@338: agriesma@338: val p = e_pos'; val c = []; agriesma@338: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); agriesma@338: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))"; agriesma@338: agriesma@338: (*14.3.03*) agriesma@338: val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))"; agriesma@338: val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; agriesma@338: "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)"; agriesma@338: val Some (t,_) = rewrite_set_ thy false cancel_p t; term2str t; agriesma@338: cancel_p_ thy t; agriesma@338: agriesma@338: val t = str2term "(3 + x) * (3 + -1 * x)"; agriesma@338: val Some (t,_) = rewrite_set_ thy false expand_poly t; term2str t; agriesma@338: "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))"; agriesma@338: val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; agriesma@338: "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))"; agriesma@338: val Some (t,_) = rewrite_set_ thy false simplify_power t; term2str t; agriesma@338: "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))"; agriesma@338: val Some (t,_) = rewrite_set_ thy false collect_numerals t; term2str t; agriesma@338: "9 + (0 * x + -1 * x ^^^ 2)"; agriesma@338: val Some (t,_) = rewrite_set_ thy false reduce_012 t; term2str t; agriesma@338: "9 + - (x ^^^ 2)"; agriesma@338: (*14.3.03*) agriesma@338: agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*"(3 + -1 * x) / (3 + x)"*) agriesma@338: if nxt = ("End_Proof'",End_Proof') then () agriesma@338: else raise error "details.sml, changed behaviour in: cancel_p, without detail"; agriesma@338: agriesma@338: "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; agriesma@338: "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; agriesma@338: "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; agriesma@338: val p = e_pos'; val c = []; agriesma@338: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); agriesma@338: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) agriesma@338: agriesma@338: (*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml: agriesma@338: fun make_deriv ... Rls_ not yet impl. (| Thm | Calc) agriesma@338: Rls_ needed for make_polynomial ---------------------- agriesma@338: val nxt = ("Detail",Detail);"----------------------"; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: if nxt = ("End_Detail",End_Detail) then () agriesma@338: else raise error "details.sml: new behav. in Detail make_polynomial"; agriesma@338: ----------------------------------------------------------------------*) agriesma@338: agriesma@338: (*--------------- agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) agriesma@338: val nxt = ("Detail",Detail);"----------------------"; agriesma@338: val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)")) agriesma@338: andalso nxt = ("End_Proof'",End_Proof') then () agriesma@338: else raise error "new behaviour in details.sml, cancel_p afterwards"; agriesma@338: agriesma@338: ----------------*) agriesma@338: agriesma@338: agriesma@338: agriesma@338: agriesma@338: agriesma@338: val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))", agriesma@338: "realTestFind s"]; agriesma@338: val (dI',pI',mI') = agriesma@338: ("Test.thy",["detail","test"],("Test.thy","test_detail_poly")); agriesma@338: agriesma@338: val p = e_pos'; val c = []; agriesma@338: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); agriesma@338: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: (*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ---------------------------- agriesma@338: (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*) agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) agriesma@338: val nxt = ("Detail",Detail);"----------------------"; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: val (p,_,f,nxt,_,pt) = me nxt p [] pt; agriesma@338: -------------------------------------------------------------------------*) agriesma@338: agriesma@338: agriesma@338: