Re: [isabelle] Mistakes in Proving
On 13.10.2010 22:07, miramirkhani at ce.sharif.edu wrote:
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….”.
The simplifier can only make use of the third lemma if it can prove its
precondition to be true (to see why it cannot solve this, you can look
at the simplifier's trace). As the third lemma is not an equation, you
are better off using it as an introduction rule (using the rule method
or e.g. the intro: option of auto).
This archive was generated by a fusion of
Pipermail (Mailman edition) and