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