Re: [isabelle] [Noob] Proof on trees



Hi Rustom and Daniel,

This was my trial using a structured proof. It goes trough using just the
simplifier.

lemma "(dfs1 xs)@l  = dfs2 xs l"
   proof (induction xs arbitrary:l)
     case Tip
     show ?case by simp
  next
    case (Node tr1 a tr2)
    show ?case
      proof -
       have "dfs1 (Node tr1 a tr2) @ l=((dfs1 tr1) @ (a# dfs1 tr2))@l" by
simp
       also have "... = dfs1 tr1 @ ((a# dfs1 tr2)@l)" by simp
       also have "... = dfs1 tr1 @ (a # (dfs1 tr2 @l))" by simp
       also have "... = dfs1 tr1 @ (a # (dfs2 tr2 l))" using Node.IH by simp
       also have "... = dfs2 tr1 (a # (dfs2 tr2 l))" using Node.IH by simp
       also have "... = dfs2 (Node tr1 a tr2) l " by simp
       finally show ?case by this
      qed
  qed

On Thu, May 26, 2016 at 2:06 PM, Daniel Horne <d.horne at danielhorne.co.uk>
wrote:

> Played about with it a bit, and the following went through OK:
>
> lemma "(dfs1 xs)@list  = dfs2 xs list"
>  apply(induction xs arbitrary:list)
>  apply(auto)
> by (metis Cons_eq_appendI append_assoc)
>
>
> induction is a newer method than induct_tac, though I don't know the
> details. Once I'd changed that, sledgehammer came up with the.."by (metis
> Cons_eq_appendI append_assoc)"
>
>
> --
> DH
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil



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