Re: [isabelle] Mistakes in Proving



On 13.10.2010 22:07, 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….”.

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 MHonArc.