*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Mistakes in Proving*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Thu, 14 Oct 2010 17:28:05 +0200*In-reply-to*: <39157.188.136.139.90.1287000445.squirrel@ce.sharif.edu>*References*: <39157.188.136.139.90.1287000445.squirrel@ce.sharif.edu>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.11) Gecko/20100805 Icedove/3.0.6

On 13.10.2010 22:07, miramirkhani at ce.sharif.edu wrote:

Dear All, I want to prove a simple theorem. The proof seems to be straightforward but I can’t figure out the mistakes I’m making. The first three lemmas bellow are proved and I want to prove the 4th lemma. P is a predicate and f,g,h and r are functions. 1. [iff] "P(x) -> f(x) \<in> g(x)" 2. [iff]"P(x)-> ( f(x) \<in> r(g((x)) )" 3. "y \<in> r(g(z)) => y \<in> h(w)" 4. "P(x) -> f(x) \<in> h(w)" I give the first two to the simplifier by using the iff attribute, then I add the 3rd lemma to the simplification rules and use the simp method but it fails and I get : “Empty result sequence….”.

**References**:**[isabelle] Mistakes in Proving***From:*miramirkhani

- Previous by Date: [isabelle] Infinite variable chasing
- Next by Date: Re: [isabelle] Infinite variable chasing
- Previous by Thread: Re: [isabelle] Mistakes in Proving
- Next by Thread: [isabelle] Infinite variable chasing
- Cl-isabelle-users October 2010 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