neuper@37906: (* RL 09.02 
neuper@37906:  testexamples for RatEq, equations with fractions
neuper@37906: 
neuper@37906:  Compiler.Control.Print.printDepth:=10; (*4 default*)
neuper@37906:  Compiler.Control.Print.printDepth:=5; (*4 default*)
neuper@37906:  trace_rewrite:=true;
neuper@37906: 
neuper@37906:  use"kbtest/rateq.sml";
neuper@37906:  *)
neuper@37906: "----------- rateq.sml begin--------";
neuper@37906: "---------(1/x=5) ---------------------";
neuper@37906: "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
neuper@37906: 
neuper@37906: val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RatEq.thy  false RatEq_prls t;
neuper@37906: val result = term2str t_;
neuper@37906: if result <>  "True"  then raise error "rateq.sml: new behaviour 1:" else ();
neuper@37906: 
neuper@37906: val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in  x";
neuper@37926: val SOME(t_, _) = rewrite_set_ RatEq.thy  false RatEq_prls t;
neuper@37906: val result = term2str t_;
neuper@37906: if result <>  "False"  then raise error "rateq.sml: new behaviour 2:" else ();
neuper@37906: 
neuper@37906: val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";
neuper@37926: val SOME(t_,_) = rewrite_set_ RatEq.thy  false RatEq_prls t;
neuper@37906: val result = term2str t_;
neuper@37906: if result <>  "False"  then raise error "rateq.sml: new behaviour 3:" else ();
neuper@37906: 
neuper@37906: val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
neuper@37926: val SOME(t_,_) = rewrite_set_ RatEq.thy  false RatEq_prls t;
neuper@37906: val result = term2str t_;
neuper@37906: if result <>  "True"  then raise error "rateq.sml: new behaviour 4:" else ();
neuper@37906: 
neuper@37906: val result = match_pbl ["equality (x=1)","solveFor x","solutions L"] 
neuper@37906:                 (get_pbt ["rational","univariate","equation"]); 
neuper@37906: case result of NoMatch' _  => ()  | _ => raise error "rateq.sml: new behaviour: 5";
neuper@37906: 
neuper@37906: val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"] 
neuper@37906:                 (get_pbt ["rational","univariate","equation"]); 
neuper@37906: case result of Matches' _  => ()  | _ => raise error "rateq.sml: new behaviour: 6";
neuper@37906: 
neuper@37906: 
neuper@37906: (*---------rateq---- 23.8.02 ---------------------*)
neuper@37906: "---------(1/x=5) ---------------------";
neuper@37906: val fmz = ["equality (1/x=5)","solveFor x","solutions L"];
neuper@37906: (* refine fmz ["univariate","equation"];
neuper@37906:    *)
neuper@37906: 
neuper@37906: val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906:    --------------------------------------- Refine_Tacitly*)
neuper@37906: (*  nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906:    --------------------------------------- Refine_Tacitly*)
neuper@37906: (*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*) 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = Apply_Method ["PolyEq", "normalize_poly"])*)
neuper@37906: 
neuper@37906: (* get_obj g_fmz pt [2];
neuper@37906:    *)
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt = ("Subproblem",  Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*  ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* "x = 1 / 5" *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then () 
neuper@37906: else  raise error "rateq.sml: new behaviour: [x = 1 / 5]";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*)
neuper@37906: "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
neuper@37906: (*EP Schalk_II_p68_n40*)
neuper@37906: val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/5)","solveFor x","solutions L"];
neuper@37906: (* val fmz = ["equality (3+x= 9*x^^^4+((1+2*x)/x^^^2)^^^2 + 6*(x^^^2*((1+2*x)/x^^^2)))",
neuper@37906: 	   "solveFor x","solutions L"];*)
neuper@37906: 
neuper@37906: (* refine fmz ["univariate","equation"];
neuper@37906: *)
neuper@37906: 
neuper@37906: val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
neuper@37906: (*val p = e_pos'; 
neuper@37906: val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* nxt = ("Model_Problem", Model_Problem
neuper@37906:      ["abcFormula","degree_2","polynomial","univariate","equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* "x = -2, x = 10" *)
neuper@37906: if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then() 
neuper@37906: else  raise error "rateq.sml: new behaviour: [x = -2, x = 10]";
neuper@37906: 
neuper@37906: "----------- rateq.sml end--------";