# [isabelle] Occur-Check Lemma and Unifikations-Algorithmus

```Good evening,

I am working with Isabelle, but in the following lemmas I cannot solve the problem. Can you tell me how I can complete the proof of the following lemma?

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"
apply (induct rule: trm.inducts)
apply (simp_all)
...
done

If I would find a solution, how could I prove this lemma in Isabelle, then I could continue working on this and expand the following Lemma:

lemma MGU_Var[intro]:
assumes no_occ: "\<not>occ (Var v) t"
shows "MGU [(v,t)] (Var v) t"
proof (intro MGUI exI)
show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
apply (cases "Var v = t")
apply (auto simp:subst_no_occ)
proof -
fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>"
then have "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>"
proof -
fix s  have "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th
apply (induct s)
apply (auto)
qed
qed
qed

Unfortunately I can not verify that my assumption is correct, because there must first be proved Lemma no_subst_occ for it. It would be very kind of you, if you could help me in this case.

For a better understanding of the unification algorithm and further lemma is stated that I was able to prove already. I can send it to you if you want it.

Greetings Anja

--
NEU: FreePhone - 0ct/min Handyspartarif mit Geld-zurück-Garantie!
Jetzt informieren: http://www.gmx.net/de/go/freephone

```

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