Prove a theorem in an Isar style.
This macro is like defthm,
but instead of
See the community book
(defisar name formula :proof ... :disable ... :rule-classes ...)
Name of the theorem to prove.
This is the same as in defthm.
Formula of the theorem to prove.
This is the same as in defthm.
<hyp1>, ..., <hypn>be the hypotheses and conclbe the conclusion of the formula, defined as follows:
formulais not an implication, i.e. it does not have the form (implies ... ...), then nis 0 (i.e. there are no hypihypotheses) and conclis all of formula.
formulahas the form (implies hyps concl). In this case, conclis the conclusion of the implication. For the hypotheses, there are two cases.
hypsis not a conjunction, i.e. it does not have the form (and ...), then nis 1 (i.e. there is just one hypothesis) and <hyp1>is all of hyps.
hypshas the form (and <hyp1> ... <hypn>). In this case, <hyp1>, ..., <hypn>are the conjuncts.
Isar-style proof to prove the theorem.
It must be a non-empty list(cmd1 cmd2 ...)
of commands, where each command must be one of the following:
An assumption command of the form(:assume (<id> <fact>))
<id>is a keyword that names the fact proved by this command. <fact>is a formula that is the fact proved by this command. It must be one of <hyp1>, ..., <hypn>, or easily derivable from them in the empty ACL2 theory (i.e. minor, easily bridgeable differences are allowed); it may use variables introduced by preceding :letcommands.
This command serves to give a name to one of the theorem's hypotheses so that the fact (i.e. hypothesis) can be referenced in subsequent commands.
An abbreviation of the form(:let (<var> <term>))
<var>is an ACL2 variable symbol that must not occur in formulaand that must be distinct from all the ones introduced by other instances of the :letcommand in the proof. <term>is an ACL2 term, to which <varis bound. This binding is local to the proof, and can make the proof steps more concise and readable. See below for more details on the generated events.
A derivation command of the form(:derive (<id> <fact>) :from (<id1> <id2> ...) :hints <hints>) ; or other defrule options
<nameis a keyword that names the fact proved by this command. <fact>is a formula that is the fact proved by this command. It must be provable by ACL2 from the facts referenced in :from(see below) using the hints in :hints(see below). It may use variables introduced by preceding :letcommands. <id1>, <id2>, ... are names of previously proved facts (via :assumeor :derivecommands). If there are no names, the whole :from (...)may be omitted. <hints>are regular ACL2 hints, used to prove <fact>from the names facts. This may be omitted, just like in defthm. In addition, any of the defrule options may be used.
A proof-finishing command of the form(:qed)
It must be used when enough facts have been derived that, when put all together, suffice to prove the theorem's conclusion from the hypotheses without any additional hints. See below for more details on the generated events.
<id>fact names must be distinct.
There must be at most one
:qedcommand, and if there is one it must appear at the end. Its presence is necessary to complete the proof. However, while incrementally constructing the proof, it may be omitted and the defisarevent will still succeed, but it will not generate any permanent theorem (it will only check the commands present in the script).
Specifies if the theorem is disabled.
Specifies the rule classes of the theorem.
(defthm name<id> (let* ((<var1> <term1>) (<var2> <term2>) ...) (implies (and <hyp1> ... <hypn>) <fact>)) :rule-classes nil :hints (("Goal" :in-theory nil)))
where the let* bindings are from
(defrule name<id> (let* ((<var1> <term1>) (<var2> <term2>) ...) (implies (and <fact1> <fact2> ...) <fact>)) :rule-classes nil :hints <hints>) ; or other defrule options
(defthm name (implies (and <hyp1> ... <hypn>) <concl>) :hints (("Goal" :use <ids>)))