38 (_))" 9) |
38 (_))" 9) |
39 |
39 |
40 axioms |
40 axioms |
41 |
41 |
42 (* normalize *) |
42 (* normalize *) |
43 makex1_x "a^^^1 = a" |
43 makex1_x: "a^^^1 = a" |
44 real_assoc_1 "a+(b+c) = a+b+c" |
44 real_assoc_1: "a+(b+c) = a+b+c" |
45 real_assoc_2 "a*(b*c) = a*b*c" |
45 real_assoc_2: "a*(b*c) = a*b*c" |
46 |
46 |
47 (* simplification of root*) |
47 (* simplification of root*) |
48 sqrt_square_1 "[|0 <= a|] ==> (sqrt a)^^^2 = a" |
48 sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a" |
49 sqrt_square_2 "sqrt (a ^^^ 2) = a" |
49 sqrt_square_2: "sqrt (a ^^^ 2) = a" |
50 sqrt_times_root_1 "sqrt a * sqrt b = sqrt(a*b)" |
50 sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)" |
51 sqrt_times_root_2 "a * sqrt b * sqrt c = a * sqrt(b*c)" |
51 sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)" |
52 |
52 |
53 (* isolate one root on the LEFT or RIGHT hand side of the equation *) |
53 (* isolate one root on the LEFT or RIGHT hand side of the equation *) |
54 sqrt_isolate_l_add1 "[|bdv occurs_in c|] ==> |
54 sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==> |
55 (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" |
55 (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" |
56 sqrt_isolate_l_add2 "[|bdv occurs_in c|] ==> |
56 sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==> |
57 (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" |
57 (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" |
58 sqrt_isolate_l_add3 "[|bdv occurs_in c|] ==> |
58 sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==> |
59 (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" |
59 (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" |
60 sqrt_isolate_l_add4 "[|bdv occurs_in c|] ==> |
60 sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==> |
61 (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" |
61 (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" |
62 sqrt_isolate_l_add5 "[|bdv occurs_in c|] ==> |
62 sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==> |
63 (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" |
63 (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" |
64 sqrt_isolate_l_add6 "[|bdv occurs_in c|] ==> |
64 sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==> |
65 (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" |
65 (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" |
66 sqrt_isolate_r_add1 "[|bdv occurs_in f|] ==> |
66 sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==> |
67 (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" |
67 (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" |
68 sqrt_isolate_r_add2 "[|bdv occurs_in f|] ==> |
68 sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==> |
69 (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" |
69 (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" |
70 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*) |
70 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*) |
71 sqrt_isolate_r_add3 "[|bdv occurs_in f|] ==> |
71 sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==> |
72 (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" |
72 (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" |
73 sqrt_isolate_r_add4 "[|bdv occurs_in f|] ==> |
73 sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==> |
74 (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" |
74 (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" |
75 sqrt_isolate_r_add5 "[|bdv occurs_in f|] ==> |
75 sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==> |
76 (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" |
76 (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" |
77 sqrt_isolate_r_add6 "[|bdv occurs_in f|] ==> |
77 sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==> |
78 (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" |
78 (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" |
79 |
79 |
80 (* eliminate isolates sqrt *) |
80 (* eliminate isolates sqrt *) |
81 sqrt_square_equation_both_1 "[|bdv occurs_in b; bdv occurs_in d|] ==> |
81 sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==> |
82 ( (sqrt a + sqrt b = sqrt c + sqrt d) = |
82 ( (sqrt a + sqrt b = sqrt c + sqrt d) = |
83 (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" |
83 (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" |
84 sqrt_square_equation_both_2 "[|bdv occurs_in b; bdv occurs_in d|] ==> |
84 sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==> |
85 ( (sqrt a - sqrt b = sqrt c + sqrt d) = |
85 ( (sqrt a - sqrt b = sqrt c + sqrt d) = |
86 (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" |
86 (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" |
87 sqrt_square_equation_both_3 "[|bdv occurs_in b; bdv occurs_in d|] ==> |
87 sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==> |
88 ( (sqrt a + sqrt b = sqrt c - sqrt d) = |
88 ( (sqrt a + sqrt b = sqrt c - sqrt d) = |
89 (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" |
89 (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" |
90 sqrt_square_equation_both_4 "[|bdv occurs_in b; bdv occurs_in d|] ==> |
90 sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==> |
91 ( (sqrt a - sqrt b = sqrt c - sqrt d) = |
91 ( (sqrt a - sqrt b = sqrt c - sqrt d) = |
92 (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" |
92 (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" |
93 sqrt_square_equation_left_1 "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> |
93 sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> |
94 ( (sqrt (a) = b) = (a = (b^^^2)))" |
94 ( (sqrt (a) = b) = (a = (b^^^2)))" |
95 sqrt_square_equation_left_2 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> |
95 sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> |
96 ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" |
96 ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" |
97 sqrt_square_equation_left_3 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> |
97 sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> |
98 ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" |
98 ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" |
99 (* small hack: thm 4-6 are not needed if rootnormalize is well done*) |
99 (* small hack: thm 4-6 are not needed if rootnormalize is well done*) |
100 sqrt_square_equation_left_4 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> |
100 sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> |
101 ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" |
101 ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" |
102 sqrt_square_equation_left_5 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> |
102 sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> |
103 ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" |
103 ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" |
104 sqrt_square_equation_left_6 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> |
104 sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> |
105 ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" |
105 ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" |
106 sqrt_square_equation_right_1 "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> |
106 sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> |
107 ( (a = sqrt (b)) = (a^^^2 = b))" |
107 ( (a = sqrt (b)) = (a^^^2 = b))" |
108 sqrt_square_equation_right_2 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> |
108 sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> |
109 ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" |
109 ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" |
110 sqrt_square_equation_right_3 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> |
110 sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> |
111 ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" |
111 ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" |
112 (* small hack: thm 4-6 are not needed if rootnormalize is well done*) |
112 (* small hack: thm 4-6 are not needed if rootnormalize is well done*) |
113 sqrt_square_equation_right_4 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> |
113 sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> |
114 ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" |
114 ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" |
115 sqrt_square_equation_right_5 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> |
115 sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> |
116 ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" |
116 ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" |
117 sqrt_square_equation_right_6 "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> |
117 sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> |
118 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))" |
118 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))" |
119 |
119 |
120 ML {* |
120 ML {* |
121 val thy = @{theory}; |
121 val thy = @{theory}; |
122 |
122 |