12 trace_rewrite:=true; |
12 trace_rewrite:=true; |
13 trace_rewrite:=false; |
13 trace_rewrite:=false; |
14 *) |
14 *) |
15 val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x"; |
15 val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x"; |
16 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
16 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
17 if (term2str t) = "False" then () |
17 if (term2str t) = "HOL.False" then () |
18 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
18 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
19 |
19 |
20 val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; |
20 val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; |
21 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
21 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
22 if (term2str t) = "False" then () |
22 if (term2str t) = "HOL.False" then () |
23 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
23 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
24 |
24 |
25 val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; |
25 val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; |
26 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
26 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
27 if (term2str t) = "False" then () |
27 if (term2str t) = "HOL.False" then () |
28 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
28 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
29 |
29 |
30 val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; |
30 val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; |
31 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
31 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
32 if (term2str t) = "True" then () |
32 if (term2str t) = "HOL.True" then () |
33 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
33 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
34 |
34 |
35 val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
35 val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
36 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
36 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
37 if (term2str t) = "True" then () |
37 if (term2str t) = "HOL.True" then () |
38 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
38 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
39 |
39 |
40 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
40 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
41 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
41 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
42 if (term2str t) = "True" then () |
42 if (term2str t) = "HOL.True" then () |
43 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
43 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
44 |
44 |
45 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; |
45 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; |
46 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
46 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
47 if (term2str t) = "True" then () |
47 if (term2str t) = "HOL.True" then () |
48 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
48 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
49 |
49 |
50 |
50 |
51 "--------------------- test thm rootrat_equation_left_1 ---------------------"; |
51 "--------------------- test thm rootrat_equation_left_1 ---------------------"; |
52 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"]; |
52 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"]; |