Re: [isabelle] Help on ind_cases

On Tue, 18 Jul 2006, Temesghen Kahsai wrote:

> 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') "

This based on a misunderstanding of how to read goal states:
\<And> P'. (P |--> P')  ==> (P |--> P') means that for some 
arbitrary-but-fixed P' you may assume (P |--> P') and have to show
(P |--> P').

Written in Isar it becomes something like this:

  fix P'
  assume "(P  |-->  P')"
  show "(P  |-->  P')" sorry

This is the most basic proof decomposition form of Isar.  There is some
additional flexibility here, e.g. fixed variables can get any name, 
assumptions can be ignored, the whole problem may be generalized etc.


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