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



Am Donnerstag, den 31.03.2011, 13:29 +0200 schrieb Søren Haagerup:
> 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

- Do not add catafunc_def, this is the wrong simp rule. The rules
  catafunc.simps are automatically added to the simpset by primrec.

  This also adds the rules for "app" to the simp set, which is the
  inverse of cata_rewrite, and hence when you add cata_rewrite without
  removing app.simps, like "simp add: cata_rewrite" the simplifier does
  not terminate. Instead use "simp add: cata_rewrite del: app.simps"

- You cata_helper lemma is always a good idea to add. Probably named
  added to the simplifier. However adding rules to the automatization
  needs some experience, but you should try to play with it. (they also 
  look like nice dest rules)

- The "case" command lets you specify the fixed variables no need to
  add "fix" and "assume".

- If you use "case" with the method "induct" the thesis is not 
  named ?thesis but ?case, the facts are named after the case name (look
at Isabelle / Show me / Facts) :

  proof (induct c)
    case (Cons1 a b c) then show ?case ...
  next
    case (Cons2 a b c) then show ?case ...
  qed

- In your structured cata_uniq you do not need the additional
    show "" proof -  ...  qed
  command.

- My solution would be:

  lemma cata_uniq:
    "cata c f b ==> c as = catafunc f b as"
  proof (induct as)
    case (Snoc as a)
    then have "c (app as (Singleton a)) = b (catafunc f b as) (f a)"
      by (simp_all add: cata_def del: app.simps)
    then show ?case
      by simp
  qed (simp add: cata_def)
    (** the method supplied to "qed" is applied to the remaining goals.
        Here it is the Singleton case. **)

- Another possible solution would be:

  lemma cata_uniq:
    "cata c f b ==> c as = catafunc f b as"
  proof (induct as)
    case (Snoc as a) then show ?case
      by (simp add: cata_def cons_rewrite del: app.simps) simp
  qed (simp add: cata_def)

This is shorted but probably not as readable and stable as the previous
proof.

The lines

      by (simp add: cata_def cons_rewrite del: app.simps)
         simp

are the same as

 proof (simp add: cata_def cons_rewrite del: app.simps)
 qed simp


Hope this helps,
  Johannes

> Is there a way to make a concise structured proof of this fact?
> 
> Best regards,
> Søren








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