neuper@37906
|
1 |
(*.(c) by Richard Lang, 2003 .*)
|
neuper@37906
|
2 |
(* collecting all knowledge for Root Equations
|
neuper@37906
|
3 |
created by: rlang
|
neuper@37906
|
4 |
date: 02.08
|
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 |
(* use"../knowledge/RootEq.ML";
|
neuper@37906
|
10 |
use"knowledge/RootEq.ML";
|
neuper@37906
|
11 |
use"RootEq.ML";
|
neuper@37906
|
12 |
|
neuper@37906
|
13 |
remove_thy"RootEq";
|
neuper@37906
|
14 |
use_thy"Isac";
|
neuper@37906
|
15 |
|
neuper@37906
|
16 |
use"ROOT.ML";
|
neuper@37906
|
17 |
cd"knowledge";
|
neuper@37906
|
18 |
*)
|
neuper@37906
|
19 |
|
neuper@37906
|
20 |
RootEq = Root +
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
(*-------------------- consts------------------------------------------------*)
|
neuper@37906
|
23 |
consts
|
neuper@37906
|
24 |
(*-------------------------root-----------------------*)
|
neuper@37906
|
25 |
is'_rootTerm'_in :: [real, real] => bool ("_ is'_rootTerm'_in _")
|
neuper@37906
|
26 |
is'_sqrtTerm'_in :: [real, real] => bool ("_ is'_sqrtTerm'_in _")
|
neuper@37906
|
27 |
is'_normSqrtTerm'_in :: [real, real] => bool ("_ is'_normSqrtTerm'_in _")
|
neuper@37906
|
28 |
(*----------------------scripts-----------------------*)
|
neuper@37906
|
29 |
Norm'_sq'_root'_equation
|
neuper@37906
|
30 |
:: "[bool,real, \
|
neuper@37906
|
31 |
\ bool list] => bool list"
|
neuper@37906
|
32 |
("((Script Norm'_sq'_root'_equation (_ _ =))// \
|
neuper@37906
|
33 |
\ (_))" 9)
|
neuper@37906
|
34 |
Solve'_sq'_root'_equation
|
neuper@37906
|
35 |
:: "[bool,real, \
|
neuper@37906
|
36 |
\ bool list] => bool list"
|
neuper@37906
|
37 |
("((Script Solve'_sq'_root'_equation (_ _ =))// \
|
neuper@37906
|
38 |
\ (_))" 9)
|
neuper@37906
|
39 |
Solve'_left'_sq'_root'_equation
|
neuper@37906
|
40 |
:: "[bool,real, \
|
neuper@37906
|
41 |
\ bool list] => bool list"
|
neuper@37906
|
42 |
("((Script Solve'_left'_sq'_root'_equation (_ _ =))// \
|
neuper@37906
|
43 |
\ (_))" 9)
|
neuper@37906
|
44 |
Solve'_right'_sq'_root'_equation
|
neuper@37906
|
45 |
:: "[bool,real, \
|
neuper@37906
|
46 |
\ bool list] => bool list"
|
neuper@37906
|
47 |
("((Script Solve'_right'_sq'_root'_equation (_ _ =))// \
|
neuper@37906
|
48 |
\ (_))" 9)
|
neuper@37906
|
49 |
|
neuper@37906
|
50 |
(*-------------------- rules------------------------------------------------*)
|
neuper@37906
|
51 |
rules
|
neuper@37906
|
52 |
|
neuper@37906
|
53 |
(* normalize *)
|
neuper@37906
|
54 |
makex1_x
|
neuper@37906
|
55 |
"a^^^1 = a"
|
neuper@37906
|
56 |
real_assoc_1
|
neuper@37906
|
57 |
"a+(b+c) = a+b+c"
|
neuper@37906
|
58 |
real_assoc_2
|
neuper@37906
|
59 |
"a*(b*c) = a*b*c"
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
(* simplification of root*)
|
neuper@37906
|
62 |
sqrt_square_1
|
neuper@37906
|
63 |
"[|0 <= a|] ==> (sqrt a)^^^2 = a"
|
neuper@37906
|
64 |
sqrt_square_2
|
neuper@37906
|
65 |
"sqrt (a ^^^ 2) = a"
|
neuper@37906
|
66 |
sqrt_times_root_1
|
neuper@37906
|
67 |
"sqrt a * sqrt b = sqrt(a*b)"
|
neuper@37906
|
68 |
sqrt_times_root_2
|
neuper@37906
|
69 |
"a * sqrt b * sqrt c = a * sqrt(b*c)"
|
neuper@37906
|
70 |
|
neuper@37906
|
71 |
(* isolate one root on the LEFT or RIGHT hand side of the equation *)
|
neuper@37906
|
72 |
sqrt_isolate_l_add1
|
neuper@37906
|
73 |
"[|bdv occurs_in c|] ==> (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
|
neuper@37906
|
74 |
sqrt_isolate_l_add2
|
neuper@37906
|
75 |
"[|bdv occurs_in c|] ==>(a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
|
neuper@37906
|
76 |
sqrt_isolate_l_add3
|
neuper@37906
|
77 |
"[|bdv occurs_in c|] ==> (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d+ (-1) * a)"
|
neuper@37906
|
78 |
sqrt_isolate_l_add4
|
neuper@37906
|
79 |
"[|bdv occurs_in c|] ==>(a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d+ (-1) * a)"
|
neuper@37906
|
80 |
sqrt_isolate_l_add5
|
neuper@37906
|
81 |
"[|bdv occurs_in c|] ==> (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
|
neuper@37906
|
82 |
sqrt_isolate_l_add6
|
neuper@37906
|
83 |
"[|bdv occurs_in c|] ==>(a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
|
neuper@37906
|
84 |
sqrt_isolate_r_add1
|
neuper@37906
|
85 |
"[|bdv occurs_in f|] ==>(a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
|
neuper@37906
|
86 |
sqrt_isolate_r_add2
|
neuper@37906
|
87 |
"[|bdv occurs_in f|] ==>(a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
|
neuper@37906
|
88 |
(* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
|
neuper@37906
|
89 |
sqrt_isolate_r_add3
|
neuper@37906
|
90 |
"[|bdv occurs_in f|] ==>(a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
|
neuper@37906
|
91 |
sqrt_isolate_r_add4
|
neuper@37906
|
92 |
"[|bdv occurs_in f|] ==>(a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
|
neuper@37906
|
93 |
sqrt_isolate_r_add5
|
neuper@37906
|
94 |
"[|bdv occurs_in f|] ==>(a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
|
neuper@37906
|
95 |
sqrt_isolate_r_add6
|
neuper@37906
|
96 |
"[|bdv occurs_in f|] ==>(a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
|
neuper@37906
|
97 |
|
neuper@37906
|
98 |
(* eliminate isolates sqrt *)
|
neuper@37906
|
99 |
sqrt_square_equation_both_1
|
neuper@37906
|
100 |
"[|bdv occurs_in b; bdv occurs_in d|] ==>
|
neuper@37906
|
101 |
( (sqrt a + sqrt b = sqrt c + sqrt d) =
|
neuper@37906
|
102 |
(a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
|
neuper@37906
|
103 |
sqrt_square_equation_both_2
|
neuper@37906
|
104 |
"[|bdv occurs_in b; bdv occurs_in d|] ==>
|
neuper@37906
|
105 |
( (sqrt a - sqrt b = sqrt c + sqrt d) =
|
neuper@37906
|
106 |
(a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
|
neuper@37906
|
107 |
sqrt_square_equation_both_3
|
neuper@37906
|
108 |
"[|bdv occurs_in b; bdv occurs_in d|] ==>
|
neuper@37906
|
109 |
( (sqrt a + sqrt b = sqrt c - sqrt d) =
|
neuper@37906
|
110 |
(a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
|
neuper@37906
|
111 |
sqrt_square_equation_both_4
|
neuper@37906
|
112 |
"[|bdv occurs_in b; bdv occurs_in d|] ==>
|
neuper@37906
|
113 |
( (sqrt a - sqrt b = sqrt c - sqrt d) =
|
neuper@37906
|
114 |
(a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
|
neuper@37906
|
115 |
sqrt_square_equation_left_1
|
neuper@37906
|
116 |
"[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> ( (sqrt (a) = b) = (a = (b^^^2)))"
|
neuper@37906
|
117 |
sqrt_square_equation_left_2
|
neuper@37906
|
118 |
"[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
|
neuper@37906
|
119 |
sqrt_square_equation_left_3
|
neuper@37906
|
120 |
"[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
|
neuper@37906
|
121 |
(* small hack: thm 4-6 are not needed if rootnormalize is well done*)
|
neuper@37906
|
122 |
sqrt_square_equation_left_4
|
neuper@37906
|
123 |
"[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
|
neuper@37906
|
124 |
sqrt_square_equation_left_5
|
neuper@37906
|
125 |
"[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
|
neuper@37906
|
126 |
sqrt_square_equation_left_6
|
neuper@37906
|
127 |
"[|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))"
|
neuper@37906
|
128 |
sqrt_square_equation_right_1
|
neuper@37906
|
129 |
"[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> ( (a = sqrt (b)) = (a^^^2 = b))"
|
neuper@37906
|
130 |
sqrt_square_equation_right_2
|
neuper@37906
|
131 |
"[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
|
neuper@37906
|
132 |
sqrt_square_equation_right_3
|
neuper@37906
|
133 |
"[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
|
neuper@37906
|
134 |
(* small hack: thm 4-6 are not needed if rootnormalize is well done*)
|
neuper@37906
|
135 |
sqrt_square_equation_right_4
|
neuper@37906
|
136 |
"[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
|
neuper@37906
|
137 |
sqrt_square_equation_right_5
|
neuper@37906
|
138 |
"[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
|
neuper@37906
|
139 |
sqrt_square_equation_right_6
|
neuper@37906
|
140 |
"[|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))))"
|
neuper@37906
|
141 |
|
neuper@37906
|
142 |
end
|