123 (*-------------------------functions---------------------*) |
123 (*-------------------------functions---------------------*) |
124 (* true if bdv is under sqrt of a Equation*) |
124 (* true if bdv is under sqrt of a Equation*) |
125 fun is_rootTerm_in t v = |
125 fun is_rootTerm_in t v = |
126 let |
126 let |
127 fun coeff_in c v = member op = (vars c) v; |
127 fun coeff_in c v = member op = (vars c) v; |
128 fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:") |
128 fun findroot (_ $ _ $ _ $ _) v = error("is_rootTerm_in:") |
129 (* at the moment there is no term like this, but ....*) |
129 (* at the moment there is no term like this, but ....*) |
130 | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v |
130 | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v |
131 | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v) |
131 | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v) |
132 | findroot (t as (Const ("NthRoot.sqrt",_) $ t2)) v = coeff_in t2 v |
132 | findroot (t as (Const ("NthRoot.sqrt",_) $ t2)) v = coeff_in t2 v |
133 | findroot (_ $ t2) v = (findroot t2 v) |
133 | findroot (_ $ t2) v = (findroot t2 v) |
137 end; |
137 end; |
138 |
138 |
139 fun is_sqrtTerm_in t v = |
139 fun is_sqrtTerm_in t v = |
140 let |
140 let |
141 fun coeff_in c v = member op = (vars c) v; |
141 fun coeff_in c v = member op = (vars c) v; |
142 fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:") |
142 fun findsqrt (_ $ _ $ _ $ _) v = error("is_sqrteqation_in:") |
143 (* at the moment there is no term like this, but ....*) |
143 (* at the moment there is no term like this, but ....*) |
144 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v) |
144 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v) |
145 | findsqrt (t as (Const ("NthRoot.sqrt",_) $ a)) v = coeff_in a v |
145 | findsqrt (t as (Const ("NthRoot.sqrt",_) $ a)) v = coeff_in a v |
146 | findsqrt (_ $ t1) v = (findsqrt t1 v) |
146 | findsqrt (_ $ t1) v = (findsqrt t1 v) |
147 | findsqrt _ _ = false; |
147 | findsqrt _ _ = false; |
152 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv, |
152 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv, |
153 and the subterm ist connected with + or * --> is normalized*) |
153 and the subterm ist connected with + or * --> is normalized*) |
154 fun is_normSqrtTerm_in t v = |
154 fun is_normSqrtTerm_in t v = |
155 let |
155 let |
156 fun coeff_in c v = member op = (vars c) v; |
156 fun coeff_in c v = member op = (vars c) v; |
157 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:") |
157 fun isnorm (_ $ _ $ _ $ _) v = error("is_normSqrtTerm_in:") |
158 (* at the moment there is no term like this, but ....*) |
158 (* at the moment there is no term like this, but ....*) |
159 | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
159 | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
160 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
160 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
161 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false |
161 | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false |
162 | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse |
162 | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse |