[isabelle] Mistakes in Proving
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and