[isabelle-dev] [isabelle] Imperative HOL: typo?
Christian Sternagel
c.sternagel at gmail.com
Fri Sep 26 14:12:00 CEST 2014
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"
More information about the isabelle-dev
mailing list