Re: [isabelle] [Noob] Proof on trees
In this case, I am especially also interested in knowing why the structured
proofs goes thorugh using just the simplifier
and the script fails to succeed. A lot of people in this list might be
able to give a sound explanation for it. I don't think it is related to the
use of induct_tac instead of induction, but I can't say much about it.
lemma "(dfs1 xs)@l = dfs2 xs l"
proof (induction xs arbitrary:l)
show ?case by simp
case (Node tr1 a tr2)
have "dfs1 (Node tr1 a tr2) @ l=((dfs1 tr1) @ (a# dfs1 tr2))@l" by
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
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
lemma " (dfs1 xs)@l = dfs2 xs l"
apply(induction xs arbitrary:l)
On Sat, May 28, 2016 at 1:19 PM, Rustom Mody <rustompmody at gmail.com> wrote:
> On Fri, May 27, 2016 at 1:46 AM, Alfio Martini <alfio.martini at acm.org>
> > Hi Rustom and Daniel,
> > This was my trial using a structured proof. It goes trough using just the
> > simplifier.
> Thanks Alfio and Daniel
> After learning about induction instead of induct_tac some other proofs that
> I was stuck with are not going through.
> But I really dont know what's happening :-)
> Can someone point me to references on the differences??
> Thanks again
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
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