[isabelle] Help on ind_cases

Hi all,

In the middle of a proof, I have to proof the following:

 \<And> P'. (P  |-->  P')    ==>     \<exists>Q'. (Q  |--> Q')

where P P' Q and Q' are processes. I know that (P |--> P') is false , therefore the implication is true.
So i did like follows:

show "\<And> P'. (P  |-->  P')    ==>     \<exists>Q'. (Q  |--> Q')  "
by(ind_cases " P'. (P  |-->  P') ")

and the proof is correct. But on the list of the sub-goals compare the following:

\<And> P'. (P  |-->  P')  ==> (P  |-->  P')

which can be proven like this:
show "\<And> P'. (P  |-->  P')  ==> (P  |-->  P') "
by auto

But the problem is: this sub-goal is still present on the list of the sub-goals that has to be proven. I guess I'm doing a stupid error, but I couldn't figure it out where. Any advice?



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