9 "-----------------------------------------------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------------------------"; |
10 "table of contents -----------------------------------------------------------------------------"; |
10 "table of contents -----------------------------------------------------------------------------"; |
11 "-----------------------------------------------------------------------------------------------"; |
11 "-----------------------------------------------------------------------------------------------"; |
12 "-------- fun poly_of_term ---------------------------------------------------------------------"; |
12 "-------- fun poly_of_term ---------------------------------------------------------------------"; |
13 "-------- fun is_poly --------------------------------------------------------------------------"; |
13 "-------- fun is_poly --------------------------------------------------------------------------"; |
|
14 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
14 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
15 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
15 "-------- fun cancel_p special cases -----------------------------------------------------------"; |
16 "-------- fun cancel_p special cases -----------------------------------------------------------"; |
16 "-------- complex examples: rls norm_Rational --------------------------------------------------"; |
17 "-------- complex examples: rls norm_Rational --------------------------------------------------"; |
17 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------"; |
18 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------"; |
18 "-----------------------------------------------------------------------------------------------"; |
19 "-----------------------------------------------------------------------------------------------"; |
100 "-------- fun is_poly --------------------------------------------------------------------------"; |
101 "-------- fun is_poly --------------------------------------------------------------------------"; |
101 if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1") |
102 if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1") |
102 then () else error "is_poly 1 changed"; |
103 then () else error "is_poly 1 changed"; |
103 if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1")) |
104 if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1")) |
104 then () else error "is_poly 2 changed"; |
105 then () else error "is_poly 2 changed"; |
|
106 |
|
107 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
|
108 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
|
109 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
|
110 if is_ratpolyexp @{term "14 * x * y / (x * y)"} |
|
111 then () else error "is_ratpolyexp (14 * x * y / (x * y)) CHANGED"; |
|
112 if is_ratpolyexp @{term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"} |
|
113 then () else error "is_ratpolyexp (2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1) CHANGED"; |
|
114 |
|
115 if is_ratpolyexp @{term "((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x))"} |
|
116 then error "is_ratpolyexp (((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x)) CHANGED" else (); |
|
117 if is_ratpolyexp @{term "1 + sqrt x + sqrt y"} |
|
118 then error "is_ratpolyexp (1 + sqrt x + sqrt y) CHANGED" else (); |
|
119 |
105 |
120 |
106 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
121 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
107 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
122 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
108 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
123 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
109 val expT = HOLogic.realT |
124 val expT = HOLogic.realT |