読者です 読者をやめる 読者になる 読者になる

set_goal

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