bool(3)

==>の定義．

# IMP_DEF;;
val it : thm = |- (==>) = (\p q. p /\ q <=> p)

MP `ASM1 |- a ==> b` `ASM2 |- a` gives `ASM1+ASM2 |- b`
モーダス・ポーネンス．

# MP (ASSUME `p==>q`) (ASSUME `p:bool`);;
val it : thm = p, p ==> q |- q

DISCH `a` `ASM,a |- b` gives `ASM |- a ==> b`
DISCH_ALL repeats DISCH until there are no more hypotheses.
仮定から結論の含意の前件への移行

# DISCH_ALL it;;
val it : thm = |- (p ==> q) ==> p ==> q
# DISCH `p:bool` (ASSUME `p:bool`);;
val it : thm = |- p ==> p

UNDISCH `ASM |- a ==> b` gives `ASM,a |- b`
UNDISCH_ALL repeats UNDISCH until the conclusion is not an implication
結論の含意の前件から仮定への移行

# UNDISCH (ASSUME `p==>q==>r`);;
val it : thm = p, p ==> q ==> r |- q ==> r
# UNDISCH it;;
val it : thm = p, q, p ==> q ==> r |- r
# DISCH_ALL it;;
val it : thm = |- (p ==> q ==> r) ==> q ==> p ==> r
# UNDISCH_ALL it;;
val it : thm = p, q, p ==> q ==> r |- r

含意の推移律．
IMP_TRANS `ASM1 |- a ==> b` `ASM2 |- b ==> c` gives `ASM1+ASM2 |- a ==> c`

含意の反対称律．
IMP_ANTISYM_RULE `ASM1 |- a ==> b` `ASM2 |- b ==> a` gives `ASM1+ASM2 |- a = b`

同値の含意への分解．
EQ_IMP_RULE `ASM |- (a:bool) = b` gives (`ASM |- a ==> b`, `ASM |- b ==> a`)

仮定の導入．
ADD_ASSUM `a` `ASM |- b` gives `ASM,a |- b`

# ASSUME `p:bool`;;
val it : thm = p |- p
# ADD_ASSUM `q:bool` it;;
val it : thm = p, q |- p

let thm1 = UNDISCH (REAL_RING `x = &1 ==> x * x = &1`)
and thm2 = UNDISCH (REAL_RING `y = &0 ==> y * y = &0`);;
MP (ASSUME `x * x = &1 ==> y = &0`) thm1;;
PROVE_HYP it thm2;;

let LIMP_INTRO thm1 thm2 = PROVE_HYP (MP (ASSUME (mk_binop `==>` (concl(thm1)) (hd(hyp thm2)))) thm1) thm2;;

let RIMP_INTRO thm = DISCH (hd(hyp(thm))) thm ;;