41 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true |
41 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true |
42 if false then (term)^2 contains no (sq)root *) |
42 if false then (term)^2 contains no (sq)root *) |
43 fun is_rootRatAddTerm_in t v = |
43 fun is_rootRatAddTerm_in t v = |
44 let |
44 let |
45 fun coeff_in c v = member op = (vars c) v; |
45 fun coeff_in c v = member op = (vars c) v; |
46 fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = |
46 fun rootadd (t as (Const ("Groups.plus_class.plus",_) $ t2 $ t3)) v = |
47 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v) |
47 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v) |
48 | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = |
48 | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v = |
49 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v) |
49 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v) |
50 | rootadd _ _ = false; |
50 | rootadd _ _ = false; |
51 fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:") |
51 fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:") |
52 (* at the moment there is no term like this, but ....*) |
52 (* at the moment there is no term like this, but ....*) |
53 | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v = |
53 | findrootrat (t as (Const ("Rings.inverse_class.divide",_) $ _ $ t3)) v = |
54 if (is_rootTerm_in t3 v) then rootadd t3 v else false |
54 if (is_rootTerm_in t3 v) then rootadd t3 v else false |
55 | findrootrat (_ $ t1 $ t2) v = |
55 | findrootrat (_ $ t1 $ t2) v = |
56 (findrootrat t1 v) orelse (findrootrat t2 v) |
56 (findrootrat t1 v) orelse (findrootrat t2 v) |
57 | findrootrat (_ $ t1) v = (findrootrat t1 v) |
57 | findrootrat (_ $ t1) v = (findrootrat t1 v) |
58 | findrootrat _ _ = false; |
58 | findrootrat _ _ = false; |