bool(4)

/\の定義．

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 = (CONJUNCT1 th, CONJUNCT2 th)
CONJUNCTS th gives a list of theorems, one for each conjunct of the
          conclusion of th (no matter how they are associated)

# CONJ (ASSUME `p:bool`) (ASSUME `q:bool`);;
val it : thm = p, q |- p /\ q

\/ の定義

OR_DEF: `(\/) = \t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t`
DISJ1 `ASM |- a` `b` gives `ASM |- a \/ b`
DISJ2 `a` `ASM |- b` gives `ASM |- a \/ b`
DISJ_CASES `ASM1 |- a \/ b` `ASM2,a |- c` `ASM3,b |- c` gives
           `ASM1,ASM2,ASM3 |- c`
SIMPLE_DISJ_CASES `ASM1,a |- c` `ASM2,b |- c` gives
                  `ASM1,ASM2,a \/ b |- c` (a and b must be the first
                  hypotheses)

# SIMPLE_DISJ_CASES (ASSUME `p:bool`) (ASSUME `p:bool`);;
val it : thm = p \/ p |- p

# let thm1 = UNDISCH(REAL_RING `x = &1==> x * x = &1`)
  and thm2 = UNDISCH(REAL_RING `x = -- &1==> x * x = &1`);;
2 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
val thm1 : thm = x = &1 |- x * x = &1
val thm2 : thm = x = -- &1 |- x * x = &1

# SIMPLE_DISJ_CASES thm1 thm2;;
val it : thm = x = &1 \/ x = -- &1 |- x * x = &1