# Re: [isabelle] [isabelle-dev] Occur-Check Problem in Isabelle

*To*: Anja Gerbes <anja.gerbes at googlemail.com>, isabelle-users at cl.cam.ac.uk
*Subject*: Re: [isabelle] [isabelle-dev] Occur-Check Problem in Isabelle
*From*: Lars Noschinski <noschinl at in.tum.de>
*Date*: Wed, 13 Jul 2011 23:50:41 +0200
*In-reply-to*: <CAMy1mr_RZxnYBkjRHNBPK=aR7kKzq1RHc_LKCsZsYnvZkc_Ebw@mail.gmail.com>
*References*: <CAMy1mr-2=54==MJRQtZUyeoXaRt8YLc9HJHsYzzbCKG_CPGT4A@mail.gmail.com> <4E1E0410.2050402@in.tum.de> <CAMy1mr_RZxnYBkjRHNBPK=aR7kKzq1RHc_LKCsZsYnvZkc_Ebw@mail.gmail.com>
*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.17) Gecko/20110606 Icedove/3.1.10

Hi Anja,
On 13.07.2011 23:00, Anja Gerbes wrote:

thanks for the reply.
This problem was already known to me, so I've asked this question.

`You should have mentioned this in your question. It takes quite some
``time to identify a problem; in particular in someone's else theory.
`

The problem is here that the definition of trm (and apply_subst)
contain nested recursion and hence you need to do induction over
both apply_subst and apply_subst_list at the same time.

You can do simultaneous induction if you connect the goals by "and":
lemma subst_no_occ:
shows "\<not> occ (Var v) t
\<Longrightarrow> Var v \<noteq> t
\<Longrightarrow> t \<triangleleft> [(v,s)] = t"
and "\<not> occ_list (Var v) ts
\<Longrightarrow> (\<And>u. u \<in> set ts
\<Longrightarrow> Var v \<noteq> u)
\<Longrightarrow> apply_subst_list ts [(v,s)] = ts"
proof (induct rule: trm.inducts)
...
-- Lars

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