set_goal([`&0 < b pow 2 - &4 * a * c`],`?x. a * x pow 2 + b * x + c = &0`);;
e(ASM_CASES_TAC `a = &0`);;
e(ASM_CASES_TAC `b = &0`);;
e( X_GET_TAC 0 );;
e( ASM_SIMP_TAC [] );;
e( ARITH_TAC );;
e( EXISTS_TAC `-- c / b` );;
e( ASM_REAL_FIELD_TAC );;
e( EXISTS_TAC `(sqrt (b pow 2 - &4 * a * c) - b) / (&2 * a)` );;
e( POP_ASSUM MP_TAC );;
e( FIRST_X_ASSUM (MP_TAC o (MATCH_MP REAL_LT_IMP_LE) ) );;
e( SIMP_TAC [POW_2;GSYM SQRT_POW2] );;
e( REAL_FIELD_TAC );;
top_thm();;
# set_goal([`&0 < b pow 2 - &4 * a * c`],`?x. a * x pow 2 + b * x + c = &0`);;
val it : goalstack = 1 subgoal (1 total)
0 [`&0 < b pow 2 - &4 * a * c`]
`?x. a * x pow 2 + b * x + c = &0`
# e(ASM_CASES_TAC `a = &0`);;
val it : goalstack = 2 subgoals (2 total)
0 [`&0 < b pow 2 - &4 * a * c`]
1 [`~(a = &0)`]
`?x. a * x pow 2 + b * x + c = &0`
0 [`&0 < b pow 2 - &4 * a * c`]
1 [`a = &0`]
`?x. a * x pow 2 + b * x + c = &0`
# e(ASM_CASES_TAC `b = &0`);;
val it : goalstack = 2 subgoals (3 total)
0 [`&0 < b pow 2 - &4 * a * c`]
1 [`a = &0`]
2 [`~(b = &0)`]
`?x. a * x pow 2 + b * x + c = &0`
0 [`&0 < b pow 2 - &4 * a * c`]
1 [`a = &0`]
2 [`b = &0`]
`?x. a * x pow 2 + b * x + c = &0`
# e( X_GET_TAC 0 );;
val it : goalstack = 1 subgoal (3 total)
0 [`a = &0`]
1 [`b = &0`]
`&0 < b pow 2 - &4 * a * c ==> (?x. a * x pow 2 + b * x + c = &0)`
# e( ASM_SIMP_TAC [] );;
val it : goalstack = 1 subgoal (3 total)
0 [`a = &0`]
1 [`b = &0`]
`&0 < &0 pow 2 - &4 * &0 * c ==> (?x. &0 * x pow 2 + &0 * x + c = &0)`
# e( ARITH_TAC );;
val it : goalstack = 1 subgoal (2 total)
0 [`&0 < b pow 2 - &4 * a * c`]
1 [`a = &0`]
2 [`~(b = &0)`]
`?x. a * x pow 2 + b * x + c = &0`
# e( EXISTS_TAC `-- c / b` );;
val it : goalstack = 1 subgoal (2 total)
0 [`&0 < b pow 2 - &4 * a * c`]
1 [`a = &0`]
2 [`~(b = &0)`]
`a * (--c / b) pow 2 + b * --c / b + c = &0`
# e( ASM_REAL_FIELD_TAC );;
2 basis elements and 0 critical pairs
5 basis elements and 3 critical pairs
5 basis elements and 2 critical pairs
5 basis elements and 1 critical pairs
5 basis elements and 0 critical pairs
val it : goalstack = 1 subgoal (1 total)
0 [`&0 < b pow 2 - &4 * a * c`]
1 [`~(a = &0)`]
`?x. a * x pow 2 + b * x + c = &0`
# e( EXISTS_TAC `(sqrt (b pow 2 - &4 * a * c) - b) / (&2 * a)` );;
val it : goalstack = 1 subgoal (1 total)
0 [`&0 < b pow 2 - &4 * a * c`]
1 [`~(a = &0)`]
`a * ((sqrt (b pow 2 - &4 * a * c) - b) / (&2 * a)) pow 2 +
b * (sqrt (b pow 2 - &4 * a * c) - b) / (&2 * a) +
c =
&0`
# e( POP_ASSUM MP_TAC );;
val it : goalstack = 1 subgoal (1 total)
0 [`&0 < b pow 2 - &4 * a * c`]
`~(a = &0)
==> a * ((sqrt (b pow 2 - &4 * a * c) - b) / (&2 * a)) pow 2 +
b * (sqrt (b pow 2 - &4 * a * c) - b) / (&2 * a) +
c =
&0`
# e( FIRST_X_ASSUM (MP_TAC o (MATCH_MP REAL_LT_IMP_LE) ) );;
val it : goalstack = 1 subgoal (1 total)
`&0 <= b pow 2 - &4 * a * c
==> ~(a = &0)
==> a * ((sqrt (b pow 2 - &4 * a * c) - b) / (&2 * a)) pow 2 +
b * (sqrt (b pow 2 - &4 * a * c) - b) / (&2 * a) +
c =
&0`
# e( SIMP_TAC [POW_2;GSYM SQRT_POW2] );;
val it : goalstack = 1 subgoal (1 total)
`sqrt (b * b - &4 * a * c) * sqrt (b * b - &4 * a * c) = b * b - &4 * a * c
==> ~(a = &0)
==> a *
(sqrt (b * b - &4 * a * c) - b) / (&2 * a) *
(sqrt (b * b - &4 * a * c) - b) / (&2 * a) +
b * (sqrt (b * b - &4 * a * c) - b) / (&2 * a) +
c =
&0`
# e( REAL_FIELD_TAC );;
3 basis elements and 0 critical pairs
4 basis elements and 1 critical pairs
4 basis elements and 0 critical pairs
val it : goalstack = No subgoals
# top_thm () ;;
val it : thm = &0 < b pow 2 - &4 * a * c |- ?x. a * x pow 2 + b * x + c = &0
