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

CLICK HERE to find out more related problems solutions.

Leave a Comment

Your email address will not be published.

Scroll to Top