Re: [isabelle] Converting apply-style induction to Structured Isar



Quoting Søren Haagerup <shaagerup at gmail.com>:

Hello,

I have a hard time going from Apply-style induction proofs to the
Structured Isar-style.

In the apply-style case, the proof of "cata_uniq" is a mere 4 lines:
http://gawis.dk/misc/apply_sample.thy

In the structured style, I need to write much more:
http://gawis.dk/misc/structured_sample.thy

Is there a way to make a concise structured proof of this fact?

Well, you have to keep in mind that a 'good' Isar proof conveys more
information than an apply-script. In a 'good' Isar proof you should
be able to easily read off the proof idea. This means in practice
that an Isar proof is sometimes a bit more verbose.

However looking at your proof, I would formulate it as follows.

 lemma cata_uniq :
   assumes a: "cata c f b"
   shows "c as = catafunc f b as"
 proof (induct as)
   case (Singleton a)
   show "c (Singleton a) = catafunc f b (Singleton a)"
     using a by (simp add: catafunc_def cata_def)
 next
   case (Snoc as a)
   have hyp: "c as = catafunc f b as" by fact
have "c (Snoc as a) = c (app as (Singleton a))" by (simp only: cons_rewrite)
   also have "... = b (c as) (f a)"
using cata_helper(3)[OF a, of as "Singleton a"] cata_helper(2)[OF a, of a] by auto
   also have "... = b (catafunc f b as) (f a)" using hyp by auto
   finally show "c (Snoc as a) = catafunc f b (Snoc as a)"
     by simp
qed

1.) As suggested before, I fix the variables at the case-level. This gets rid of the explicit fix lines.

2.) Also often I start with a proof like yours (which contains forward and backward reasoning steps). If possible, I then reformulate these proofs to be completely forward proofs, which tend to be slightly shorter (you can save the lines about opening and closing subproofs).

3.) If you think that the Singleton-case is too trivial and should not be shown explicitly, you can 'hide' it by discharging it at the qed-statement, like this:


lemma cata_uniq :
 assumes a: "cata c f b"
 shows "c as = catafunc f b as"
proof (induct as)
  case (Snoc as a)
  have hyp: "c as = catafunc f b as" by fact
  have "c (Snoc as a) = c (app as (Singleton a))" by (simp only: cons_rewrite)
  also have "... = b (c as) (f a)"
using cata_helper(3)[OF a, of as "Singleton a"] cata_helper(2)[OF a, of a] by auto
  also have "... = b (catafunc f b as) (f a)" using hyp by auto
  finally show "c (Snoc as a) = catafunc f b (Snoc as a)"
    by simp
qed (simp add: a[unfolded cata_def])


OK, this is not as short as your apply-script and the two solutions,
but as said above the purpose of an Isar proof is not to be as concise as
an apply-script, but to easily read off the proof idea (your calculation).
This might mean in this case that the proof is a bit more verbose (but this
is not always the case).

I have a hard time going from Apply-style induction proofs to the
Structured Isar-style.

My experience is also that going from an apply script to an Isar proof
is not that easy. Fiddling with an apply script usually completely buries
the proof idea. Constructing then the corresponding Isar proof means that
one has to think again about what are the important steps in the proof are.
That can sometimes be non-obvious.

Hope this helps,
Christian







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.