Re: [isabelle] [Noob] Proof on trees



Also, I had another look at doing it with induct_tac, as such:

lemma "â list .(dfs1 xs)@list  = dfs2 xs list"
 apply(induct_tac xs)
 apply(auto)
by (metis Cons_eq_appendI append_assoc)


As induct_tac doesn't have the "arbitrary" parameter, I had to specify that by putting the universal quantifier on it instead.

I've previously been cautioned against doing this, but it might help understand the difference.


--

DH



On28/05/2016 17:19, Rustom Mody wrote:

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
Rusi





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