16 val thy = @{theory "RootRatEq"}; |
16 val thy = @{theory "RootRatEq"}; |
17 |
17 |
18 "------------ tests on predicates -------------------------------"; |
18 "------------ tests on predicates -------------------------------"; |
19 "------------ tests on predicates -------------------------------"; |
19 "------------ tests on predicates -------------------------------"; |
20 "------------ 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"; |
21 val t1 = (Thm.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; |
22 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
23 if (term2str t) = "False" then () |
23 if (term2str t) = "False" then () |
24 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
24 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
25 |
25 |
26 val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; |
26 val t1 = (Thm.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; |
27 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
28 if (term2str t) = "False" then () |
28 if (term2str t) = "False" then () |
29 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
29 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
30 |
30 |
31 val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; |
31 val t1 = (Thm.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; |
32 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
33 if (term2str t) = "False" then () |
33 if (term2str t) = "False" then () |
34 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
34 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
35 |
35 |
36 val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; |
36 val t1 = (Thm.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; |
37 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
38 if (term2str t) = "True" then () |
38 if (term2str t) = "True" then () |
39 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
39 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
40 |
40 |
41 val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
41 val t1 = (Thm.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; |
42 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
43 if (term2str t) = "True" then () |
43 if (term2str t) = "True" then () |
44 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
44 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
45 |
45 |
46 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
46 val t1 = (Thm.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; |
47 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
48 if (term2str t) = "True" then () |
48 if (term2str t) = "True" then () |
49 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
49 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
50 |
50 |
51 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; |
51 val t1 = (Thm.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; |
52 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; |
53 if (term2str t) = "True" then () |
53 if (term2str t) = "True" then () |
54 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
54 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
55 |
55 |
56 "------------ test thm rootrat_equation_left_1 -------------------"; |
56 "------------ test thm rootrat_equation_left_1 -------------------"; |