Prove a theorem in an Isar style.

This macro is like `defthm`,
but instead of

See the file

(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.Let

<hyp1> , ...,<hypn> be the hypotheses andconcl be the conclusion of the formula, defined as follows:

- If
formula is not an implication, i.e. it does not have the form(implies ... ...) , thenn is 0 (i.e. there are nohypi hypotheses) andconcl is all offormula .- Otherwise,
formula has the form(implies hyps concl) . In this case,concl is the conclusion of the implication. For the hypotheses, there are two cases.- If
hyps is not a conjunction, i.e. it does not have the form(and ...) , thenn is 1 (i.e. there is just one hypothesis) and<hyp1> is all ofhyps .- Otherwise,
hyps has 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>))where:

<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:let commands.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>))where:

<var> is an ACL2 variable symbol that must not occur informula and that must be distinct from all the ones introduced by other instances of the:let command in the proof.<term> is an ACL2 term, to which<var is 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 optionswhere:

<name 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 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:let commands.<id1> ,<id2> , ... are names of previously proved facts (via:assume or:derive commands). 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 indefthm. In addition, any of thedefruleoptions 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.

All the

<id> fact names must be distinct.There must be at most one

:qed command, 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 thedefisar event 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.

Each

(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
the

Each

(defrule name<id> (let* ((<var1> <term1>) (<var2> <term2>) ...) (implies (and <fact1> <fact2> ...) <fact>)) :rule-classes nil :hints <hints>) ; or other defrule options

where `let*` bindings are from
the

The

(defthm name (implies (and <hyp1> ... <hypn>) <concl>) :hints (("Goal" :use <ids>)))

where

The

- Defisar-implementation
- Implementation of
`defisar`.