LK in HOL Light

■　前件の導入

# g`a==>b`;;
Warning: Free variables in goal: a, b
val it : goalstack = 1 subgoal (1 total)

`a ==> b`

# e(DISCH_THEN(fun t->ALL_TAC));;
val it : goalstack = 1 subgoal (1 total)

`b`

■　仮定の導入

# g`a==>b`;;
Warning: Free variables in goal: a, b
val it : goalstack = 1 subgoal (1 total)

`a ==> b`

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

0 [`a`]

`b`

# e(FIRST_X_ASSUM(fun t->ALL_TAC));;
val it : goalstack = 1 subgoal (1 total)

`b`

■　後件の導入

# g`a==>(b1\/b2)`;;
Warning: Free variables in goal: a, b1, b2
val it : goalstack = 1 subgoal (1 total)

`a ==> b1 \/ b2`

# e(DISCH_THEN(fun t->DISJ1_TAC THEN MP_TAC t));;
val it : goalstack = 1 subgoal (1 total)

`a ==> b1`

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

`a ==> b1 \/ b2`

# e(DISCH_THEN(fun t->DISJ2_TAC THEN MP_TAC t));;
val it : goalstack = 1 subgoal (1 total)

`a ==> b2`