[isabelle-dev] Occur-Check Problem in Isabelle

[Anja Gerbes]

Good evening,

Lars has kindly helped me in setting up the lemma subst_no_occ. After
much reflection,
Ican 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?

Thank you in advance

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110716/6c6f7868/attachment-0002.html>