*To*: Lukas Bulwahn <bulwahn at in.tum.de>*Subject*: Re: [isabelle] Mistakes in Proving*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Thu, 14 Oct 2010 14:38:51 +0300*Cc*: isabelle-users at cl.cam.ac.uk, miramirkhani at ce.sharif.edu*In-reply-to*: <4CB617E7.6050506@in.tum.de>*References*: <39157.188.136.139.90.1287000445.squirrel@ce.sharif.edu> <4CB617E7.6050506@in.tum.de>

Hello Najma, Lukas, It seems that Lukas' counter example is for a different problem than the original one. It is important what are constants and what are variables in the original lemmas of Najma. If P, f, g, r and h are constants, and all other are variables, than lemma 4 is provable using lemmas 2 and 3. consts f1 :: "'a => 'b" g1 :: "'a => 'b set" r1 :: "'b set => 'b set" h1 :: "'c => 'b set" P1 :: "'a => bool"; lemma B1: "P1(x) ==> ( f1(x) \<in> r1(g1((x)) ))"; sorry; lemma C1: "y \<in> r1(g1(z)) ==> y \<in> h1(w)"; sorry; lemma "P1(x) ==> f1(x) \<in> h1(w)" apply (rule C1); apply (rule B1); by simp; Automating this proof is a different problem that I don't know how to answer. Best regards, Viorel On Wed, 2010-10-13 at 22:34 +0200, Lukas Bulwahn wrote: > Hello Najma, > > > I copied your lemmas to Isabelle, corrected the syntax and used the > counterexample generators refute and nitpick (based on SAT solving > technology) to find an counterexample why the fourth does not follow > from the first three: > > lemma > assumes "P x --> f x \<in> g x" > assumes "P x --> f x \<in> r (g x)" > assumes "y \<in> r(g z) --> y \<in> h w" > shows "P x --> f x \<in> h w" > refute > nitpick[show_consts] > > Both tools output a model that show that you cannot derive the fourth > from the first three in general. > > refute says: > > *** Model found: *** > Size of types: 'a: 2, 'b: 1, 'c: 1 > w: c0 > h: {(c0, {(b0, False)})} > y: b0 > z: a0 > r: {({(b0, True)}, {(b0, True)}), ({(b0, False)}, {(b0, False)})} > f: {(a0, b0), (a1, b0)} > g: {(a0, {(b0, False)}), (a1, {(b0, True)})} > x: a1 > P: {(a0, False), (a1, True)} > > and nitpick says: > > Nitpick found a counterexample for card 'a = 2, card 'b = 2, and card 'c > = 2: > > Constants: > P = {a1, a2?} > f = (%x. _)(a1 := b1) > g = (%x. _)(a1 := {b1}, a2 := {}) > h = (%x. _)(c1 := {b2?}, c2 := ?) > r = (%x. _)({b1, b2} := ?, {b1} := {b1, b2?}, {b2} := ?, {} := {b1?}) > w = c1 > x = a1 > y = b2 > z = a2 > > But just try it yourself... > > > So in your case, you are either trying to prove something that does not > hold (the counterexample should give you a hint why not) or > the proof is really dependent on the definitions of the functions f, > g,h,r and predicate P. > > > I hope this helps. > > > Lukas > > On 10/13/2010 10:07 PM, 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….”. > > > > What’s wrong with my proof? > > > > Any hints would be of a great help to me > > > > -- > > Kind Regards > > Najma > > > > > > > > > > > > > > > > >

**Follow-Ups**:**Re: [isabelle] Mistakes in Proving***From:*Lars Noschinski

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

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

**Re: [isabelle] Mistakes in Proving***From:*Lukas Bulwahn

- Previous by Date: Re: [isabelle] Mistakes in Proving
- Next by Date: Re: [isabelle] Mistakes in Proving
- Previous by Thread: Re: [isabelle] Mistakes in Proving
- Next by Thread: Re: [isabelle] Mistakes in Proving
- 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