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
# 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"
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
