1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,145 @@
1.4 +(* RL 09.02
1.5 + testexamples for RatEq, equations with fractions
1.6 +
1.7 + Compiler.Control.Print.printDepth:=10; (*4 default*)
1.8 + Compiler.Control.Print.printDepth:=5; (*4 default*)
1.9 + trace_rewrite:=true;
1.10 +
1.11 + use"kbtest/rateq.sml";
1.12 + *)
1.13 +"----------- rateq.sml begin--------";
1.14 +"---------(1/x=5) ---------------------";
1.15 +"--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
1.16 +
1.17 +val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
1.18 +val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
1.19 +val result = term2str t_;
1.20 +if result <> "True" then raise error "rateq.sml: new behaviour 1:" else ();
1.21 +
1.22 +val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x";
1.23 +val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
1.24 +val result = term2str t_;
1.25 +if result <> "False" then raise error "rateq.sml: new behaviour 2:" else ();
1.26 +
1.27 +val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";
1.28 +val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t;
1.29 +val result = term2str t_;
1.30 +if result <> "False" then raise error "rateq.sml: new behaviour 3:" else ();
1.31 +
1.32 +val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
1.33 +val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t;
1.34 +val result = term2str t_;
1.35 +if result <> "True" then raise error "rateq.sml: new behaviour 4:" else ();
1.36 +
1.37 +val result = match_pbl ["equality (x=1)","solveFor x","solutions L"]
1.38 + (get_pbt ["rational","univariate","equation"]);
1.39 +case result of NoMatch' _ => () | _ => raise error "rateq.sml: new behaviour: 5";
1.40 +
1.41 +val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
1.42 + (get_pbt ["rational","univariate","equation"]);
1.43 +case result of Matches' _ => () | _ => raise error "rateq.sml: new behaviour: 6";
1.44 +
1.45 +
1.46 +(*---------rateq---- 23.8.02 ---------------------*)
1.47 +"---------(1/x=5) ---------------------";
1.48 +val fmz = ["equality (1/x=5)","solveFor x","solutions L"];
1.49 +(* refine fmz ["univariate","equation"];
1.50 + *)
1.51 +
1.52 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.53 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.54 +(* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.55 + --------------------------------------- Refine_Tacitly*)
1.56 +(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
1.57 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.58 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.59 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.60 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.61 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.62 +(* val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"])*)
1.63 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.64 +(* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.65 + --------------------------------------- Refine_Tacitly*)
1.66 +(*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
1.67 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.68 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.69 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.70 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.71 +(*val nxt = Apply_Method ["PolyEq", "normalize_poly"])*)
1.72 +
1.73 +(* get_obj g_fmz pt [2];
1.74 + *)
1.75 +
1.76 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.77 +(**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)
1.78 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.79 +(* val nxt = ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1.80 +
1.81 +
1.82 +
1.83 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.84 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.85 +(* ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)
1.86 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.87 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.88 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.89 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.90 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.91 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.92 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.93 +(* "x = 1 / 5" *)
1.94 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.95 +if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then ()
1.96 +else raise error "rateq.sml: new behaviour: [x = 1 / 5]";
1.97 +
1.98 +
1.99 +
1.100 +(*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*)
1.101 +"--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
1.102 +(*EP Schalk_II_p68_n40*)
1.103 +val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/5)","solveFor x","solutions L"];
1.104 +(* val fmz = ["equality (3+x= 9*x^^^4+((1+2*x)/x^^^2)^^^2 + 6*(x^^^2*((1+2*x)/x^^^2)))",
1.105 + "solveFor x","solutions L"];*)
1.106 +
1.107 +(* refine fmz ["univariate","equation"];
1.108 +*)
1.109 +
1.110 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.111 +(*val p = e_pos';
1.112 +val c = [];
1.113 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.114 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.115 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.116 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.117 +(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
1.118 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.119 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.120 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.121 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.122 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.123 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.124 +(* nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
1.125 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.126 +(* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
1.127 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.128 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.129 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.130 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.131 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.132 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.133 +(* ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) *)
1.134 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.135 +(* nxt = ("Model_Problem", Model_Problem
1.136 + ["abcFormula","degree_2","polynomial","univariate","equation"])*)
1.137 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.138 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.139 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.140 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.141 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.142 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.143 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.144 +(* "x = -2, x = 10" *)
1.145 +if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then()
1.146 +else raise error "rateq.sml: new behaviour: [x = -2, x = 10]";
1.147 +
1.148 +"----------- rateq.sml end--------";