Email Gateway (Aug 18 2022 at 09:30): Email Gateway (Aug 18 2022 at 09:30):From: Temesghen Kahsai <lememta@gmail.com>
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?
Thanks.
-T
Email Gateway (Aug 18 2022 at 09:30):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: May 03 2024 at 04:19 UTC