1 (*.(c) by Richard Lang, 2003 .*) |
|
2 (* theory collecting all knowledge for RootEquations |
|
3 created by: rlang |
|
4 date: 02.09 |
|
5 changed by: rlang |
|
6 last change by: rlang |
|
7 date: 02.11.14 |
|
8 *) |
|
9 |
|
10 (* use"IsacKnowledge/RootEq.ML"; |
|
11 use"RootEq.ML"; |
|
12 |
|
13 use"ROOT.ML"; |
|
14 cd"knowledge"; |
|
15 |
|
16 remove_thy"RootEq"; |
|
17 use_thy"IsacKnowledge/Isac"; |
|
18 *) |
|
19 "******* RootEq.ML begin *******"; |
|
20 |
|
21 theory' := overwritel (!theory', [("RootEq.thy",RootEq.thy)]); |
|
22 (*-------------------------functions---------------------*) |
|
23 (* true if bdv is under sqrt of a Equation*) |
|
24 fun is_rootTerm_in t v = |
|
25 let |
|
26 fun coeff_in c v = member op = (vars c) v; |
|
27 fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:") |
|
28 (* at the moment there is no term like this, but ....*) |
|
29 | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v |
|
30 | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v) |
|
31 | findroot (t as (Const ("Root.sqrt",_) $ t2)) v = coeff_in t2 v |
|
32 | findroot (_ $ t2) v = (findroot t2 v) |
|
33 | findroot _ _ = false; |
|
34 in |
|
35 findroot t v |
|
36 end; |
|
37 |
|
38 fun is_sqrtTerm_in t v = |
|
39 let |
|
40 fun coeff_in c v = member op = (vars c) v; |
|
41 fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:") |
|
42 (* at the moment there is no term like this, but ....*) |
|
43 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v) |
|
44 | findsqrt (t as (Const ("Root.sqrt",_) $ a)) v = coeff_in a v |
|
45 | findsqrt (_ $ t1) v = (findsqrt t1 v) |
|
46 | findsqrt _ _ = false; |
|
47 in |
|
48 findsqrt t v |
|
49 end; |
|
50 |
|
51 (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv, |
|
52 and the subterm ist connected with + or * --> is normalized*) |
|
53 fun is_normSqrtTerm_in t v = |
|
54 let |
|
55 fun coeff_in c v = member op = (vars c) v; |
|
56 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:") |
|
57 (* at the moment there is no term like this, but ....*) |
|
58 | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
|
59 | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v |
|
60 | isnorm (Const ("op -",_) $ _ $ _) v = false |
|
61 | isnorm (Const ("HOL.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse |
|
62 (is_sqrtTerm_in t2 v) |
|
63 | isnorm (Const ("Root.sqrt",_) $ t1) v = coeff_in t1 v |
|
64 | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v |
|
65 | isnorm _ _ = false; |
|
66 in |
|
67 isnorm t v |
|
68 end; |
|
69 |
|
70 fun eval_is_rootTerm_in _ _ (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ = |
|
71 if is_rootTerm_in t v then |
|
72 SOME ((term2str p) ^ " = True", |
|
73 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
74 else SOME ((term2str p) ^ " = True", |
|
75 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
76 | eval_is_rootTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE); |
|
77 |
|
78 fun eval_is_sqrtTerm_in _ _ (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ = |
|
79 if is_sqrtTerm_in t v then |
|
80 SOME ((term2str p) ^ " = True", |
|
81 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
82 else SOME ((term2str p) ^ " = True", |
|
83 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
84 | eval_is_sqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE); |
|
85 |
|
86 fun eval_is_normSqrtTerm_in _ _ (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ = |
|
87 if is_normSqrtTerm_in t v then |
|
88 SOME ((term2str p) ^ " = True", |
|
89 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
90 else SOME ((term2str p) ^ " = True", |
|
91 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
92 | eval_is_normSqrtTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE); |
|
93 |
|
94 (*-------------------------rulse-------------------------*) |
|
95 val RootEq_prls = (*15.10.02:just the following order due to subterm evaluation*) |
|
96 append_rls "RootEq_prls" e_rls |
|
97 [Calc ("Atools.ident",eval_ident "#ident_"), |
|
98 Calc ("Tools.matches",eval_matches ""), |
|
99 Calc ("Tools.lhs" ,eval_lhs ""), |
|
100 Calc ("Tools.rhs" ,eval_rhs ""), |
|
101 Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""), |
|
102 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""), |
|
103 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""), |
|
104 Calc ("op =",eval_equal "#equal_"), |
|
105 Thm ("not_true",num_str not_true), |
|
106 Thm ("not_false",num_str not_false), |
|
107 Thm ("and_true",num_str and_true), |
|
108 Thm ("and_false",num_str and_false), |
|
109 Thm ("or_true",num_str or_true), |
|
110 Thm ("or_false",num_str or_false) |
|
111 ]; |
|
112 |
|
113 val RootEq_erls = |
|
114 append_rls "RootEq_erls" Root_erls |
|
115 [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq) |
|
116 ]; |
|
117 |
|
118 val RootEq_crls = |
|
119 append_rls "RootEq_crls" Root_crls |
|
120 [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq) |
|
121 ]; |
|
122 |
|
123 val rooteq_srls = |
|
124 append_rls "rooteq_srls" e_rls |
|
125 [Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""), |
|
126 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""), |
|
127 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "") |
|
128 ]; |
|
129 |
|
130 ruleset' := overwritelthy thy (!ruleset', |
|
131 [("RootEq_erls",RootEq_erls), (*FIXXXME:del with rls.rls'*) |
|
132 ("rooteq_srls",rooteq_srls) |
|
133 ]); |
|
134 |
|
135 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*) |
|
136 val sqrt_isolate = prep_rls( |
|
137 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), |
|
138 erls = RootEq_erls, srls = Erls, calc = [], |
|
139 (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""), |
|
140 ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""), |
|
141 ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""), |
|
142 ("sqrt_square_equation_left_6",""),("sqrt_square_equation_right_1",""), |
|
143 ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""), |
|
144 ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""), |
|
145 ("sqrt_square_equation_right_6","")],*) |
|
146 rules = [ |
|
147 Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *) |
|
148 Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *) |
|
149 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *) |
|
150 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *) |
|
151 Thm("sqrt_square_equation_both_1",num_str sqrt_square_equation_both_1), |
|
152 (* (sqrt a + sqrt b = sqrt c + sqrt d) -> (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
|
153 Thm("sqrt_square_equation_both_2",num_str sqrt_square_equation_both_2), |
|
154 (* (sqrt a - sqrt b = sqrt c + sqrt d) -> (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) |
|
155 Thm("sqrt_square_equation_both_3",num_str sqrt_square_equation_both_3), |
|
156 (* (sqrt a + sqrt b = sqrt c - sqrt d) -> (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
|
157 Thm("sqrt_square_equation_both_4",num_str sqrt_square_equation_both_4), |
|
158 (* (sqrt a - sqrt b = sqrt c - sqrt d) -> (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) |
|
159 Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1), (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) |
|
160 Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), (* a+ sqrt(x)=d -> sqrt(x) = d-a *) |
|
161 Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) |
|
162 Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) |
|
163 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 *) |
|
164 Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6), (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) |
|
165 (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*) (* b*sqrt(x) = d sqrt(x) d/b *) |
|
166 Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1), (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) |
|
167 Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2), (* a= d+ sqrt(x) -> a-d= sqrt(x) *) |
|
168 Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3), (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) |
|
169 Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4), (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) |
|
170 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)*) |
|
171 Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6), (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) |
|
172 (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*) (* a=e*sqrt(x) -> a/e = sqrt(x) *) |
|
173 Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1), |
|
174 (* sqrt(x)=b -> x=b^2 *) |
|
175 Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2), |
|
176 (* c*sqrt(x)=b -> c^2*x=b^2 *) |
|
177 Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3), |
|
178 (* c/sqrt(x)=b -> c^2/x=b^2 *) |
|
179 Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4), |
|
180 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) |
|
181 Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5), |
|
182 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *) |
|
183 Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6), |
|
184 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *) |
|
185 Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1), |
|
186 (* a=sqrt(x) ->a^2=x *) |
|
187 Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2), |
|
188 (* a=c*sqrt(x) ->a^2=c^2*x *) |
|
189 Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3), |
|
190 (* a=c/sqrt(x) ->a^2=c^2/x *) |
|
191 Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4), |
|
192 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *) |
|
193 Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5), |
|
194 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *) |
|
195 Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6) |
|
196 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *) |
|
197 ], |
|
198 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
199 }:rls); |
|
200 ruleset' := overwritelthy thy (!ruleset', |
|
201 [("sqrt_isolate",sqrt_isolate) |
|
202 ]); |
|
203 (* -- left 28.08.02--*) |
|
204 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*) |
|
205 val l_sqrt_isolate = prep_rls( |
|
206 Rls {id = "l_sqrt_isolate", preconds = [], |
|
207 rew_ord = ("termlessI",termlessI), |
|
208 erls = RootEq_erls, srls = Erls, calc = [], |
|
209 (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""), |
|
210 ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""), |
|
211 ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""), |
|
212 ("sqrt_square_equation_left_6","")],*) |
|
213 rules = [ |
|
214 Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *) |
|
215 Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *) |
|
216 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *) |
|
217 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *) |
|
218 Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1), (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) |
|
219 Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2), (* a+ sqrt(x)=d -> sqrt(x) = d-a *) |
|
220 Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3), (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) |
|
221 Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4), (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) |
|
222 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 *) |
|
223 Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6), (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) |
|
224 (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*) (* b*sqrt(x) = d sqrt(x) d/b *) |
|
225 Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1), |
|
226 (* sqrt(x)=b -> x=b^2 *) |
|
227 Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2), |
|
228 (* a*sqrt(x)=b -> a^2*x=b^2*) |
|
229 Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3), |
|
230 (* c/sqrt(x)=b -> c^2/x=b^2 *) |
|
231 Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4), |
|
232 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) |
|
233 Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5), |
|
234 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *) |
|
235 Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6) |
|
236 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *) |
|
237 ], |
|
238 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
239 }:rls); |
|
240 ruleset' := overwritelthy thy (!ruleset', |
|
241 [("l_sqrt_isolate",l_sqrt_isolate) |
|
242 ]); |
|
243 |
|
244 (* -- right 28.8.02--*) |
|
245 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*) |
|
246 val r_sqrt_isolate = prep_rls( |
|
247 Rls {id = "r_sqrt_isolate", preconds = [], |
|
248 rew_ord = ("termlessI",termlessI), |
|
249 erls = RootEq_erls, srls = Erls, calc = [], |
|
250 (*asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_right_1",""), |
|
251 ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""), |
|
252 ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""), |
|
253 ("sqrt_square_equation_right_6","")],*) |
|
254 rules = [ |
|
255 Thm("sqrt_square_1",num_str sqrt_square_1), (* (sqrt a)^^^2 -> a *) |
|
256 Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) -> a *) |
|
257 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt a sqrt b -> sqrt(ab) *) |
|
258 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a sqrt b sqrt c -> a sqrt(bc) *) |
|
259 Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1), (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) |
|
260 Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2), (* a= d+ sqrt(x) -> a-d= sqrt(x) *) |
|
261 Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3), (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) |
|
262 Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4), (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) |
|
263 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)*) |
|
264 Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6), (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) |
|
265 (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*) (* a=e*sqrt(x) -> a/e = sqrt(x) *) |
|
266 Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1), |
|
267 (* a=sqrt(x) ->a^2=x *) |
|
268 Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2), |
|
269 (* a=c*sqrt(x) ->a^2=c^2*x *) |
|
270 Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3), |
|
271 (* a=c/sqrt(x) ->a^2=c^2/x *) |
|
272 Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4), |
|
273 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *) |
|
274 Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5), |
|
275 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *) |
|
276 Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6) |
|
277 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *) |
|
278 ], |
|
279 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
280 }:rls); |
|
281 ruleset' := overwritelthy thy (!ruleset', |
|
282 [("r_sqrt_isolate",r_sqrt_isolate) |
|
283 ]); |
|
284 |
|
285 val rooteq_simplify = prep_rls( |
|
286 Rls {id = "rooteq_simplify", |
|
287 preconds = [], rew_ord = ("termlessI",termlessI), |
|
288 erls = RootEq_erls, srls = Erls, calc = [], |
|
289 (*asm_thm = [("sqrt_square_1","")],*) |
|
290 rules = [Thm ("real_assoc_1",num_str real_assoc_1), (* a+(b+c) = a+b+c *) |
|
291 Thm ("real_assoc_2",num_str real_assoc_2), (* a*(b*c) = a*b*c *) |
|
292 Calc ("op +",eval_binop "#add_"), |
|
293 Calc ("op -",eval_binop "#sub_"), |
|
294 Calc ("op *",eval_binop "#mult_"), |
|
295 Calc ("HOL.divide", eval_cancel "#divide_"), |
|
296 Calc ("Root.sqrt",eval_sqrt "#sqrt_"), |
|
297 Calc ("Atools.pow" ,eval_binop "#power_"), |
|
298 Thm("real_plus_binom_pow2",num_str real_plus_binom_pow2), |
|
299 Thm("real_minus_binom_pow2",num_str real_minus_binom_pow2), |
|
300 Thm("realpow_mul",num_str realpow_mul), (* (a * b)^n = a^n * b^n*) |
|
301 Thm("sqrt_times_root_1",num_str sqrt_times_root_1), (* sqrt b * sqrt c = sqrt(b*c) *) |
|
302 Thm("sqrt_times_root_2",num_str sqrt_times_root_2), (* a * sqrt a * sqrt b = a * sqrt(a*b) *) |
|
303 Thm("sqrt_square_2",num_str sqrt_square_2), (* sqrt (a^^^2) = a *) |
|
304 Thm("sqrt_square_1",num_str sqrt_square_1) (* sqrt a ^^^ 2 = a *) |
|
305 ], |
|
306 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
307 }:rls); |
|
308 ruleset' := overwritelthy thy (!ruleset', |
|
309 [("rooteq_simplify",rooteq_simplify) |
|
310 ]); |
|
311 |
|
312 (*-------------------------Problem-----------------------*) |
|
313 (* |
|
314 (get_pbt ["root","univariate","equation"]); |
|
315 show_ptyps(); |
|
316 *) |
|
317 (* ---------root----------- *) |
|
318 store_pbt |
|
319 (prep_pbt RootEq.thy "pbl_equ_univ_root" [] e_pblID |
|
320 (["root","univariate","equation"], |
|
321 [("#Given" ,["equality e_","solveFor v_"]), |
|
322 ("#Where" ,["(lhs e_) is_rootTerm_in (v_::real) | \ |
|
323 \(rhs e_) is_rootTerm_in (v_::real)"]), |
|
324 ("#Find" ,["solutions v_i_"]) |
|
325 ], |
|
326 RootEq_prls, SOME "solve (e_::bool, v_)", |
|
327 [])); |
|
328 (* ---------sqrt----------- *) |
|
329 store_pbt |
|
330 (prep_pbt RootEq.thy "pbl_equ_univ_root_sq" [] e_pblID |
|
331 (["sq","root","univariate","equation"], |
|
332 [("#Given" ,["equality e_","solveFor v_"]), |
|
333 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\ |
|
334 \ ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |\ |
|
335 \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\ |
|
336 \ ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]), |
|
337 ("#Find" ,["solutions v_i_"]) |
|
338 ], |
|
339 RootEq_prls, SOME "solve (e_::bool, v_)", |
|
340 [["RootEq","solve_sq_root_equation"]])); |
|
341 (* ---------normalize----------- *) |
|
342 store_pbt |
|
343 (prep_pbt RootEq.thy "pbl_equ_univ_root_norm" [] e_pblID |
|
344 (["normalize","root","univariate","equation"], |
|
345 [("#Given" ,["equality e_","solveFor v_"]), |
|
346 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\ |
|
347 \ Not((lhs e_) is_normSqrtTerm_in (v_::real))) | \ |
|
348 \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\ |
|
349 \ Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]), |
|
350 ("#Find" ,["solutions v_i_"]) |
|
351 ], |
|
352 RootEq_prls, SOME "solve (e_::bool, v_)", |
|
353 [["RootEq","norm_sq_root_equation"]])); |
|
354 |
|
355 (*-------------------------methods-----------------------*) |
|
356 (* ---- root 20.8.02 ---*) |
|
357 store_met |
|
358 (prep_met RootEq.thy "met_rooteq" [] e_metID |
|
359 (["RootEq"], |
|
360 [], |
|
361 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
|
362 crls=RootEq_crls, nrls=norm_Poly(*, |
|
363 asm_rls=[],asm_thm=[]*)}, "empty_script")); |
|
364 (*-- normalize 20.10.02 --*) |
|
365 store_met |
|
366 (prep_met RootEq.thy "met_rooteq_norm" [] e_metID |
|
367 (["RootEq","norm_sq_root_equation"], |
|
368 [("#Given" ,["equality e_","solveFor v_"]), |
|
369 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\ |
|
370 \ Not((lhs e_) is_normSqrtTerm_in (v_::real))) | \ |
|
371 \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\ |
|
372 \ Not((rhs e_) is_normSqrtTerm_in (v_::real)))"]), |
|
373 ("#Find" ,["solutions v_i_"]) |
|
374 ], |
|
375 {rew_ord'="termlessI", |
|
376 rls'=RootEq_erls, |
|
377 srls=e_rls, |
|
378 prls=RootEq_prls, |
|
379 calc=[], |
|
380 crls=RootEq_crls, nrls=norm_Poly(*, |
|
381 asm_rls=[], |
|
382 asm_thm=[("sqrt_square_1","")]*)}, |
|
383 "Script Norm_sq_root_equation (e_::bool) (v_::real) = \ |
|
384 \(let e_ = ((Repeat(Try (Rewrite makex1_x False))) @@ \ |
|
385 \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \ |
|
386 \ (Try (Rewrite_Set rooteq_simplify True)) @@ \ |
|
387 \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \ |
|
388 \ (Try (Rewrite_Set rooteq_simplify True))) e_ \ |
|
389 \ in ((SubProblem (RootEq_,[univariate,equation], \ |
|
390 \ [no_met]) [bool_ e_, real_ v_])))" |
|
391 )); |
|
392 |
|
393 store_met |
|
394 (prep_met RootEq.thy "met_rooteq_sq" [] e_metID |
|
395 (["RootEq","solve_sq_root_equation"], |
|
396 [("#Given" ,["equality e_","solveFor v_"]), |
|
397 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &\ |
|
398 \ ((lhs e_) is_normSqrtTerm_in (v_::real)) ) |\ |
|
399 \( ((rhs e_) is_sqrtTerm_in (v_::real)) &\ |
|
400 \ ((rhs e_) is_normSqrtTerm_in (v_::real)) )"]), |
|
401 ("#Find" ,["solutions v_i_"]) |
|
402 ], |
|
403 {rew_ord'="termlessI", |
|
404 rls'=RootEq_erls, |
|
405 srls = rooteq_srls, |
|
406 prls = RootEq_prls, |
|
407 calc = [], |
|
408 crls=RootEq_crls, nrls=norm_Poly(*, |
|
409 asm_rls = [], |
|
410 asm_thm = [("sqrt_square_1",""),("sqrt_square_equation_left_1",""), |
|
411 ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""), |
|
412 ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""), |
|
413 ("sqrt_square_equation_left_6",""),("sqrt_square_equation_right_1",""), |
|
414 ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""), |
|
415 ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""), |
|
416 ("sqrt_square_equation_right_6","")]*)}, |
|
417 "Script Solve_sq_root_equation (e_::bool) (v_::real) = \ |
|
418 \(let e_ = \ |
|
419 \ ((Try (Rewrite_Set_Inst [(bdv,v_::real)] sqrt_isolate True)) @@ \ |
|
420 \ (Try (Rewrite_Set rooteq_simplify True)) @@ \ |
|
421 \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \ |
|
422 \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \ |
|
423 \ (Try (Rewrite_Set rooteq_simplify True))) e_;\ |
|
424 \ (L_::bool list) = \ |
|
425 \ (if (((lhs e_) is_sqrtTerm_in v_) | ((rhs e_) is_sqrtTerm_in v_))\ |
|
426 \ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \ |
|
427 \ [no_met]) [bool_ e_, real_ v_]) \ |
|
428 \ else (SubProblem (RootEq_,[univariate,equation], \ |
|
429 \ [no_met]) [bool_ e_, real_ v_])) \ |
|
430 \ in Check_elementwise L_ {(v_::real). Assumptions})" |
|
431 )); |
|
432 |
|
433 (*-- right 28.08.02 --*) |
|
434 store_met |
|
435 (prep_met RootEq.thy "met_rooteq_sq_right" [] e_metID |
|
436 (["RootEq","solve_right_sq_root_equation"], |
|
437 [("#Given" ,["equality e_","solveFor v_"]), |
|
438 ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]), |
|
439 ("#Find" ,["solutions v_i_"]) |
|
440 ], |
|
441 {rew_ord'="termlessI", |
|
442 rls'=RootEq_erls, |
|
443 srls=e_rls, |
|
444 prls=RootEq_prls, |
|
445 calc=[], |
|
446 crls=RootEq_crls, nrls=norm_Poly(*, |
|
447 asm_rls=[], |
|
448 asm_thm=[("sqrt_square_1",""),("sqrt_square_1",""),("sqrt_square_equation_right_1",""), |
|
449 ("sqrt_square_equation_right_2",""),("sqrt_square_equation_right_3",""), |
|
450 ("sqrt_square_equation_right_4",""),("sqrt_square_equation_right_5",""), |
|
451 ("sqrt_square_equation_right_6","")]*)}, |
|
452 "Script Solve_right_sq_root_equation (e_::bool) (v_::real) = \ |
|
453 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] r_sqrt_isolate False)) @@ \ |
|
454 \ (Try (Rewrite_Set rooteq_simplify False)) @@ \ |
|
455 \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \ |
|
456 \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \ |
|
457 \ (Try (Rewrite_Set rooteq_simplify False))) e_\ |
|
458 \ in if ((rhs e_) is_sqrtTerm_in v_) \ |
|
459 \ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \ |
|
460 \ [no_met]) [bool_ e_, real_ v_]) \ |
|
461 \ else ((SubProblem (RootEq_,[univariate,equation], \ |
|
462 \ [no_met]) [bool_ e_, real_ v_])))" |
|
463 )); |
|
464 |
|
465 (*-- left 28.08.02 --*) |
|
466 store_met |
|
467 (prep_met RootEq.thy "met_rooteq_sq_left" [] e_metID |
|
468 (["RootEq","solve_left_sq_root_equation"], |
|
469 [("#Given" ,["equality e_","solveFor v_"]), |
|
470 ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]), |
|
471 ("#Find" ,["solutions v_i_"]) |
|
472 ], |
|
473 {rew_ord'="termlessI", |
|
474 rls'=RootEq_erls, |
|
475 srls=e_rls, |
|
476 prls=RootEq_prls, |
|
477 calc=[], |
|
478 crls=RootEq_crls, nrls=norm_Poly(*, |
|
479 asm_rls=[], |
|
480 asm_thm=[("sqrt_square_1",""),("sqrt_square_equation_left_1",""), |
|
481 ("sqrt_square_equation_left_2",""),("sqrt_square_equation_left_3",""), |
|
482 ("sqrt_square_equation_left_4",""),("sqrt_square_equation_left_5",""), |
|
483 ("sqrt_square_equation_left_6","")]*)}, |
|
484 "Script Solve_left_sq_root_equation (e_::bool) (v_::real) = \ |
|
485 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] l_sqrt_isolate False)) @@ \ |
|
486 \ (Try (Rewrite_Set rooteq_simplify False)) @@ \ |
|
487 \ (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ \ |
|
488 \ (Try (Repeat (Rewrite_Set make_rooteq False))) @@ \ |
|
489 \ (Try (Rewrite_Set rooteq_simplify False))) e_\ |
|
490 \ in if ((lhs e_) is_sqrtTerm_in v_) \ |
|
491 \ then (SubProblem (RootEq_,[normalize,root,univariate,equation], \ |
|
492 \ [no_met]) [bool_ e_, real_ v_]) \ |
|
493 \ else ((SubProblem (RootEq_,[univariate,equation], \ |
|
494 \ [no_met]) [bool_ e_, real_ v_])))" |
|
495 )); |
|
496 |
|
497 calclist':= overwritel (!calclist', |
|
498 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", |
|
499 eval_is_rootTerm_in"")), |
|
500 ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", |
|
501 eval_is_sqrtTerm_in"")), |
|
502 ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", |
|
503 eval_is_normSqrtTerm_in"")) |
|
504 ]);(*("", ("", "")),*) |
|
505 "******* RootEq.ML end *******"; |
|