/\の定義． AND_DEF: `(/\) = \t1 t2. (\f:bool->bool->bool. f t1 t2) = (\f. f T T)` CONJ `ASM1 |- a` `ASM2 |- b` gives `ASM1+ASM2 |- a /\ b` CONJUNCT1 `ASM |- a /\ b` gives `ASM1 |- a` CONJUNCT2 `ASM |- a /\ b` gives `ASM1 |- b` CONJ_PAIR th…

==>の定義． # 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…

Tの定義． T_DEF: `T = ((\x:bool. x) = (\x:bool. x))` TRUTH: `|- T` EQT_ELIM `ASM1 |- a = T` gives `ASM1 |- a` EQT_INTRO `ASM1 |- a` gives `ASM1 |- a = T` Fの定義． F_DEF: `F = !t:bool. t` NOT_DEF: `(~) = \t. t ==> F` NOT_ELIM `ASM |- ~a` g…

PINST tyin tmin th instantiates types in th according to tyin and terms according to tmin. # let th = MESON[] `(x:A = y) <=> (y = x)`;; ... val th : thm = |- x = y <=> y = x # PINST [`:num`,`:A`] [`2 + 2`,`x:A`; `4`,`y:A`] th;; val it : th…