Email Gateway (Aug 18 2022 at 11:35): Email Gateway (Aug 18 2022 at 11:35):From: Jean Martina <Jean.Martina@cl.cam.ac.uk>
Actually I had the same problem to start understanding the method. But
as Larry told, it is everything in the JCS paper (page 19). Other
interesting reading is Giampaolo's thesis.
The basic idea is that you first get rid of the existential
quantification applying the introduction rules (this is basic theorem
proving strategy). This leaves you with two sub-goals.
The second you eliminate directly, because it is the empty trace. Just
give the inductive definition to the empty trace and voilà. To the other
sub-goal, as the name of the lemma proposes it is the possibility, so
you should give then the path to reach this possible state.
The 6 sub-goals produced, are basically the path construction to reach
the state in the lemma. The you just apply the possibility, it will lead
you to the proof by Isabelle's reasoner.
Jean
Lawrence Paulson escreveu:
Last updated: May 03 2024 at 12:27 UTC