[isabelle-dev] [isabelle] Imperative HOL: typo?

[Florian Haftmann]

Hi Christian,

since nobody else volunteers, I will take this up.

Thanks a lot!

	Florian

On 26.09.2014 14:12, Christian Sternagel wrote:
> I moved this thread from isabelle-users to isabelle-dev. (Please let me
> know in case this was the wrong call.)
> 
> Dear all,
> 
> I tried the variant of the lemma from my previous mail and the result is
> in the attached patch (created with "hg qnew"). For testing I ran
> 
> isabelle build -b HOL-Imperative_HOL
> 
> as well as
> 
> isabelle afp_build Separation_Logic_Imperative_HOL
> 
> as far as I can tell the only session in the AFP depending on
> Imperative_HOL.
> 
> I did not obtain any errors.
> 
> cheers
> 
> chris
> 
> On 09/26/2014 01:00 PM, Christian Sternagel wrote:
>> 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
>>>>
>>>
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141002/e46c44a3/attachment.asc>