Isabelle/HOL Support Wiki

Site Tools

reference:assumption

Assumption

assumption solves a subgoal if the consequent is (literally) contained in the set of assumptions.

Definition

[The assumption method] proves a subgoal by finding a matching assumption.

(From “Isabelle/HOL – A Proof Assisstant for Higher-Order Logic”, Nipkow et al, 2009)

Example

Assume you have this goal in your proof state:

$\quad[|\ a \wedge b; c\ |] \Longrightarrow a \wedge b$

applying assumption now with

apply assumption

solves this goal.

Non-Example

The goal

$\quad[|\ a \wedge b; c\ |] \Longrightarrow a$

can not be solved by assumption as a is not included in the set of assumptions. You have to eliminate the $\wedge$ first.

Variants

• assumption+ applies as many assumption steps in sequence as possible