tactics の選択

∀，∃を消去するには，仮定と結論を分離し，十分条件などに帰着させる方法が一般的です．

# g `(!x. &0<x ==> a<x )==> a<= &0` ;;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)

`(!x. &0 < x ==> a < x) ==> a <= &0`

# e( STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`!x. &0 < x ==> a < x`]

`a <= &0`

# e( POP_ASSUM (MP_TAC o (SPEC `a / &2`) )  );;
val it : goalstack = 1 subgoal (1 total)

`(&0 < a / &2 ==> a < a / &2) ==> a <= &0`

# e( ARITH_TAC );;
val it : goalstack = No subgoals

# g `a<= &0==>(!x. &0<x ==> a<x)` ;;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)

`a <= &0 ==> (!x. &0 < x ==> a < x)`

# e( REPEAT STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`a <= &0`]
  1 [`&0 < x`]

`a < x`

# e( REPEAT (POP_ASSUM MP_TAC));;
val it : goalstack = 1 subgoal (1 total)

`a <= &0 ==> &0 < x ==> a < x`

# e( ARITH_TAC );;
val it : goalstack = No subgoals

# g `(?x. &0<x /\ x<a) ==> &0<a` ;;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)

`(?x. &0 < x /\ x < a) ==> &0 < a`

# e( REPEAT STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 < x`]
  1 [`x < a`]

`&0 < a`

# e( REPEAT (POP_ASSUM MP_TAC));;
val it : goalstack = 1 subgoal (1 total)

`&0 < x ==> x < a ==> &0 < a`

# e( ARITH_TAC );;
val it : goalstack = No subgoals

# g `&0<a ==> (?x. &0<x /\ x<a)` ;;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)

`&0 < a ==> (?x. &0 < x /\ x < a)`

# e( STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 < a`]

`?x. &0 < x /\ x < a`

# e( EXISTS_TAC `a / &2`);;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 < a`]

`&0 < a / &2 /\ a / &2 < a`

# e( POP_ASSUM MP_TAC );;
val it : goalstack = 1 subgoal (1 total)

`&0 < a ==> &0 < a / &2 /\ a / &2 < a`

# e( ARITH_TAC );;
val it : goalstack = No subgoals

一方，必要に応じてＡ，Ｂ|-ＣをＡ|-Ｂ⇒Ｃに UNDISCH_TAC して結論Ｂ⇒Ｃを

# search[name"LEFT_IMP"];;
val it : (string * thm) list =
  [("LEFT_IMP_FORALL_THM", |- !P Q. (!x. P x) ==> Q <=> (?x. P x ==> Q));
   ("LEFT_IMP_EXISTS_THM", |- !P Q. (?x. P x) ==> Q <=> (!x. P x ==> Q))]
# search[name"RIGHT_IMP"];;
val it : (string * thm) list =
  [("RIGHT_IMP_FORALL_THM", |- !P Q. P ==> (!x. Q x) <=> (!x. P ==> Q x));
   ("RIGHT_IMP_EXISTS_THM", |- !P Q. P ==> (?x. Q x) <=> (?x. P ==> Q x))]

を参照して REWRITE_TAC し，結論全体の量化に書き換えれば，GEN_TAC,EXISTS_TAC で処理できます．

# g `(!x. &0<x ==> a<x )==> a<= &0` ;;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)

`(!x. &0 < x ==> a < x) ==> a <= &0`

# e( REWRITE_TAC [LEFT_IMP_FORALL_THM]  );;
val it : goalstack = 1 subgoal (1 total)

`?x. (&0 < x ==> a < x) ==> a <= &0`

# e( EXISTS_TAC `a / &2`);;
val it : goalstack = 1 subgoal (1 total)

`(&0 < a / &2 ==> a < a / &2) ==> a <= &0`

# e( ARITH_TAC );;
val it : goalstack = No subgoals

# g `a<= &0==>(!x. &0<x ==> a<x)` ;;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)

`a <= &0 ==> (!x. &0 < x ==> a < x)`

# e( REWRITE_TAC [RIGHT_IMP_FORALL_THM]  );;
val it : goalstack = 1 subgoal (1 total)

`!x. a <= &0 ==> &0 < x ==> a < x`

# e( ARITH_TAC );;
val it : goalstack = No subgoals

# g `(?x. &0<x /\ x<a) ==> &0<a` ;;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)

`(?x. &0 < x /\ x < a) ==> &0 < a`

# e( REWRITE_TAC [LEFT_IMP_EXISTS_THM]  );;
val it : goalstack = 1 subgoal (1 total)

`!x. &0 < x /\ x < a ==> &0 < a`

# e( GEN_TAC );;
val it : goalstack = 1 subgoal (1 total)

`&0 < x /\ x < a ==> &0 < a`

# e( ARITH_TAC );;
val it : goalstack = No subgoals

# g `&0<a ==> (?x. &0<x /\ x<a)` ;;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)

`&0 < a ==> (?x. &0 < x /\ x < a)`

# e( REWRITE_TAC [RIGHT_IMP_EXISTS_THM]  );;
val it : goalstack = 1 subgoal (1 total)

`?x. &0 < a ==> &0 < x /\ x < a`

# e( EXISTS_TAC `a / &2`);;
val it : goalstack = 1 subgoal (1 total)

`&0 < a ==> &0 < a / &2 /\ a / &2 < a`

# e( ARITH_TAC );;
val it : goalstack = No subgoals