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

• To: Anja Gerbes <anja.gerbes at googlemail.com>
• Subject: Re: [isabelle] [isabelle-dev] Occur-Check Problem in Isabelle
• From: Lars Noschinski <noschinl at in.tum.de>
• Date: Wed, 13 Jul 2011 22:47:19 +0200
• Cc: isabelle-users at cl.cam.ac.uk
• References: <CAMy1mr-2=54==MJRQtZUyeoXaRt8YLc9HJHsYzzbCKG_CPGT4A@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,

> bin Studenten an der Goethe-Uni in Frankfurt und beschäftige mich sehr
> stark mit dem Isabelle Beweis-System.

```
The usual language on the Isabelle mailing lists is english. Also, please note that this list is for discussions about the development _of_ Isabelle. Using (or developing _in_ Isabelle) is on-topic on the isabelle-users at cl.cam.ac.uk mailing list[1]. I'm redirecting your post there.
```
> Currently I am sitting at the following problem in Isabelle.
>
> In the lemma "subst_no_occ" I get no further, I strongly suspect that I
> am in the functions"apply_subst" and "occ" have overlooked something
> important and something gets lost in the proof.

> lemma subst_no_occ: "\neg occ (Var v) t \Longrightarrow Var v \neq t
>    \Longrightarrow t \triangleleft [(v,s)] = t"

You meant "\<not>" instead of "\<neg>" here, right?

> apply(induct t)
> apply(simp)
> apply(simp)
> apply(simp)
> apply(simp)
> done

```
Your example is incomplete, so it is hard to give useful advice. I tried to complete it as follows:
```
--------------
datatype 'a trm = Var 'a | Fn 'a "('a trm list)"
type_synonym 'a subst = "('a \<times> 'a trm) list"

abbreviation (input) eq where "eq x \<equiv> \<lambda> y. x = y"

```
fun assoc :: "'a \<Rightarrow> 'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" where
```  "assoc v d [] = d"
| "assoc v d ((u, t) # xs) = (if (v = u) then t else assoc v d xs)"
--------------

```
In this case, "apply (induct t)" introduces a new schematic variable into the goal, which is instantiated by the second "simp". The goals which remains after the 4th simp is actually unsolvable; quickcheck finds a counter example.
```
```
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.
```
-- Lars

[1]: https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users

```

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