Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Occur Check Problem in Isabelle

view this post on Zulip Email Gateway (Aug 18 2022 at 17:54):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Anja,

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?

  1. For the benefit of the readers who did not follow the thread on isabelle-dev, it would help if you could provide some context and explan what you want to achieve. People here are unlikely to finish your proofs for you, but they will gladly help with conceptual roadblocks.

  2. The formatting of your code got lost at some point. It now looks like this:

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

With code like this, you're unlikely to get a helpful answer.

  1. My general advice for learning Isabelle, which I've shared with your supervisor in an informal discussion earlier tonight (and he seemed not to disagree, but that could have been the wine), would be to tackle an easier problem than unification first and gain some experience and confidence doing that. Some people have observed that there's no learning curve when learning an interactive theorem prover, but rather a "series of steep cliffs". If the cliffs are steep, you can compensate by taking smaller strides.

I hope this helps.

Regards,

Jasmin

view this post on Zulip Email Gateway (Aug 18 2022 at 17:54):

From: Alexander Krauss <krauss@in.tum.de>
On 07/20/2011 11:41 PM, Jasmin Blanchette wrote:

  1. For the benefit of the readers who did not follow the thread on
    isabelle-dev, it would help if you could provide some context and
    explan what you want to achieve.
    [...]
  1. The formatting of your code got lost at some point.
    [...]
  1. My general advice for learning Isabelle, which I've shared with
    your supervisor in an informal discussion earlier tonight (and he
    seemed not to disagree, but that could have been the wine), would be
    to tackle an easier problem than unification first and gain some
    experience and confidence doing that.

Let me add:

  1. Please do not attempt to send your questions/followups off-list to
    individuals who responded previously. Instead, keep the mailing list on
    Cc. Keeping the discussion public is important, since

a) it ensures that others can learn from your problems/solutions,
b) it distributes the question answering workload over community members,
c) if questions are public (and permanently archived) they are often
better thought-out, and
d) it allows the assessment of how much of the work is actually your
own, which is important if the work is part of coursework or a thesis.

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 17:55):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Anja,

you might also have a look at IsaFoR at
http://cl-informatik.uibk.ac.at/software/ceta/

It contains several formalizations about terms and term rewriting, including a fully formalized unification algorithm for first order terms (theory Substitution.thy).

Cheers,
René

view this post on Zulip Email Gateway (Aug 18 2022 at 18:09):

From: Anja Gerbes <agerb@gmx.de>
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?

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

Last updated: Apr 26 2024 at 12:28 UTC