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
unfolding the most elegant way. It also helps while writing the proofs. Internally, this is (mostly?) equivalent to using the
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
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.