Isabelle/HOL Support Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.

====== 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

Isabelle/HOL Support Wiki

User Tools

Site Tools

Page Tools