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