*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Imperative HOL: typo?*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Fri, 26 Sep 2014 13:00:39 +0200*In-reply-to*: <54173706.7010209@informatik.tu-muenchen.de>*References*: <5416F46A.1090308@gmail.com> <54173706.7010209@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.1

Dear Florian,

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? Floriancheers chris

**References**:**[isabelle] Imperative HOL: typo?***From:*Christian Sternagel

**Re: [isabelle] Imperative HOL: typo?***From:*Florian Haftmann

- Previous by Date: [isabelle] CPP 2015: second call for papers
- Next by Date: Re: [isabelle] Malformed syntax error clears only on scroll to bottom
- Previous by Thread: Re: [isabelle] Imperative HOL: typo?
- Next by Thread: [isabelle] Is there a way to unfold an equality rule automatically
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list