Email Gateway (Aug 19 2022 at 15:56): Email Gateway (Aug 19 2022 at 15:56):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Florian,
I will check your proposal. However, I was more confused by the first
premise of "successE" referring to "f" while afterwards the command is
sometimes referred to by "c". Shouldn't it be the same (either "f" or
"c") throughout the lemma?
lemma successE:
assumes "success f h"
obtains r h' where "execute f h = Some (r, h')"
using assms by (auto simp: success_def)
shouldn't that imply the other two equations?
cheers
chris
Email Gateway (Aug 19 2022 at 16:08):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Imperative HOLers,
Is the "c" in the following lemma (to be found in
~~/src/HOL/Imperative_HOL/Heap_Monad.thy") seems strange:
lemma successE:
assumes "success f h"
obtains r h' where "r = fst (the (execute c h))"
and "h' = snd (the (execute c h))"
and "execute f h ≠ None"
using assms by (simp add: success_def)
cheers
chris
Email Gateway (Aug 19 2022 at 16:08):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
Is the "c" in the following lemma (to be found in
~~/src/HOL/Imperative_HOL/Heap_Monad.thy") seems strange:lemma successE:
assumes "success f h"
obtains r h' where "r = fst (the (execute c h))"
and "h' = snd (the (execute c h))"
and "execute f h ≠ None"
using assms by (simp add: success_def)
Strange, indeed, particularly since the first two obtained claused are
essentially definitional tautologies.
Maybe this would suite better:
lemma successE:
assumes "success f h"
obtains r h' where "r = fst (the (execute c h))"
and "h' = snd (the (execute c h))"
and "execute f h = Some (r, h')"
using assms by (simp add: success_def)
There are actually some proofs using successE. How do they perform with
this lemma definition changed?
Florian
cheers
chris
Last updated: Apr 25 2024 at 16:19 UTC