Re: [isabelle] Imperative HOL: typo?



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

On 09/15/2014 08:59 PM, Florian Haftmann wrote:
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






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