reference:assumption
This is an old revision of the document!
Table of Contents
assumption solves a subgoal if the consequent is (literally) contained in the set of assumptions.
Definition
[Theassumptionmethod] 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
reference/assumption.1307714534.txt.gz · Last modified: by 131.246.41.159