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