# Expanding all definitions in Isabelle lemma

## My recommendation: `unfolding`

There is a special keyword `unfolding` for unpacking definitions at the start of proofs. For your example this would read:

``````unfolding b0_def b1_def by simp
``````

I consider `unfolding` the most elegant way. It also helps while writing the proofs. Internally, this is (mostly?) equivalent to using the `unfold`-method:

``````apply (unfold b0_def b1_def) by simp
``````

This will recursively (!) use the set of equalities you supply to rewrite the proof goal. (Due to the recursion, you should rather not supply a set of equalities that could generate cycles…)

## Alternative: Using the simplifier

In cases with possible loops, the simplifier might be able to reach a nice unfolding without running into these cycles, maybe by interleaving with other simplifications. In such cases, `by (simp add: b0_def b1_def)`, as you’ve suggested, is great!

## Alternative definition: Maybe it’s just an `abbreviation` (and no `definition`)?

If you find yourself unfolding a definition in every single instance, you could consider, using `abbreviation` instead of `definition`. Then, some Isabelle magic will do the packing/unpacking for you without further hints. `abbeviation` does only affect how the user communicates with Isabelle. It does not introduce new symbols at the object level, and consequently, there would be no `b1_def` facts and the like.

``````abbreviation b0 :: "nat⇒nat"
where "b0 n ≡ (n mod 2)"
``````

## Usually not recommended: Building something like an abbreviation using the simplifier

If you (for whatever reason) want to have a defined name at the object level, but unfold it in almost every instance, you can also feed the defining equality directly into the simplifier.

``````definition b0 :: "nat⇒nat"
where [simp]: "b0 n ≡ (n mod 2)"
``````

(Usually there should be little reason for the last option.)