LP, the Larch Prover -- Proofs of conditionals


Proofs of formulas involving the conditional operator if can be carried out using a simplified proof by cases. The commands
prove if t1 then t2 else t3 by if-method
prove (if t1 then t2 else t3) = t4 by if-method
direct LP to prove the conjectures by division into two cases, t1 and ~t1. LP substitutes new constants for the free variables of t1 in all terms ti to obtain terms ti'. In the first case, it assumes t1' as an additional hypothesis and attempts to prove t2' (or t2' = t4') as a subgoal. In the second case, it assumes t1' = false as an additional hypothesis and attempts to prove t3' (or t3' = t4'). The names of the hypotheses have the form <simpleId>IfHyp.<number>, where <simpleId> is the current value of the name-prefix setting.

The command resume by if-method directs LP to resume the proof of the current conjecture using this method. It is applicable only when the current conjecture has been reduced to a formula of the form if t1 then t2 else t3 or of the form (if t1 then t2 else t3) = t4, where t4 does not begin with if.