# [isabelle] Occur Check Problem in Isabelle

```Good evening,

I can not prove the lemma, however.
Can you tell me how I should do in the proof of the
lemma continues to Isabelle runs through here?

Anja Gerbes

datatype 'a trm =             Var 'a           | Fn 'a "('a
trm) list"
types          'a subst = "('a \<times> 'a trm) list"
text {* Applying a substitution to a variable: *}        fun assoc
:: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow>
'b"        where          "assoc x d [] = d"        | "assoc x d ((p,q)#t)
= (if x = p then q else assoc x d t)"
text {* Applying a substitution to a term: *}        primrec
apply_subst_list :: "('a trm) list \<Rightarrow> 'a subst \<Rightarrow> ('a
trm) list"  and                apply_subst :: "'a trm \<Rightarrow> 'a
subst  \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60) where
"apply_subst_list [] s = []"        | "apply_subst_list (x#xs) s =
(apply_subst x s)#(apply_subst_list xs s)"        | "(Var v)
\<triangleleft> s = assoc v (Var v) s"        | "(Fn f xs) \<triangleleft>
s = (Fn f (apply_subst_list xs s))"
text {* Composition of substitutions: *}        fun compose :: "'a
subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>"
80)        where          " [] \<bullet> bl = bl"        | "((a,b) # al)
\<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
text {* Equivalence of substitutions: *}        definition eqv
(infix "=\<^sub>s" 50)        where          "s1 =\<^sub>s s2 \<equiv>
\<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2"
text {* Occurs Check: *}
fun eq :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
where         "eq x y = (if x = y then True else False)"
primrec occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" and
occ_list :: "'a trm \<Rightarrow> 'a trm list
\<Rightarrow> bool" where          "occ u (Var v)     = False"        |
"occ u (Fn f xs)   = (if (list_ex (eq u) xs) then True else (occ_list u
xs))"        | "occ_list u []     = False"        | "occ_list u (x#xs) =
(if occ u x then True else occ_list u xs)"
text {* Listenverarbeitung und Unifikationalgorithmus: *}
fun  unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
and             unify_list :: "'a trm list \<Rightarrow> 'a trm list
\<Rightarrow> 'a subst option" where          "unify u (Var v) = (if (occ
(Var v) u)                                   then None
else Some [(v, u)])"        | "unify
(Var v) u = (if (occ (Var v) u)
then None                                  else Some
[(v, u)])"        | "unify (Fn f xs) (Fn g ys) = (if (f \<noteq> g) then
None else unify_list xs ys)"          | "unify_list [] [] = Some[]"
| "unify_list (x#xs) (y#ys) = (case unify x y of
None \<Rightarrow> None
| Some subst \<Rightarrow> case
unify_list xs ys of
None \<Rightarrow> None
| Some
subst' \<Rightarrow> Some (subst \<bullet> subst'))"        | "unify_list _
_ = None"                 subsection {* Specification: Most general
unifiers *}
definition          "Unifier \<sigma> t u \<equiv>
(t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
definition          "MGU \<sigma> t u  \<equiv> Unifier \<sigma> t
u \<and>  (\<forall>\<theta>. Unifier \<theta> t u
\<longrightarrow> (\<exists>\<gamma>. \<theta>  =\<^sub>s \<sigma>
\<bullet> \<gamma>))"
lemma MGUI[intro]:          "\<lbrakk>t  \<triangleleft> \<sigma>
= u \<triangleleft>  \<sigma>; \<And>\<theta>. t \<triangleleft>  \<theta>
= u \<triangleleft> \<theta>  \<Longrightarrow> \<exists>\<gamma>. \<theta>
=\<^sub>s \<sigma> \<bullet>  \<gamma>\<rbrakk>
\<Longrightarrow> MGU \<sigma> t u"          by (simp only:Unifier_def
MGU_def, auto)
lemma MGU_sym[sym]:          "MGU \<sigma> s t \<Longrightarrow>
MGU \<sigma> t s"          by (auto simp:MGU_def Unifier_def)
subsection {* Basic lemmas *}
lemma apply_empty[simp]: "t \<triangleleft> [] = t"        apply
(induct t)        apply (simp)        apply (simp)        apply (simp)
apply (simp)        done
lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
by (induct \<sigma>) auto
lemma assoc_compose[simp]:"assoc a (Var a) (s1 \<bullet> s2) =
assoc a (Var a) s1 \<triangleleft> s2"        apply(induct_tac s1)
apply(simp)        apply(auto)        done
lemma  apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) =
t \<triangleleft> s1 \<triangleleft> s2"        apply (induct t)
apply(simp)        apply(simp)        apply(simp)        apply(simp)
done
subsection {* Partial correctness *}
text {* Some lemmas about occ and MGU: *}
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
--
NEU: FreePhone - kostenlos mobil telefonieren!
Jetzt informieren: http://www.gmx.net/de/go/freephone

```

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