## 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.)

CLICK HERE to find out more related problems solutions.