1.1 --- a/src/Tools/isac/IsacKnowledge/RootEq.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,505 +0,0 @@
1.4 -(*.(c) by Richard Lang, 2003 .*)
1.5 -(* theory collecting all knowledge for RootEquations
1.6 - created by: rlang
1.7 - date: 02.09
1.8 - changed by: rlang
1.9 - last change by: rlang
1.10 - date: 02.11.14
1.11 -*)
1.12 -
1.13 -(* use"IsacKnowledge/RootEq.ML";
1.14 - use"RootEq.ML";
1.15 -
1.16 - use"ROOT.ML";
1.17 - cd"knowledge";
1.18 -
1.19 - remove_thy"RootEq";
1.20 - use_thy"IsacKnowledge/Isac";
1.21 - *)
1.22 -"******* RootEq.ML begin *******";
1.23 -
1.24 -theory' := overwritel (!theory', [("RootEq.thy",RootEq.thy)]);
1.25 -(*-------------------------functions---------------------*)
1.26 -(* true if bdv is under sqrt of a Equation*)
1.27 -fun is_rootTerm_in t v =
1.28 - let
1.29 - fun coeff_in c v = member op = (vars c) v;
1.30 - fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:")
1.31 - (* at the moment there is no term like this, but ....*)
1.32 - | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
1.33 - | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v)
1.34 - | findroot (t as (Const ("Root.sqrt",_) $ t2)) v = coeff_in t2 v
1.35 - | findroot (_ $ t2) v = (findroot t2 v)
1.36 - | findroot _ _ = false;
1.37 - in
1.38 - findroot t v
1.39 - end;
1.40 -
1.41 - fun is_sqrtTerm_in t v =
1.42 - let
1.43 - fun coeff_in c v = member op = (vars c) v;
1.44 - fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:")
1.45 - (* at the moment there is no term like this, but ....*)
1.46 - | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
1.47 - | findsqrt (t as (Const ("Root.sqrt",_) $ a)) v = coeff_in a v
1.48 - | findsqrt (_ $ t1) v = (findsqrt t1 v)
1.49 - | findsqrt _ _ = false;
1.50 - in
1.51 - findsqrt t v
1.52 - end;
1.53 -
1.54 -(* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv,
1.55 -and the subterm ist connected with + or * --> is normalized*)
1.56 - fun is_normSqrtTerm_in t v =
1.57 - let
1.58 - fun coeff_in c v = member op = (vars c) v;
1.59 - fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
1.60 - (* at the moment there is no term like this, but ....*)
1.61 - | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
1.62 - | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
1.63 - | isnorm (Const ("op -",_) $ _ $ _) v = false
1.64 - | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse
1.65 - (is_sqrtTerm_in t2 v)
1.66 - | isnorm (Const ("Root.sqrt",_) $ t1) v = coeff_in t1 v
1.67 - | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v
1.68 - | isnorm _ _ = false;
1.69 - in
1.70 - isnorm t v
1.71 - end;
1.72 -
1.73 -fun eval_is_rootTerm_in _ _ (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ =
1.74 - if is_rootTerm_in t v then
1.75 - SOME ((term2str p) ^ " = True",
1.76 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.77 - else SOME ((term2str p) ^ " = True",
1.78 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.79 - | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
1.80 -
1.81 -fun eval_is_sqrtTerm_in _ _ (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ =
1.82 - if is_sqrtTerm_in t v then
1.83 - SOME ((term2str p) ^ " = True",
1.84 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.85 - else SOME ((term2str p) ^ " = True",
1.86 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.87 - | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
1.88 -
1.89 -fun eval_is_normSqrtTerm_in _ _ (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ =
1.90 - if is_normSqrtTerm_in t v then
1.91 - SOME ((term2str p) ^ " = True",
1.92 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.93 - else SOME ((term2str p) ^ " = True",
1.94 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.95 - | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
1.96 -
1.97 -(*-------------------------rulse-------------------------*)
1.98 -val RootEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
1.99 - append_rls "RootEq_prls" e_rls
1.100 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.101 - Calc ("Tools.matches",eval_matches ""),
1.102 - Calc ("Tools.lhs" ,eval_lhs ""),
1.103 - Calc ("Tools.rhs" ,eval_rhs ""),
1.104 - Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
1.105 - Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
1.106 - Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
1.107 - Calc ("op =",eval_equal "#equal_"),
1.108 - Thm ("not_true",num_str not_true),
1.109 - Thm ("not_false",num_str not_false),
1.110 - Thm ("and_true",num_str and_true),
1.111 - Thm ("and_false",num_str and_false),
1.112 - Thm ("or_true",num_str or_true),
1.113 - Thm ("or_false",num_str or_false)
1.114 - ];
1.115 -
1.116 -val RootEq_erls =
1.117 - append_rls "RootEq_erls" Root_erls
1.118 - [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
1.119 - ];
1.120 -
1.121 -val RootEq_crls =
1.122 - append_rls "RootEq_crls" Root_crls
1.123 - [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
1.124 - ];
1.125 -
1.126 -val rooteq_srls =
1.127 - append_rls "rooteq_srls" e_rls
1.128 - [Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
1.129 - Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
1.130 - Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
1.131 - ];
1.132 -
1.133 -ruleset' := overwritelthy thy (!ruleset',
1.134 - [("RootEq_erls",RootEq_erls), (*FIXXXME:del with rls.rls'*)
1.135 - ("rooteq_srls",rooteq_srls)
1.136 - ]);
1.137 -
1.138 -(*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
1.139 - val sqrt_isolate = prep_rls(
1.140 - Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
1.141 - erls = RootEq_erls, srls = Erls, calc = [],
1.142 - (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""),
1.143 - ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),
1.144 - ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),
1.145 - ("sqrt_square_equation_left_6",""),("sqrt_square_equation_right_1",""),
1.146 - ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),
1.147 - ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),
1.148 - ("sqrt_square_equation_right_6","")],*)
1.149 - rules = [
1.150 - Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *)
1.151 - Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *)
1.152 - Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *)
1.153 - Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *)
1.154 - Thm("sqrt_square_equation_both_1",num_str sqrt_square_equation_both_1),
1.155 - (* (sqrt a + sqrt b = sqrt c + sqrt d) -> (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
1.156 - Thm("sqrt_square_equation_both_2",num_str sqrt_square_equation_both_2),
1.157 - (* (sqrt a - sqrt b = sqrt c + sqrt d) -> (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
1.158 - Thm("sqrt_square_equation_both_3",num_str sqrt_square_equation_both_3),
1.159 - (* (sqrt a + sqrt b = sqrt c - sqrt d) -> (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
1.160 - Thm("sqrt_square_equation_both_4",num_str sqrt_square_equation_both_4),
1.161 - (* (sqrt a - sqrt b = sqrt c - sqrt d) -> (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
1.162 - Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1), (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
1.163 - Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
1.164 - Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
1.165 - Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
1.166 - Thm("sqrt_isolate_l_add5",num_str sqrt_isolate_l_add5), (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
1.167 - Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6), (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
1.168 - (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*) (* b*sqrt(x) = d sqrt(x) d/b *)
1.169 - Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1), (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
1.170 - Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2), (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
1.171 - Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3), (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
1.172 - Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4), (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
1.173 - Thm("sqrt_isolate_r_add5",num_str sqrt_isolate_r_add5), (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
1.174 - Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6), (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
1.175 - (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*) (* a=e*sqrt(x) -> a/e = sqrt(x) *)
1.176 - Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1),
1.177 - (* sqrt(x)=b -> x=b^2 *)
1.178 - Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2),
1.179 - (* c*sqrt(x)=b -> c^2*x=b^2 *)
1.180 - Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),
1.181 - (* c/sqrt(x)=b -> c^2/x=b^2 *)
1.182 - Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4),
1.183 - (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
1.184 - Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5),
1.185 - (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
1.186 - Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6),
1.187 - (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
1.188 - Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),
1.189 - (* a=sqrt(x) ->a^2=x *)
1.190 - Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),
1.191 - (* a=c*sqrt(x) ->a^2=c^2*x *)
1.192 - Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),
1.193 - (* a=c/sqrt(x) ->a^2=c^2/x *)
1.194 - Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4),
1.195 - (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
1.196 - Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5),
1.197 - (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
1.198 - Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)
1.199 - (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
1.200 - ],
1.201 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.202 - }:rls);
1.203 -ruleset' := overwritelthy thy (!ruleset',
1.204 - [("sqrt_isolate",sqrt_isolate)
1.205 - ]);
1.206 -(* -- left 28.08.02--*)
1.207 -(*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
1.208 - val l_sqrt_isolate = prep_rls(
1.209 - Rls {id = "l_sqrt_isolate", preconds = [],
1.210 - rew_ord = ("termlessI",termlessI),
1.211 - erls = RootEq_erls, srls = Erls, calc = [],
1.212 - (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""),
1.213 - ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),
1.214 - ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),
1.215 - ("sqrt_square_equation_left_6","")],*)
1.216 - rules = [
1.217 - Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *)
1.218 - Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *)
1.219 - Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *)
1.220 - Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *)
1.221 - Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1), (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
1.222 - Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
1.223 - Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
1.224 - Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
1.225 - Thm("sqrt_isolate_l_add5",num_str sqrt_isolate_l_add5), (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
1.226 - Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6), (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
1.227 - (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*) (* b*sqrt(x) = d sqrt(x) d/b *)
1.228 - Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1),
1.229 - (* sqrt(x)=b -> x=b^2 *)
1.230 - Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2),
1.231 - (* a*sqrt(x)=b -> a^2*x=b^2*)
1.232 - Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),
1.233 - (* c/sqrt(x)=b -> c^2/x=b^2 *)
1.234 - Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4),
1.235 - (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
1.236 - Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5),
1.237 - (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
1.238 - Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6)
1.239 - (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
1.240 - ],
1.241 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.242 - }:rls);
1.243 -ruleset' := overwritelthy thy (!ruleset',
1.244 - [("l_sqrt_isolate",l_sqrt_isolate)
1.245 - ]);
1.246 -
1.247 -(* -- right 28.8.02--*)
1.248 -(*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
1.249 - val r_sqrt_isolate = prep_rls(
1.250 - Rls {id = "r_sqrt_isolate", preconds = [],
1.251 - rew_ord = ("termlessI",termlessI),
1.252 - erls = RootEq_erls, srls = Erls, calc = [],
1.253 - (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_right_1",""),
1.254 - ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),
1.255 - ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),
1.256 - ("sqrt_square_equation_right_6","")],*)
1.257 - rules = [
1.258 - Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *)
1.259 - Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *)
1.260 - Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *)
1.261 - Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *)
1.262 - Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1), (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
1.263 - Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2), (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
1.264 - Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3), (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
1.265 - Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4), (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
1.266 - Thm("sqrt_isolate_r_add5",num_str sqrt_isolate_r_add5), (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
1.267 - Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6), (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
1.268 - (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*) (* a=e*sqrt(x) -> a/e = sqrt(x) *)
1.269 - Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),
1.270 - (* a=sqrt(x) ->a^2=x *)
1.271 - Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),
1.272 - (* a=c*sqrt(x) ->a^2=c^2*x *)
1.273 - Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),
1.274 - (* a=c/sqrt(x) ->a^2=c^2/x *)
1.275 - Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4),
1.276 - (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
1.277 - Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5),
1.278 - (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
1.279 - Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)
1.280 - (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
1.281 - ],
1.282 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.283 - }:rls);
1.284 -ruleset' := overwritelthy thy (!ruleset',
1.285 - [("r_sqrt_isolate",r_sqrt_isolate)
1.286 - ]);
1.287 -
1.288 -val rooteq_simplify = prep_rls(
1.289 - Rls {id = "rooteq_simplify",
1.290 - preconds = [], rew_ord = ("termlessI",termlessI),
1.291 - erls = RootEq_erls, srls = Erls, calc = [],
1.292 - (*asm_thm = [("sqrt_square_1","")],*)
1.293 - rules = [Thm ("real_assoc_1",num_str real_assoc_1), (* a+(b+c) = a+b+c *)
1.294 - Thm ("real_assoc_2",num_str real_assoc_2), (* a*(b*c) = a*b*c *)
1.295 - Calc ("op +",eval_binop "#add_"),
1.296 - Calc ("op -",eval_binop "#sub_"),
1.297 - Calc ("op *",eval_binop "#mult_"),
1.298 - Calc ("HOL.divide", eval_cancel "#divide_"),
1.299 - Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.300 - Calc ("Atools.pow" ,eval_binop "#power_"),
1.301 - Thm("real_plus_binom_pow2",num_str real_plus_binom_pow2),
1.302 - Thm("real_minus_binom_pow2",num_str real_minus_binom_pow2),
1.303 - Thm("realpow_mul",num_str realpow_mul), (* (a * b)^n = a^n * b^n*)
1.304 - Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt b * sqrt c = sqrt(b*c) *)
1.305 - Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
1.306 - Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) = a *)
1.307 - Thm("sqrt_square_1",num_str sqrt_square_1) (* sqrt a ^^^ 2 = a *)
1.308 - ],
1.309 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.310 - }:rls);
1.311 - ruleset' := overwritelthy thy (!ruleset',
1.312 - [("rooteq_simplify",rooteq_simplify)
1.313 - ]);
1.314 -
1.315 -(*-------------------------Problem-----------------------*)
1.316 -(*
1.317 -(get_pbt ["root","univariate","equation"]);
1.318 -show_ptyps();
1.319 -*)
1.320 -(* ---------root----------- *)
1.321 -store_pbt
1.322 - (prep_pbt RootEq.thy "pbl_equ_univ_root" [] e_pblID
1.323 - (["root","univariate","equation"],
1.324 - [("#Given" ,["equality e_","solveFor v_"]),
1.325 - ("#Where" ,["(lhs e_) is_rootTerm_in (v_::real) | \
1.326 - \(rhs e_) is_rootTerm_in (v_::real)"]),
1.327 - ("#Find" ,["solutions v_i_"])
1.328 - ],
1.329 - RootEq_prls, SOME "solve (e_::bool, v_)",
1.330 - []));
1.331 -(* ---------sqrt----------- *)
1.332 -store_pbt
1.333 - (prep_pbt RootEq.thy "pbl_equ_univ_root_sq" [] e_pblID
1.334 - (["sq","root","univariate","equation"],
1.335 - [("#Given" ,["equality e_","solveFor v_"]),
1.336 - ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\
1.337 - \ ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |\
1.338 - \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\
1.339 - \ ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]),
1.340 - ("#Find" ,["solutions v_i_"])
1.341 - ],
1.342 - RootEq_prls, SOME "solve (e_::bool, v_)",
1.343 - [["RootEq","solve_sq_root_equation"]]));
1.344 -(* ---------normalize----------- *)
1.345 -store_pbt
1.346 - (prep_pbt RootEq.thy "pbl_equ_univ_root_norm" [] e_pblID
1.347 - (["normalize","root","univariate","equation"],
1.348 - [("#Given" ,["equality e_","solveFor v_"]),
1.349 - ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\
1.350 - \ Not((lhs e_) is_normSqrtTerm_in (v_::real))) | \
1.351 - \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\
1.352 - \ Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),
1.353 - ("#Find" ,["solutions v_i_"])
1.354 - ],
1.355 - RootEq_prls, SOME "solve (e_::bool, v_)",
1.356 - [["RootEq","norm_sq_root_equation"]]));
1.357 -
1.358 -(*-------------------------methods-----------------------*)
1.359 -(* ---- root 20.8.02 ---*)
1.360 -store_met
1.361 - (prep_met RootEq.thy "met_rooteq" [] e_metID
1.362 - (["RootEq"],
1.363 - [],
1.364 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.365 - crls=RootEq_crls, nrls=norm_Poly(*,
1.366 - asm_rls=[],asm_thm=[]*)}, "empty_script"));
1.367 -(*-- normalize 20.10.02 --*)
1.368 -store_met
1.369 - (prep_met RootEq.thy "met_rooteq_norm" [] e_metID
1.370 - (["RootEq","norm_sq_root_equation"],
1.371 - [("#Given" ,["equality e_","solveFor v_"]),
1.372 - ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\
1.373 - \ Not((lhs e_) is_normSqrtTerm_in (v_::real))) | \
1.374 - \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\
1.375 - \ Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]),
1.376 - ("#Find" ,["solutions v_i_"])
1.377 - ],
1.378 - {rew_ord'="termlessI",
1.379 - rls'=RootEq_erls,
1.380 - srls=e_rls,
1.381 - prls=RootEq_prls,
1.382 - calc=[],
1.383 - crls=RootEq_crls, nrls=norm_Poly(*,
1.384 - asm_rls=[],
1.385 - asm_thm=[("sqrt_square_1","")]*)},
1.386 - "Script Norm_sq_root_equation (e_::bool) (v_::real) = \
1.387 - \(let e_ = ((Repeat(Try (Rewrite makex1_x False))) @@ \
1.388 - \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \
1.389 - \ (Try (Rewrite_Set rooteq_simplify True)) @@ \
1.390 - \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \
1.391 - \ (Try (Rewrite_Set rooteq_simplify True))) e_ \
1.392 - \ in ((SubProblem (RootEq_,[univariate,equation], \
1.393 - \ [no_met]) [bool_ e_, real_ v_])))"
1.394 - ));
1.395 -
1.396 -store_met
1.397 - (prep_met RootEq.thy "met_rooteq_sq" [] e_metID
1.398 - (["RootEq","solve_sq_root_equation"],
1.399 - [("#Given" ,["equality e_","solveFor v_"]),
1.400 - ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\
1.401 - \ ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |\
1.402 - \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\
1.403 - \ ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]),
1.404 - ("#Find" ,["solutions v_i_"])
1.405 - ],
1.406 - {rew_ord'="termlessI",
1.407 - rls'=RootEq_erls,
1.408 - srls = rooteq_srls,
1.409 - prls = RootEq_prls,
1.410 - calc = [],
1.411 - crls=RootEq_crls, nrls=norm_Poly(*,
1.412 - asm_rls = [],
1.413 - asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""),
1.414 - ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),
1.415 - ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),
1.416 - ("sqrt_square_equation_left_6",""),("sqrt_square_equation_right_1",""),
1.417 - ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),
1.418 - ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),
1.419 - ("sqrt_square_equation_right_6","")]*)},
1.420 -"Script Solve_sq_root_equation (e_::bool) (v_::real) = \
1.421 -\(let e_ = \
1.422 -\ ((Try (Rewrite_Set_Inst [(bdv,v_::real)] sqrt_isolate True)) @@ \
1.423 -\ (Try (Rewrite_Set rooteq_simplify True)) @@ \
1.424 -\ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \
1.425 -\ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \
1.426 -\ (Try (Rewrite_Set rooteq_simplify True))) e_;\
1.427 -\ (L_::bool list) = \
1.428 -\ (if (((lhs e_) is_sqrtTerm_in v_) | ((rhs e_) is_sqrtTerm_in v_))\
1.429 -\ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \
1.430 -\ [no_met]) [bool_ e_, real_ v_]) \
1.431 -\ else (SubProblem (RootEq_,[univariate,equation], \
1.432 -\ [no_met]) [bool_ e_, real_ v_])) \
1.433 -\ in Check_elementwise L_ {(v_::real). Assumptions})"
1.434 - ));
1.435 -
1.436 -(*-- right 28.08.02 --*)
1.437 -store_met
1.438 - (prep_met RootEq.thy "met_rooteq_sq_right" [] e_metID
1.439 - (["RootEq","solve_right_sq_root_equation"],
1.440 - [("#Given" ,["equality e_","solveFor v_"]),
1.441 - ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]),
1.442 - ("#Find" ,["solutions v_i_"])
1.443 - ],
1.444 - {rew_ord'="termlessI",
1.445 - rls'=RootEq_erls,
1.446 - srls=e_rls,
1.447 - prls=RootEq_prls,
1.448 - calc=[],
1.449 - crls=RootEq_crls, nrls=norm_Poly(*,
1.450 - asm_rls=[],
1.451 - asm_thm=[("sqrt_square_1",""),("sqrt_square_1",""),("sqrt_square_equation_right_1",""),
1.452 - ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""),
1.453 - ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""),
1.454 - ("sqrt_square_equation_right_6","")]*)},
1.455 - "Script Solve_right_sq_root_equation (e_::bool) (v_::real) = \
1.456 - \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] r_sqrt_isolate False)) @@ \
1.457 - \ (Try (Rewrite_Set rooteq_simplify False)) @@ \
1.458 - \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \
1.459 - \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \
1.460 - \ (Try (Rewrite_Set rooteq_simplify False))) e_\
1.461 - \ in if ((rhs e_) is_sqrtTerm_in v_) \
1.462 - \ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \
1.463 - \ [no_met]) [bool_ e_, real_ v_]) \
1.464 - \ else ((SubProblem (RootEq_,[univariate,equation], \
1.465 - \ [no_met]) [bool_ e_, real_ v_])))"
1.466 - ));
1.467 -
1.468 -(*-- left 28.08.02 --*)
1.469 -store_met
1.470 - (prep_met RootEq.thy "met_rooteq_sq_left" [] e_metID
1.471 - (["RootEq","solve_left_sq_root_equation"],
1.472 - [("#Given" ,["equality e_","solveFor v_"]),
1.473 - ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]),
1.474 - ("#Find" ,["solutions v_i_"])
1.475 - ],
1.476 - {rew_ord'="termlessI",
1.477 - rls'=RootEq_erls,
1.478 - srls=e_rls,
1.479 - prls=RootEq_prls,
1.480 - calc=[],
1.481 - crls=RootEq_crls, nrls=norm_Poly(*,
1.482 - asm_rls=[],
1.483 - asm_thm=[("sqrt_square_1",""),("sqrt_square_equation_left_1",""),
1.484 - ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""),
1.485 - ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""),
1.486 - ("sqrt_square_equation_left_6","")]*)},
1.487 - "Script Solve_left_sq_root_equation (e_::bool) (v_::real) = \
1.488 - \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] l_sqrt_isolate False)) @@ \
1.489 - \ (Try (Rewrite_Set rooteq_simplify False)) @@ \
1.490 - \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \
1.491 - \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \
1.492 - \ (Try (Rewrite_Set rooteq_simplify False))) e_\
1.493 - \ in if ((lhs e_) is_sqrtTerm_in v_) \
1.494 - \ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \
1.495 - \ [no_met]) [bool_ e_, real_ v_]) \
1.496 - \ else ((SubProblem (RootEq_,[univariate,equation], \
1.497 - \ [no_met]) [bool_ e_, real_ v_])))"
1.498 - ));
1.499 -
1.500 -calclist':= overwritel (!calclist',
1.501 - [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in",
1.502 - eval_is_rootTerm_in"")),
1.503 - ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in",
1.504 - eval_is_sqrtTerm_in"")),
1.505 - ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in",
1.506 - eval_is_normSqrtTerm_in""))
1.507 - ]);(*("", ("", "")),*)
1.508 -"******* RootEq.ML end *******";