[isabelle] Mistakes in Proving



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.