Methods

Logical reasoning

Introduction

Methods: intro | intros

Apply introduction rules, i.e. those declared [intro]. intros applies as many rules as it can before solving side conditions.

Elimination

Method: elim [args]

elim m will perform induction on term m using the appropriate elimination rule. The improper variant elim will eliminate the first term in the goal premises that it is able to.

Remark. In contrast to the usual Curry-Howard setting in which entire conditional statements are encoded in a type family, statements and proofs in Isabelle/Isar may contain premises in the context, such that the application of an elimination rule to a goal does not bind all instances of the term being eliminated. In such cases, in order to correctly perform pattern-matching or induction on a term t one would first need to convert the goal statement by pushing all context premises containing t into a Π-type so that the application of the elimination rule can correctly match all occurrences of t. The elim method automatically does this.

Side conditions

Global theory flag: declare [[solve_side_conds=<n>]]

Most methods will attempt to automatically solve ancilliary side conditions that arise, allowing the user to focus on proving the core goals in the argument. The solve_side_conds flag modifies this behavior according to the table below.

n	Behavior
2	Default; run full type-checking/inference.
1	Only solve type judgments t: T if t is fully elaborated and a fact t: T' is known, where T unifies with T'.
Any other	Do not attempt to solve side conditions.