[isabelle] Occur-Check Lemma and Unifikations-Algorithmus
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?
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)
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:
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)
fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>"
then have "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>"
fix s have "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th
apply (induct s)
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.
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