# Re: [isabelle] Mistakes in Proving

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

`
`

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