For pedagogical reasons I want to do elementary calculational proofs, without automation. Here is a silly example that works:
lemma calculation_silly: "(0::nat) * 3 = 3 * 0"
proof -
have "(0::nat) * 3 = 0" unfolding Nat.times_nat.mult_0 ..
also have "... = 0 * 0" unfolding Nat.times_nat.mult_0 ..
also have "... = 0" unfolding Nat.times_nat.mult_0 ..
also have "... = 3 * 0" unfolding Nat.mult_0_right ..
finally show ?thesis .
qed
but then if I prove this lemma:
lemma zero_one: "(0::nat) < 1"
proof -
have "0 < Suc 0" unfolding Nat.zero_less_Suc ..
also have "Suc 0 = 1" by (rule One_nat_def[symmetric])
finally show ?thesis .
qed
and trying to prove the base case of an inductive goal similarly:
lemma "(∑i=1..n::nat. (2*i - 1)) = n * n"
proof (induct n)
case 0
then show "(∑i = 1..0::nat. 2 * i - 1) = 0 * 0"
proof -
have "(∑i = 1..0::nat. 2 * i - 1) = (∑i∈ {1..0::nat}. 2 * i - 1)" ..
also have "... = (∑ (i::nat)∈{}. 2*i-1)" unfolding atLeastatMost_empty[OF zero_one] ..
also have "... = (0::nat)" unfolding sum.empty ..
also have "... = (0::nat) * 0" unfolding Nat.mult_0_right ..
finally show ?thesis .
Isabelle "forgets" the original Left Hand Side of the chain. Why is this and how could I prevent this? I cannot finish the finally show ?thesis
by a dot as with the above two examples.
Ah that one I discovered live in front of students
also is not always chaining, it can also unfold
and this leads to such weird things
The also
command is very general and not very smart. It just applies trans
rules. And the trans
rule for equality just does substitutes the left-hand side with the right-hand side in the entire calculation (the calculation being the fact accumulated so far). If that calculation is an equation, it substitutes the left-hand side and the right-hand side.
The only way I know of to avoid this is to change the equation that you are proving to something that only applies to the right-hand side but not the left-hand side, e.g. by putting more context around it. Or by hiding the left-hand side underneath a define
.
Last updated: Jun 08 2025 at 08:25 UTC