# 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
*In-reply-to*: <CAMy1mr-2=54==MJRQtZUyeoXaRt8YLc9HJHsYzzbCKG_CPGT4A@mail.gmail.com>
*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.*