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