3 (* ------------------------------------------------------------------------- *)
4 (* First the R = 0 case. *)
5 (* ------------------------------------------------------------------------- *)
8 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
9 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
10 R pow 2 = a pow 2 / &4 - b + y /\
12 s pow 2 = y pow 2 - &4 * d /\
13 D pow 2 = &3 * a pow 2 / &4 - &2 * b + &2 * s /\
14 x = --a / &4 + R / &2 + D / &2
15 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
19 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
20 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
21 R pow 2 = a pow 2 / &4 - b + y /\
23 s pow 2 = y pow 2 - &4 * d /\
24 D pow 2 = &3 * a pow 2 / &4 - &2 * b + &2 * s /\
25 x = --a / &4 + R / &2 - D / &2
26 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
30 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
31 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
32 R pow 2 = a pow 2 / &4 - b + y /\
34 s pow 2 = y pow 2 - &4 * d /\
35 E pow 2 = &3 * a pow 2 / &4 - &2 * b - &2 * s /\
36 x = --a / &4 - R / &2 + E / &2
37 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
41 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
42 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
43 R pow 2 = a pow 2 / &4 - b + y /\
45 s pow 2 = y pow 2 - &4 * d /\
46 E pow 2 = &3 * a pow 2 / &4 - &2 * b - &2 * s /\
47 x = --a / &4 - R / &2 - E / &2
48 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
52 (* ------------------------------------------------------------------------- *)
53 (* The R nonzero case. *)
54 (* ------------------------------------------------------------------------- *)
56 let QUARTIC_1' = prove
57 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
58 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
59 R pow 2 = a pow 2 / &4 - b + y /\
61 D pow 2 = &3 * a pow 2 / &4 - R pow 2 - &2 * b +
62 (&4 * a * b - &8 * c - a pow 3) / (&4 * R) /\
63 x = --a / &4 + R / &2 + D / &2
64 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
65 CONV_TAC REAL_FIELD);;
67 let QUARTIC_2' = prove
68 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
69 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
70 R pow 2 = a pow 2 / &4 - b + y /\
72 D pow 2 = &3 * a pow 2 / &4 - R pow 2 - &2 * b +
73 (&4 * a * b - &8 * c - a pow 3) / (&4 * R) /\
74 x = --a / &4 + R / &2 - D / &2
75 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
76 CONV_TAC REAL_FIELD);;
78 let QUARTIC_3' = prove
79 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
80 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
81 R pow 2 = a pow 2 / &4 - b + y /\
83 E pow 2 = &3 * a pow 2 / &4 - R pow 2 - &2 * b -
84 (&4 * a * b - &8 * c - a pow 3) / (&4 * R) /\
85 x = --a / &4 - R / &2 + E / &2
86 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
87 CONV_TAC REAL_FIELD);;
89 let QUARTIC_4' = prove
90 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
91 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
92 R pow 2 = a pow 2 / &4 - b + y /\
94 E pow 2 = &3 * a pow 2 / &4 - R pow 2 - &2 * b -
95 (&4 * a * b - &8 * c - a pow 3) / (&4 * R) /\
96 x = --a / &4 - R / &2 - E / &2
97 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
98 CONV_TAC REAL_FIELD);;
100 (* ------------------------------------------------------------------------- *)
102 (* ------------------------------------------------------------------------- *)
104 let QUARTIC_1 = prove
105 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
106 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
107 R pow 2 = a pow 2 / &4 - b + y /\
108 s pow 2 = y pow 2 - &4 * d /\
109 (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
110 else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
111 (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
112 x = --a / &4 + R / &2 + D / &2
113 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
114 CONV_TAC REAL_FIELD);;
116 (* ------------------------------------------------------------------------- *)
118 (* ------------------------------------------------------------------------- *)
120 let QUARTIC_1 = prove
121 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
122 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
123 R pow 2 = a pow 2 / &4 - b + y /\
124 s pow 2 = y pow 2 - &4 * d /\
125 (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
126 else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
127 (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
128 (E pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b - &2 * s
129 else &3 * a pow 2 / &4 - R pow 2 - &2 * b -
130 (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
131 (x = --a / &4 + R / &2 + D / &2 \/
132 x = --a / &4 - R / &2 + E / &2)
133 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
134 CONV_TAC REAL_FIELD);;
136 (* ------------------------------------------------------------------------- *)
137 (* More general case split. *)
138 (* ------------------------------------------------------------------------- *)
140 let QUARTIC_CASES = prove
141 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
142 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
143 R pow 2 = a pow 2 / &4 - b + y /\
144 s pow 2 = y pow 2 - &4 * d /\
145 (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
146 else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
147 (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
148 (E pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b - &2 * s
149 else &3 * a pow 2 / &4 - R pow 2 - &2 * b -
150 (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
151 (x = --a / &4 + R / &2 + D / &2 \/
152 x = --a / &4 + R / &2 - D / &2 \/
153 x = --a / &4 - R / &2 + E / &2 \/
154 x = --a / &4 - R / &2 - E / &2)
155 ==> x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0`,
156 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN
157 CONV_TAC REAL_FIELD);;
159 (* ------------------------------------------------------------------------- *)
160 (* Even this works --- great, that's nearly what we wanted. *)
161 (* ------------------------------------------------------------------------- *)
163 let QUARTIC_CASES = prove
164 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
165 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
166 R pow 2 = a pow 2 / &4 - b + y /\
167 s pow 2 = y pow 2 - &4 * d /\
168 (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
169 else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
170 (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
171 (E pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b - &2 * s
172 else &3 * a pow 2 / &4 - R pow 2 - &2 * b -
173 (&4 * a * b - &8 * c - a pow 3) / (&4 * R))
174 ==> (x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0 <=>
175 x = --a / &4 + R / &2 + D / &2 \/
176 x = --a / &4 + R / &2 - D / &2 \/
177 x = --a / &4 - R / &2 + E / &2 \/
178 x = --a / &4 - R / &2 - E / &2)`,
179 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN
180 CONV_TAC REAL_FIELD);;
182 (* ------------------------------------------------------------------------- *)
183 (* This is the automatic proof. *)
184 (* ------------------------------------------------------------------------- *)
186 let QUARTIC_CASES = prove
187 (`y pow 3 - b * y pow 2 + (a * c - &4 * d) * y -
188 a pow 2 * d + &4 * b * d - c pow 2 = &0 /\
189 R pow 2 = a pow 2 / &4 - b + y /\
190 s pow 2 = y pow 2 - &4 * d /\
191 (D pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b + &2 * s
192 else &3 * a pow 2 / &4 - R pow 2 - &2 * b +
193 (&4 * a * b - &8 * c - a pow 3) / (&4 * R)) /\
194 (E pow 2 = if R = &0 then &3 * a pow 2 / &4 - &2 * b - &2 * s
195 else &3 * a pow 2 / &4 - R pow 2 - &2 * b -
196 (&4 * a * b - &8 * c - a pow 3) / (&4 * R))
197 ==> (x pow 4 + a * x pow 3 + b * x pow 2 + c * x + d = &0 <=>
198 x = --a / &4 + R / &2 + D / &2 \/
199 x = --a / &4 + R / &2 - D / &2 \/
200 x = --a / &4 - R / &2 + E / &2 \/
201 x = --a / &4 - R / &2 - E / &2)`,
202 CONV_TAC REAL_FIELD);;