# [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.*