CODEWITHSUNDEEP
expressionisabelle
TFuto
TFuto

Reputation: 1452

Expanding all definitions in Isabelle lemma

How can I tell Isabelle to expand all my definitions, please, because that way the proof is trivial? Unfortunately there is no default expansion or simplification happens, and basically I get back the original expression as the subgoal.

Example:

theory Test
  imports Main

begin
 
definition b0 :: "nat⇒nat"
  where "b0 n ≡ (n mod 2)"

definition b1 :: "nat⇒nat"
  where "b1 n ≡ (n div 2)"

lemma "(a::nat)≤3 ∧ (b::nat)≤3 ⟶
  2*(b1 a)+(b0 a)+2*(b1 b)+(b0 b) = a+b"
  apply auto
  oops

end

Respose before oops:

proof (prove)
goal (1 subgoal):
 1. a ≤ 3 ⟹
    b ≤ 3 ⟹ 2 * b1 a + b0 a + 2 * b1 b + b0 b = a + b

Upvotes: 1

Views: 597

Answers (2)

Ben Keks
Ben Keks

Reputation: 1071

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

Upvotes: 4

TFuto
TFuto

Reputation: 1452

Yes, I keep forgetting that definitions are not used in simplifications by default.

Adding the definitions explicitly to the simplification rules solves this problem:

lemma "(a::nat)≤3 ∧ (b::nat)≤3 ⟶
  2*(b1 a)+(b0 a)+2*(b1 b)+(b0 b) = a+b"
  by (simp add: b0_def b1_def)

This way the definitions (b0, b1) are correctly used.

Upvotes: 0

Related Questions