<div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 16px; "><span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">Good evening</span><span title="Zur Anzeige alternativer Übersetzungen klicken">,</span><br>
<br><span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">Lars</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">has</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">kindly</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">helped me</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">in setting up the</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">lemma</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">subst_no_occ</span><span title="Zur Anzeige alternativer Übersetzungen klicken">.</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">After much</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">reflection, I</span><span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">can not prove</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">the lemma</span><span title="Zur Anzeige alternativer Übersetzungen klicken" class="">, however</span><span title="Zur Anzeige alternativer Übersetzungen klicken">.</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">Can you</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">tell</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">me how</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">I</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">should</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">do</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">in the proof</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">of the lemma</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">continues</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">to</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">Isabelle</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">runs through</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">here</span><span title="Zur Anzeige alternativer Übersetzungen klicken">?</span><br>
<br><span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">Thank you in advance</span><br><br><span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">Anja</span> <span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken">Gerbes</span></span></div>
<div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 16px; "><span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken"><br></span></span></div><div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 16px; "><span class="hps" title="Zur Anzeige alternativer Übersetzungen klicken"><br>
</span></span></div><div><br></div><div>datatype 'a trm = </div><div>    Var 'a </div><div>  | Fn 'a "('a trm) list"</div><div><br></div><div>types</div><div>  'a subst = "('a \<times> 'a trm) list"</div>

<div><br></div><div>text {* Applying a substitution to a variable: *}</div><div>fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"</div>

<div>where</div><div>  "assoc x d [] = d"</div><div>| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"</div><div><br></div><div>text {* Applying a substitution to a term: *}</div><div>primrec apply_subst_list :: "('a trm) list \<Rightarrow> 'a subst \<Rightarrow> ('a trm) list"  and</div>

<div>        apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60) where</div><div>  "apply_subst_list [] s = []"</div>

<div>| "apply_subst_list (x#xs) s = (apply_subst x s)#(apply_subst_list xs s)"</div><div>| "(Var v) \<triangleleft> s = assoc v (Var v) s"</div><div>| "(Fn f xs) \<triangleleft> s = (Fn f (apply_subst_list xs s))"</div>

<div><br></div><div>text {* Composition of substitutions: *}</div><div>fun compose :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)</div>

<div>where</div><div>  " [] \<bullet> bl = bl"</div><div>| "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"</div><div><br></div><div>text {* Equivalence of substitutions: *}</div>

<div>definition eqv (infix "=\<^sub>s" 50)</div><div>where</div><div>  "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" </div><div>

<br></div><div>text {* Occurs Check: *}</div><div><br></div><div>fun eq :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"</div><div>where</div><div> "eq x y = (if x = y then True else False)"</div>

<div><br></div><div>primrec occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" and</div><div>        occ_list :: "'a trm \<Rightarrow> 'a trm list \<Rightarrow> bool" where</div>

<div>  "occ u (Var v)     = False"</div><div>| "occ u (Fn f xs)   = (if (list_ex (eq u) xs) then True else (occ_list u xs))"</div><div>| "occ_list u []     = False"</div><div>| "occ_list u (x#xs) = (if occ u x then True else occ_list u xs)"</div>

<div><br></div><div>text {* Listenverarbeitung und Unifikationalgorithmus: *}</div><div>fun  unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option" and</div><div>     unify_list :: "'a trm list \<Rightarrow> 'a trm list \<Rightarrow> 'a subst option" where</div>

<div>  "unify u (Var v) = (if (occ (Var v) u) </div><div>                          then None</div><div>                          else Some [(v, u)])"</div><div>| "unify (Var v) u = (if (occ (Var v) u) </div>

<div>                          then None</div><div>                          else Some [(v, u)])"</div><div>| "unify (Fn f xs) (Fn g ys) = (if (f \<noteq> g) then None else unify_list xs ys)"</div><div>

| "unify_list [] [] = Some[]"</div><div>| "unify_list (x#xs) (y#ys) = (case unify x y of </div><div>                                   None \<Rightarrow> None </div><div>                                 | Some subst \<Rightarrow> case unify_list xs ys of</div>

<div>                                                     None \<Rightarrow> None</div><div>                                                   | Some subst' \<Rightarrow> Some (subst \<bullet> subst'))"</div>

<div>| "unify_list _ _ = None"</div><div> </div><div>subsection {* Specification: Most general unifiers *}</div><div><br></div><div>definition</div><div>  "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"</div>

<div><br></div><div>definition</div><div>  "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u </div><div>  \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"</div>

<div><br></div><div>lemma MGUI[intro]:</div><div>  "\<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></div>

<div>  \<Longrightarrow> MGU \<sigma> t u"</div><div>  by (simp only:Unifier_def MGU_def, auto)</div><div><br></div><div>lemma MGU_sym[sym]:</div><div>  "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"</div>

<div>  by (auto simp:MGU_def Unifier_def)</div><div><br></div><div>subsection {* Basic lemmas *}</div><div><br></div><div>lemma apply_empty[simp]: "t \<triangleleft> [] = t"</div><div>apply (induct t)</div>

<div>apply (simp)</div><div>apply (simp)</div><div>apply (simp)</div><div>apply (simp)</div><div>done </div><div><br></div><div>lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"</div>

<div>by (induct \<sigma>) auto</div><div><br></div><div>lemma assoc_compose[simp]:"assoc a (Var a) (s1 \<bullet> s2) = assoc a (Var a) s1 \<triangleleft> s2"</div><div>apply(induct_tac s1)</div>

<div>apply(simp)</div><div>apply(auto)</div><div>done</div><div><br></div><div>lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"</div>

<div>apply (induct t)</div><div>apply(simp)</div><div>apply(simp)</div><div>apply(simp)</div><div>apply(simp)</div><div>done</div><div><br></div><div>subsection {* Partial correctness *}</div><div><br></div><div>text {* Some lemmas about occ and MGU: *}</div>

<div><br></div><div>lemma subst_no_occ:</div><div> shows "\<not> occ (Var v) t</div><div>     \<Longrightarrow> Var v \<noteq> t</div><div>     \<Longrightarrow> t \<triangleleft> [(v,s)] = t"</div>

<div>   and "\<not> occ_list (Var v) ts</div><div>     \<Longrightarrow> (\<And>u. u \<in> set ts</div><div>       \<Longrightarrow> Var v \<noteq> u)</div><div>     \<Longrightarrow> apply_subst_list ts [(v,s)] = ts"</div>

<div>apply (induct rule: trm.inducts)</div><div>apply (simp_all)</div><div>...</div><div>done</div><div><br></div>