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

[Christian Sternagel]

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
>>>
>>
-------------- next part --------------
# HG changeset patch
# Parent 126c353540fc081be30ce08a10c14f9d8da332f6
tuned Heap_Monad.successE

diff -r 126c353540fc -r 9a54096ae0af src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Fri Sep 26 09:58:35 2014 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Sep 26 14:05:14 2014 +0200
@@ -255,8 +255,7 @@
 lemma effect_nthE [effect_elims]:
   assumes "effect (nth a i) h h' r"
   obtains "i < length h a" "r = get h a ! i" "h' = h"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_upd [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -276,8 +275,7 @@
 lemma effect_updE [effect_elims]:
   assumes "effect (upd i v a) h h' r"
   obtains "r = a" "h' = update a i v h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_map_entry [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -298,8 +296,7 @@
 lemma effect_map_entryE [effect_elims]:
   assumes "effect (map_entry i f a) h h' r"
   obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_swap [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -320,8 +317,7 @@
 lemma effect_swapE [effect_elims]:
   assumes "effect (swap i x a) h h' r"
   obtains "r = get h a ! i" "h' = update a i x h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_freeze [execute_simps]:
   "execute (freeze a) h = Some (get h a, h)"
diff -r 126c353540fc -r 9a54096ae0af src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Sep 26 09:58:35 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Sep 26 14:05:14 2014 +0200
@@ -82,10 +82,8 @@
 
 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 \<noteq> None"
-  using assms by (simp add: success_def)
+  obtains r h' where "execute f h = Some (r, h')"
+  using assms by (auto simp: success_def)
 
 named_theorems success_intros "introduction rules for success"
 
@@ -266,11 +264,11 @@
 
 lemma execute_bind_success:
   "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
-  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
+  by (cases f h rule: Heap_cases) (auto elim: successE simp add: bind_def)
 
 lemma success_bind_executeI:
   "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
-  by (auto intro!: successI elim!: successE simp add: bind_def)
+  by (auto intro!: successI elim: successE simp add: bind_def)
 
 lemma success_bind_effectI [success_intros]:
   "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"