1.1 --- a/src/sml/FE-interface/interface.sml Thu Aug 24 12:51:16 2006 +0200
1.2 +++ b/src/sml/FE-interface/interface.sml Fri Aug 25 16:46:20 2006 +0200
1.3 @@ -314,7 +314,6 @@
1.4 *)
1.5 fun interSteps cI ip =
1.6 (let val ((pt,p), tacis) = get_calc cI
1.7 - (*val ip = get_pos cI iI*)(*WN050215 quick and dirty*)
1.8 in if (not o is_interpos) ip
1.9 then interStepsERROR cI "only formulae with position (_,Res) \
1.10 \may have intermediate steps above them"
2.1 --- a/src/sml/IsacKnowledge/Rational.ML Thu Aug 24 12:51:16 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Rational.ML Fri Aug 25 16:46:20 2006 +0200
2.3 @@ -2783,7 +2783,7 @@
2.4 Remark: the reverse ruleset does _NOT_ work properly with other input !.*)
2.5 (*WN020824 wir werden "uberlegen, wie wir ungeeignete inputs zur"uckweisen*)
2.6
2.7 -val {rules=rules,rew_ord=(_,ro),...} =
2.8 +val {rules, rew_ord=(_,ro),...} =
2.9 rep_rls (assoc_rls "make_polynomial");
2.10 val thy = Rational.thy;
2.11
2.12 @@ -2801,18 +2801,23 @@
2.13 list); (*derivation from given term to normalform
2.14 in reverse order with sym_thm;
2.15 (#) could be extracted from here by (map #1)*).*)
2.16 +(* val {rules=rules,rew_ord=(_,ro),...} =
2.17 + rep_rls (assoc_rls "make_polynomial") (*USE ALWAYS, SEE val cancel_p*);
2.18 + val (thy, eval_rls, ro) =(Rational.thy, Atools_erls, ro) (*..val cancel_p*);
2.19 + val t = t;
2.20 + *)
2.21 fun init_state thy eval_rls ro t =
2.22 - let val Some (t',_) = factout_p_ thy t;
2.23 - val Some (t'',asm) = cancel_p_ thy t;
2.24 - val der = reverse_deriv thy eval_rls rules ro None t';
2.25 + let val Some (t',_) = factout_p_ thy t
2.26 + val Some (t'',asm) = cancel_p_ thy t
2.27 + val der = reverse_deriv thy eval_rls rules ro None t'
2.28 val der = der @ [(Thm ("real_mult_div_cancel2",
2.29 num_str real_mult_div_cancel2),
2.30 (t'',asm))]
2.31 - val rs = (distinct_Thm o (map #1)) der;
2.32 + val rs = (distinct_Thm o (map #1)) der
2.33 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
2.34 "sym_real_mult_0",
2.35 - "sym_real_mult_1"]) rs;
2.36 - in (t,t'',[rs(*here only _ONE_*)],der) end;
2.37 + "sym_real_mult_1"]) rs
2.38 + in (t,t'',[rs(*here only _ONE_ WN060925 why?*)],der) end;
2.39
2.40 (*.locate_rule = fn : rule list -> term -> rule
2.41 -> (rule * (term * term list) option) list.
3.1 --- a/src/sml/ME/rewtools.sml Thu Aug 24 12:51:16 2006 +0200
3.2 +++ b/src/sml/ME/rewtools.sml Fri Aug 25 16:46:20 2006 +0200
3.3 @@ -77,7 +77,11 @@
3.4 term list)) : ... under these assumptions.
3.5 list :
3.6 returns empty list for a normal form
3.7 -040214: FIXME treats rules as in Rls, _not_ as in Seq*)
3.8 +FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
3.9 +
3.10 +WN060825 too complicated for the intended use by cancel_, common_nominator_
3.11 +and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
3.12 + -- replaced below*)
3.13 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
3.14 let
3.15 datatype switch = Appl | Noap;
3.16 @@ -127,11 +131,6 @@
3.17 rew_once (rts @ [(t,r,(t',a'))]) t' Appl rrs');
3.18
3.19 in rew_once [] tt Noap rs end;
3.20 -(*
3.21 - val t9 = (term_of o the o (parse thy)) "(8*(-1 + x))/(9*(-1 + x))";
3.22 - val rst = make_deriv thy eval_rls make_polynomial None t9;
3.23 - writeln(trtas2str rst);
3.24 -*)
3.25
3.26 (*.toggles the marker for 'fun sym_thm'.*)
3.27 fun sym_thmID (thmID : thmID) =
3.28 @@ -169,7 +168,7 @@
3.29 rew_ord=rew_ord};
3.30
3.31 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
3.32 - | sym_Thm (Rls_ rls) = Rls_ (sym_rls rls)
3.33 + | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
3.34 | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
3.35 (*
3.36 val th = Thm ("real_one_collect",num_str real_one_collect);
3.37 @@ -180,6 +179,7 @@
3.38 ML> val it =
3.39 Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)
3.40
3.41 +
3.42 (*version for reverse rewrite used before 040214*)
3.43 fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
3.44 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
4.1 --- a/src/smltest/IsacKnowledge/rational.sml Thu Aug 24 12:51:16 2006 +0200
4.2 +++ b/src/smltest/IsacKnowledge/rational.sml Fri Aug 25 16:46:20 2006 +0200
4.3 @@ -33,6 +33,7 @@
4.4 "-------- me Schalk I No.186 -------------------------------------";
4.5 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
4.6 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
4.7 +"-------- investigate format of factout_ and factout_p_ ----------";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -2023,7 +2024,7 @@
4.12 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
4.13 states:=[];
4.14 CalcTree
4.15 -[(["term ((14 * x * y) / ( x * y ))", "normalform N"],
4.16 +[(["term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
4.17 ("Rational.thy",["rational","simplification"],
4.18 ["simplification","of_rationals"]))];
4.19 Iterator 1;
4.20 @@ -2040,4 +2041,30 @@
4.21 (*WN060823 cancel_p_ init_state does not terminate, see Rational.ML
4.22 interSteps 1 ([1,2,1],Res);
4.23 val ((pt,p),_) = get_calc 1; show_pt pt;
4.24 -*)
4.25 \ No newline at end of file
4.26 +*)
4.27 +
4.28 +"-------- investigate format of factout_ and factout_p_ ----------";
4.29 +"-------- investigate format of factout_ and factout_p_ ----------";
4.30 +"-------- investigate format of factout_ and factout_p_ ----------";
4.31 +val {rules, rew_ord = (_,ro),...} = rep_rls (assoc_rls "make_polynomial");
4.32 +val (thy, eval_rls) = (Rational.thy, Atools_erls)(*see 'fun init_state'*);
4.33 +val Rrls {scr = Rfuns {init_state,...},...} = assoc_rls "cancel_p";
4.34 +
4.35 +"----- see Rational.ML, local cancel_p, fun init_state";
4.36 +val t = str2term "(a^^^2 + (-1)*b^^^2) / (a^^^2 + (-2)*a*b + b^^^2)";
4.37 +val Some (t',_) = factout_p_ thy t; term2str t';
4.38 +(*
4.39 +val rtas = reverse_deriv thy eval_rls rules ro None t';
4.40 +writeln(trtas2str rst);
4.41 +*)
4.42 +
4.43 +
4.44 +"----- see Rational.ML, local cancel_p, fun init_state";
4.45 +val t = str2term "a^^^2 / a";
4.46 +val Some (t',_) = factout_p_ thy t; term2str t';
4.47 +(*val it = "1 * a * (1 * a) / (1 * (1 * a))" ... can be canceled with
4.48 + real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
4.49 +(*
4.50 +val rtas = reverse_deriv thy eval_rls rules ro None t';
4.51 +writeln(rtas2str rtas);
4.52 +*)
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/smltest/IsacKnowledge/root.sml Fri Aug 25 16:46:20 2006 +0200
5.3 @@ -0,0 +1,15 @@
5.4 +(* testexamples for Root, radicals
5.5 + *)
5.6 +
5.7 +val thy = Root.thy;
5.8 +
5.9 +val t = str2term "sqrt 1";
5.10 +val Some (t',_) = rewrite_set_ thy false Root_erls t;
5.11 +if term2str t' = "1" then () else raise error "root.sml: diff.behav. sqrt 1";
5.12 +val t = str2term "sqrt -1";
5.13 +val None = rewrite_set_ thy false Root_erls t;
5.14 +
5.15 +val t = str2term "sqrt 0";
5.16 +val Some (t',_) = rewrite_set_ thy false Root_erls t;
5.17 +term2str t';
5.18 +if term2str t' = "0" then () else raise error "root.sml: diff.behav. sqrt 1";
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/smltest/IsacKnowledge/rootrateq.sml Fri Aug 25 16:46:20 2006 +0200
6.3 @@ -0,0 +1,229 @@
6.4 +(* testexamples for RootratEq, equations mixing fractions and roots
6.5 + use"rootrateq.sml";
6.6 + *)
6.7 +
6.8 +val thy = Isac.thy;
6.9 +
6.10 +"--------------------- tests on predicates -------------------------------";
6.11 +"--------------------- tests on predicates -------------------------------";
6.12 +"--------------------- tests on predicates -------------------------------";
6.13 +(*
6.14 + Compiler.Control.Print.printDepth:=5; (*4 default*)
6.15 + trace_rewrite:=true;
6.16 + trace_rewrite:=false;
6.17 +*)
6.18 +val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
6.19 +val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
6.20 +if (term2str t) = "False" then ()
6.21 + else raise error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
6.22 +
6.23 +val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
6.24 +val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
6.25 +if (term2str t) = "False" then ()
6.26 + else raise error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
6.27 +
6.28 +val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
6.29 +val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
6.30 +if (term2str t) = "False" then ()
6.31 + else raise error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
6.32 +
6.33 +val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
6.34 +val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
6.35 +if (term2str t) = "True" then ()
6.36 + else raise error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
6.37 +
6.38 +val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
6.39 +val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
6.40 +if (term2str t) = "True" then ()
6.41 + else raise error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
6.42 +
6.43 +val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
6.44 +val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
6.45 +if (term2str t) = "True" then ()
6.46 + else raise error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
6.47 +
6.48 +val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
6.49 +val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
6.50 +if (term2str t) = "True" then ()
6.51 + else raise error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
6.52 +
6.53 +
6.54 +"--------------------- test thm rootrat_equation_left_1 ---------------------";
6.55 +val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"];
6.56 +val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
6.57 +
6.58 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.59 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.63 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.64 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.65 +(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
6.66 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.67 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.68 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.69 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.72 +(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
6.73 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.74 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.75 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.76 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.77 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.79 +(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
6.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.81 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.82 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.83 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.84 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.85 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.86 +if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then ()
6.87 +else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
6.88 +(*-> Subproblem ("RootEq.thy", ["polynomial", ...])*)
6.89 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.90 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.92 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.93 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.94 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.98 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.99 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
6.100 + | _ => raise error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
6.101 +
6.102 +"--------------------- test thm rootrat_equation_left_2 ---------------------";
6.103 +val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
6.104 +val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
6.105 +
6.106 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.107 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.108 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.109 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.110 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.111 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.112 +(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
6.113 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.114 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.115 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.116 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.117 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.118 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.119 +(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
6.120 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.121 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.122 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.123 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.124 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.125 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.126 +(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
6.127 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.128 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.129 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.130 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.131 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.132 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.133 +if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
6.134 +else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
6.135 +(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
6.136 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.137 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.138 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.139 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.140 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.141 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.142 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.143 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.144 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.145 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.146 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
6.147 + | _ => raise error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
6.148 +
6.149 +"--------------------- test thm rootrat_equation_right_1 ---------------";
6.150 +val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
6.151 +val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
6.152 +
6.153 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.154 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.155 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.156 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.157 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.158 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.159 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.160 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.161 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.162 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.163 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.164 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.165 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.166 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.167 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.168 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.169 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.170 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.171 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.172 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.173 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.174 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.175 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.176 +if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then ()
6.177 +else raise error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1";
6.178 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.179 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.180 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.181 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.182 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.183 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.184 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.185 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.186 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.187 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.188 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.189 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
6.190 + | _ => raise error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
6.191 +
6.192 +"--------------------- test thm rootrat_equation_right_2 --------------------";
6.193 +val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
6.194 +val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
6.195 +
6.196 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.197 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.198 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.199 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.200 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.201 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.202 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.203 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.204 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.205 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.206 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.207 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.208 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.209 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.210 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.211 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.212 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.213 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.214 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.215 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.216 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.217 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.218 +if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
6.219 +else raise error "rootrateq.sml: diff.behav. in rootrat_equation_right_2";
6.220 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.221 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.222 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.223 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.224 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.225 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.226 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.227 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.228 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.229 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.230 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.231 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
6.232 + | _ => raise error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";