Performing Calculation in Interactive Theorem Proving

摘要

An LCF style tactic can be used to verify that the conclusion is a logical consequence of the premises, however, in mathematical practice, we often construct a conclusion in a proof step. This paper proposes a calculational style of tactic, and illustrates the characteristic and the realization issues of the tactics on the top of a theorem prover.