"returns_result h p r \<longleftrightarrow> (case h \<turnstile> p of Inr (r', _) \<Rightarrow> r = r' | Inl _ \<Rightarrow> False)"
fun select_result ("|(_)|\<^sub>r")
where
"select_result (Inr (r, _)) = r"
| "select_result (Inl _) = undefined"
lemma returns_result_eq [elim]: "h \<turnstile> f \<rightarrow>\<^sub>r y \<Longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>r y' \<Longrightarrow> y = y'"
"returns_result_heap h p r h' \<longleftrightarrow> (case h \<turnstile> p of Inr (r', h'') \<Rightarrow> r = r' \<and> h' = h'' | Inl _ \<Rightarrow> False)"
"h \<turnstile> f \<rightarrow>\<^sub>h h' \<Longrightarrow> pure f h \<Longrightarrow> h = h'"
by (meson pure_def is_OK_returns_heap_I returns_heap_eq)
lemma pure_eq_iff:
"(\<forall>h' x. h \<turnstile> f \<rightarrow>\<^sub>r x \<longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h' \<longrightarrow> h = h') \<longleftrightarrow> pure f h"
by(auto simp add: pure_def)
subsection \<open>Bind\<close>
lemma bind_assoc [simp]:
"((bind f g) \<bind> h) = (f \<bind> (\<lambda>x. (g x \<bind> h)))"
by(auto simp add: bind_def split: sum.splits)
lemma bind_returns_result_E:
assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y"
obtains x h' where "h \<turnstile> f \<rightarrow>\<^sub>r x" and "h \<turnstile> f \<rightarrow>\<^sub>h h'" and "h' \<turnstile> g x \<rightarrow>\<^sub>r y"
using assms by(auto simp add: bind_def returns_result_def returns_heap_def execute_def
split: sum.splits)
lemma bind_returns_result_E2:
assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y" and "pure f h"
obtains x where "h \<turnstile> f \<rightarrow>\<^sub>r x" and "h \<turnstile> g x \<rightarrow>\<^sub>r y"
using assms pure_returns_heap_eq bind_returns_result_E by metis
lemma bind_returns_result_E3:
assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y" and "h \<turnstile> f \<rightarrow>\<^sub>r x" and "pure f h"
shows "h \<turnstile> g x \<rightarrow>\<^sub>r y"
using assms returns_result_eq bind_returns_result_E2 by metis
lemma bind_returns_result_E4:
assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y" and "h \<turnstile> f \<rightarrow>\<^sub>r x"
obtains h' where "h \<turnstile> f \<rightarrow>\<^sub>h h'" and "h' \<turnstile> g x \<rightarrow>\<^sub>r y"
using assms returns_result_eq bind_returns_result_E by metis
lemma bind_returns_heap_E:
assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>h h''"
obtains x h' where "h \<turnstile> f \<rightarrow>\<^sub>r x" and "h \<turnstile> f \<rightarrow>\<^sub>h h'" and "h' \<turnstile> g x \<rightarrow>\<^sub>h h''"
using assms by(auto simp add: bind_def returns_result_def returns_heap_def execute_def
split: sum.splits)
lemma bind_returns_heap_E2 [elim]:
assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>h h'" and "pure f h"
obtains x where "h \<turnstile> f \<rightarrow>\<^sub>r x" and "h \<turnstile> g x \<rightarrow>\<^sub>h h'"
using assms pure_returns_heap_eq by (fastforce elim: bind_returns_heap_E)
lemma bind_returns_heap_E3 [elim]:
assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>h h'" and "h \<turnstile> f \<rightarrow>\<^sub>r x" and "pure f h"
shows "h \<turnstile> g x \<rightarrow>\<^sub>h h'"
using assms pure_returns_heap_eq returns_result_eq by (fastforce elim: bind_returns_heap_E)
lemma bind_returns_heap_E4:
assumes "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>h h''" and "h \<turnstile> f \<rightarrow>\<^sub>h h'"
obtains x where "h \<turnstile> f \<rightarrow>\<^sub>r x" and "h' \<turnstile> g x \<rightarrow>\<^sub>h h''"
using assms
by (metis bind_returns_heap_E returns_heap_eq)
lemma bind_returns_error_I [intro]:
assumes "h \<turnstile> f \<rightarrow>\<^sub>e e"
shows "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>e e"
assumes "pure f h" and "h \<turnstile> f \<rightarrow>\<^sub>r x" and "h \<turnstile> g x \<rightarrow>\<^sub>r y"
shows "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y"
using assms
by (meson bind_returns_result_I pure_def is_OK_returns_result_I)
lemma bind_pure_returns_result_I2 [intro]:
assumes "pure f h" and "h \<turnstile> ok f" and "\<And>x. h \<turnstile> f \<rightarrow>\<^sub>r x \<Longrightarrow> h \<turnstile> g x \<rightarrow>\<^sub>r y"
shows "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y"
using assms by auto
lemma bind_returns_heap_I [intro]:
assumes "h \<turnstile> f \<rightarrow>\<^sub>r x" and "h \<turnstile> f \<rightarrow>\<^sub>h h'" and "h' \<turnstile> g x \<rightarrow>\<^sub>h h''"
shows "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>h h''"
assumes "h \<turnstile> f \<rightarrow>\<^sub>h h'" and "\<And>x. h \<turnstile> f \<rightarrow>\<^sub>r x \<Longrightarrow> h' \<turnstile> g x \<rightarrow>\<^sub>h h''"
shows "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>h h''"
using assms
by (meson bind_returns_heap_I is_OK_returns_heap_I is_OK_returns_result_E)
lemma bind_is_OK_I [intro]:
assumes "h \<turnstile> f \<rightarrow>\<^sub>r x" and "h \<turnstile> f \<rightarrow>\<^sub>h h'" and "h' \<turnstile> ok (g x)"
shows "h \<turnstile> ok (f \<bind> g)"
by (meson assms(1) assms(2) assms(3) bind_returns_heap_I is_OK_returns_heap_E
is_OK_returns_heap_I)
lemma bind_is_OK_I2 [intro]:
assumes "h \<turnstile> ok f" and "\<And>x h'. h \<turnstile> f \<rightarrow>\<^sub>r x \<Longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h' \<Longrightarrow> h' \<turnstile> ok (g x)"
shows "h \<turnstile> ok (f \<bind> g)"
using assms by blast
lemma bind_is_OK_pure_I [intro]:
assumes "pure f h" and "h \<turnstile> ok f" and "\<And>x. h \<turnstile> f \<rightarrow>\<^sub>r x \<Longrightarrow> h \<turnstile> ok (g x)"
shows "h \<turnstile> ok (f \<bind> g)"
using assms by blast
lemma bind_pure_I:
assumes "pure f h" and "\<And>x. h \<turnstile> f \<rightarrow>\<^sub>r x \<Longrightarrow> pure (g x) h"
shows "pure (f \<bind> g) h"
using assms
by (metis bind_returns_heap_E2 pure_def pure_returns_heap_eq is_OK_returns_heap_E)
lemma pure_pure:
assumes "h \<turnstile> ok f" and "pure f h"
shows "h \<turnstile> f \<rightarrow>\<^sub>h h"
using assms returns_heap_eq
unfolding pure_def
by auto
lemma bind_returns_error_eq:
assumes "h \<turnstile> f \<rightarrow>\<^sub>e e"
fun map_M :: "('x \<Rightarrow> ('heap, 'e, 'result) prog) \<Rightarrow> 'x list \<Rightarrow> ('heap, 'e, 'result list) prog"
where
"map_M f [] = return []"
| "map_M f (x#xs) = do {
y \<leftarrow> f x;
ys \<leftarrow> map_M f xs;
return (y # ys)
}"
lemma map_M_ok_I [intro]:
"(\<And>x. x \<in> set xs \<Longrightarrow> h \<turnstile> ok (f x)) \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> pure (f x) h) \<Longrightarrow> h \<turnstile> ok (map_M f xs)"
apply(induct xs)
by (simp_all add: bind_is_OK_I2 bind_is_OK_pure_I)
lemma map_M_pure_I : "\<And>h. (\<And>x. x \<in> set xs \<Longrightarrow> pure (f x) h) \<Longrightarrow> pure (map_M f xs) h"
apply(induct xs)
apply(simp)
by(auto intro!: bind_pure_I)
lemma map_M_pure_E :
assumes "h \<turnstile> map_M g xs \<rightarrow>\<^sub>r ys" and "x \<in> set xs" and "\<And>x h. x \<in> set xs \<Longrightarrow> pure (g x) h"
obtains y where "h \<turnstile> g x \<rightarrow>\<^sub>r y" and "y \<in> set ys"
apply(insert assms, induct xs arbitrary: ys)
apply(simp)
apply(auto elim!: bind_returns_result_E)[1]
by (metis (full_types) pure_returns_heap_eq)
lemma map_M_pure_E2:
assumes "h \<turnstile> map_M g xs \<rightarrow>\<^sub>r ys" and "y \<in> set ys" and "\<And>x h. x \<in> set xs \<Longrightarrow> pure (g x) h"
obtains x where "h \<turnstile> g x \<rightarrow>\<^sub>r y" and "x \<in> set xs"
apply(insert assms, induct xs arbitrary: ys)
apply(simp)
apply(auto elim!: bind_returns_result_E)[1]
by (metis (full_types) pure_returns_heap_eq)
subsection \<open>Forall\<close>
fun forall_M :: "('y \<Rightarrow> ('heap, 'e, 'result) prog) \<Rightarrow> 'y list \<Rightarrow> ('heap, 'e, unit) prog"
"(\<And>x. x \<in> set xs \<Longrightarrow> h \<turnstile> ok (P x)) \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> pure (P x) h) \<Longrightarrow> h \<turnstile> ok (filter_M P xs)"
assumes "h \<turnstile> filter_M P xs \<rightarrow>\<^sub>r ys" and "\<And>h x. x \<in> set xs \<Longrightarrow> pure (P x) h" and "x \<in> set xs" and
and "\<forall>x \<in> set xs. h \<turnstile> P x \<rightarrow>\<^sub>r False"
shows "h \<turnstile> filter_M P xs \<rightarrow>\<^sub>r []"
using assms
apply(induct xs)
by(auto intro!: bind_pure_returns_result_I)
lemma filter_M_subset_2: "h \<turnstile> filter_M P xs \<rightarrow>\<^sub>r ys \<Longrightarrow> h' \<turnstile> filter_M P xs \<rightarrow>\<^sub>r ys'
\<Longrightarrow> (\<And>x. pure (P x) h) \<Longrightarrow> (\<And>x. pure (P x) h')
\<Longrightarrow> (\<forall>b. \<forall>x \<in> set xs. h \<turnstile> P x \<rightarrow>\<^sub>r True \<longrightarrow> h' \<turnstile> P x \<rightarrow>\<^sub>r b \<longrightarrow> b)
\<Longrightarrow> set ys \<subseteq> set ys'"
proof -
assume 1: "h \<turnstile> filter_M P xs \<rightarrow>\<^sub>r ys" and 2: "h' \<turnstile> filter_M P xs \<rightarrow>\<^sub>r ys'"
and 3: "(\<And>x. pure (P x) h)" and "(\<And>x. pure (P x) h')"
and 4: "\<forall>b. \<forall>x\<in>set xs. h \<turnstile> P x \<rightarrow>\<^sub>r True \<longrightarrow> h' \<turnstile> P x \<rightarrow>\<^sub>r b \<longrightarrow> b"
have h1: "\<forall>x \<in> set xs. h' \<turnstile> ok (P x)"
using 2 3 \<open>(\<And>x. pure (P x) h')\<close>
apply(induct xs arbitrary: ys')
by(auto elim!: bind_returns_result_E2)
then have 5: "\<forall>x\<in>set xs. h \<turnstile> P x \<rightarrow>\<^sub>r True \<longrightarrow> h' \<turnstile> P x \<rightarrow>\<^sub>r True"
using 4
apply(auto)[1]
by (metis is_OK_returns_result_E)
show ?thesis
using 1 2 3 5 \<open>(\<And>x. pure (P x) h')\<close>
lemma filter_M_filter: "h \<turnstile> filter_M P xs \<rightarrow>\<^sub>r ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> pure (P x) h)
\<Longrightarrow> (\<forall>x \<in> set xs. h \<turnstile> ok P x) \<and> ys = filter (\<lambda>x. |h \<turnstile> P x|\<^sub>r) xs"
apply(induct xs arbitrary: ys)
by(auto elim!: bind_returns_result_E2)
lemma filter_M_filter2: "(\<And>x. x \<in> set xs \<Longrightarrow> pure (P x) h \<and> h \<turnstile> ok P x)
\<Longrightarrow> filter (\<lambda>x. |h \<turnstile> P x|\<^sub>r) xs = ys \<Longrightarrow> h \<turnstile> filter_M P xs \<rightarrow>\<^sub>r ys"
\<Rightarrow> ('heap, 'e, 'y list) prog) f xs \<rightarrow>\<^sub>r ys" and "y \<in> set ys" and "\<And>x h. x \<in> set xs \<Longrightarrow> pure (f x) h"
obtains x where "h \<turnstile> f x \<rightarrow>\<^sub>r Some y" and "x \<in> set xs"
proof -
obtain ys_opts ys_no_opts where
ys_opts: "h \<turnstile> map_M f xs \<rightarrow>\<^sub>r ys_opts" and
have "\<forall>y \<in> set ys_no_opts. y \<noteq> None"
using ys_no_opts filter_M_holds_for_result
by fastforce
then have "Some y \<in> set ys_no_opts"
using map_M_pure_E2 ys \<open>y \<in> set ys\<close>
by (metis (no_types, lifting) option.collapse return_pure return_returns_result)
then have "Some y \<in> set ys_opts"
using filter_M_subset ys_no_opts by fastforce
then show "(\<And>x. h \<turnstile> f x \<rightarrow>\<^sub>r Some y \<Longrightarrow> x \<in> set xs \<Longrightarrow> thesis) \<Longrightarrow> thesis"
by (metis assms(3) map_M_pure_E2 ys_opts)
qed
subsection \<open>Iterate\<close>
fun iterate_M :: "('heap, 'e, 'result) prog list \<Rightarrow> ('heap, 'e, 'result) prog"
and g1 g2 :: "'result \<Rightarrow> ('heap, 'e, 'result2) prog"
assumes "h \<turnstile> f1 = h \<turnstile> f2"
and "\<And>y h'. h \<turnstile> f1 \<rightarrow>\<^sub>r y \<Longrightarrow> h \<turnstile> f1 \<rightarrow>\<^sub>h h' \<Longrightarrow> h' \<turnstile> g1 y = h' \<turnstile> g2 y"
and "\<And>x. h \<turnstile> f \<rightarrow>\<^sub>r x = h' \<turnstile> f \<rightarrow>\<^sub>r x"
and "\<And>x. h \<turnstile> f \<rightarrow>\<^sub>r x \<Longrightarrow> h \<turnstile> g x \<rightarrow>\<^sub>r y = h' \<turnstile> g x \<rightarrow>\<^sub>r y'"
shows "h \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y = h' \<turnstile> f \<bind> g \<rightarrow>\<^sub>r y'"
"preserved f h h' \<longleftrightarrow> (\<forall>x. h \<turnstile> f \<rightarrow>\<^sub>r x \<longleftrightarrow> h' \<turnstile> f \<rightarrow>\<^sub>r x)"
"reads S f h h' \<Longrightarrow> \<forall>P \<in> S' - S. reflp P \<and> transp P \<Longrightarrow> S \<subseteq> S' \<Longrightarrow> reads S' f h h'"
\<longleftrightarrow> (h \<turnstile> setter \<rightarrow>\<^sub>h h' \<longrightarrow> (\<exists>progs. set progs \<subseteq> S \<and> h \<turnstile> iterate_M progs \<rightarrow>\<^sub>h h'))"
lemma writes_singleton [simp]: "writes (all_args f) (f a) h h'"
apply(auto simp add: writes_def all_args_def)[1]
apply(rule exI[where x="[f a]"])
by(auto)
lemma writes_singleton2 [simp]: "writes {f} f h h'"
apply(auto simp add: writes_def all_args_def)[1]
apply(rule exI[where x="[f]"])
by(auto)
lemma writes_union_left_I:
assumes "writes S f h h'"
shows "writes (S \<union> S') f h h'"
using assms
by(auto simp add: writes_def)
lemma writes_union_right_I:
assumes "writes S' f h h'"
shows "writes (S \<union> S') f h h'"
using assms
by(auto simp add: writes_def)
lemma writes_union_minus_split:
assumes "writes (S - S2) f h h'"
and "writes (S' - S2) f h h'"
shows "writes ((S \<union> S') - S2) f h h'"
using assms
by(auto simp add: writes_def)
lemma writes_subset: "writes S f h h' \<Longrightarrow> S \<subseteq> S' \<Longrightarrow> writes S' f h h'"
by(auto simp add: writes_def)
lemma writes_error [simp]: "writes S (error e) h h'"
by(simp add: writes_def)
lemma writes_not_ok [simp]: "\<not>h \<turnstile> ok f \<Longrightarrow> writes S f h h'"
by(auto simp add: writes_def)
lemma writes_pure [simp]:
assumes "pure f h"
shows "writes S f h h'"
using assms
apply(auto simp add: writes_def)[1]
by (metis bot.extremum iterate_M.simps(1) list.set(1) pure_returns_heap_eq return_returns_heap)
lemma writes_bind:
assumes "\<And>h2. writes S f h h2"
assumes "\<And>x h2. h \<turnstile> f \<rightarrow>\<^sub>r x \<Longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h2 \<Longrightarrow> writes S (g x) h2 h'"