1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Aug 26 10:03:53 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Aug 26 18:15:30 2010 +0200
1.3 @@ -6,137 +6,645 @@
1.4 last change by: rlang
1.5 date: 02.11.14
1.6 *)
1.7 -(* use"../knowledge/RootEq.ML";
1.8 - use"knowledge/RootEq.ML";
1.9 - use"RootEq.ML";
1.10
1.11 - remove_thy"RootEq";
1.12 - use_thy"Isac";
1.13 +theory RootEq imports Root end
1.14
1.15 - use"ROOT.ML";
1.16 - cd"knowledge";
1.17 - *)
1.18 -
1.19 -RootEq = Root +
1.20 -
1.21 -(*-------------------- consts------------------------------------------------*)
1.22 consts
1.23 (*-------------------------root-----------------------*)
1.24 - is'_rootTerm'_in :: [real, real] => bool ("_ is'_rootTerm'_in _")
1.25 - is'_sqrtTerm'_in :: [real, real] => bool ("_ is'_sqrtTerm'_in _")
1.26 - is'_normSqrtTerm'_in :: [real, real] => bool ("_ is'_normSqrtTerm'_in _")
1.27 + is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
1.28 + is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _")
1.29 + is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _")
1.30 +
1.31 (*----------------------scripts-----------------------*)
1.32 Norm'_sq'_root'_equation
1.33 - :: "[bool,real, \
1.34 - \ bool list] => bool list"
1.35 - ("((Script Norm'_sq'_root'_equation (_ _ =))// \
1.36 - \ (_))" 9)
1.37 + :: "[bool,real,
1.38 + bool list] => bool list"
1.39 + ("((Script Norm'_sq'_root'_equation (_ _ =))//
1.40 + (_))" 9)
1.41 Solve'_sq'_root'_equation
1.42 - :: "[bool,real, \
1.43 - \ bool list] => bool list"
1.44 - ("((Script Solve'_sq'_root'_equation (_ _ =))// \
1.45 - \ (_))" 9)
1.46 + :: "[bool,real,
1.47 + bool list] => bool list"
1.48 + ("((Script Solve'_sq'_root'_equation (_ _ =))//
1.49 + (_))" 9)
1.50 Solve'_left'_sq'_root'_equation
1.51 - :: "[bool,real, \
1.52 - \ bool list] => bool list"
1.53 - ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// \
1.54 - \ (_))" 9)
1.55 + :: "[bool,real,
1.56 + bool list] => bool list"
1.57 + ("((Script Solve'_left'_sq'_root'_equation (_ _ =))//
1.58 + (_))" 9)
1.59 Solve'_right'_sq'_root'_equation
1.60 - :: "[bool,real, \
1.61 - \ bool list] => bool list"
1.62 - ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// \
1.63 - \ (_))" 9)
1.64 + :: "[bool,real,
1.65 + bool list] => bool list"
1.66 + ("((Script Solve'_right'_sq'_root'_equation (_ _ =))//
1.67 + (_))" 9)
1.68
1.69 -(*-------------------- rules------------------------------------------------*)
1.70 -rules
1.71 +axioms
1.72
1.73 (* normalize *)
1.74 - makex1_x
1.75 - "a^^^1 = a"
1.76 - real_assoc_1
1.77 - "a+(b+c) = a+b+c"
1.78 - real_assoc_2
1.79 - "a*(b*c) = a*b*c"
1.80 + makex1_x "a^^^1 = a"
1.81 + real_assoc_1 "a+(b+c) = a+b+c"
1.82 + real_assoc_2 "a*(b*c) = a*b*c"
1.83
1.84 (* simplification of root*)
1.85 - sqrt_square_1
1.86 - "[|0 <= a|] ==> (sqrt a)^^^2 = a"
1.87 - sqrt_square_2
1.88 - "sqrt (a ^^^ 2) = a"
1.89 - sqrt_times_root_1
1.90 - "sqrt a * sqrt b = sqrt(a*b)"
1.91 - sqrt_times_root_2
1.92 - "a * sqrt b * sqrt c = a * sqrt(b*c)"
1.93 + sqrt_square_1 "[|0 <= a|] ==> (sqrt a)^^^2 = a"
1.94 + sqrt_square_2 "sqrt (a ^^^ 2) = a"
1.95 + sqrt_times_root_1 "sqrt a * sqrt b = sqrt(a*b)"
1.96 + sqrt_times_root_2 "a * sqrt b * sqrt c = a * sqrt(b*c)"
1.97
1.98 (* isolate one root on the LEFT or RIGHT hand side of the equation *)
1.99 - sqrt_isolate_l_add1
1.100 - "[|bdv occurs_in c|] ==> (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
1.101 - sqrt_isolate_l_add2
1.102 - "[|bdv occurs_in c|] ==>(a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
1.103 - sqrt_isolate_l_add3
1.104 - "[|bdv occurs_in c|] ==> (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d+ (-1) * a)"
1.105 - sqrt_isolate_l_add4
1.106 - "[|bdv occurs_in c|] ==>(a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d+ (-1) * a)"
1.107 - sqrt_isolate_l_add5
1.108 - "[|bdv occurs_in c|] ==> (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
1.109 - sqrt_isolate_l_add6
1.110 - "[|bdv occurs_in c|] ==>(a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
1.111 - sqrt_isolate_r_add1
1.112 - "[|bdv occurs_in f|] ==>(a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
1.113 - sqrt_isolate_r_add2
1.114 - "[|bdv occurs_in f|] ==>(a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
1.115 + sqrt_isolate_l_add1 "[|bdv occurs_in c|] ==>
1.116 + (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
1.117 + sqrt_isolate_l_add2 "[|bdv occurs_in c|] ==>
1.118 + (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
1.119 + sqrt_isolate_l_add3 "[|bdv occurs_in c|] ==>
1.120 + (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)"
1.121 + sqrt_isolate_l_add4 "[|bdv occurs_in c|] ==>
1.122 + (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)"
1.123 + sqrt_isolate_l_add5 "[|bdv occurs_in c|] ==>
1.124 + (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
1.125 + sqrt_isolate_l_add6 "[|bdv occurs_in c|] ==>
1.126 + (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
1.127 + sqrt_isolate_r_add1 "[|bdv occurs_in f|] ==>
1.128 + (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
1.129 + sqrt_isolate_r_add2 "[|bdv occurs_in f|] ==>
1.130 + (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
1.131 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
1.132 - sqrt_isolate_r_add3
1.133 - "[|bdv occurs_in f|] ==>(a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
1.134 - sqrt_isolate_r_add4
1.135 - "[|bdv occurs_in f|] ==>(a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
1.136 - sqrt_isolate_r_add5
1.137 - "[|bdv occurs_in f|] ==>(a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
1.138 - sqrt_isolate_r_add6
1.139 - "[|bdv occurs_in f|] ==>(a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
1.140 + sqrt_isolate_r_add3 "[|bdv occurs_in f|] ==>
1.141 + (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
1.142 + sqrt_isolate_r_add4 "[|bdv occurs_in f|] ==>
1.143 + (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
1.144 + sqrt_isolate_r_add5 "[|bdv occurs_in f|] ==>
1.145 + (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
1.146 + sqrt_isolate_r_add6 "[|bdv occurs_in f|] ==>
1.147 + (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
1.148
1.149 (* eliminate isolates sqrt *)
1.150 - sqrt_square_equation_both_1
1.151 - "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.152 - ( (sqrt a + sqrt b = sqrt c + sqrt d) =
1.153 - (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
1.154 - sqrt_square_equation_both_2
1.155 - "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.156 - ( (sqrt a - sqrt b = sqrt c + sqrt d) =
1.157 - (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
1.158 - sqrt_square_equation_both_3
1.159 - "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.160 - ( (sqrt a + sqrt b = sqrt c - sqrt d) =
1.161 - (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
1.162 - sqrt_square_equation_both_4
1.163 - "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.164 - ( (sqrt a - sqrt b = sqrt c - sqrt d) =
1.165 - (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
1.166 - sqrt_square_equation_left_1
1.167 - "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> ( (sqrt (a) = b) = (a = (b^^^2)))"
1.168 - sqrt_square_equation_left_2
1.169 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
1.170 - sqrt_square_equation_left_3
1.171 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
1.172 + sqrt_square_equation_both_1 "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.173 + ( (sqrt a + sqrt b = sqrt c + sqrt d) =
1.174 + (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
1.175 + sqrt_square_equation_both_2 "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.176 + ( (sqrt a - sqrt b = sqrt c + sqrt d) =
1.177 + (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
1.178 + sqrt_square_equation_both_3 "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.179 + ( (sqrt a + sqrt b = sqrt c - sqrt d) =
1.180 + (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
1.181 + sqrt_square_equation_both_4 "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.182 + ( (sqrt a - sqrt b = sqrt c - sqrt d) =
1.183 + (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
1.184 + sqrt_square_equation_left_1 "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
1.185 + ( (sqrt (a) = b) = (a = (b^^^2)))"
1.186 + sqrt_square_equation_left_2 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
1.187 + ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
1.188 + sqrt_square_equation_left_3 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
1.189 + ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
1.190 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
1.191 - sqrt_square_equation_left_4
1.192 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
1.193 - sqrt_square_equation_left_5
1.194 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
1.195 - sqrt_square_equation_left_6
1.196 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"
1.197 - sqrt_square_equation_right_1
1.198 - "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> ( (a = sqrt (b)) = (a^^^2 = b))"
1.199 - sqrt_square_equation_right_2
1.200 - "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
1.201 - sqrt_square_equation_right_3
1.202 - "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
1.203 + sqrt_square_equation_left_4 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
1.204 + ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
1.205 + sqrt_square_equation_left_5 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
1.206 + ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
1.207 + sqrt_square_equation_left_6 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
1.208 + ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"
1.209 + sqrt_square_equation_right_1 "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
1.210 + ( (a = sqrt (b)) = (a^^^2 = b))"
1.211 + sqrt_square_equation_right_2 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
1.212 + ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
1.213 + sqrt_square_equation_right_3 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
1.214 + ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
1.215 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
1.216 - sqrt_square_equation_right_4
1.217 - "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
1.218 - sqrt_square_equation_right_5
1.219 - "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
1.220 - sqrt_square_equation_right_6
1.221 - "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
1.222 -
1.223 + sqrt_square_equation_right_4 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
1.224 + ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
1.225 + sqrt_square_equation_right_5 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
1.226 + ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
1.227 + sqrt_square_equation_right_6 "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
1.228 + ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
1.229 +
1.230 +ML {*
1.231 +(*-------------------------functions---------------------*)
1.232 +(* true if bdv is under sqrt of a Equation*)
1.233 +fun is_rootTerm_in t v =
1.234 + let
1.235 + fun coeff_in c v = member op = (vars c) v;
1.236 + fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:")
1.237 + (* at the moment there is no term like this, but ....*)
1.238 + | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
1.239 + | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v)
1.240 + | findroot (t as (Const ("Root.sqrt",_) $ t2)) v = coeff_in t2 v
1.241 + | findroot (_ $ t2) v = (findroot t2 v)
1.242 + | findroot _ _ = false;
1.243 + in
1.244 + findroot t v
1.245 + end;
1.246 +
1.247 + fun is_sqrtTerm_in t v =
1.248 + let
1.249 + fun coeff_in c v = member op = (vars c) v;
1.250 + fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:")
1.251 + (* at the moment there is no term like this, but ....*)
1.252 + | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
1.253 + | findsqrt (t as (Const ("Root.sqrt",_) $ a)) v = coeff_in a v
1.254 + | findsqrt (_ $ t1) v = (findsqrt t1 v)
1.255 + | findsqrt _ _ = false;
1.256 + in
1.257 + findsqrt t v
1.258 + end;
1.259 +
1.260 +(* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
1.261 +and the subterm ist connected with + or * --> is normalized*)
1.262 + fun is_normSqrtTerm_in t v =
1.263 + let
1.264 + fun coeff_in c v = member op = (vars c) v;
1.265 + fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
1.266 + (* at the moment there is no term like this, but ....*)
1.267 + | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
1.268 + | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
1.269 + | isnorm (Const ("op -",_) $ _ $ _) v = false
1.270 + | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
1.271 + (is_sqrtTerm_in t2 v)
1.272 + | isnorm (Const ("Root.sqrt",_) $ t1) v = coeff_in t1 v
1.273 + | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
1.274 + | isnorm _ _ = false;
1.275 + in
1.276 + isnorm t v
1.277 + end;
1.278 +
1.279 +fun eval_is_rootTerm_in _ _
1.280 + (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ =
1.281 + if is_rootTerm_in t v then
1.282 + SOME ((term2str p) ^ " = True",
1.283 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.284 + else SOME ((term2str p) ^ " = True",
1.285 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.286 + | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
1.287 +
1.288 +fun eval_is_sqrtTerm_in _ _
1.289 + (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ =
1.290 + if is_sqrtTerm_in t v then
1.291 + SOME ((term2str p) ^ " = True",
1.292 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.293 + else SOME ((term2str p) ^ " = True",
1.294 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.295 + | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
1.296 +
1.297 +fun eval_is_normSqrtTerm_in _ _
1.298 + (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ =
1.299 + if is_normSqrtTerm_in t v then
1.300 + SOME ((term2str p) ^ " = True",
1.301 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.302 + else SOME ((term2str p) ^ " = True",
1.303 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.304 + | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
1.305 +
1.306 +(*-------------------------rulse-------------------------*)
1.307 +val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
1.308 + append_rls "RootEq_prls" e_rls
1.309 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.310 + Calc ("Tools.matches",eval_matches ""),
1.311 + Calc ("Tools.lhs" ,eval_lhs ""),
1.312 + Calc ("Tools.rhs" ,eval_rhs ""),
1.313 + Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
1.314 + Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
1.315 + Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
1.316 + Calc ("op =",eval_equal "#equal_"),
1.317 + Thm ("not_true",num_str not_true),
1.318 + Thm ("not_false",num_str not_false),
1.319 + Thm ("and_true",num_str and_true),
1.320 + Thm ("and_false",num_str and_false),
1.321 + Thm ("or_true",num_str or_true),
1.322 + Thm ("or_false",num_str or_false)
1.323 + ];
1.324 +
1.325 +val RootEq_erls =
1.326 + append_rls "RootEq_erls" Root_erls
1.327 + [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
1.328 + ];
1.329 +
1.330 +val RootEq_crls =
1.331 + append_rls "RootEq_crls" Root_crls
1.332 + [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
1.333 + ];
1.334 +
1.335 +val rooteq_srls =
1.336 + append_rls "rooteq_srls" e_rls
1.337 + [Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
1.338 + Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in""),
1.339 + Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
1.340 + ];
1.341 +
1.342 +ruleset' := overwritelthy thy (!ruleset',
1.343 + [("RootEq_erls",RootEq_erls),
1.344 + (*FIXXXME:del with rls.rls'*)
1.345 + ("rooteq_srls",rooteq_srls)
1.346 + ]);
1.347 +
1.348 +(*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
1.349 + val sqrt_isolate = prep_rls(
1.350 + Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
1.351 + erls = RootEq_erls, srls = Erls, calc = [],
1.352 + rules = [
1.353 + Thm("sqrt_square_1",num_str sqrt_square_1),
1.354 + (* (sqrt a)^^^2 -> a *)
1.355 + Thm("sqrt_square_2",num_str sqrt_square_2),
1.356 + (* sqrt (a^^^2) -> a *)
1.357 + Thm("sqrt_times_root_1",num_str sqrt_times_root_1),
1.358 + (* sqrt a sqrt b -> sqrt(ab) *)
1.359 + Thm("sqrt_times_root_2",num_str sqrt_times_root_2),
1.360 + (* a sqrt b sqrt c -> a sqrt(bc) *)
1.361 + Thm("sqrt_square_equation_both_1",
1.362 + num_str sqrt_square_equation_both_1),
1.363 + (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
1.364 + (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
1.365 + Thm("sqrt_square_equation_both_2",
1.366 + num_str sqrt_square_equation_both_2),
1.367 + (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
1.368 + (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
1.369 + Thm("sqrt_square_equation_both_3",
1.370 + num_str sqrt_square_equation_both_3),
1.371 + (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
1.372 + (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
1.373 + Thm("sqrt_square_equation_both_4",
1.374 + num_str sqrt_square_equation_both_4),
1.375 + (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
1.376 + (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
1.377 + Thm("sqrt_isolate_l_add1",
1.378 + num_str sqrt_isolate_l_add1),
1.379 + (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
1.380 + Thm("sqrt_isolate_l_add2",
1.381 + num_str sqrt_isolate_l_add2),
1.382 + (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
1.383 + Thm("sqrt_isolate_l_add3",
1.384 + num_str sqrt_isolate_l_add3),
1.385 + (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
1.386 + Thm("sqrt_isolate_l_add4",
1.387 + num_str sqrt_isolate_l_add4),
1.388 + (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
1.389 + Thm("sqrt_isolate_l_add5",
1.390 + num_str sqrt_isolate_l_add5),
1.391 + (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
1.392 + Thm("sqrt_isolate_l_add6",
1.393 + num_str sqrt_isolate_l_add6),
1.394 + (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
1.395 + (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*)
1.396 + (* b*sqrt(x) = d sqrt(x) d/b *)
1.397 + Thm("sqrt_isolate_r_add1",
1.398 + num_str sqrt_isolate_r_add1),
1.399 + (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
1.400 + Thm("sqrt_isolate_r_add2",
1.401 + num_str sqrt_isolate_r_add2),
1.402 + (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
1.403 + Thm("sqrt_isolate_r_add3",
1.404 + num_str sqrt_isolate_r_add3),
1.405 + (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
1.406 + Thm("sqrt_isolate_r_add4",
1.407 + num_str sqrt_isolate_r_add4),
1.408 + (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
1.409 + Thm("sqrt_isolate_r_add5",
1.410 + num_str sqrt_isolate_r_add5),
1.411 + (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
1.412 + Thm("sqrt_isolate_r_add6",
1.413 + num_str sqrt_isolate_r_add6),
1.414 + (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
1.415 + (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*)
1.416 + (* a=e*sqrt(x) -> a/e = sqrt(x) *)
1.417 + Thm("sqrt_square_equation_left_1",
1.418 + num_str sqrt_square_equation_left_1),
1.419 + (* sqrt(x)=b -> x=b^2 *)
1.420 + Thm("sqrt_square_equation_left_2",
1.421 + num_str sqrt_square_equation_left_2),
1.422 + (* c*sqrt(x)=b -> c^2*x=b^2 *)
1.423 + Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),
1.424 + (* c/sqrt(x)=b -> c^2/x=b^2 *)
1.425 + Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4),
1.426 + (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
1.427 + Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5),
1.428 + (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
1.429 + Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6),
1.430 + (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
1.431 + Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),
1.432 + (* a=sqrt(x) ->a^2=x *)
1.433 + Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),
1.434 + (* a=c*sqrt(x) ->a^2=c^2*x *)
1.435 + Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),
1.436 + (* a=c/sqrt(x) ->a^2=c^2/x *)
1.437 + Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4),
1.438 + (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
1.439 + Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5),
1.440 + (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
1.441 + Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)
1.442 + (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
1.443 + ],scr = Script ((term_of o the o (parse thy)) "empty_script")
1.444 + }:rls);
1.445 +
1.446 +ruleset' := overwritelthy thy (!ruleset',
1.447 + [("sqrt_isolate",sqrt_isolate)
1.448 + ]);
1.449 +(* -- left 28.08.02--*)
1.450 +(*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
1.451 + val l_sqrt_isolate = prep_rls(
1.452 + Rls {id = "l_sqrt_isolate", preconds = [],
1.453 + rew_ord = ("termlessI",termlessI),
1.454 + erls = RootEq_erls, srls = Erls, calc = [],
1.455 + rules = [
1.456 + Thm("sqrt_square_1",num_str sqrt_square_1),
1.457 + (* (sqrt a)^^^2 -> a *)
1.458 + Thm("sqrt_square_2",num_str sqrt_square_2),
1.459 + (* sqrt (a^^^2) -> a *)
1.460 + Thm("sqrt_times_root_1",num_str sqrt_times_root_1),
1.461 + (* sqrt a sqrt b -> sqrt(ab) *)
1.462 + Thm("sqrt_times_root_2",num_str sqrt_times_root_2),
1.463 + (* a sqrt b sqrt c -> a sqrt(bc) *)
1.464 + Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1),
1.465 + (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
1.466 + Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2),
1.467 + (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
1.468 + Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3),
1.469 + (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
1.470 + Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4),
1.471 + (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
1.472 + Thm("sqrt_isolate_l_add5",num_str sqrt_isolate_l_add5),
1.473 + (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
1.474 + Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6),
1.475 + (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
1.476 + (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*)
1.477 + (* b*sqrt(x) = d sqrt(x) d/b *)
1.478 + Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1),
1.479 + (* sqrt(x)=b -> x=b^2 *)
1.480 + Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2),
1.481 + (* a*sqrt(x)=b -> a^2*x=b^2*)
1.482 + Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),
1.483 + (* c/sqrt(x)=b -> c^2/x=b^2 *)
1.484 + Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4),
1.485 + (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
1.486 + Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5),
1.487 + (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
1.488 + Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6)
1.489 + (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
1.490 + ],
1.491 + scr = Script ((term_of o the o (parse thy)) "empty_script")
1.492 + }:rls);
1.493 +
1.494 +ruleset' := overwritelthy thy (!ruleset',
1.495 + [("l_sqrt_isolate",l_sqrt_isolate)
1.496 + ]);
1.497 +
1.498 +(* -- right 28.8.02--*)
1.499 +(*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
1.500 + val r_sqrt_isolate = prep_rls(
1.501 + Rls {id = "r_sqrt_isolate", preconds = [],
1.502 + rew_ord = ("termlessI",termlessI),
1.503 + erls = RootEq_erls, srls = Erls, calc = [],
1.504 + rules = [
1.505 + Thm("sqrt_square_1",num_str sqrt_square_1),
1.506 + (* (sqrt a)^^^2 -> a *)
1.507 + Thm("sqrt_square_2",num_str sqrt_square_2),
1.508 + (* sqrt (a^^^2) -> a *)
1.509 + Thm("sqrt_times_root_1",num_str sqrt_times_root_1),
1.510 + (* sqrt a sqrt b -> sqrt(ab) *)
1.511 + Thm("sqrt_times_root_2",num_str sqrt_times_root_2),
1.512 + (* a sqrt b sqrt c -> a sqrt(bc) *)
1.513 + Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1),
1.514 + (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
1.515 + Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2),
1.516 + (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
1.517 + Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3),
1.518 + (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
1.519 + Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4),
1.520 + (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
1.521 + Thm("sqrt_isolate_r_add5",num_str sqrt_isolate_r_add5),
1.522 + (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
1.523 + Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6),
1.524 + (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
1.525 + (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*)
1.526 + (* a=e*sqrt(x) -> a/e = sqrt(x) *)
1.527 + Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),
1.528 + (* a=sqrt(x) ->a^2=x *)
1.529 + Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),
1.530 + (* a=c*sqrt(x) ->a^2=c^2*x *)
1.531 + Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),
1.532 + (* a=c/sqrt(x) ->a^2=c^2/x *)
1.533 + Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4),
1.534 + (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
1.535 + Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5),
1.536 + (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
1.537 + Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)
1.538 + (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
1.539 + ],
1.540 + scr = Script ((term_of o the o (parse thy)) "empty_script")
1.541 + }:rls);
1.542 +
1.543 +ruleset' := overwritelthy thy (!ruleset',
1.544 + [("r_sqrt_isolate",r_sqrt_isolate)
1.545 + ]);
1.546 +
1.547 +val rooteq_simplify = prep_rls(
1.548 + Rls {id = "rooteq_simplify",
1.549 + preconds = [], rew_ord = ("termlessI",termlessI),
1.550 + erls = RootEq_erls, srls = Erls, calc = [],
1.551 + (*asm_thm = [("sqrt_square_1","")],*)
1.552 + rules = [Thm ("real_assoc_1",num_str real_assoc_1),
1.553 + (* a+(b+c) = a+b+c *)
1.554 + Thm ("real_assoc_2",num_str real_assoc_2),
1.555 + (* a*(b*c) = a*b*c *)
1.556 + Calc ("op +",eval_binop "#add_"),
1.557 + Calc ("op -",eval_binop "#sub_"),
1.558 + Calc ("op *",eval_binop "#mult_"),
1.559 + Calc ("HOL.divide", eval_cancel "#divide_"),
1.560 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.561 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.562 + Thm("real_plus_binom_pow2",num_str real_plus_binom_pow2),
1.563 + Thm("real_minus_binom_pow2",num_str real_minus_binom_pow2),
1.564 + Thm("realpow_mul",num_str realpow_mul),
1.565 + (* (a * b)^n = a^n * b^n*)
1.566 + Thm("sqrt_times_root_1",num_str sqrt_times_root_1),
1.567 + (* sqrt b * sqrt c = sqrt(b*c) *)
1.568 + Thm("sqrt_times_root_2",num_str sqrt_times_root_2),
1.569 + (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
1.570 + Thm("sqrt_square_2",num_str sqrt_square_2),
1.571 + (* sqrt (a^^^2) = a *)
1.572 + Thm("sqrt_square_1",num_str sqrt_square_1)
1.573 + (* sqrt a ^^^ 2 = a *)
1.574 + ],
1.575 + scr = Script ((term_of o the o (parse thy)) "empty_script")
1.576 + }:rls);
1.577 + ruleset' := overwritelthy thy (!ruleset',
1.578 + [("rooteq_simplify",rooteq_simplify)
1.579 + ]);
1.580 +
1.581 +(*-------------------------Problem-----------------------*)
1.582 +(*
1.583 +(get_pbt ["root","univariate","equation"]);
1.584 +show_ptyps();
1.585 +*)
1.586 +(* ---------root----------- *)
1.587 +store_pbt
1.588 + (prep_pbt RootEq.thy "pbl_equ_univ_root" [] e_pblID
1.589 + (["root","univariate","equation"],
1.590 + [("#Given" ,["equality e_","solveFor v_"]),
1.591 + ("#Where" ,["(lhs e_) is_rootTerm_in (v_::real) | " ^
1.592 + "(rhs e_) is_rootTerm_in (v_::real)"]),
1.593 + ("#Find" ,["solutions v_i_"])
1.594 + ],
1.595 + RootEq_prls, SOME "solve (e_::bool, v_)",
1.596 + []));
1.597 +(* ---------sqrt----------- *)
1.598 +store_pbt
1.599 + (prep_pbt RootEq.thy "pbl_equ_univ_root_sq" [] e_pblID
1.600 + (["sq","root","univariate","equation"],
1.601 + [("#Given" ,["equality e_","solveFor v_"]),
1.602 + ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
1.603 + " ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |" ^
1.604 + "( ((rhs e_) is_sqrtTerm_in (v_::real)) &" ^
1.605 + " ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]),
1.606 + ("#Find" ,["solutions v_i_"])
1.607 + ],
1.608 + RootEq_prls, SOME "solve (e_::bool, v_)",
1.609 + [["RootEq","solve_sq_root_equation"]]));
1.610 +(* ---------normalize----------- *)
1.611 +store_pbt
1.612 + (prep_pbt RootEq.thy "pbl_equ_univ_root_norm" [] e_pblID
1.613 + (["normalize","root","univariate","equation"],
1.614 + [("#Given" ,["equality e_","solveFor v_"]),
1.615 + ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
1.616 + " Not((lhs e_) is_normSqrtTerm_in (v_::real))) | " ^
1.617 + "( ((rhs e_) is_sqrtTerm_in (v_::real)) &" ^
1.618 + " Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),
1.619 + ("#Find" ,["solutions v_i_"])
1.620 + ],
1.621 + RootEq_prls, SOME "solve (e_::bool, v_)",
1.622 + [["RootEq","norm_sq_root_equation"]]));
1.623 +
1.624 +(*-------------------------methods-----------------------*)
1.625 +(* ---- root 20.8.02 ---*)
1.626 +store_met
1.627 + (prep_met RootEq.thy "met_rooteq" [] e_metID
1.628 + (["RootEq"],
1.629 + [],
1.630 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.631 + crls=RootEq_crls, nrls=norm_Poly(*,
1.632 + asm_rls=[],asm_thm=[]*)}, "empty_script"));
1.633 +(*-- normalize 20.10.02 --*)
1.634 +store_met
1.635 + (prep_met RootEq.thy "met_rooteq_norm" [] e_metID
1.636 + (["RootEq","norm_sq_root_equation"],
1.637 + [("#Given" ,["equality e_","solveFor v_"]),
1.638 + ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
1.639 + " Not((lhs e_) is_normSqrtTerm_in (v_::real))) | " ^
1.640 + "( ((rhs e_) is_sqrtTerm_in (v_::real)) &" ^
1.641 + " Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),
1.642 + ("#Find" ,["solutions v_i_"])
1.643 + ],
1.644 + {rew_ord'="termlessI",
1.645 + rls'=RootEq_erls,
1.646 + srls=e_rls,
1.647 + prls=RootEq_prls,
1.648 + calc=[],
1.649 + crls=RootEq_crls, nrls=norm_Poly(*,
1.650 + asm_rls=[],
1.651 + asm_thm=[("sqrt_square_1","")]*)},
1.652 + "Script Norm_sq_root_equation (e_::bool) (v_::real) = " ^
1.653 + "(let e_ = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
1.654 + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
1.655 + " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
1.656 + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
1.657 + " (Try (Rewrite_Set rooteq_simplify True))) e_ " ^
1.658 + " in ((SubProblem (RootEq_,[univariate,equation], " ^
1.659 + " [no_met]) [bool_ e_, real_ v_])))"
1.660 + ));
1.661 +
1.662 +store_met
1.663 + (prep_met RootEq.thy "met_rooteq_sq" [] e_metID
1.664 + (["RootEq","solve_sq_root_equation"],
1.665 + [("#Given" ,["equality e_","solveFor v_"]),
1.666 + ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
1.667 + " ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |" ^
1.668 + "( ((rhs e_) is_sqrtTerm_in (v_::real)) &" ^
1.669 + " ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]),
1.670 + ("#Find" ,["solutions v_i_"])
1.671 + ],
1.672 + {rew_ord'="termlessI",
1.673 + rls'=RootEq_erls,
1.674 + srls = rooteq_srls,
1.675 + prls = RootEq_prls,
1.676 + calc = [],
1.677 + crls=RootEq_crls, nrls=norm_Poly},
1.678 +"Script Solve_sq_root_equation (e_::bool) (v_::real) = " ^
1.679 +"(let e_ = " ^
1.680 +" ((Try (Rewrite_Set_Inst [(bdv,v_::real)] sqrt_isolate True)) @@ " ^
1.681 +" (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
1.682 +" (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
1.683 +" (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
1.684 +" (Try (Rewrite_Set rooteq_simplify True))) e_;" ^
1.685 +" (L_::bool list) = " ^
1.686 +" (if (((lhs e_) is_sqrtTerm_in v_) | ((rhs e_) is_sqrtTerm_in v_))" ^
1.687 +" then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
1.688 +" [no_met]) [bool_ e_, real_ v_]) " ^
1.689 +" else (SubProblem (RootEq_,[univariate,equation], " ^
1.690 +" [no_met]) [bool_ e_, real_ v_])) " ^
1.691 +" in Check_elementwise L_ {(v_::real). Assumptions})"
1.692 + ));
1.693 +
1.694 +(*-- right 28.08.02 --*)
1.695 +store_met
1.696 + (prep_met RootEq.thy "met_rooteq_sq_right" [] e_metID
1.697 + (["RootEq","solve_right_sq_root_equation"],
1.698 + [("#Given" ,["equality e_","solveFor v_"]),
1.699 + ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]),
1.700 + ("#Find" ,["solutions v_i_"])
1.701 + ],
1.702 + {rew_ord'="termlessI",
1.703 + rls'=RootEq_erls,
1.704 + srls=e_rls,
1.705 + prls=RootEq_prls,
1.706 + calc=[],
1.707 + crls=RootEq_crls, nrls=norm_Poly},
1.708 + "Script Solve_right_sq_root_equation (e_::bool) (v_::real) = " ^
1.709 + "(let e_ = " ^
1.710 + " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] r_sqrt_isolate False)) @@ " ^
1.711 + " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
1.712 + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
1.713 + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
1.714 + " (Try (Rewrite_Set rooteq_simplify False))) e_ " ^
1.715 + " in if ((rhs e_) is_sqrtTerm_in v_) " ^
1.716 + " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
1.717 + " [no_met]) [bool_ e_, real_ v_]) " ^
1.718 + " else ((SubProblem (RootEq_,[univariate,equation], " ^
1.719 + " [no_met]) [bool_ e_, real_ v_])))"
1.720 + ));
1.721 +
1.722 +(*-- left 28.08.02 --*)
1.723 +store_met
1.724 + (prep_met RootEq.thy "met_rooteq_sq_left" [] e_metID
1.725 + (["RootEq","solve_left_sq_root_equation"],
1.726 + [("#Given" ,["equality e_","solveFor v_"]),
1.727 + ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]),
1.728 + ("#Find" ,["solutions v_i_"])
1.729 + ],
1.730 + {rew_ord'="termlessI",
1.731 + rls'=RootEq_erls,
1.732 + srls=e_rls,
1.733 + prls=RootEq_prls,
1.734 + calc=[],
1.735 + crls=RootEq_crls, nrls=norm_Poly},
1.736 + "Script Solve_left_sq_root_equation (e_::bool) (v_::real) = " ^
1.737 + "(let e_ = " ^
1.738 + " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] l_sqrt_isolate False)) @@ " ^
1.739 + " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
1.740 + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
1.741 + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
1.742 + " (Try (Rewrite_Set rooteq_simplify False))) e_ " ^
1.743 + " in if ((lhs e_) is_sqrtTerm_in v_) " ^
1.744 + " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
1.745 + " [no_met]) [bool_ e_, real_ v_]) " ^
1.746 + " else ((SubProblem (RootEq_,[univariate,equation], " ^
1.747 + " [no_met]) [bool_ e_, real_ v_])))"
1.748 + ));
1.749 +
1.750 +calclist':= overwritel (!calclist',
1.751 + [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in",
1.752 + eval_is_rootTerm_in"")),
1.753 + ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in",
1.754 + eval_is_sqrtTerm_in"")),
1.755 + ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in",
1.756 + eval_is_normSqrtTerm_in""))
1.757 + ]);(*("", ("", "")),*)
1.758 +*}
1.759 +
1.760 end