# 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
• 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.