Email Gateway (Aug 18 2022 at 19:25): Email Gateway (Aug 18 2022 at 19:25):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
I am a bit confused about using Isar on some simple inductions.
Suppose that I have a proof that is nearly automatic except that I need
to apply a single simplification first. Here's a small example:
theory EvenDouble
imports Main
begin
fun evenb :: "nat ⇒ bool" where
"evenb 0 = True" |
"evenb (Suc 0) = False" |
"evenb (Suc (Suc n)) = evenb n"
primrec double :: "nat ⇒ nat ⇒ nat" where
"double 0 y = y" |
"double (Suc x) y = double x (Suc (Suc y))"
lemma dd: "double (Suc x) y = Suc (Suc (double x y))"
by (induct x arbitrary: y) simp_all
theorem even_double: "evenb (double x 0)"
proof (induct x)
case (Suc x) thus ?case by (simp only: dd) simp
qed simp
end
I do not like the proof of even_double because the whole point is to show
the main critical step, and I feel like that is lost by just chaining a
couple of methods together. However, being a total noob, I cannot see
how to insert that intermediate simplification explicitly before showing
the ?case. In particular, everything that I put between "thus ?case" and
the "case" causes the induction hypothesis to be removed from my current
facts, and I do not want to remove facts; I just want to show that single
simplification and then use the facts later. How do I do this in Isar?
Email Gateway (Aug 18 2022 at 19:25):From: Brian Huffman <huffman@in.tum.de>
Instead of "by (simp only: dd) simp", try "unfolding dd by simp".
The "unfolding" command will do rewriting on the goal and in the
chained facts, but unlike "apply simp" it leaves the chained facts as
chained facts.
Email Gateway (Aug 18 2022 at 19:25):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
This works great. Thank you. Is there a place where I can read up on all
of these? Right now I am just going through the many tutorials.
Email Gateway (Aug 18 2022 at 19:26):From: Tobias Nipkow <nipkow@in.tum.de>
In general, if you want to show more steps of an equational proof, you can do so
via the "also/finally" elements:
theorem even_double: "evenb (double x 0)"
proof (induct x)
case (Suc x)
have "evenb (double (Suc x) 0) = evenb(Suc(Suc(double x 0)))"
by(simp only: dd)
also have "... = evenb(double x 0)" by(simp only: evenb.simps)
also have "... = True" by(simp add: Suc)
finally show ?case by simp
qed simp
Tobias
Email Gateway (Aug 18 2022 at 19:26):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Thank you! Having seen the also/finally elements, I was not sure how to
use them, and I guess I did not get the "..." part last time I tried them.
Last updated: Apr 30 2024 at 16:19 UTC