		Search-engine friendly clone of the ACL2 documentation.

Isar

Defisar

Prove a theorem in an Isar style.

Introduction

This macro is like defthm, but instead of :hints or :instructions, it accepts an Isar-style proof script. The script, starting with the hypotheses of the theorem's formula, derives intermediate facts, provable via ACL2's :hints mechanism, and eventually derives the conclusion of the theorem's formula, thus proving the theorem. It also provides the ability to introduce local variables to abbreviate terms and make the formulas more concise and readable.

See the community book kestrel/isar/defisar-tests.lisp for examples of use of this macro.

General Form

(defisar name
  formula
  :proof   ...
  :disable ...
  :rule-classes ...)

Inputs

name

Name of the theorem to prove.
This is the same as in defthm.

formula

Formula of the theorem to prove.
This is the same as in defthm.
Let <hyp1>, ..., <hypn> be the hypotheses and concl be the conclusion of the formula, defined as follows:
If formula is not an implication, i.e. it does not have the form (implies ... ...), then n is 0 (i.e. there are no hypi hypotheses) and concl is all of formula.
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 ...), then n is 1 (i.e. there is just one hypothesis) and <hyp1> is all of hyps.
Otherwise, hyps has the form (and <hyp1> ... <hypn>). In this case, <hyp1>, ..., <hypn> are the conjuncts.

:proof — no default

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 in formula 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 options
where:
<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 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.
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 the defisar event will still succeed, but it will not generate any permanent theorem (it will only check the commands present in the script).

:disable — default nil

Specifies if the theorem is disabled.

:rule-classes — default :rewrite

Specifies the rule classes of the theorem.

Generated Events

Each :assume command generates a 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 the :let commands that precede the :assume command.

Each :derive command generates a theorem

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

where <fact1>, <fact2>, ... are the facts named by <id1>, <id2>, ... in :from, and where the let* bindings are from the :let commands that precede the :derive command.

The :qed command generates a theorem

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

where <ids> is a list of all the names of the facts proved by the script before the :qed.

The :let command does not generate any events. It introduces abbreviations that may be used in subsequent commands.

Subtopics

Defisar-implementation: Implementation of defisar.