1 (* testexamples for RootratEq, equations mixing fractions and roots |
1 (* testexamples for RootratEq, equations mixing fractions and roots |
2 use"rootrateq.sml"; |
2 WN120314 some complicated equations still are outcommented. |
3 *) |
3 *) |
4 |
4 |
5 |
5 "-----------------------------------------------------------------"; |
6 "--------------------- tests on predicates -------------------------------"; |
6 "table of contents -----------------------------------------------"; |
7 "--------------------- tests on predicates -------------------------------"; |
7 "-----------------------------------------------------------------"; |
8 "--------------------- tests on predicates -------------------------------"; |
8 "------------ tests on predicates -------------------------------"; |
9 |
9 "------------ test thm rootrat_equation_left_1 -------------------"; |
10 (*=== inhibit exn ?============================================================= |
10 "------------ test thm rootrat_equation_left_2 -------------------"; |
11 |
11 "------------ test thm rootrat_equation_right_1 ------------------"; |
12 val thy = (theory "Isac"); |
12 "------------ test thm rootrat_equation_right_2 ------------------"; |
13 |
13 "-----------------------------------------------------------------"; |
14 (* |
14 "-----------------------------------------------------------------"; |
15 Compiler.Control.Print.printDepth:=5; (*4 default*) |
15 |
16 trace_rewrite:=true; |
16 val thy = @{theory "RootRatEq"}; |
17 trace_rewrite:=false; |
17 |
|
18 "------------ tests on predicates -------------------------------"; |
|
19 "------------ tests on predicates -------------------------------"; |
|
20 "------------ tests on predicates -------------------------------"; |
|
21 val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x"; |
|
22 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
|
23 if (term2str t) = "False" then () |
|
24 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
|
25 |
|
26 val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; |
|
27 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
|
28 if (term2str t) = "False" then () |
|
29 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
|
30 |
|
31 val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; |
|
32 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
|
33 if (term2str t) = "False" then () |
|
34 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
|
35 |
|
36 val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; |
|
37 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
|
38 if (term2str t) = "True" then () |
|
39 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
|
40 |
|
41 val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
|
42 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
|
43 if (term2str t) = "True" then () |
|
44 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
|
45 |
|
46 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
|
47 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
|
48 if (term2str t) = "True" then () |
|
49 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
|
50 |
|
51 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; |
|
52 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
|
53 if (term2str t) = "True" then () |
|
54 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
|
55 |
|
56 "------------ test thm rootrat_equation_left_1 -------------------"; |
|
57 "------------ test thm rootrat_equation_left_1 -------------------"; |
|
58 "------------ test thm rootrat_equation_left_1 -------------------"; |
|
59 val c = []; |
|
60 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= (0::real))", "solveFor x","solutions L"]; |
|
61 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
|
62 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
63 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
66 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
67 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
68 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
69 if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then () |
|
70 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a"; |
|
71 (*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"])*) |
|
72 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
73 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
74 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
75 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
76 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p''',_,f,nxt,_,pt''') = me nxt p c pt; |
|
77 |
|
78 (*we investigate, why the next step results in Empty_Tac*) |
|
79 f2str f = "1 = 2 * (1 + -1 * sqrt x)"; |
|
80 nxt = ("Rewrite_Set", Rewrite_Set "make_rooteq"); |
|
81 (*... these ar the step's arguments; from these we do directly ...*) |
|
82 val SOME t = parseNEW ctxt "1 = 2 * (1 + -1 * sqrt x)" |
|
83 val SOME (t, _) = rewrite_set_ thy true make_rooteq t; |
|
84 term2str t = "1 = 2 + -2 * sqrt x"; |
|
85 (*... which works; thus error must be in script interpretation*) |
|
86 |
|
87 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); |
|
88 val (pt, p) = case locatetac tac (pt,p) of |
|
89 ("ok", (_, _, ptp)) => ptp; |
|
90 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
|
91 val pIopt = get_pblID (pt,ip); |
|
92 ip; (*= ([3, 2], Res)*) |
|
93 tacis; (*= []*) |
|
94 pIopt; (*= SOME ["sq", "root'", "univariate", "equation"]*) |
|
95 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
|
96 "~~~~~ fun nxt_solve_, args:"; (*stopped due to strange exn |
|
97 "check_elementwise: no set 1 = 2 + -2 * sqrt x"*) |
|
98 |
|
99 (*---- 2nd try: we investigate the script ["RootEq","solve_sq_root_equation"] found via pbl*) |
|
100 val t = str2term "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)"; |
|
101 val t = str2term ("((lhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x) |" ^ |
|
102 " ((rhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x)"); |
|
103 val SOME (t, _) = rewrite_set_ thy true rooteq_srls t; |
|
104 term2str t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take |
|
105 [univariate,equation] and to refine to ["sq", "root'", "univariate", "equation"] in 2002*) |
|
106 |
|
107 (*(*these are the errors during stepping into the code:*) |
|
108 nxt_solve_ (pt,ip); (*check_elementwise: no set 1 = 2 + -2 * sqrt x: fun mk_set raises |
|
109 this exn in Check_elementwise ONLY ?!?*) |
|
110 step p ((pt, e_pos'),[]); (* = ("helpless",*) |
18 *) |
111 *) |
19 val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x"; |
112 |
20 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
113 val (p,_,f,nxt,_,pt) = me nxt p''' c pt'''; |
21 if (term2str t) = "HOL.False" then () |
114 f2str f = "1 = 2 + -2 * sqrt x)"; (* <<<-------------- this should be*) |
22 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
115 fst nxt = "Empty_Tac"; (* <<<-------------- this we have*) |
23 |
116 (*============ inhibit exn WN120314: stopped due to effort; continue with equ-solver |
24 val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; |
117 The equation is strange: it calls script ["RootEq","solve_sq_root_equation"] twice |
25 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
118 and works differently due to an "if" in that script. |
26 if (term2str t) = "HOL.False" then () |
119 |
27 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
120 if f2str f = "1 = 2 + -2 * sqrt x" then () |
28 |
121 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 b"; |
29 val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; |
122 (*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"]) ?!? the SAME as above*) |
30 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
123 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
31 if (term2str t) = "HOL.False" then () |
124 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
32 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
125 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
33 |
126 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
34 val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; |
127 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
35 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
128 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
36 if (term2str t) = "HOL.True" then () |
129 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
37 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
130 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
38 |
131 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
39 val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
132 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
40 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
41 if (term2str t) = "HOL.True" then () |
134 if f2str f = "1 = 4 * x" then () |
42 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
135 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 c"; |
43 |
136 (*-> Subproblem ("PolyEq", ["normalize", "polynomial", "univariate", "equation"])*) |
44 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
45 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
46 if (term2str t) = "HOL.True" then () |
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
47 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
140 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
48 |
141 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
49 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; |
142 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
50 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
143 if f2str f = "1 + -4 * x = 0" then () |
51 if (term2str t) = "HOL.True" then () |
|
52 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
|
53 |
|
54 |
|
55 "--------------------- test thm rootrat_equation_left_1 ---------------------"; |
|
56 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"]; |
|
57 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
|
58 |
|
59 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
60 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
61 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
62 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
63 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
66 (*-> Subproblem ("RootEq", ["univariate", ...])*) |
|
67 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
68 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
69 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
70 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
71 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
72 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
73 (*-> Subproblem ("RootEq", ["univariate", ...])*) |
|
74 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
75 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
76 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
77 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
78 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
79 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
80 (*-> Subproblem ("RootEq", ["univariate", ...])*) |
|
81 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
82 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
83 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
84 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
85 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
86 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
87 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then () |
|
88 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1"; |
144 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1"; |
89 (*-> Subproblem ("RootEq", ["polynomial", ...])*) |
145 (*-> Subproblem ("PolyEq", ["degree_1", "polynomial", "univariate", "equation"])*) |
90 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
146 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
91 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
147 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
92 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
148 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
93 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
149 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
94 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
150 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |