theorem or_not: all P:bool, Q:bool.
if (P or Q) and not P
then Q
proof
arbitrary P:bool, Q:bool
suppose prem
cases conjunct 0 of prem
case p {
conclude false by apply (conjunct 1 of prem) to p
}
case q {
q
}
end
theorem ex_mid: all b:bool. b or not b
proof
arbitrary b:bool
switch b {
case true { . }
case false { . }
}
end
theorem or_sym: all P:bool, Q:bool. (P or Q) = (Q or P)
proof
arbitrary P:bool, Q:bool
switch P {
case true { . }
case false { . }
}
end
theorem and_sym: all P:bool, Q:bool. (P and Q) = (Q and P)
proof
arbitrary P:bool, Q:bool
switch P {
case true { . }
case false { . }
}
end
theorem eq_true: all P:bool. P ⇔ (P = true)
proof
arbitrary P:bool
switch P {
case true { . }
case false { . }
}
end
theorem eq_false: all P:bool. not P ⇔ P = false
proof
arbitrary P:bool
switch P {
case true { . }
case false { . }
}
end
theorem iff_equal: all P:bool, Q:bool.
if (P ⇔ Q)
then P = Q
proof
arbitrary P:bool, Q:bool
switch P {
case true {
suppose q
rewrite (apply eq_true to q)
}
case false {
suppose not_q
rewrite (apply eq_false to not_q)
}
}
end
theorem iff_symm: all P:bool, Q:bool.
if (P ⇔ Q) then (Q ⇔ P)
proof
arbitrary P:bool, Q:bool
assume: P ⇔ Q
have fwd: if Q then P by assume: Q apply (recall P ⇔ Q) to (recall Q)
have bkwd: if P then Q by assume: P apply (recall P ⇔ Q) to (recall P)
fwd, bkwd
end
theorem iff_trans: all P:bool, Q:bool, R:bool.
if (P ⇔ Q) and (Q ⇔ R) then (P ⇔ R)
proof
arbitrary P:bool, Q:bool, R:bool
assume prem: (P ⇔ Q) and (Q ⇔ R)
have fwd: if P then R by {
assume: P
have: Q by apply prem to recall P
conclude R by apply prem to recall Q
}
have bkwd: if R then P by {
assume: R
have: Q by apply prem to recall R
conclude P by apply prem to recall Q
}
fwd, bkwd
end
theorem contrapositive: all P : bool, Q : bool.
if (if P then Q) and not Q then not P
proof
arbitrary P : bool, Q : bool
switch Q {
case true { . }
case false { . }
}
end
theorem double_neg: all P: bool.
(not (not P)) = P
proof
arbitrary P:bool
switch P {
case true {
evaluate
}
case false {
evaluate
}
}
end
fun xor(x : bool, y : bool) {
if x then not y
else y
}
theorem xor_true: all b:bool. xor(true, b) = not b
proof
arbitrary b:bool
switch b {
case true {
evaluate
}
case false {
evaluate
}
}
end
theorem xor_false: all b:bool. xor(false, b) = b
proof
arbitrary b:bool
switch b {
case true {
evaluate
}
case false {
evaluate
}
}
end
theorem xor_commute: all a:bool, b:bool. xor(a,b) = xor(b,a)
proof
arbitrary a:bool, b:bool
switch a {
case true {
switch b {
case true {
evaluate
}
case false {
evaluate
}
}
}
case false {
switch b {
case true {
evaluate
}
case false {
evaluate
}
}
}
}
end