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.firstname.lastname@example.org> <CAMy1mr_RZxnYBkjRHNBPK=aR7kKzq1RHc_LKCsZsYnvZkc_Ebw@mail.gmail.com>
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:126.96.36.199) Gecko/20110606 Icedove/3.1.10
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":
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and