Search code examples
z3isabellesmthol

What does it mean for a fact used in Isabelle to have a number after the name?

Most of the proofs suggested by Sledgehammer use this notation of number inside of parentheses:

   by (smt (z3) ApplyAllResult.distinct(1)
            ApplyResult.case(1)
            ApplyResult.case(2)
            ApplyResult.exhaust
            applyInput.simps(1))

What does it mean for the fact to have such number?

Solution

  • Isabelle permits the use of fact lists indexed by a natural number starting with 1. Given a fact list fs and an index i, you can access an individual fact from the list by using the syntax fs(i). You can also select multiple facts from the list using multiple indexes (e.g., fs(1,3)), ranges (e.g. fs(2-5), fs(3-)) or a combination of both (e.g., fs(2,4-6)).

    Examples of predefined fact lists are assms (which contains the assumptions of a theorem) and f.simps (which contains the equations defining function f).