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



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.