Re: [isabelle] Occur Check Problem in Isabelle

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.

3. 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.



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