Re: [isabelle] Imperative HOL: typo?



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
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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