Re: [isabelle] [Noob] Proof on trees



Alfio Martini wrote:
> Hi Daniel,
> ,
> I am especially also interested in knowing why the structured proofs goes
> thorugh using just the simplifier and the script fails to succeed.

When faced with proving

  "dfs1 (Node tr1 a tr2) @ xs = dfs2 (Node tr1 a tr2) xs"

the simplifier first unfolds the left-hand side to

  "(dfs1 tr1 @ a # dfs1 tr2) @ xs"

At this point, there are two possibilities:

a) use the induction hypothesis and rewrite that term further to

    "dfs2 tr1 (a # dfs1 tr2) @ xs"

  at which point the simplifier gets stuck; in fact it's hard to
  make progress from here because the xs is outside of the call
  "dfs2 tr1 ...", but the right-hand side will expand to
  "dfs2 tr1 (a # dfs2 tr2 xs)" with the xs inside of the
  "dfs2 tr1 ..." call.

b) use the associativity of append and its definition to obtain

    "dfs1 tr1 @ a # dfs1 tr2 @ xs"

  and only then apply the induction hypothesis which results in

    "dfs2 tr1 (a # dfs2 tr2 xs)"

Unfortunately, if the induction hypothesis is available for
simplification, the simplifier prefers a) and the proof fails.

The following works, but looks fragile:

  lemma "dfs1 tr @ xs = dfs2 tr xs"
  proof (induction tr arbitrary: xs)
    case Tip
    show ?case by simp
  next
    case (Node tr1 a tr2)
    show ?case
      apply simp
      apply (simp add: Node.IH)
    done
  qed

I would prove the symmetric version of the lemma which avoids these
complications:

  lemma dfs2_dfs1_conv: "dfs2 t xs = dfs1 t @ xs"
  by (induct t arbitrary: xs) auto

Cheers,

Bertram




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