*To*: Anja Gerbes <agerb at gmx.de>*Subject*: Re: [isabelle] Occur Check Problem in Isabelle*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Wed, 20 Jul 2011 23:41:54 +0200*Cc*: "Dr. David Sabel" <sabel at ki.informatik.uni-frankfurt.de>, cl-isabelle-users ML <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <20110716204840.271970@gmx.net>*References*: <20110716204840.271970@gmx.net>

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. Regards, Jasmin

**Follow-Ups**:**Re: [isabelle] Occur Check Problem in Isabelle***From:*Alexander Krauss

**References**:**[isabelle] Occur Check Problem in Isabelle***From:*Anja Gerbes

- Previous by Date: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus
- Next by Date: Re: [isabelle] Occur Check Problem in Isabelle
- Previous by Thread: [isabelle] Occur Check Problem in Isabelle
- Next by Thread: Re: [isabelle] Occur Check Problem in Isabelle
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list