adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib/monads/trace: copy in definitions and rules from nondet 

This fills out the trace monad rule set by copying in as many
definitions and rules as possible from the nondet monad. Most of these
do not immediately work for the trace monad, see the next commit for the
required changes.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2023-08-24 15:25:01 +10:00 committed by Corey Lewis
parent 7999632872
commit d66ac95f44
12 changed files with 2363 additions and 66 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

343
lib/Monads/trace/Trace_Empty_Fail.thy Normal file
View File

@ -0,0 +1,343 @@
(*
* Copyright 2023, Proofcraft Pty Ltd
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
theory Trace_Empty_Fail
imports
Trace_Monad
WPSimp
begin
section \<open>Monads that are wellformed w.r.t. failure\<close>
text \<open>
Usually, well-formed monads constructed from the primitives in Nondet_Monad will have the following
property: if they return an empty set of results, they will have the failure flag set.\<close>
definition empty_fail :: "('s,'a) nondet_monad \<Rightarrow> bool" where
"empty_fail m \<equiv> \<forall>s. fst (m s) = {} \<longrightarrow> snd (m s)"
text \<open>Useful in forcing otherwise unknown executions to have the @{const empty_fail} property.\<close>
definition mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" where
"mk_ef S \<equiv> (fst S, fst S = {} \<or> snd S)"
subsection \<open>WPC setup\<close>
lemma wpc_helper_empty_fail_final:
"empty_fail f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (empty_fail f)"
by (clarsimp simp: wpc_helper_def)
wpc_setup "\<lambda>m. empty_fail m" wpc_helper_empty_fail_final
subsection \<open>@{const empty_fail} intro/dest rules\<close>
lemma empty_failI:
"(\<And>s. fst (m s) = {} \<Longrightarrow> snd (m s)) \<Longrightarrow> empty_fail m"
by (simp add: empty_fail_def)
lemma empty_failD:
"\<lbrakk> empty_fail m; fst (m s) = {} \<rbrakk> \<Longrightarrow> snd (m s)"
by (simp add: empty_fail_def)
lemma empty_fail_not_snd:
"\<lbrakk> \<not> snd (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (m s)"
by (fastforce simp: empty_fail_def)
lemmas empty_failD2 = empty_fail_not_snd[rotated]
lemma empty_failD3:
"\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {}"
by (drule(1) empty_failD2, clarsimp)
lemma empty_fail_bindD1:
"empty_fail (a >>= b) \<Longrightarrow> empty_fail a"
unfolding empty_fail_def bind_def
by (fastforce simp: split_def image_image)
subsection \<open>Wellformed monads\<close>
(*
Collect generic empty_fail lemmas here:
- naming convention is emtpy_fail_NAME.
- add lemmas with assumptions to [empty_fail_cond] set
- add lemmas without assumption to [empty_fail_term] set
*)
named_theorems empty_fail_term
named_theorems empty_fail_cond
lemma empty_fail_K_bind[empty_fail_cond]:
"empty_fail f \<Longrightarrow> empty_fail (K_bind f x)"
by simp
lemma empty_fail_fun_app[empty_fail_cond]:
"empty_fail (f x) \<Longrightarrow> empty_fail (f $ x)"
by simp
(* empty_fail as such does not need context, but empty_fail_select_f does, so we need to build
up context in other rules *)
lemma empty_fail_If[empty_fail_cond]:
"\<lbrakk> P \<Longrightarrow> empty_fail f; \<not>P \<Longrightarrow> empty_fail g \<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)"
by (simp split: if_split)
lemma empty_fail_If_applied[empty_fail_cond]:
"\<lbrakk> P \<Longrightarrow> empty_fail (f x); \<not>P \<Longrightarrow> empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail ((if P then f else g) x)"
by simp
lemma empty_fail_put[empty_fail_term]:
"empty_fail (put f)"
by (simp add: put_def empty_fail_def)
lemma empty_fail_modify[empty_fail_term]:
"empty_fail (modify f)"
by (simp add: empty_fail_def simpler_modify_def)
lemma empty_fail_gets[empty_fail_term]:
"empty_fail (gets f)"
by (simp add: empty_fail_def simpler_gets_def)
lemma empty_fail_select[empty_fail_cond]:
"S \<noteq> {} \<Longrightarrow> empty_fail (select S)"
by (simp add: empty_fail_def select_def)
lemma empty_fail_select_f[empty_fail_cond]:
assumes ef: "fst S = {} \<Longrightarrow> snd S"
shows "empty_fail (select_f S)"
by (fastforce simp add: empty_fail_def select_f_def intro: ef)
lemma empty_fail_bind[empty_fail_cond]:
"\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)"
by (fastforce simp: bind_def empty_fail_def split_def)
lemma empty_fail_return[empty_fail_term]:
"empty_fail (return x)"
by (simp add: empty_fail_def return_def)
lemma empty_fail_returnOk[empty_fail_term]:
"empty_fail (returnOk v)"
by (fastforce simp: returnOk_def empty_fail_term)
lemma empty_fail_throwError[empty_fail_term]:
"empty_fail (throwError v)"
by (fastforce simp: throwError_def empty_fail_term)
lemma empty_fail_lift[empty_fail_cond]:
"\<lbrakk> \<And>x. empty_fail (f x) \<rbrakk> \<Longrightarrow> empty_fail (lift f x)"
unfolding lift_def
by (auto simp: empty_fail_term split: sum.split)
lemma empty_fail_liftE[empty_fail_cond]:
"empty_fail f \<Longrightarrow> empty_fail (liftE f)"
by (simp add: liftE_def empty_fail_cond empty_fail_term)
lemma empty_fail_bindE[empty_fail_cond]:
"\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)"
by (simp add: bindE_def empty_fail_cond)
lemma empty_fail_mapM[empty_fail_cond]:
assumes m: "\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)"
shows "empty_fail (mapM m xs)"
using m
proof (induct xs)
case Nil
thus ?case by (simp add: mapM_def sequence_def empty_fail_term)
next
case Cons
have P: "\<And>m x xs. mapM m (x # xs) = (do y \<leftarrow> m x; ys \<leftarrow> (mapM m xs); return (y # ys) od)"
by (simp add: mapM_def sequence_def Let_def)
from Cons
show ?case by (simp add: P m empty_fail_cond empty_fail_term)
qed
lemma empty_fail_fail[empty_fail_term]:
"empty_fail fail"
by (simp add: fail_def empty_fail_def)
lemma empty_fail_assert[empty_fail_term]:
"empty_fail (assert P)"
unfolding assert_def by (simp add: empty_fail_term)
lemma empty_fail_assert_opt[empty_fail_term]:
"empty_fail (assert_opt x)"
by (simp add: assert_opt_def empty_fail_term split: option.splits)
lemma empty_fail_mk_ef[empty_fail_term]:
"empty_fail (mk_ef o m)"
by (simp add: empty_fail_def mk_ef_def)
lemma empty_fail_gets_the[empty_fail_term]:
"empty_fail (gets_the f)"
unfolding gets_the_def
by (simp add: empty_fail_cond empty_fail_term)
lemma empty_fail_gets_map[empty_fail_term]:
"empty_fail (gets_map f p)"
unfolding gets_map_def
by (simp add: empty_fail_term empty_fail_cond)
lemma empty_fail_whenEs[empty_fail_cond]:
"(P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (whenE P f)"
"(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unlessE P f)"
by (auto simp add: whenE_def unlessE_def empty_fail_term)
lemma empty_fail_assertE[empty_fail_term]:
"empty_fail (assertE P)"
by (simp add: assertE_def empty_fail_term)
lemma empty_fail_get[empty_fail_term]:
"empty_fail get"
by (simp add: empty_fail_def get_def)
lemma empty_fail_catch[empty_fail_cond]:
"\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)"
by (simp add: catch_def empty_fail_cond empty_fail_term split: sum.split)
lemma empty_fail_guard[empty_fail_term]:
"empty_fail (state_assert G)"
by (clarsimp simp: state_assert_def empty_fail_cond empty_fail_term)
lemma empty_fail_spec[empty_fail_term]:
"empty_fail (state_select F)"
by (clarsimp simp: state_select_def empty_fail_def)
lemma empty_fail_when[empty_fail_cond]:
"(P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x)"
unfolding when_def
by (simp add: empty_fail_term)
lemma empty_fail_unless[empty_fail_cond]:
"(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unless P f)"
unfolding unless_def
by (simp add: empty_fail_cond)
lemma empty_fail_liftM[empty_fail_cond]:
"empty_fail m \<Longrightarrow> empty_fail (liftM f m)"
unfolding liftM_def
by (fastforce simp: empty_fail_term empty_fail_cond)
lemma empty_fail_liftME[empty_fail_cond]:
"empty_fail m \<Longrightarrow> empty_fail (liftME f m)"
unfolding liftME_def
by (simp add: empty_fail_term empty_fail_cond)
lemma empty_fail_handleE[empty_fail_cond]:
"\<lbrakk> empty_fail L; \<And>r. empty_fail (R r) \<rbrakk> \<Longrightarrow> empty_fail (L <handle> R)"
by (clarsimp simp: handleE_def handleE'_def empty_fail_term empty_fail_cond split: sum.splits)
lemma empty_fail_handle'[empty_fail_cond]:
"\<lbrakk>empty_fail f; \<And>e. empty_fail (handler e)\<rbrakk> \<Longrightarrow> empty_fail (f <handle2> handler)"
unfolding handleE'_def
by (fastforce simp: empty_fail_term empty_fail_cond split: sum.splits)
lemma empty_fail_sequence[empty_fail_cond]:
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence ms)"
unfolding sequence_def
by (induct ms; simp add: empty_fail_term empty_fail_cond)
lemma empty_fail_sequence_x[empty_fail_cond]:
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence_x ms)"
unfolding sequence_x_def
by (induct ms; simp add: empty_fail_term empty_fail_cond)
lemma empty_fail_sequenceE[empty_fail_cond]:
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE ms)"
unfolding sequenceE_def
by (induct ms; simp add: empty_fail_term empty_fail_cond)
lemma empty_fail_sequenceE_x[empty_fail_cond]:
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE_x ms)"
unfolding sequenceE_x_def
by (induct ms; simp add: empty_fail_term empty_fail_cond)
lemma empty_fail_mapM_x[empty_fail_cond]:
"(\<And>m. m \<in> f ` set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapM_x f ms)"
unfolding mapM_x_def
by (fastforce intro: empty_fail_term empty_fail_cond)
lemma empty_fail_mapME[empty_fail_cond]:
"(\<And>m. m \<in> f ` set xs \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapME f xs)"
unfolding mapME_def
by (fastforce intro: empty_fail_term empty_fail_cond)
lemma empty_fail_mapME_x[empty_fail_cond]:
"(\<And>m'. m' \<in> f ` set xs \<Longrightarrow> empty_fail m') \<Longrightarrow> empty_fail (mapME_x f xs)"
unfolding mapME_x_def
by (fastforce intro: empty_fail_term empty_fail_cond)
lemma empty_fail_filterM[empty_fail_cond]:
"(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail (P m)) \<Longrightarrow> empty_fail (filterM P ms)"
by (induct ms; simp add: empty_fail_term empty_fail_cond)
lemma empty_fail_zipWithM_x[empty_fail_cond]:
"(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM_x f xs ys)"
unfolding zipWithM_x_def zipWith_def
by (fastforce intro: empty_fail_term empty_fail_cond)
lemma empty_fail_zipWithM[empty_fail_cond]:
"(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM f xs ys)"
unfolding zipWithM_def zipWith_def
by (fastforce intro: empty_fail_term empty_fail_cond)
lemma empty_fail_maybeM[empty_fail_cond]:
"\<forall>x. empty_fail (f x) \<Longrightarrow> empty_fail (maybeM f t)"
unfolding maybeM_def
by (fastforce intro: empty_fail_term split: option.splits)
lemma empty_fail_ifM[empty_fail_cond]:
"\<lbrakk> empty_fail P; empty_fail a; empty_fail b \<rbrakk> \<Longrightarrow> empty_fail (ifM P a b)"
by (simp add: ifM_def empty_fail_cond)
lemma empty_fail_ifME[empty_fail_cond]:
"\<lbrakk> empty_fail P; empty_fail a; empty_fail b \<rbrakk> \<Longrightarrow> empty_fail (ifME P a b)"
by (simp add: ifME_def empty_fail_cond)
lemma empty_fail_whenM[empty_fail_cond]:
"\<lbrakk> empty_fail P; empty_fail f \<rbrakk> \<Longrightarrow> empty_fail (whenM P f)"
by (simp add: whenM_def empty_fail_term empty_fail_cond)
lemma empty_fail_andM[empty_fail_cond]:
"\<lbrakk> empty_fail A; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (andM A B)"
by (simp add: andM_def empty_fail_term empty_fail_cond)
lemma empty_fail_orM[empty_fail_cond]:
"\<lbrakk> empty_fail A; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (orM A B)"
by (simp add: orM_def empty_fail_term empty_fail_cond)
lemma empty_fail_notM[empty_fail_cond]:
"empty_fail A \<Longrightarrow> empty_fail (notM A)"
by (simp add: notM_def empty_fail_term empty_fail_cond)
(* not everything [simp] by default, because side conditions can slow down simp a lot *)
lemmas empty_fail[wp, intro!] = empty_fail_term empty_fail_cond
lemmas [simp] = empty_fail_term
subsection \<open>Equations and legacy names\<close>
lemma empty_fail_select_eq[simp]:
"empty_fail (select V) = (V \<noteq> {})"
by (clarsimp simp: select_def empty_fail_def)
lemma empty_fail_liftM_eq[simp]:
"empty_fail (liftM f m) = empty_fail m"
unfolding liftM_def
by (fastforce dest: empty_fail_bindD1)
lemma empty_fail_liftE_eq[simp]:
"empty_fail (liftE f) = empty_fail f"
by (fastforce simp: liftE_def empty_fail_def bind_def)
lemma liftME_empty_fail_eq[simp]:
"empty_fail (liftME f m) = empty_fail m"
unfolding liftME_def
by (fastforce dest: empty_fail_bindD1 simp: bindE_def)
(* legacy name binding *)
lemmas empty_fail_error_bits = empty_fail_returnOk empty_fail_throwError empty_fail_liftE_eq
end

4
lib/Monads/trace/Trace_In_Monad.thy
View File

@ -54,6 +54,10 @@ lemma inl_whenE:
"((Inl x, s') \<in> mres (whenE P f s)) = (P \<and> (Inl x, s') \<in> mres (f s))"
by (auto simp add: in_whenE)
lemma inr_in_unlessE_throwError[termination_simp]:
"(Inr (), s') \<in> fst (unlessE P (throwError E) s) = (P \<and> s'=s)"
by (simp add: unlessE_def returnOk_def throwError_def return_def)
lemma in_fail:
"r \<in> mres (fail s) = False"
by (simp add: fail_def mres_def)

183
lib/Monads/trace/Trace_Lemmas.thy
View File

@ -30,17 +30,169 @@ lemma bind_apply_cong':
lemmas bind_apply_cong = bind_apply_cong'[rule_format, fundef_cong]
lemma bind_cong[fundef_cong]:
"\<lbrakk> f = f'; \<And>v s s'. (v, s') \<in> fst (f' s) \<Longrightarrow> g v s' = g' v s' \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'"
by (auto simp: bind_def Let_def split_def intro: rev_image_eqI)
lemma bindE_cong[fundef_cong]:
"\<lbrakk> M = M' ; \<And>v s s'. (Inr v, s') \<in> fst (M' s) \<Longrightarrow> N v s' = N' v s' \<rbrakk> \<Longrightarrow> bindE M N = bindE M' N'"
by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_cong)
lemma bindE_apply_cong[fundef_cong]:
"\<lbrakk> f s = f' s'; \<And>rv st. (Inr rv, st) \<in> fst (f' s') \<Longrightarrow> g rv st = g' rv st \<rbrakk>
\<Longrightarrow> (f >>=E g) s = (f' >>=E g') s'"
by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_apply_cong)
lemma K_bind_apply_cong[fundef_cong]:
"\<lbrakk> f st = f' st' \<rbrakk> \<Longrightarrow> K_bind f arg st = K_bind f' arg' st'"
by simp
lemma when_apply_cong[fundef_cong]:
"\<lbrakk> C = C'; s = s'; C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> when C m s = when C' m' s'"
by (simp add: when_def)
lemma unless_apply_cong[fundef_cong]:
"\<lbrakk> C = C'; s = s'; \<not> C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> unless C m s = unless C' m' s'"
by (simp add: when_def unless_def)
lemma whenE_apply_cong[fundef_cong]:
"\<lbrakk> C = C'; s = s'; C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> whenE C m s = whenE C' m' s'"
by (simp add: whenE_def)
lemma unlessE_apply_cong[fundef_cong]:
"\<lbrakk> C = C'; s = s'; \<not> C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> unlessE C m s = unlessE C' m' s'"
by (simp add: unlessE_def)
subsection \<open>Simplifying Monads\<close>
lemma nested_bind[simp]:
"do x <- do y <- f; return (g y) od; h x od = do y <- f; h (g y) od"
by (clarsimp simp: bind_def Let_def split_def return_def)
lemma bind_dummy_ret_val:
"do y \<leftarrow> a; b od = do a; b od"
by simp
lemma fail_update[iff]:
"fail (f s) = fail s"
by (simp add: fail_def)
lemma fail_bind[simp]:
"fail >>= f = fail"
by (simp add: bind_def fail_def)
lemma fail_bindE[simp]:
"fail >>=E f = fail"
by (simp add: bindE_def bind_def fail_def)
lemma assert_A_False[simp]:
"assert False = fail"
by (simp add: assert_def)
lemma assert_A_True[simp]:
"assert True = return ()"
by (simp add: assert_def)
lemma assert_False[simp]:
"assert False >>= f = fail"
by simp
lemma assert_True[simp]:
"assert True >>= f = f ()"
by simp
lemma assertE_False[simp]:
"assertE False >>=E f = fail"
by (simp add: assertE_def)
lemma assertE_True[simp]:
"assertE True >>=E f = f ()"
by (simp add: assertE_def)
lemma when_False_bind[simp]:
"when False g >>= f = f ()"
by (rule ext) (simp add: when_def bind_def return_def)
lemma when_True_bind[simp]:
"when True g >>= f = g >>= f"
by (simp add: when_def bind_def return_def)
lemma whenE_False_bind[simp]:
"whenE False g >>=E f = f ()"
by (simp add: whenE_def bindE_def returnOk_def lift_def)
lemma whenE_True_bind[simp]:
"whenE True g >>=E f = g >>=E f"
by (simp add: whenE_def bindE_def returnOk_def lift_def)
lemma when_True[simp]:
"when True X = X"
by (clarsimp simp: when_def)
lemma when_False[simp]:
"when False X = return ()"
by (clarsimp simp: when_def)
lemma unless_False[simp]:
"unless False X = X"
by (clarsimp simp: unless_def)
lemma unlessE_False[simp]:
"unlessE False f = f"
unfolding unlessE_def by fastforce
lemma unless_True[simp]:
"unless True X = return ()"
by (clarsimp simp: unless_def)
lemma unlessE_True[simp]:
"unlessE True f = returnOk ()"
unfolding unlessE_def by fastforce
lemma unlessE_whenE:
"unlessE P = whenE (\<not>P)"
by (rule ext) (simp add: unlessE_def whenE_def)
lemma unless_when:
"unless P = when (\<not>P)"
by (rule ext) (simp add: unless_def when_def)
lemma gets_to_return[simp]:
"gets (\<lambda>s. v) = return v"
by (clarsimp simp: gets_def put_def get_def bind_def return_def)
lemma assert_opt_Some:
"assert_opt (Some x) = return x"
by (simp add: assert_opt_def)
lemma assertE_liftE:
"assertE P = liftE (assert P)"
by (simp add: assertE_def assert_def liftE_def returnOk_def)
lemma liftE_handleE'[simp]:
"(liftE a <handle2> b) = liftE a"
by (clarsimp simp: liftE_def handleE'_def)
lemma liftE_handleE[simp]:
"(liftE a <handle> b) = liftE a"
unfolding handleE_def by simp
lemma alternative_bind:
"((a \<sqinter> b) >>= c) = ((a >>= c) \<sqinter> (b >>= c))"
by (fastforce simp add: alternative_def bind_def split_def)
lemma alternative_refl:
"(a \<sqinter> a) = a"
by (simp add: alternative_def)
lemma alternative_com:
"(f \<sqinter> g) = (g \<sqinter> f)"
by (auto simp: alternative_def)
lemma liftE_alternative:
"liftE (a \<sqinter> b) = (liftE a \<sqinter> liftE b)"
by (simp add: liftE_def alternative_bind)
subsection \<open>Lifting and Alternative Basic Definitions\<close>
@ -65,7 +217,7 @@ lemma liftM_id[simp]:
by (auto simp: liftM_def)
lemma liftM_bind:
"liftM t f >>= g = (f >>= (\<lambda>x. g (t x)))"
"liftM t f >>= g = f >>= (\<lambda>x. g (t x))"
by (simp add: liftM_def bind_assoc)
lemma gets_bind_ign:
@ -86,4 +238,33 @@ lemma bind_eqI:
"\<lbrakk> f = f'; \<And>x. g x = g' x \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'"
by (auto simp: bind_def split_def)
lemma condition_split:
"P (condition C a b s) \<longleftrightarrow> (C s \<longrightarrow> P (a s)) \<and> (\<not>C s \<longrightarrow> P (b s))"
by (clarsimp simp: condition_def)
lemma condition_split_asm:
"P (condition C a b s) \<longleftrightarrow> (\<not>(C s \<and> \<not> P (a s) \<or> \<not>C s \<and> \<not>P (b s)))"
by (clarsimp simp: condition_def)
lemmas condition_splits = condition_split condition_split_asm
lemma condition_true_triv[simp]:
"condition (\<lambda>_. True) A B = A"
by (fastforce split: condition_splits)
lemma condition_false_triv[simp]:
"condition (\<lambda>_. False) A B = B"
by (fastforce split: condition_splits)
lemma condition_true:
"P s \<Longrightarrow> condition P A B s = A s"
by (clarsimp simp: condition_def)
lemma condition_false:
"\<not> P s \<Longrightarrow> condition P A B s = B s"
by (clarsimp simp: condition_def)
lemmas arg_cong_bind = arg_cong2[where f=bind]
lemmas arg_cong_bind1 = arg_cong_bind[OF refl ext]
end

76
lib/Monads/trace/Trace_Monad.thy
View File

@ -46,6 +46,23 @@ text \<open>
pair of result and state when the computation did not fail.\<close>
type_synonym ('s, 'a) tmonad = "'s \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set"
text \<open>
Print the type @{typ "('s,'a) nondet_monad"} instead of its unwieldy expansion.
Needs an AST translation in code, because it needs to check that the state variable
@{typ 's} occurs twice. This comparison is not guaranteed to always work as expected
(AST instances might have different decoration), but it does seem to work here.\<close>
print_ast_translation \<open>
let
fun monad_tr _ [t1, Ast.Appl [Ast.Constant @{type_syntax prod},
Ast.Appl [Ast.Constant @{type_syntax set},
Ast.Appl [Ast.Constant @{type_syntax prod}, t2, t3]],
Ast.Constant @{type_syntax bool}]] =
if t3 = t1
then Ast.Appl [Ast.Constant @{type_syntax "nondet_monad"}, t1, t2]
else raise Match
in [(@{type_syntax "fun"}, monad_tr)] end
\<close>
text \<open>Returns monad results, ignoring failures and traces.\<close>
definition mres :: "((tmid \<times> 's) list \<times> ('s, 'a) tmres) set \<Rightarrow> ('a \<times> 's) set" where
"mres r = Result -` (snd ` r)"
@ -124,6 +141,12 @@ text \<open>
FIXME: The @{text select_f} function was left out here until we figure
out what variant we actually need.\<close>
text \<open>@{text select_state} takes a relationship between
states, and outputs nondeterministically a state
related to the input state.\<close>
definition state_select :: "('s \<times> 's) set \<Rightarrow> ('s, unit) nondet_monad" where
"state_select r \<equiv> \<lambda>s. ((\<lambda>x. ((), x)) ` {s'. (s, s') \<in> r}, \<not> (\<exists>s'. (s, s') \<in> r))"
subsection "Failure"
text \<open>
@ -185,6 +208,13 @@ text \<open>
definition gets_the :: "('s \<Rightarrow> 'a option) \<Rightarrow> ('s, 'a) tmonad" where
"gets_the f \<equiv> gets f >>= assert_opt"
text \<open>
Get a map (such as a heap) from the current state and apply an argument to the map.
Fail if the map returns @{const None}, otherwise return the value.\<close>
definition
gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) nondet_monad" where
"gets_map f p \<equiv> gets f >>= (\<lambda>m. assert_opt (m p))"
subsection \<open>The Monad Laws\<close>
@ -490,6 +520,10 @@ text \<open>The same for the exception monad:\<close>
definition liftME :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'e+'a) tmonad \<Rightarrow> ('s,'e+'b) tmonad" where
"liftME f m \<equiv> doE x \<leftarrow> m; returnOk (f x) odE"
text \<open> Execute @{term f} for @{term "Some x"}, otherwise do nothing. \<close>
definition maybeM :: "('a \<Rightarrow> ('s, unit) nondet_monad) \<Rightarrow> 'a option \<Rightarrow> ('s, unit) nondet_monad" where
"maybeM f y \<equiv> case y of Some x \<Rightarrow> f x | None \<Rightarrow> return ()"
text \<open>Run a sequence of monads from left to right, ignoring return values.\<close>
definition sequence_x :: "('s, 'a) tmonad list \<Rightarrow> ('s, unit) tmonad" where
"sequence_x xs \<equiv> foldr (\<lambda>x y. x >>= (\<lambda>_. y)) xs (return ())"
@ -678,6 +712,48 @@ definition whileLoopE ::
notation (output)
whileLoopE ("(whileLoopE (_)// (_))" [1000, 1000] 1000)
section "Combinators that have conditions with side effects"
definition notM :: "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
"notM m = do c \<leftarrow> m; return (\<not> c) od"
definition
whileM :: "('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, unit) nondet_monad" where
"whileM C B \<equiv> do
c \<leftarrow> C;
whileLoop (\<lambda>c s. c) (\<lambda>_. do B; C od) c;
return ()
od"
definition
ifM :: "('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow>
('s, 'a) nondet_monad" where
"ifM test t f = do
c \<leftarrow> test;
if c then t else f
od"
definition ifME ::
"('a, 'b + bool) nondet_monad \<Rightarrow> ('a, 'b + 'c) nondet_monad \<Rightarrow> ('a, 'b + 'c) nondet_monad
\<Rightarrow> ('a, 'b + 'c) nondet_monad" where
"ifME test t f = doE
c \<leftarrow> test;
if c then t else f
odE"
definition
whenM :: "('s, bool) nondet_monad \<Rightarrow> ('s, unit) nondet_monad \<Rightarrow> ('s, unit) nondet_monad" where
"whenM t m = ifM t m (return ())"
definition
orM :: "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
"orM a b = ifM a (return True) b"
definition
andM :: "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
"andM a b = ifM a b (return False)"
subsection "Await command"
text \<open>@{term "Await c f"} blocks the execution until @{term "c"} is true,

341
lib/Monads/trace/Trace_Monad_Equations.thy
View File

@ -10,11 +10,350 @@
theory Trace_Monad_Equations
imports
Trace_Lemmas
Trace_No_Fail
begin
lemmas assertE_assert = assertE_liftE
lemma assert_def2:
"assert v = assert_opt (if v then Some () else None)"
by (cases v; simp add: assert_def assert_opt_def)
lemma return_returnOk:
"return (Inr x) = returnOk x"
unfolding returnOk_def by simp
lemma exec_modify:
"(modify f >>= g) s = g () (f s)"
by (simp add: bind_def simpler_modify_def)
lemma bind_return_eq:
"(a >>= return) = (b >>= return) \<Longrightarrow> a = b"
apply (clarsimp simp:bind_def)
apply (rule ext)
apply (drule_tac x= x in fun_cong)
apply (auto simp:return_def split_def)
done
lemmas bind_then_eq = arg_cong2[where f=bind, OF _ refl]
lemma bindE_bind_linearise:
"((f >>=E g) >>= h) =
(f >>= case_sum (h o Inl) (\<lambda>rv. g rv >>= h))"
apply (simp add: bindE_def bind_assoc)
apply (rule ext, rule bind_apply_cong, rule refl)
apply (simp add: lift_def throwError_def split: sum.split)
done
lemma throwError_bind:
"(throwError e >>= f) = (f (Inl e))"
by (simp add: throwError_def)
lemma bind_bindE_assoc:
"((f >>= g) >>=E h)
= f >>= (\<lambda>rv. g rv >>=E h)"
by (simp add: bindE_def bind_assoc)
lemma returnOk_bind:
"returnOk v >>= f = (f (Inr v))"
by (simp add: returnOk_def)
lemma liftE_bind:
"(liftE m >>= m') = (m >>= (\<lambda>rv. m' (Inr rv)))"
by (simp add: liftE_def)
lemma catch_throwError: "catch (throwError ft) g = g ft"
by (simp add: catch_def throwError_bind)
lemma cart_singleton_image:
"S \<times> {s} = (\<lambda>v. (v, s)) ` S"
by auto
lemma liftE_bindE_handle:
"((liftE f >>=E (\<lambda>x. g x)) <handle> h)
= f >>= (\<lambda>x. g x <handle> h)"
by (simp add: liftE_bindE handleE_def handleE'_def
bind_assoc)
lemma catch_liftE:
"catch (liftE g) h = g"
by (simp add: catch_def liftE_def)
lemma catch_liftE_bindE:
"catch (liftE g >>=E (\<lambda>x. f x)) h = g >>= (\<lambda>x. catch (f x) h)"
by (simp add: liftE_bindE catch_def bind_assoc)
lemma returnOk_catch_bind:
"catch (returnOk v) h >>= g = g v"
by (simp add: returnOk_liftE catch_liftE)
lemma liftE_bindE_assoc:
"(liftE f >>=E g) >>= h = f >>= (\<lambda>x. g x >>= h)"
by (simp add: liftE_bindE bind_assoc)
lemma unlessE_throw_catch_If:
"catch (unlessE P (throwError e) >>=E f) g
= (if P then catch (f ()) g else g e)"
by (simp add: unlessE_def catch_throwError split: if_split)
lemma whenE_bindE_throwError_to_if:
"whenE P (throwError e) >>=E (\<lambda>_. b) = (if P then (throwError e) else b)"
unfolding whenE_def bindE_def
by (auto simp: Nondet_Monad.lift_def throwError_def returnOk_def)
lemma alternative_liftE_returnOk:
"(liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)"
by (simp add: liftE_def alternative_def returnOk_def bind_def return_def)
lemma gets_the_return:
"(return x = gets_the f) = (\<forall>s. f s = Some x)"
apply (subst fun_eq_iff)
apply (simp add: return_def gets_the_def exec_gets
assert_opt_def fail_def
split: option.split)
apply auto
done
lemma gets_the_returns:
"(return x = gets_the f) = (\<forall>s. f s = Some x)"
"(returnOk x = gets_the g) = (\<forall>s. g s = Some (Inr x))"
"(throwError x = gets_the h) = (\<forall>s. h s = Some (Inl x))"
by (simp_all add: returnOk_def throwError_def
gets_the_return)
lemma all_rv_choice_fn_eq_pred:
"\<lbrakk> \<And>rv. P rv \<Longrightarrow> \<exists>fn. f rv = g fn \<rbrakk> \<Longrightarrow> \<exists>fn. \<forall>rv. P rv \<longrightarrow> f rv = g (fn rv)"
apply (rule_tac x="\<lambda>rv. SOME h. f rv = g h" in exI)
apply (clarsimp split: if_split)
by (meson someI_ex)
lemma all_rv_choice_fn_eq:
"\<lbrakk> \<And>rv. \<exists>fn. f rv = g fn \<rbrakk>
\<Longrightarrow> \<exists>fn. f = (\<lambda>rv. g (fn rv))"
using all_rv_choice_fn_eq_pred[where f=f and g=g and P=\<top>]
by (simp add: fun_eq_iff)
lemma gets_the_eq_bind:
"\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk>
\<Longrightarrow> \<exists>fn. (f >>= g) = gets_the (fn o fn')"
apply (clarsimp dest!: all_rv_choice_fn_eq)
apply (rule_tac x="\<lambda>s. case (fn s) of None \<Rightarrow> None | Some v \<Rightarrow> fna v s" in exI)
apply (simp add: gets_the_def bind_assoc exec_gets
assert_opt_def fun_eq_iff
split: option.split)
done
lemma gets_the_eq_bindE:
"\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk>
\<Longrightarrow> \<exists>fn. (f >>=E g) = gets_the (fn o fn')"
apply (simp add: bindE_def)
apply (erule gets_the_eq_bind)
apply (simp add: lift_def gets_the_returns split: sum.split)
apply fastforce
done
lemma gets_the_fail:
"(fail = gets_the f) = (\<forall>s. f s = None)"
by (simp add: gets_the_def exec_gets assert_opt_def
fail_def return_def fun_eq_iff
split: option.split)
lemma gets_the_asserts:
"(fail = gets_the f) = (\<forall>s. f s = None)"
"(assert P = gets_the g) = (\<forall>s. g s = (if P then Some () else None))"
"(assertE P = gets_the h) = (\<forall>s. h s = (if P then Some (Inr ()) else None))"
by (simp add: assert_def assertE_def gets_the_fail gets_the_returns
split: if_split)+
lemma ex_const_function:
"\<exists>f. \<forall>s. f (f' s) = v"
by force
lemma gets_the_condsE:
"(\<exists>fn. whenE P f = gets_the (fn o fn'))
= (P \<longrightarrow> (\<exists>fn. f = gets_the (fn o fn')))"
"(\<exists>fn. unlessE P g = gets_the (fn o fn'))
= (\<not> P \<longrightarrow> (\<exists>fn. g = gets_the (fn o fn')))"
by (simp add: whenE_def unlessE_def gets_the_returns ex_const_function
split: if_split)+
lemma let_into_return:
"(let f = x in m f) = (do f \<leftarrow> return x; m f od)"
by simp
lemma liftME_return:
"liftME f (returnOk v) = returnOk (f v)"
by (simp add: liftME_def)
lemma fold_bindE_into_list_case:
"(doE v \<leftarrow> f; case_list (g v) (h v) x odE)
= (case_list (doE v \<leftarrow> f; g v odE) (\<lambda>x xs. doE v \<leftarrow> f; h v x xs odE) x)"
by (simp split: list.split)
lemma whenE_liftE:
"whenE P (liftE f) = liftE (when P f)"
by (simp add: whenE_def when_def returnOk_liftE)
lemma whenE_whenE_body:
"whenE P (throwError f) >>=E (\<lambda>_. whenE Q (throwError f) >>=E r) = whenE (P \<or> Q) (throwError f) >>=E r"
apply (cases P)
apply (simp add: whenE_def)
apply simp
done
lemma whenE_whenE_same:
"whenE P (throwError f) >>=E (\<lambda>_. whenE P (throwError g) >>=E r) = whenE P (throwError f) >>=E r"
apply (cases P)
apply (simp add: whenE_def)
apply simp
done
lemma maybe_fail_bind_fail:
"unless P fail >>= (\<lambda>_. fail) = fail"
"when P fail >>= (\<lambda>_. fail) = fail"
by (clarsimp simp: bind_def fail_def return_def
unless_def when_def)+
lemma select_singleton[simp]:
"select {x} = return x"
by (fastforce simp add: fun_eq_iff select_def return_def)
lemma return_modify:
"return () = modify id"
by (simp add: return_def simpler_modify_def)
lemma liftE_liftM_liftME:
"liftE (liftM f m) = liftME f (liftE m)"
by (simp add: liftE_liftM liftME_liftM liftM_def)
lemma bind_return_unit:
"f = (f >>= (\<lambda>x. return ()))"
by simp
lemma modify_id_return:
"modify id = return ()"
by (simp add: simpler_modify_def return_def)
lemma liftE_bind_return_bindE_returnOk:
"liftE (v >>= (\<lambda>rv. return (f rv)))
= (liftE v >>=E (\<lambda>rv. returnOk (f rv)))"
by (simp add: liftE_bindE, simp add: liftE_def returnOk_def)
lemma bind_eqI:
"g = g' \<Longrightarrow> f >>= g = f >>= g'" by simp
lemma unlessE_throwError_returnOk:
"(if P then returnOk v else throwError x)
= (unlessE P (throwError x) >>=E (\<lambda>_. returnOk v))"
by (cases P, simp_all add: unlessE_def)
lemma gets_the_bind_eq:
"\<lbrakk> f s = Some x; g x s = h s \<rbrakk>
\<Longrightarrow> (gets_the f >>= g) s = h s"
by (simp add: gets_the_def bind_assoc exec_gets assert_opt_def)
lemma zipWithM_x_modify:
"zipWithM_x (\<lambda>a b. modify (f a b)) as bs
= modify (\<lambda>s. foldl (\<lambda>s (a, b). f a b s) s (zip as bs))"
apply (simp add: zipWithM_x_def zipWith_def sequence_x_def)
apply (induct ("zip as bs"))
apply (simp add: simpler_modify_def return_def)
apply (rule ext)
apply (simp add: simpler_modify_def bind_def split_def)
done
lemma assert2:
"(do v1 \<leftarrow> assert P; v2 \<leftarrow> assert Q; c od)
= (do v \<leftarrow> assert (P \<and> Q); c od)"
by (simp add: assert_def split: if_split)
lemma assert_opt_def2:
"assert_opt v = (do assert (v \<noteq> None); return (the v) od)"
by (simp add: assert_opt_def split: option.split)
lemma gets_assert:
"(do v1 \<leftarrow> assert v; v2 \<leftarrow> gets f; c v1 v2 od)
= (do v2 \<leftarrow> gets f; v1 \<leftarrow> assert v; c v1 v2 od)"
by (simp add: simpler_gets_def return_def assert_def fail_def bind_def
split: if_split)
lemma modify_assert:
"(do v2 \<leftarrow> modify f; v1 \<leftarrow> assert v; c v1 od)
= (do v1 \<leftarrow> assert v; v2 \<leftarrow> modify f; c v1 od)"
by (simp add: simpler_modify_def return_def assert_def fail_def bind_def
split: if_split)
lemma gets_fold_into_modify:
"do x \<leftarrow> gets f; modify (g x) od = modify (\<lambda>s. g (f s) s)"
"do x \<leftarrow> gets f; _ \<leftarrow> modify (g x); h od
= do modify (\<lambda>s. g (f s) s); h od"
by (simp_all add: fun_eq_iff modify_def bind_assoc exec_gets
exec_get exec_put)
lemma bind_assoc2:
"(do x \<leftarrow> a; _ \<leftarrow> b; c x od) = (do x \<leftarrow> (do x' \<leftarrow> a; _ \<leftarrow> b; return x' od); c x od)"
by (simp add: bind_assoc)
lemma bind_assoc_return_reverse:
"do x \<leftarrow> f;
_ \<leftarrow> g x;
h x
od =
do x \<leftarrow> do x \<leftarrow> f;
_ \<leftarrow> g x;
return x
od;
h x
od"
by (simp only: bind_assoc return_bind)
lemma if_bind:
"(if P then (a >>= (\<lambda>_. b)) else return ()) =
(if P then a else return ()) >>= (\<lambda>_. if P then b else return ())"
by (cases P; simp)
lemma bind_liftE_distrib: "(liftE (A >>= (\<lambda>x. B x))) = (liftE A >>=E (\<lambda>x. liftE (\<lambda>s. B x s)))"
by (clarsimp simp: liftE_def bindE_def lift_def bind_assoc)
lemma if_catch_distrib:
"((if P then f else g) <catch> h) = (if P then f <catch> h else g <catch> h)"
by (simp split: if_split)
lemma will_throw_and_catch:
"f = throwError e \<Longrightarrow> (f <catch> (\<lambda>_. g)) = g"
by (simp add: catch_def throwError_def)
lemma catch_is_if:
"(doE x <- f; g x odE <catch> h) =
do
rv <- f;
if sum.isl rv then h (projl rv) else g (projr rv) <catch> h
od"
apply (simp add: bindE_def catch_def bind_assoc cong: if_cong)
apply (rule bind_cong, rule refl)
apply (clarsimp simp: Nondet_Monad.lift_def throwError_def split: sum.splits)
done
lemma liftE_K_bind: "liftE ((K_bind (\<lambda>s. A s)) x) = K_bind (liftE (\<lambda>s. A s)) x"
by clarsimp
lemma monad_eq_split_tail:
"\<lbrakk>f = g; a s = b s\<rbrakk> \<Longrightarrow> (a >>= f) s = ((b >>= g) s)"
by (simp add:bind_def)
lemma assert_opt_If:
"assert_opt v = If (v = None) fail (return (the v))"
by (simp add: assert_opt_def split: option.split)
lemma if_to_top_of_bind:
"(bind (If P x y) z) = If P (bind x z) (bind y z)"
by (simp split: if_split)
lemma if_to_top_of_bindE:
"(bindE (If P x y) z) = If P (bindE x z) (bindE y z)"
by (simp split: if_split)
lemma modify_id:
"modify id = return ()"
by (simp add: modify_def get_def bind_def put_def return_def)

807
lib/Monads/trace/Trace_More_VCG.thy
View File

@ -13,8 +13,815 @@ theory Trace_More_VCG
Trace_VCG
begin
lemma hoare_take_disjunct:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> (False \<or> P'' rv s)\<rbrace>
\<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>"
by (erule hoare_strengthen_post, simp)
lemma hoare_post_add:
"\<lbrace>P\<rbrace> S \<lbrace>\<lambda>r s. R r s \<and> Q r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>"
by (erule hoare_strengthen_post, simp)
lemma hoare_post_addE:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. R s \<and> Q s\<rbrace>, \<lbrace>T\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. Q s\<rbrace>, \<lbrace>T\<rbrace>"
by (erule hoare_post_impErr'; simp)
lemma hoare_pre_add:
"(\<forall>s. P s \<longrightarrow> R s) \<Longrightarrow> (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<longleftrightarrow> \<lbrace>P and R\<rbrace> f \<lbrace>Q\<rbrace>)"
apply (subst iff_conv_conj_imp)
by(intro conjI impI; rule hoare_weaken_pre, assumption, clarsimp)
lemma hoare_pre_addE:
"(\<forall>s. P s \<longrightarrow> R s) \<Longrightarrow> (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace> \<longleftrightarrow> \<lbrace>P and R\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>)"
apply (subst iff_conv_conj_imp)
by(intro conjI impI; rule hoare_weaken_preE, assumption, clarsimp)
lemma hoare_name_pre_state:
"\<lbrakk> \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
by (clarsimp simp: valid_def)
lemma hoare_name_pre_stateE:
"\<lbrakk>\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
by (clarsimp simp: validE_def2)
lemma valid_prove_more: (* FIXME: duplicate *)
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>"
by (rule hoare_post_add)
lemma hoare_vcg_if_lift:
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P then X rv s else Y rv s\<rbrace>"
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P then X rv else Y rv\<rbrace>"
by (auto simp: valid_def split_def)
lemma hoare_vcg_if_lift_strong:
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>P\<rbrace>; \<lbrace>\<lambda>s. \<not> P' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>R'\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. if P' s then Q' s else R' s\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then Q rv s else R rv s\<rbrace>"
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>P\<rbrace>; \<lbrace>\<lambda>s. \<not> P' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace> Q\<rbrace>; \<lbrace>R'\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. if P' s then Q' s else R' s\<rbrace> f \<lbrace>\<lambda>rv s. (if P rv s then Q rv else R rv) s\<rbrace>"
by (wpsimp wp: hoare_vcg_imp_lift' | assumption | fastforce)+
lemma hoare_vcg_imp_lift_pre_add:
"\<lbrakk> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. R rv s\<rbrace>; f \<lbrace>\<lambda>s. \<not> Q s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> R rv s\<rbrace>"
apply (rule hoare_weaken_pre)
apply (rule hoare_vcg_imp_lift')
apply fastforce
apply fastforce
apply (clarsimp simp: pred_conj_def valid_def)
done
lemma hoare_pre_tautI:
"\<lbrakk> \<lbrace>A and P\<rbrace> a \<lbrace>B\<rbrace>; \<lbrace>A and not P\<rbrace> a \<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace>"
by (fastforce simp: valid_def split_def pred_conj_def pred_neg_def)
lemma hoare_lift_Pf_pre_conj:
assumes P: "\<And>x. \<lbrace>\<lambda>s. Q x s\<rbrace> m \<lbrace>P x\<rbrace>"
assumes f: "\<And>P. \<lbrace>\<lambda>s. P (g s) \<and> R s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>"
shows "\<lbrace>\<lambda>s. Q (g s) s \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. P (f s) rv s\<rbrace>"
apply (clarsimp simp: valid_def)
apply (rule use_valid [OF _ P], simp)
apply (rule use_valid [OF _ f], simp, simp)
done
lemmas hoare_lift_Pf4 = hoare_lift_Pf_pre_conj[where R=\<top>, simplified]
lemmas hoare_lift_Pf3 = hoare_lift_Pf4[where f=f and g=f for f]
lemmas hoare_lift_Pf2 = hoare_lift_Pf3[where P="\<lambda>f _. P f" for P]
lemmas hoare_lift_Pf = hoare_lift_Pf2[where Q=P and P=P for P]
lemmas hoare_lift_Pf3_pre_conj = hoare_lift_Pf_pre_conj[where f=f and g=f for f]
lemmas hoare_lift_Pf2_pre_conj = hoare_lift_Pf3_pre_conj[where P="\<lambda>f _. P f" for P]
lemmas hoare_lift_Pf_pre_conj' = hoare_lift_Pf2_pre_conj[where Q=P and P=P for P]
lemma hoare_if_r_and:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace>
= \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not>R r \<longrightarrow> Q' r s)\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_convert_imp:
"\<lbrakk> \<lbrace>\<lambda>s. \<not> P s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> Q s\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. P s \<longrightarrow> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> S rv s\<rbrace>"
apply (simp only: imp_conv_disj)
apply (erule(1) hoare_vcg_disj_lift)
done
lemma hoare_vcg_ex_lift_R:
"\<lbrakk> \<And>v. \<lbrace>P v\<rbrace> f \<lbrace>Q v\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>v. P v s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>v. Q v rv s\<rbrace>,-"
apply (simp add: validE_R_def validE_def)
apply (rule hoare_strengthen_post, erule hoare_vcg_ex_lift)
apply (auto split: sum.split)
done
lemma hoare_case_option_wpR:
"\<lbrakk>\<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>,-; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace>,-\<rbrakk> \<Longrightarrow>
\<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>,-"
by (cases v) auto
lemma hoare_vcg_conj_liftE_R:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>,-; \<lbrace>Q\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> Q' rv s\<rbrace>, -"
apply (simp add: validE_R_def validE_def valid_def split: sum.splits)
apply blast
done
lemma K_valid[wp]:
"\<lbrace>K P\<rbrace> f \<lbrace>\<lambda>_. K P\<rbrace>"
by (simp add: valid_def)
lemma hoare_vcg_exI:
"\<lbrace>P\<rbrace> f \<lbrace>Q x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>"
apply (simp add: valid_def split_def)
apply blast
done
lemma hoare_exI_tuple:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>(rv,rv') s. Q x rv rv' s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>(rv,rv') s. \<exists>x. Q x rv rv' s\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_ex_all:
"(\<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>"
apply (rule iffI)
apply (fastforce simp: valid_def)+
done
lemma hoare_imp_eq_substR:
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<longrightarrow> Q x s\<rbrace>,-"
by (fastforce simp add: valid_def validE_R_def validE_def split: sum.splits)
lemma hoare_split_bind_case_sum:
assumes x: "\<And>rv. \<lbrace>R rv\<rbrace> g rv \<lbrace>Q\<rbrace>"
"\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>"
assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
shows "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>"
apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]])
apply (case_tac x, simp_all add: x)
done
lemma hoare_split_bind_case_sumE:
assumes x: "\<And>rv. \<lbrace>R rv\<rbrace> g rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
"\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
shows "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
apply (unfold validE_def)
apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]])
apply (case_tac x, simp_all add: x [unfolded validE_def])
done
lemma assertE_sp:
"\<lbrace>P\<rbrace> assertE Q \<lbrace>\<lambda>rv s. Q \<and> P s\<rbrace>,\<lbrace>E\<rbrace>"
by (clarsimp simp: assertE_def) wp
lemma throwErrorE_E [wp]:
"\<lbrace>Q e\<rbrace> throwError e -, \<lbrace>Q\<rbrace>"
by (simp add: validE_E_def) wp
lemma gets_inv [simp]:
"\<lbrace> P \<rbrace> gets f \<lbrace> \<lambda>r. P \<rbrace>"
by (simp add: gets_def, wp)
lemma select_inv:
"\<lbrace> P \<rbrace> select S \<lbrace> \<lambda>r. P \<rbrace>"
by (simp add: select_def valid_def)
lemmas return_inv = hoare_return_drop_var
lemma assert_inv: "\<lbrace>P\<rbrace> assert Q \<lbrace>\<lambda>r. P\<rbrace>"
unfolding assert_def
by (cases Q) simp+
lemma assert_opt_inv: "\<lbrace>P\<rbrace> assert_opt Q \<lbrace>\<lambda>r. P\<rbrace>"
unfolding assert_opt_def
by (cases Q) simp+
lemma case_options_weak_wp:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace> g x \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>Q\<rbrace>"
apply (cases opt)
apply (clarsimp elim!: hoare_weaken_pre)
apply (rule hoare_weaken_pre [where Q=P'])
apply simp+
done
lemma case_option_wp_None_return:
assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace> f x \<lbrace>\<lambda>_. Q\<rbrace>"
shows "\<lbrakk>\<And>x s. (Q and P x) s \<Longrightarrow> P' x s \<rbrakk>
\<Longrightarrow> \<lbrace>Q and (\<lambda>s. opt \<noteq> None \<longrightarrow> P (the opt) s)\<rbrace>
(case opt of None \<Rightarrow> return () | Some x \<Rightarrow> f x)
\<lbrace>\<lambda>_. Q\<rbrace>"
by (cases opt; wpsimp)
lemma case_option_wp_None_returnOk:
assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace> f x \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>"
shows "\<lbrakk>\<And>x s. (Q and P x) s \<Longrightarrow> P' x s \<rbrakk>
\<Longrightarrow> \<lbrace>Q and (\<lambda>s. opt \<noteq> None \<longrightarrow> P (the opt) s)\<rbrace>
(case opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> f x)
\<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>"
by (cases opt; wpsimp)
lemma list_cases_weak_wp:
assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
assumes "\<And>x xs. \<lbrace>P_B\<rbrace> b x xs \<lbrace>Q\<rbrace>"
shows
"\<lbrace>P_A and P_B\<rbrace>
case ts of
[] \<Rightarrow> a
| x#xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace>"
apply (cases ts)
apply (simp, rule hoare_weaken_pre, rule assms, simp)+
done
lemmas hoare_FalseE_R = hoare_FalseE[where E="\<top>\<top>", folded validE_R_def]
lemma hoare_vcg_if_lift2:
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>"
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>"
by (auto simp: valid_def split_def)
lemma hoare_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *)
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow>
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>, -"
"\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow>
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>, -"
by (auto simp: valid_def validE_R_def validE_def split_def)
lemma hoare_vcg_imp_liftE:
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, \<lbrace>A\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>A\<rbrace> \<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, \<lbrace>A\<rbrace>"
apply (simp only: imp_conv_disj)
apply (clarsimp simp: validE_def valid_def split_def sum.case_eq_if)
done
lemma hoare_list_all_lift:
"(\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace> f \<lbrace>\<lambda>rv. Q r\<rbrace>)
\<Longrightarrow> \<lbrace>\<lambda>s. list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. list_all (\<lambda>r. Q r s) xs\<rbrace>"
apply (induct xs; simp)
apply wpsimp
apply (rule hoare_vcg_conj_lift; simp)
done
lemma undefined_valid: "\<lbrace>\<bottom>\<rbrace> undefined \<lbrace>Q\<rbrace>"
by (rule hoare_pre_cont)
lemma assertE_wp:
"\<lbrace>\<lambda>s. F \<longrightarrow> Q () s\<rbrace> assertE F \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
apply (rule hoare_pre)
apply (unfold assertE_def)
apply wp
apply simp
done
lemma doesn't_grow_proof:
assumes y: "\<And>s. finite (S s)"
assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
shows "\<lbrace>\<lambda>s. card (S s) < n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>"
apply (clarsimp simp: valid_def)
apply (subgoal_tac "S b \<subseteq> S s")
apply (drule card_mono [OF y], simp)
apply clarsimp
apply (rule ccontr)
apply (subgoal_tac "x \<notin> S b", simp)
apply (erule use_valid [OF _ x])
apply simp
done
lemma hoare_vcg_propE_R:
"\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>, -"
by (simp add: validE_R_def validE_def valid_def split_def split: sum.split)
lemma set_preserved_proof:
assumes y: "\<And>x. \<lbrace>\<lambda>s. Q s \<and> x \<in> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<in> S s\<rbrace>"
assumes x: "\<And>x. \<lbrace>\<lambda>s. Q s \<and> x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
shows "\<lbrace>\<lambda>s. Q s \<and> P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
apply (clarsimp simp: valid_def)
by (metis (mono_tags, lifting) equalityI post_by_hoare subsetI x y)
lemma set_shrink_proof:
assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
shows
"\<lbrace>\<lambda>s. \<forall>S'. S' \<subseteq> S s \<longrightarrow> P S'\<rbrace>
f
\<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
apply (clarsimp simp: valid_def)
apply (drule spec, erule mp)
apply (clarsimp simp: subset_iff)
apply (rule ccontr)
apply (drule(1) use_valid [OF _ x])
apply simp
done
lemma shrinks_proof:
assumes y: "\<And>s. finite (S s)"
assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
assumes z: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
assumes w: "\<And>s. P s \<Longrightarrow> x \<in> S s"
shows "\<lbrace>\<lambda>s. card (S s) \<le> n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>"
apply (clarsimp simp: valid_def)
apply (subgoal_tac "S b \<subset> S s")
apply (drule psubset_card_mono [OF y], simp)
apply (rule psubsetI)
apply clarsimp
apply (rule ccontr)
apply (subgoal_tac "x \<notin> S b", simp)
apply (erule use_valid [OF _ x])
apply simp
by (metis use_valid w z)
lemma use_validE_R:
"\<lbrakk> (Inr r, s') \<in> fst (f s); \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; P s \<rbrakk> \<Longrightarrow> Q r s'"
unfolding validE_R_def validE_def
by (frule(2) use_valid, simp)
lemma valid_preservation_ex:
assumes x: "\<And>x P. \<lbrace>\<lambda>s. P (f s x :: 'b)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s x)\<rbrace>"
shows "\<lbrace>\<lambda>s. P (f s :: 'a \<Rightarrow> 'b)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s)\<rbrace>"
apply (clarsimp simp: valid_def)
apply (erule subst[rotated, where P=P])
apply (rule ext)
apply (erule use_valid [OF _ x])
apply simp
done
lemmas valid_prove_more' = valid_prove_more[where Q="\<lambda>rv. Q" for Q]
lemma whenE_inv:
assumes a: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
shows "\<lbrace>P\<rbrace> whenE Q f \<lbrace>\<lambda>_. P\<rbrace>"
by (wpsimp wp: a)
lemma whenE_throwError_wp:
"\<lbrace>\<lambda>s. \<not> P \<longrightarrow> Q s\<rbrace> whenE P (throwError e) \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<top>\<top>\<rbrace>"
by wpsimp
lemma ifM_throwError_returnOk:
"\<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace> ifM test (throwError e) (returnOk ()) \<lbrace>\<lambda>_. P\<rbrace>, -"
by (fastforce simp: ifM_def returnOk_def throwError_def return_def validE_R_def valid_def
validE_def bind_def
split: if_splits)
lemma ifME_liftE:
"ifME (liftE test) a b = ifM test a b"
by (simp add: ifME_def ifM_def liftE_bindE)
lemma gets_the_inv: "\<lbrace>P\<rbrace> gets_the V \<lbrace>\<lambda>rv. P\<rbrace>" by wpsimp
lemma select_f_inv:
"\<lbrace>P\<rbrace> select_f S \<lbrace>\<lambda>_. P\<rbrace>"
by (simp add: select_f_def valid_def)
lemmas state_unchanged = in_inv_by_hoareD [THEN sym]
lemma validI:
assumes rl: "\<And>s r s'. \<lbrakk> P s; (r, s') \<in> fst (S s) \<rbrakk> \<Longrightarrow> Q r s'"
shows "\<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>"
unfolding valid_def using rl by safe
lemma opt_return_pres_lift:
assumes x: "\<And>v. \<lbrace>P\<rbrace> f v \<lbrace>\<lambda>rv. P\<rbrace>"
shows "\<lbrace>P\<rbrace> case x of None \<Rightarrow> return () | Some v \<Rightarrow> f v \<lbrace>\<lambda>rv. P\<rbrace>"
by (wpsimp wp: x)
lemma valid_return_unit:
"\<lbrace>P\<rbrace> f >>= (\<lambda>_. return ()) \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>"
apply (rule validI)
apply (fastforce simp: valid_def return_def bind_def split_def)
done
lemma static_imp_wp:
"\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
by (cases P, simp_all add: valid_def)
lemma static_imp_wpE :
"\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
by (cases P, simp_all)
lemma static_imp_conj_wp:
"\<lbrakk> \<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace> m \<lbrace>R'\<rbrace> \<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>"
apply (rule hoare_vcg_conj_lift)
apply (rule static_imp_wp)
apply assumption+
done
lemma hoare_eq_P:
assumes "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
shows "\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>"
by (rule assms)
lemma hoare_validE_R_conj:
"\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>, -"
by (simp add: valid_def validE_def validE_R_def Let_def split_def split: sum.splits)
lemma hoare_vcg_const_imp_lift_R:
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. F \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. F \<longrightarrow> Q rv s\<rbrace>,-"
by (cases F, simp_all)
lemma hoare_vcg_disj_lift_R:
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
shows "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-"
using assms
by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
lemmas throwError_validE_R = throwError_wp [where E="\<top>\<top>", folded validE_R_def]
lemma valid_case_option_post_wp:
"(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>rv. Q x\<rbrace>) \<Longrightarrow>
\<lbrace>\<lambda>s. case ep of Some x \<Rightarrow> P x s | _ \<Rightarrow> True\<rbrace>
f \<lbrace>\<lambda>rv s. case ep of Some x \<Rightarrow> Q x s | _ \<Rightarrow> True\<rbrace>"
by (cases ep, simp_all add: hoare_vcg_prop)
lemma P_bool_lift:
assumes t: "\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>"
assumes f: "\<lbrace>\<lambda>s. \<not>Q s\<rbrace> f \<lbrace>\<lambda>r s. \<not>Q s\<rbrace>"
shows "\<lbrace>\<lambda>s. P (Q s)\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>"
apply (clarsimp simp: valid_def)
apply (subgoal_tac "Q b = Q s")
apply simp
apply (rule iffI)
apply (rule classical)
apply (drule (1) use_valid [OF _ f])
apply simp
apply (erule (1) use_valid [OF _ t])
done
lemmas fail_inv = hoare_fail_any[where Q="\<lambda>_. P" and P=P for P]
lemma gets_sp: "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv. P and (\<lambda>s. f s = rv)\<rbrace>"
by (wp, simp)
lemma post_by_hoare2:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; (r, s') \<in> fst (f s); P s \<rbrakk> \<Longrightarrow> Q r s'"
by (rule post_by_hoare, assumption+)
lemma hoare_Ball_helper:
assumes x: "\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>"
assumes y: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
shows "\<lbrace>\<lambda>s. \<forall>x \<in> S s. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S s. Q x rv s\<rbrace>"
apply (clarsimp simp: valid_def)
apply (subgoal_tac "S b = S s")
apply (erule post_by_hoare2 [OF x])
apply (clarsimp simp: Ball_def)
apply (erule_tac P1="\<lambda>x. x = S s" in post_by_hoare2 [OF y])
apply (rule refl)
done
lemma handy_prop_divs:
assumes x: "\<And>P. \<lbrace>\<lambda>s. P (Q s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s)\<rbrace>"
"\<And>P. \<lbrace>\<lambda>s. P (R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (R' rv s)\<rbrace>"
shows "\<lbrace>\<lambda>s. P (Q s \<and> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<and> R' rv s)\<rbrace>"
"\<lbrace>\<lambda>s. P (Q s \<or> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<or> R' rv s)\<rbrace>"
apply (clarsimp simp: valid_def
elim!: subst[rotated, where P=P])
apply (rule use_valid [OF _ x(1)], assumption)
apply (rule use_valid [OF _ x(2)], assumption)
apply simp
apply (clarsimp simp: valid_def
elim!: subst[rotated, where P=P])
apply (rule use_valid [OF _ x(1)], assumption)
apply (rule use_valid [OF _ x(2)], assumption)
apply simp
done
lemma hoare_as_subst:
"\<lbrakk> \<And>P. \<lbrace>\<lambda>s. P (fn s)\<rbrace> f \<lbrace>\<lambda>rv s. P (fn s)\<rbrace>;
\<And>v :: 'a. \<lbrace>P v\<rbrace> f \<lbrace>Q v\<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. P (fn s) s\<rbrace> f \<lbrace>\<lambda>rv s. Q (fn s) rv s\<rbrace>"
by (rule hoare_lift_Pf3)
lemmas hoare_vcg_ball_lift = hoare_vcg_const_Ball_lift
lemma hoare_set_preserved:
assumes x: "\<And>x. \<lbrace>fn' x\<rbrace> m \<lbrace>\<lambda>rv. fn x\<rbrace>"
shows "\<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace>"
apply (induct xs)
apply simp
apply wp
apply simp
apply (rule hoare_vcg_conj_lift)
apply (rule x)
apply assumption
done
lemma hoare_ex_pre: (* safe, unlike hoare_vcg_ex_lift *)
"(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_ex_pre_conj:
"(\<And>x. \<lbrace>\<lambda>s. P x s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>)
\<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>x. P x s) \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_conj_lift_inv:
"\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. P' s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv. I\<rbrace>;
\<And>s. P s \<Longrightarrow> P' s\<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I s\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_in_monad_post :
assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
shows "\<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (f s)\<rbrace>"
apply (clarsimp simp: valid_def)
apply (subgoal_tac "s = b", simp)
apply (simp add: state_unchanged [OF x])
done
lemma list_case_throw_validE_R:
"\<lbrakk> \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace> f y ys \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow>
\<lbrace>P\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>Q\<rbrace>,-"
apply (case_tac xs, simp_all)
apply wp
done
lemma validE_R_sp:
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
assumes y: "\<And>x. \<lbrace>Q x\<rbrace> g x \<lbrace>R\<rbrace>,-"
shows "\<lbrace>P\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>R\<rbrace>,-"
by (rule hoare_pre, wp x y, simp)
lemma valid_set_take_helper:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (xs rv s). Q x rv s\<rbrace>
\<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (take (n rv s) (xs rv s)). Q x rv s\<rbrace>"
apply (erule hoare_strengthen_post)
apply (clarsimp dest!: in_set_takeD)
done
lemma whenE_throwError_sp:
"\<lbrace>P\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv s. \<not> Q \<and> P s\<rbrace>, -"
apply (simp add: whenE_def validE_R_def)
apply (intro conjI impI; wp)
done
lemma weaker_hoare_ifE:
assumes x: "\<lbrace>P \<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
assumes y: "\<lbrace>P'\<rbrace> b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
shows "\<lbrace>P and P'\<rbrace> if test then a else b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
apply (rule hoare_vcg_precond_impE)
apply (wp x y)
apply simp
done
lemma wp_split_const_if:
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>"
shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>"
by (case_tac G, simp_all add: x y)
lemma wp_split_const_if_R:
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>,-"
by (case_tac G, simp_all add: x y)
lemma wp_throw_const_imp:
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
shows "\<lbrace>\<lambda>s. G \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. G \<longrightarrow> Q rv s\<rbrace>"
by (case_tac G, simp_all add: x hoare_vcg_prop)
lemma wp_throw_const_impE:
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
shows "\<lbrace>\<lambda>s. G \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. G \<longrightarrow> Q rv s\<rbrace>,\<lbrace>\<lambda>rv s. G \<longrightarrow> E rv s\<rbrace>"
apply (case_tac G, simp_all add: x)
apply wp
done
lemma hoare_const_imp_R:
"\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
by (cases P, simp_all)
lemma hoare_vcg_imp_lift_R:
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -"
by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
lemma hoare_disj_division:
"\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>"
apply safe
apply (rule hoare_pre_imp)
prefer 2
apply simp
apply simp
apply (rule hoare_pre_imp)
prefer 2
apply simp
apply simp
done
lemma hoare_grab_asm:
"\<lbrakk> G \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. G \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>"
by (cases G, simp+)
lemma hoare_grab_asm2:
"(P' \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>)
\<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_grab_exs:
assumes x: "\<And>x. P x \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"
shows "\<lbrace>\<lambda>s. \<exists>x. P x \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>"
apply (clarsimp simp: valid_def)
apply (erule(2) use_valid [OF _ x])
done
lemma hoare_prop_E: "\<lbrace>\<lambda>rv. P\<rbrace> f -,\<lbrace>\<lambda>rv s. P\<rbrace>"
unfolding validE_E_def
by (rule hoare_pre, wp, simp)
lemma hoare_vcg_conj_lift_R:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>,- \<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> S rv s\<rbrace>,-"
apply (simp add: validE_R_def validE_def)
apply (drule(1) hoare_vcg_conj_lift)
apply (erule hoare_strengthen_post)
apply (clarsimp split: sum.splits)
done
lemma hoare_walk_assmsE:
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" and y: "\<And>s. P s \<Longrightarrow> Q s" and z: "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. Q\<rbrace>"
shows "\<lbrace>P\<rbrace> doE x \<leftarrow> f; g odE \<lbrace>\<lambda>rv. Q\<rbrace>"
apply (wp z)
apply (simp add: validE_def)
apply (rule hoare_strengthen_post [OF x])
apply (auto simp: y split: sum.splits)
done
lemma univ_wp:
"\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>"
by (simp add: valid_def)
lemma univ_get_wp:
assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>"
shows "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>"
apply (rule hoare_pre_imp [OF _ univ_wp])
apply clarsimp
apply (drule bspec, assumption, simp)
apply (subgoal_tac "s = b", simp)
apply (simp add: state_unchanged [OF x])
done
lemma result_in_set_wp :
assumes x: "\<And>P. \<lbrace>P\<rbrace> fn \<lbrace>\<lambda>rv. P\<rbrace>"
shows "\<lbrace>\<lambda>s. True\<rbrace> fn \<lbrace>\<lambda>v s'. (v, s') \<in> fst (fn s')\<rbrace>"
by (rule hoare_pre_imp [OF _ univ_get_wp], simp_all add: x split_def) clarsimp
lemma other_result_in_set_wp:
assumes x: "\<And>P. \<lbrace>P\<rbrace> fn \<lbrace>\<lambda>rv. P\<rbrace>"
shows "\<lbrace>\<lambda>s. \<forall>(v, s) \<in> fst (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> fst (fn s')\<rbrace>"
proof -
have P: "\<And>v s. (F v = v) \<and> (v, s) \<in> fst (fn s) \<Longrightarrow> (F v, s) \<in> fst (fn s)"
by simp
show ?thesis
apply (rule hoare_post_imp [OF P], assumption)
apply (rule hoare_pre_imp)
defer
apply (rule hoare_vcg_conj_lift)
apply (rule univ_get_wp [OF x])
apply (rule result_in_set_wp [OF x])
apply clarsimp
apply (drule bspec, assumption, simp)
done
qed
lemma weak_if_wp:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>"
by (auto simp add: valid_def split_def)
lemma weak_if_wp':
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q r and Q' r\<rbrace> \<Longrightarrow>
\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>"
by (auto simp add: valid_def split_def)
lemma bindE_split_recursive_asm:
assumes x: "\<And>x s'. \<lbrakk> (Inr x, s') \<in> fst (f s) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. B x s \<and> s = s'\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
shows "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>st. A st \<and> st = s\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: validE_def valid_def bindE_def bind_def lift_def)
apply (erule allE, erule(1) impE)
apply (drule(1) bspec, simp)
apply (case_tac a, simp_all add: throwError_def return_def)
apply (drule x)
apply (clarsimp simp: validE_def valid_def)
apply (drule(1) bspec, simp)
done
lemma validE_R_abstract_rv:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. Q rv' s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
by (erule hoare_post_imp_R, simp)
lemma validE_cases_valid:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (Inr rv) s\<rbrace>,\<lbrace>\<lambda>rv s. Q (Inl rv) s\<rbrace>
\<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
apply (simp add: validE_def)
apply (erule hoare_strengthen_post)
apply (simp split: sum.split_asm)
done
lemma liftM_pre:
assumes rl: "\<lbrace>\<lambda>s. \<not> P s \<rbrace> a \<lbrace> \<lambda>_ _. False \<rbrace>"
shows "\<lbrace>\<lambda>s. \<not> P s \<rbrace> liftM f a \<lbrace> \<lambda>_ _. False \<rbrace>"
unfolding liftM_def
apply (rule seq)
apply (rule rl)
apply wp
apply simp
done
lemma hoare_gen_asm':
"(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and (\<lambda>_. P)\<rbrace> f \<lbrace>Q\<rbrace>"
apply (auto intro: hoare_assume_pre)
done
lemma hoare_gen_asm_conj:
"(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<and> P\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_add_K:
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I\<rbrace>"
by (fastforce simp: valid_def)
lemma valid_rv_lift:
"\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> P \<and> Q rv s\<rbrace>"
by (fastforce simp: valid_def)
lemma valid_imp_ex:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. rv \<longrightarrow> Q rv s x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (\<exists>x. Q rv s x)\<rbrace>"
by (fastforce simp: valid_def)
lemma valid_rv_split:
"\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> Q' s\<rbrace>\<rbrakk>
\<Longrightarrow>
\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_rv_split:
"\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (Q rv s)\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (\<not>rv) \<longrightarrow> (Q rv s)\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
apply (clarsimp simp: valid_def)
apply (case_tac a, fastforce+)
done
lemma combine_validE: "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>;
\<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace> P and P' \<rbrace> x \<lbrace> \<lambda>r. (Q r) and (Q' r) \<rbrace>,\<lbrace>\<lambda>r. (E r) and (E' r) \<rbrace>"
apply (clarsimp simp: validE_def valid_def split: sum.splits)
apply (erule allE, erule (1) impE)+
apply (drule (1) bspec)+
apply clarsimp
done
lemma valid_case_prod:
"\<lbrakk> \<And>x y. valid (P x y) (f x y) Q \<rbrakk> \<Longrightarrow> valid (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q"
by (simp add: split_def)
lemma validE_case_prod:
"\<lbrakk> \<And>x y. validE (P x y) (f x y) Q E \<rbrakk> \<Longrightarrow> validE (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q E"
by (simp add: split_def)
lemma valid_pre_satisfies_post:
"\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>"
by (clarsimp simp: valid_def)
lemma validE_pre_satisfies_post:
"\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s'; \<And>s r' s'. P s \<Longrightarrow> R r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace>"
by (clarsimp simp: validE_def2 split: sum.splits)
lemma hoare_validE_R_conjI:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - ; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, -"
apply (clarsimp simp: Ball_def validE_R_def validE_def valid_def)
by (case_tac a; fastforce)
lemma hoare_validE_E_conjI:
"\<lbrakk> \<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace> ; \<lbrace>P\<rbrace> f -, \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
apply (clarsimp simp: Ball_def validE_E_def validE_def valid_def)
by (case_tac a; fastforce)
lemma validE_R_post_conjD1:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
apply (clarsimp simp: validE_R_def validE_def valid_def)
by (case_tac a; fastforce)
lemma validE_R_post_conjD2:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-"
apply (clarsimp simp: validE_R_def validE_def valid_def)
by (case_tac a; fastforce)
lemma throw_opt_wp[wp]:
"\<lbrace>if v = None then E ex else Q (the v)\<rbrace> throw_opt ex v \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
unfolding throw_opt_def by wpsimp auto
lemma hoare_name_pre_state2:
"(\<And>s. \<lbrace>P and ((=) s)\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
by (auto simp: valid_def intro: hoare_name_pre_state)
lemma returnOk_E': "\<lbrace>P\<rbrace> returnOk r -,\<lbrace>E\<rbrace>"
by (clarsimp simp: returnOk_def validE_E_def validE_def valid_def return_def)
lemma throwError_R': "\<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>,-"
by (clarsimp simp:throwError_def validE_R_def validE_def valid_def return_def)
end

88
lib/Monads/trace/Trace_No_Fail.thy
View File

@ -42,6 +42,11 @@ subsection \<open>Bundles\<close>
bundle no_pre = hoare_pre [wp_pre del] no_fail_pre [wp_pre del]
bundle classic_wp_pre =
hoare_pre [wp_pre del]
all_classic_wp_combs[wp_comb del]
all_classic_wp_combs[wp_comb]
subsection \<open>Lemmas\<close>
@ -135,8 +140,91 @@ lemma no_fail_bind[wp]:
apply (fastforce simp: image_def)
done
lemma no_fail_assume_pre:
"(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f"
by (simp add: no_fail_def)
lemma no_fail_liftM_eq[simp]:
"no_fail P (liftM f m) = no_fail P m"
by (auto simp: liftM_def no_fail_def bind_def return_def)
lemma no_fail_liftM[wp]:
"no_fail P m \<Longrightarrow> no_fail P (liftM f m)"
by simp
lemma no_fail_pre_and:
"no_fail P f \<Longrightarrow> no_fail (P and Q) f"
by (erule no_fail_pre) simp
lemma no_fail_spec:
"\<lbrakk> \<And>s. no_fail (((=) s) and P) f \<rbrakk> \<Longrightarrow> no_fail P f"
by (simp add: no_fail_def)
lemma no_fail_assertE[wp]:
"no_fail (\<lambda>_. P) (assertE P)"
by (simp add: assertE_def split: if_split)
lemma no_fail_spec_pre:
"\<lbrakk> no_fail (((=) s) and P') f; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> no_fail (((=) s) and P) f"
by (erule no_fail_pre, simp)
lemma no_fail_whenE[wp]:
"\<lbrakk> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. G \<longrightarrow> P s) (whenE G f)"
by (simp add: whenE_def split: if_split)
lemma no_fail_unlessE[wp]:
"\<lbrakk> \<not> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)"
by (simp add: unlessE_def split: if_split)
lemma no_fail_throwError[wp]:
"no_fail \<top> (throwError e)"
by (simp add: throwError_def)
lemma no_fail_liftE[wp]:
"no_fail P f \<Longrightarrow> no_fail P (liftE f)"
unfolding liftE_def by wpsimp
lemma no_fail_gets_the[wp]:
"no_fail (\<lambda>s. f s \<noteq> None) (gets_the f)"
unfolding gets_the_def
by wpsimp
lemma no_fail_lift:
"(\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not>isl x \<longrightarrow> P s) (lift f x)"
unfolding lift_def
by (wpsimp wp: no_fail_throwError split: sum.splits | assumption)+
lemma validE_R_valid_eq:
"\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - = \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. \<not> isl rv \<longrightarrow> R (projr rv) s\<rbrace>"
unfolding validE_R_def validE_def valid_def
by (fastforce split: sum.splits prod.split)
lemma no_fail_bindE[wp]:
"\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<rbrakk>
\<Longrightarrow> no_fail (P and Q) (f >>=E g)"
unfolding bindE_def
by (wpsimp wp: no_fail_lift simp: validE_R_valid_eq | assumption)+
lemma no_fail_False[simp]:
"no_fail (\<lambda>_. False) X"
by (clarsimp simp: no_fail_def)
lemma no_fail_gets_map[wp]:
"no_fail (\<lambda>s. f s p \<noteq> None) (gets_map f p)"
unfolding gets_map_def by wpsimp
lemma no_fail_or:
"\<lbrakk>no_fail P a; no_fail Q a\<rbrakk> \<Longrightarrow> no_fail (P or Q) a"
by (clarsimp simp: no_fail_def)
lemma no_fail_state_assert[wp]:
"no_fail P (state_assert P)"
unfolding state_assert_def
by wpsimp
lemma no_fail_condition:
"\<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) (condition C A B)"
unfolding condition_def no_fail_def
by clarsimp
end

70
lib/Monads/trace/Trace_No_Throw.thy
View File

@ -25,4 +25,74 @@ definition no_throw :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'a) tmon
definition no_return :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b + 'c) tmonad \<Rightarrow> bool" where
"no_return P A \<equiv> \<lbrace> P \<rbrace> A \<lbrace>\<lambda>_ _. False\<rbrace>,\<lbrace>\<lambda>_ _. True \<rbrace>"
(* Alternative definition of no_throw; easier to work with than unfolding validE. *)
lemma no_throw_def':
"no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t) \<in> fst (A s). (\<exists>x. r = Inr x)))"
by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits)
lemma no_throw_returnOk[simp]:
"no_throw P (returnOk a)"
unfolding no_throw_def
by wp
lemma no_throw_liftE[simp]:
"no_throw P (liftE x)"
by (wpsimp simp: liftE_def no_throw_def validE_def)
lemma no_throw_bindE:
"\<lbrakk> no_throw A X; \<And>a. no_throw B (Y a); \<lbrace> A \<rbrace> X \<lbrace> \<lambda>_. B \<rbrace>,\<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk>
\<Longrightarrow> no_throw A (X >>=E Y)"
unfolding no_throw_def
using hoare_validE_cases seqE by blast
lemma no_throw_bindE_simple:
"\<lbrakk> no_throw \<top> L; \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L >>=E R)"
using hoareE_TrueI no_throw_bindE by blast
lemma no_throw_handleE_simple:
"\<lbrakk> \<And>x. no_throw \<top> L \<or> no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)"
by (fastforce simp: no_throw_def' handleE_def handleE'_def validE_def valid_def bind_def return_def
split: sum.splits)
lemma no_throw_handle2:
"\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)"
by (fastforce simp: no_throw_def' handleE'_def validE_def valid_def bind_def return_def
split: sum.splits)
lemma no_throw_handle:
"\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle> B)"
unfolding handleE_def
by (rule no_throw_handle2)
lemma no_throw_fail[simp]:
"no_throw P fail"
by (clarsimp simp: no_throw_def)
lemma handleE'_nothrow_lhs:
"no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle2> R)"
unfolding no_throw_def
using handleE'_wp[rotated] by fastforce
lemma handleE'_nothrow_rhs:
"\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle2> R)"
unfolding no_throw_def
by (metis hoareE_TrueI no_throw_def no_throw_handle2)
lemma handleE_nothrow_lhs:
"no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle> R)"
by (metis handleE'_nothrow_lhs handleE_def)
lemma handleE_nothrow_rhs:
"\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)"
by (metis no_throw_handleE_simple)
lemma condition_nothrow:
"\<lbrakk> no_throw \<top> L; no_throw \<top> R \<rbrakk> \<Longrightarrow> no_throw \<top> (condition C L R)"
by (clarsimp simp: condition_def no_throw_def validE_def2)
lemma no_throw_Inr:
"\<lbrakk> x \<in> fst (A s); no_throw P A; P s \<rbrakk> \<Longrightarrow> \<exists>y. fst x = Inr y"
by (fastforce simp: no_throw_def' split: sum.splits)
end

53
lib/Monads/trace/Trace_Sat.thy
View File

@ -26,6 +26,30 @@ definition ex_exs_validE ::
("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>, \<lbrace>_\<rbrace>") where
"\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<equiv> \<lbrace>P\<rbrace> f \<exists>\<lbrace>\<lambda>rv. case rv of Inl e \<Rightarrow> E e | Inr v \<Rightarrow> Q v\<rbrace>"
text \<open>
Seen as predicate transformer, @{const exs_valid} is the so-called conjugate wp in the literature,
i.e. with
@{term "wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"} and
@{term "cwp f Q \<equiv> not (wp f (not Q))"}, we get
@{prop "valid P f Q = (\<forall>s. P s \<longrightarrow> wp f Q s)"} and
@{prop "exs_valid P f Q = (\<forall>s. P s \<longrightarrow> cwp f Q s)"}.
See also "Predicate Calculus and Program Semantics" by E. W. Dijkstra and C. S. Scholten.\<close>
experiment
begin
definition
"wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"
definition
"cwp f Q \<equiv> not (wp f (not Q))"
lemma
"exs_valid P f Q = (\<forall>s. P s \<longrightarrow> cwp f Q s)"
unfolding exs_valid_def cwp_def wp_def by auto
end
subsection \<open>Set up for @{method wp}\<close>
@ -76,9 +100,11 @@ lemma exs_valid_return[wp]:
lemma exs_valid_select[wp]:
"\<lbrace>\<lambda>s. \<exists>r \<in> S. Q r s\<rbrace> select S \<exists>\<lbrace>Q\<rbrace>"
apply (clarsimp simp: exs_valid_def select_def mres_def)
apply (auto simp add: image_def)
done
by (clarsimp simp: exs_valid_def select_def)
lemma exs_valid_alt[wp]:
"\<lbrakk> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g \<exists>\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P or P'\<rbrace> f \<sqinter> g \<exists>\<lbrace>Q\<rbrace>"
by (fastforce simp: exs_valid_def alternative_def)
lemma exs_valid_get[wp]:
"\<lbrace>\<lambda>s. Q s s\<rbrace> get \<exists>\<lbrace> Q \<rbrace>"
@ -97,10 +123,15 @@ lemma exs_valid_fail[wp]:
unfolding fail_def exs_valid_def
by simp
lemma exs_valid_assert[wp]:
"\<lbrace>\<lambda>s. Q () s \<and> G\<rbrace> assert G \<exists>\<lbrace>Q\<rbrace>"
unfolding assert_def
by (wpsimp | rule conjI)+
lemma exs_valid_state_assert[wp]:
"\<lbrace> \<lambda>s. Q () s \<and> G s \<rbrace> state_assert G \<exists>\<lbrace> Q \<rbrace>"
by (clarsimp simp: state_assert_def exs_valid_def get_def
assert_def bind_def2 return_def mres_def)
unfolding state_assert_def
by wp
lemmas exs_valid_guard = exs_valid_state_assert
@ -108,4 +139,16 @@ lemma exs_valid_condition[wp]:
"\<lbrakk> \<lbrace>P\<rbrace> l \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> r \<exists>\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (C s \<and> P s) \<or> (\<not> C s \<and> P' s)\<rbrace> condition C l r \<exists>\<lbrace>Q\<rbrace>"
by (clarsimp simp: condition_def exs_valid_def split: sum.splits)
lemma gets_exs_valid:
"\<lbrace>(=) s\<rbrace> gets f \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
by (rule exs_valid_gets)
lemma exs_valid_assert_opt[wp]:
"\<lbrace>\<lambda>s. \<exists>x. G = Some x \<and> Q x s\<rbrace> assert_opt G \<exists>\<lbrace>Q\<rbrace>"
by (clarsimp simp: assert_opt_def exs_valid_def get_def assert_def bind_def' return_def)
lemma gets_the_exs_valid[wp]:
"\<lbrace>\<lambda>s. \<exists>x. h s = Some x \<and> Q x s\<rbrace> gets_the h \<exists>\<lbrace>Q\<rbrace>"
by (wpsimp simp: gets_the_def)
end

40
lib/Monads/trace/Trace_Strengthen_Setup.thy
View File

@ -41,6 +41,46 @@ lemma strengthen_validI[strg]:
\<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace>,\<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace>,\<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>Q'\<rbrace>)"
by (cases F, auto elim: validI_strengthen_post)
lemma wpfix_strengthen_hoare:
"(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
\<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s))
\<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>)"
by (cases F, auto elim: hoare_chain)
lemma wpfix_strengthen_validE_R_cong:
"(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
\<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s))
\<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -)"
by (cases F, auto elim: hoare_chainE simp: validE_R_def)
lemma wpfix_strengthen_validE_cong:
"(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
\<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s))
\<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (S r s) (T r s))
\<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)"
by (cases F, auto elim: hoare_chainE)
lemma wpfix_strengthen_validE_E_cong:
"(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
\<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (S r s) (T r s))
\<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f -, \<lbrace>T\<rbrace>)"
by (cases F, auto elim: hoare_chainE simp: validE_E_def)
lemma wpfix_no_fail_cong:
"(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
\<Longrightarrow> st F (\<longrightarrow>) (no_fail P f) (no_fail P' f)"
by (cases F, auto elim: no_fail_pre)
lemmas nondet_wpfix_strgs =
wpfix_strengthen_validE_R_cong
wpfix_strengthen_validE_E_cong
wpfix_strengthen_validE_cong
wpfix_strengthen_hoare
wpfix_no_fail_cong
end
lemmas nondet_wpfix_strgs[wp_fix_strgs]
= strengthen_implementation.nondet_wpfix_strgs
end

113
lib/Monads/trace/Trace_Total.thy
View File

@ -49,17 +49,40 @@ wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>!" wpc_helper_va
subsection \<open>Basic @{const validNF} theorems\<close>
lemma validNF_make_schematic_post:
"(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>!) \<Longrightarrow>
\<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>!"
by (auto simp add: valid_def validNF_def no_fail_def split: prod.splits)
lemma validE_NF_make_schematic_post:
"(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>, \<lbrace> \<lambda>rv s. E s0 rv s \<rbrace>!) \<Longrightarrow>
\<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')
\<and> (\<forall>rv s'. E s0 rv s' \<longrightarrow> E' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>, \<lbrace> E' \<rbrace>!"
by (auto simp add: validE_NF_def validE_def valid_def no_fail_def split: prod.splits sum.splits)
lemma validNF_conjD1:
"\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv s. Q rv s \<and> Q' rv s \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!"
by (fastforce simp: validNF_def valid_def no_fail_def)
lemma validNF_conjD2:
"\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv s. Q rv s \<and> Q' rv s \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q' \<rbrace>!"
by (fastforce simp: validNF_def valid_def no_fail_def)
lemma validNF[intro?]: (* FIXME lib: should be validNFI *)
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!"
by (clarsimp simp: validNF_def)
lemma validNFE:
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; \<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
by (clarsimp simp: validNF_def)
lemma validNF_valid:
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
by (clarsimp simp: validNF_def)
by (erule validNFE)
lemma validNF_no_fail:
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
by (clarsimp simp: validNF_def)
by (erule validNFE)
lemma snd_validNF:
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> Failed \<notin> snd ` (f s)"
@ -163,60 +186,45 @@ subsection "validNF compound rules"
lemma validNF_state_assert[wp]:
"\<lbrace> \<lambda>s. P () s \<and> G s \<rbrace> state_assert G \<lbrace> P \<rbrace>!"
apply (rule validNF)
apply wpsimp
apply (clarsimp simp: no_fail_def state_assert_def
bind_def2 assert_def return_def get_def)
done
by (rule validNF; wpsimp)
lemma validNF_modify[wp]:
"\<lbrace> \<lambda>s. P () (f s) \<rbrace> modify f \<lbrace> P \<rbrace>!"
apply (clarsimp simp: modify_def)
apply wp
done
by (rule validNF; wpsimp)
lemma validNF_gets[wp]:
"\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>!"
apply (clarsimp simp: gets_def)
apply wp
done
by (rule validNF; wpsimp)
lemma validNF_condition[wp]:
"\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>!"
apply rule
apply (drule validNF_valid)+
apply (erule (1) condition_wp)
apply (drule validNF_no_fail)+
apply (clarsimp simp: no_fail_def condition_def)
done
by (erule validNFE)+
(rule validNF; wpsimp wp: no_fail_condition)
lemma validNF_assert[wp]:
"\<lbrace> (\<lambda>s. P) and (R ()) \<rbrace> assert P \<lbrace> R \<rbrace>!"
apply (rule validNF)
apply (clarsimp simp: valid_def in_return)
apply (clarsimp simp: no_fail_def return_def)
done
"\<lbrace> (\<lambda>s. P) and (R ()) \<rbrace> assert P \<lbrace> R \<rbrace>!"
by (rule validNF; wpsimp)
lemma validNF_false_pre:
"\<lbrace> \<lambda>_. False \<rbrace> P \<lbrace> Q \<rbrace>!"
by (clarsimp simp: validNF_def no_fail_def)
by (rule validNF; wpsimp)
lemma validNF_chain:
"\<lbrakk>\<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s; \<And>r s. R' r s \<Longrightarrow> R r s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>!"
by (fastforce simp: validNF_def valid_def no_fail_def Ball_def)
lemma validNF_case_prod[wp]:
"\<lbrakk> \<And>x y. validNF (P x y) (B x y) Q \<rbrakk> \<Longrightarrow> validNF (case_prod P v) (case_prod (\<lambda>x y. B x y) v) Q"
"\<lbrakk>\<And>x y. \<lbrace>P x y\<rbrace> B x y \<lbrace>Q\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>case v of (x, y) \<Rightarrow> P x y\<rbrace> case v of (x, y) \<Rightarrow> B x y \<lbrace>Q\<rbrace>!"
by (metis prod.exhaust split_conv)
lemma validE_NF_case_prod[wp]:
"\<lbrakk> \<And>a b. \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow>
\<lbrace>case x of (a, b) \<Rightarrow> P a b\<rbrace> case x of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!"
apply (clarsimp simp: validE_NF_alt_def)
apply (erule validNF_case_prod)
done
"\<lbrakk> \<And>a b. \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow>
\<lbrace>case x of (a, b) \<Rightarrow> P a b\<rbrace> case x of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!"
unfolding validE_NF_alt_def
by (erule validNF_case_prod)
lemma no_fail_is_validNF_True: "no_fail P s = (\<lbrace> P \<rbrace> s \<lbrace> \<lambda>_ _. True \<rbrace>!)"
lemma no_fail_is_validNF_True:
"no_fail P s = (\<lbrace> P \<rbrace> s \<lbrace> \<lambda>_ _. True \<rbrace>!)"
by (clarsimp simp: no_fail_def validNF_def valid_def)
@ -226,13 +234,17 @@ lemma validE_NF[intro?]:
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!"
by (clarsimp simp: validE_NF_def)
lemma validE_NFE:
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!; \<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
by (clarsimp simp: validE_NF_def)
lemma validE_NF_valid:
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>"
by (clarsimp simp: validE_NF_def)
by (rule validE_NFE)
lemma validE_NF_no_fail:
"\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
by (clarsimp simp: validE_NF_def)
by (rule validE_NFE)
lemma validE_NF_weaken_pre[wp_pre]:
"\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!"
@ -263,21 +275,13 @@ lemma validE_NF_chain:
lemma validE_NF_bind_wp[wp]:
"\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!"
apply (unfold validE_NF_alt_def bindE_def)
apply (rule validNF_bind [rotated])
apply assumption
apply (clarsimp simp: lift_def throwError_def split: sum.splits)
apply wpsimp
done
by (blast intro: validE_NF hoare_vcg_seqE no_fail_pre no_fail_bindE validE_validE_R validE_weaken
elim!: validE_NFE)
lemma validNF_catch[wp]:
"\<lbrakk>\<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <catch> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>!"
apply (unfold validE_NF_alt_def catch_def)
apply (rule validNF_bind [rotated])
apply assumption
apply (clarsimp simp: lift_def throwError_def split: sum.splits)
apply wp
done
unfolding validE_NF_alt_def catch_def lift_def throwError_def
by (clarsimp simp: validNF_return split: sum.splits elim!: validNF_bind[rotated])
lemma validNF_throwError[wp]:
"\<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
@ -285,15 +289,15 @@ lemma validNF_throwError[wp]:
lemma validNF_returnOk[wp]:
"\<lbrace>P e\<rbrace> returnOk e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp
by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp
lemma validNF_whenE[wp]:
"(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!"
unfolding whenE_def by clarsimp wp
unfolding whenE_def by wpsimp
lemma validNF_nobindE[wp]:
"\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r s. B s\<rbrace>,\<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!"
by clarsimp wp
by wpsimp
text \<open>
Set up triple rules for @{term validE_NF} so that we can use @{method wp} combinator rules.\<close>
@ -336,11 +340,10 @@ lemma validE_NF_handleE[wp]:
lemma validE_NF_condition[wp]:
"\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!\<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!"
apply rule
apply (drule validE_NF_valid)+
apply wp
apply (drule validE_NF_no_fail)+
apply (clarsimp simp: no_fail_def condition_def)
done
by (erule validE_NFE)+ (wpsimp wp: no_fail_condition validE_NF)
lemma hoare_assume_preNF:
"(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!"
by (metis validNF_alt_def)
end

311
lib/Monads/trace/Trace_VCG.thy
View File

@ -71,6 +71,18 @@ definition validE_E :: (* FIXME lib: this should be an abbreviation *)
"('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'a) tmonad \<Rightarrow> ('e \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace>/ _ /-, \<lbrace>_\<rbrace>") where
"\<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<equiv> validE P f (\<lambda>x y. True) Q"
(* These lemmas are useful to apply to rules to convert valid rules into a format suitable for wp. *)
lemma valid_make_schematic_post:
"(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>) \<Longrightarrow>
\<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>"
by (auto simp add: valid_def split: prod.splits)
lemma validE_make_schematic_post:
"(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>, \<lbrace> \<lambda>rv s. E s0 rv s \<rbrace>) \<Longrightarrow>
\<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')
\<and> (\<forall>rv s'. E s0 rv s' \<longrightarrow> E' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>, \<lbrace> E' \<rbrace>"
by (auto simp add: validE_def valid_def split: prod.splits sum.splits)
section \<open>Lemmas\<close>
@ -166,7 +178,9 @@ lemma seq_ext':
\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>"
by (metis bind_wp)
lemmas seq_ext = bind_wp[rotated]
lemma seq_ext:
"\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>"
by (fastforce simp: valid_def bind_def)
lemma seqE':
"\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow>
@ -305,6 +319,12 @@ lemma use_valid:
lemmas post_by_hoare = use_valid[rotated]
lemma use_valid_inv:
assumes step: "(r, s') \<in> fst (f s)"
assumes pres: "\<And>N. \<lbrace>\<lambda>s. N (P s) \<and> E s\<rbrace> f \<lbrace>\<lambda>rv s. N (P s)\<rbrace>"
shows "E s \<Longrightarrow> P s = P s'"
using use_valid[where f=f, OF step pres[where N="\<lambda>p. p = P s"]] by simp
lemma use_validE_norm:
"\<lbrakk> (Inr r', s') \<in> mres (B s); \<lbrace>P\<rbrace> B \<lbrace>Q\<rbrace>,\<lbrace> E \<rbrace>; P s \<rbrakk> \<Longrightarrow> Q r' s'"
unfolding validE_def valid_def by force
@ -328,6 +348,22 @@ lemma hoare_gen_asm:
"(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp add: valid_def)
lemmas hoare_gen_asm_single = hoare_gen_asm[where P'="\<top>", simplified pred_conj_def simp_thms]
lemma hoare_gen_asm_lk:
"(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>K P and P'\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp add: valid_def)
\<comment> \<open>Useful for forward reasoning, when P is known.
The first version allows weakening the precondition.\<close>
lemma hoare_gen_asm_spec':
"\<lbrakk> \<And>s. P s \<Longrightarrow> S \<and> R s; S \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
by (fastforce simp: valid_def)
lemma hoare_gen_asm_spec:
"\<lbrakk> \<And>s. P s \<Longrightarrow> S; S \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
by (rule hoare_gen_asm_spec'[where S=S and R=P]) simp
lemma hoare_conjI:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>"
unfolding valid_def by blast
@ -374,10 +410,24 @@ lemma hoare_case_option_wp:
\<Longrightarrow> \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>"
by (cases v) auto
lemma hoare_case_option_wp2:
"\<lbrakk> \<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace> \<rbrakk>
\<Longrightarrow> \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv s. case v of None \<Rightarrow> Q rv s | Some x \<Rightarrow> Q' x rv s\<rbrace>"
by (cases v) auto
(* Might be useful for forward reasoning, when P is known. *)
lemma hoare_when_cases:
"\<lbrakk>\<And>s. \<lbrakk>\<not>B; P s\<rbrakk> \<Longrightarrow> Q s; B \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> when B f \<lbrace>\<lambda>_. Q\<rbrace>"
by (cases B; simp add: valid_def return_def)
lemma hoare_vcg_prop:
"\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>"
by (simp add: valid_def)
lemma validE_eq_valid:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>,\<lbrace>\<lambda>rv. Q\<rbrace> = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>"
by (simp add: validE_def)
subsection \<open>@{const valid} and @{const validE}, @{const validE_R}, @{const validE_E}\<close>
@ -489,7 +539,7 @@ lemma hoare_seq_ext_nobindE:
"\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
by (erule seqE) (clarsimp simp: validE_def)
lemmas hoare_seq_ext_skip' = hoare_seq_ext[where Q'=Q and Q=Q for Q]
lemmas hoare_seq_ext_skip' = hoare_seq_ext[where B=C and C=C for C]
lemma hoare_chain:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<And>s. R s \<Longrightarrow> P s; \<And>rv s. Q rv s \<Longrightarrow> S rv s \<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>"
@ -507,6 +557,9 @@ lemma hoare_vcg_conj_lift:
unfolding valid_def
by fastforce
\<comment> \<open>A variant which works nicely with subgoals that do not contain schematics\<close>
lemmas hoare_vcg_conj_lift_pre_fix = hoare_vcg_conj_lift[where P=R and P'=R for R, simplified]
lemma hoare_vcg_conj_liftE1:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E\<rbrace>"
unfolding valid_def validE_R_def validE_def
@ -535,6 +588,30 @@ lemma hoare_vcg_all_lift_R:
"(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, -"
by (rule hoare_vcg_const_Ball_lift_R[where S=UNIV, simplified])
lemma hoare_vcg_imp_lift:
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
by (simp only: imp_conv_disj) (rule hoare_vcg_disj_lift)
lemma hoare_vcg_imp_lift':
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
by (wpsimp wp: hoare_vcg_imp_lift)
lemma hoare_vcg_imp_conj_lift[wp_comb]:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> Q' rv s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>"
by (auto simp: valid_def)
lemmas hoare_vcg_imp_conj_lift'[wp_unsafe] = hoare_vcg_imp_conj_lift[where Q'''="\<top>\<top>", simplified]
lemma hoare_absorb_imp:
"\<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
by (erule hoare_post_imp[rotated], blast)
lemma hoare_weaken_imp:
"\<lbrakk> \<And>rv s. Q rv s \<Longrightarrow> Q' rv s ; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> R rv s\<rbrace> \<rbrakk>
\<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
by (clarsimp simp: valid_def split_def)
lemma hoare_vcg_const_imp_lift:
"\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
by (cases P, simp_all add: hoare_vcg_prop)
@ -547,6 +624,8 @@ lemma hoare_weak_lift_imp:
"\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> P' s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> Q rv s\<rbrace>"
by (auto simp add: valid_def split_def)
lemmas hoare_vcg_weaken_imp = hoare_weaken_imp (* FIXME lib: eliminate *)
lemma hoare_vcg_ex_lift:
"\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>"
by (clarsimp simp: valid_def, blast)
@ -555,6 +634,17 @@ lemma hoare_vcg_ex_lift_R1:
"(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>, -"
by (fastforce simp: valid_def validE_R_def validE_def split: sum.splits)
lemma hoare_liftP_ext:
assumes "\<And>P x. m \<lbrace>\<lambda>s. P (f s x)\<rbrace>"
shows "m \<lbrace>\<lambda>s. P (f s)\<rbrace>"
unfolding valid_def
apply clarsimp
apply (erule subst[rotated, where P=P])
apply (rule ext)
apply (drule use_valid, rule assms, rule refl)
apply simp
done
(* for instantiations *)
lemma hoare_triv: "\<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>" .
lemma hoare_trivE: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" .
@ -575,11 +665,48 @@ lemma hoare_vcg_R_conj:
unfolding validE_R_def validE_def
by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits)
lemma hoare_lift_Pf_E_R:
"\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>, -; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>, - \<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. P (f s) s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>, -"
by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
lemma hoare_lift_Pf_E_E:
"\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m -, \<lbrace>\<lambda>_. P x\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s)\<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. P (f s) s\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>"
by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)
lemma hoare_vcg_const_Ball_lift_E_E:
"(\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f -,\<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>"
unfolding validE_E_def validE_def valid_def
by (fastforce split: sum.splits)
lemma hoare_vcg_all_liftE_E:
"(\<And>x. \<lbrace>P x\<rbrace> f -, \<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>"
by (rule hoare_vcg_const_Ball_lift_E_E[where S=UNIV, simplified])
lemma hoare_vcg_imp_liftE_E:
"\<lbrakk>\<lbrace>P'\<rbrace> f -, \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow>
\<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f -, \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
by (auto simp add: valid_def validE_E_def validE_def split_def split: sum.splits)
lemma hoare_vcg_ex_liftE:
"\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>"
by (fastforce simp: validE_def valid_def split: sum.splits)
lemma hoare_vcg_ex_liftE_E:
"\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f -,\<lbrace>E x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<exists>x. E x rv s\<rbrace>"
by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)
lemma hoare_post_imp_R:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
unfolding validE_R_def
by (erule hoare_post_impErr)
lemma hoare_post_imp_E:
"\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q'\<rbrace>; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>"
unfolding validE_E_def
by (rule hoare_post_impErr)
lemma hoare_post_comb_imp_conj:
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
by (wpsimp wp: hoare_vcg_conj_lift)
@ -596,8 +723,8 @@ lemma return_wp:
by(simp add: valid_def return_def mres_def)
lemma get_wp:
"\<lbrace>\<lambda>s. Q s s\<rbrace> get \<lbrace>Q\<rbrace>"
by (simp add: get_def valid_def mres_def)
"\<lbrace>\<lambda>s. P s s\<rbrace> get \<lbrace>P\<rbrace>"
by(simp add: valid_def split_def get_def)
lemma gets_wp:
"\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>"
@ -740,10 +867,53 @@ lemma whenE_wp:
"(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>"
unfolding whenE_def by clarsimp (wp returnOk_wp)
lemma unlessE_wp:
"(\<not> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then R () else Q\<rbrace> unlessE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>"
unfolding unlessE_def
by (wpsimp wp: returnOk_wp)
lemma maybeM_wp:
"(\<And>x. y = Some x \<Longrightarrow> \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>) \<Longrightarrow>
\<lbrace>\<lambda>s. (\<forall>x. y = Some x \<longrightarrow> P x s) \<and> (y = None \<longrightarrow> Q () s)\<rbrace> maybeM m y \<lbrace>Q\<rbrace>"
unfolding maybeM_def by (cases y; simp add: bind_def return_def valid_def)
lemma notM_wp:
"\<lbrace>P\<rbrace> m \<lbrace>\<lambda>c. Q (\<not> c)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> notM m \<lbrace>Q\<rbrace>"
unfolding notM_def by (fastforce simp: bind_def return_def valid_def)
lemma ifM_wp:
assumes [wp]: "\<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>" "\<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>"
assumes [wp]: "\<lbrace>A\<rbrace> P \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>" "\<lbrace>B\<rbrace> P \<lbrace>\<lambda>c s. \<not>c \<longrightarrow> R s\<rbrace>"
shows "\<lbrace>A and B\<rbrace> ifM P f g \<lbrace>S\<rbrace>"
unfolding ifM_def using assms
by (fastforce simp: bind_def valid_def split: if_splits)
lemma andM_wp:
assumes [wp]: "\<lbrace>Q'\<rbrace> B \<lbrace>Q\<rbrace>"
assumes [wp]: "\<lbrace>P\<rbrace> A \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>" "\<lbrace>P'\<rbrace> A \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> Q False s\<rbrace>"
shows "\<lbrace>P and P'\<rbrace> andM A B \<lbrace>Q\<rbrace>"
unfolding andM_def by (wp ifM_wp return_wp)
lemma orM_wp:
assumes [wp]: "\<lbrace>Q'\<rbrace> B \<lbrace>Q\<rbrace>"
assumes [wp]: "\<lbrace>P\<rbrace> A \<lbrace>\<lambda>c s. c \<longrightarrow> Q True s\<rbrace>" "\<lbrace>P'\<rbrace> A \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> Q' s\<rbrace>"
shows "\<lbrace>P and P'\<rbrace> orM A B \<lbrace>Q\<rbrace>"
unfolding orM_def by (wp ifM_wp return_wp)
lemma whenM_wp:
assumes [wp]: "\<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>"
assumes [wp]: "\<lbrace>A\<rbrace> P \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>" "\<lbrace>B\<rbrace> P \<lbrace>\<lambda>c s. \<not>c \<longrightarrow> S () s\<rbrace>"
shows "\<lbrace>A and B\<rbrace> whenM P f \<lbrace>S\<rbrace>"
unfolding whenM_def by (wp ifM_wp return_wp)
lemma hoare_K_bind[wp_split]:
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>"
by simp
lemma validE_K_bind[wp_split]:
"\<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>, \<lbrace> E \<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> K_bind x f \<lbrace> Q \<rbrace>, \<lbrace> E \<rbrace>"
by simp
lemma hoare_fun_app_wp:
"\<lbrace>P\<rbrace> f' x \<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f' $ x \<lbrace>Q'\<rbrace>"
"\<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
@ -771,6 +941,31 @@ lemma case_option_wpE:
lemmas liftME_E_E_wp[wp_split] = validE_validE_E [OF liftME_wp, simplified, OF validE_E_validE]
lemma assert_opt_wp:
"\<lbrace>\<lambda>s. x \<noteq> None \<longrightarrow> Q (the x) s\<rbrace> assert_opt x \<lbrace>Q\<rbrace>"
unfolding assert_opt_def
by (case_tac x; wpsimp wp: fail_wp return_wp)
lemma gets_the_wp:
"\<lbrace>\<lambda>s. (f s \<noteq> None) \<longrightarrow> Q (the (f s)) s\<rbrace> gets_the f \<lbrace>Q\<rbrace>"
unfolding gets_the_def
by (wp seq_ext gets_wp assert_opt_wp)
lemma gets_the_wp': (* FIXME: should prefer this one in [wp] *)
"\<lbrace>\<lambda>s. \<forall>rv. f s = Some rv \<longrightarrow> Q rv s\<rbrace> gets_the f \<lbrace>Q\<rbrace>"
unfolding gets_the_def
by (wpsimp wp: seq_ext gets_wp assert_opt_wp)
lemma gets_map_wp:
"\<lbrace>\<lambda>s. f s p \<noteq> None \<longrightarrow> Q (the (f s p)) s\<rbrace> gets_map f p \<lbrace>Q\<rbrace>"
unfolding gets_map_def
by (wpsimp wp: seq_ext gets_wp assert_opt_wp)
lemma gets_map_wp':
"\<lbrace>\<lambda>s. \<forall>rv. f s p = Some rv \<longrightarrow> Q rv s\<rbrace> gets_map f p \<lbrace>Q\<rbrace>"
unfolding gets_map_def
by (wpsimp wp: seq_ext gets_wp assert_opt_wp)
(* FIXME: make wp *)
lemma whenE_throwError_wp:
"\<lbrace>\<lambda>s. \<not>Q \<longrightarrow> P s\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv. P\<rbrace>, -"
@ -864,6 +1059,9 @@ lemmas [wp] = hoare_vcg_prop
failE_wp
assert_wp
state_assert_wp
assert_opt_wp
gets_the_wp
gets_map_wp'
liftE_wp
alternative_wp
alternativeE_R_wp
@ -873,6 +1071,7 @@ lemmas [wp] = hoare_vcg_prop
state_select_wp
condition_wp
conditionE_wp
maybeM_wp notM_wp ifM_wp andM_wp orM_wp whenM_wp
lemmas [wp_trip] = valid_is_triple validE_is_triple validE_E_is_triple validE_R_is_triple
@ -965,8 +1164,20 @@ lemmas hoare_wp_pred_conj_elims =
hoare_elim_pred_conjE2 hoare_elim_pred_conjE_R
subsection \<open>Bundles\<close>
bundle no_pre = hoare_pre [wp_pre del]
bundle classic_wp_pre = hoare_pre [wp_pre del]
all_classic_wp_combs[wp_comb del] all_classic_wp_combs[wp_comb]
text \<open>Miscellaneous lemmas on hoare triples\<close>
lemma hoare_pre_cases:
"\<lbrakk> \<lbrace>\<lambda>s. R s \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. \<not>R s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q\<rbrace>"
unfolding valid_def by fastforce
lemma hoare_vcg_mp:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<longrightarrow> Q' r s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>"
by (auto simp: valid_def split_def)
@ -988,6 +1199,12 @@ lemma hoare_list_case:
\<lbrace>case xs of [] \<Rightarrow> P1 | y#ys \<Rightarrow> P2 y ys\<rbrace> f (case xs of [] \<Rightarrow> f1 | y#ys \<Rightarrow> f2 y ys) \<lbrace>Q\<rbrace>"
by (cases xs; simp)
lemmas whenE_wps[wp_split] =
whenE_wp whenE_wp[THEN validE_validE_R] whenE_wp[THEN validE_validE_E]
lemmas unlessE_wps[wp_split] =
unlessE_wp unlessE_wp[THEN validE_validE_R] unlessE_wp[THEN validE_validE_E]
lemma hoare_use_eq:
assumes "\<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>"
assumes "\<And>f. \<lbrace>\<lambda>s. P f s\<rbrace> m \<lbrace>\<lambda>_ s. Q f s\<rbrace>"
@ -1043,12 +1260,58 @@ lemma hoare_drop_impE_E:
lemmas hoare_drop_imps = hoare_drop_imp hoare_drop_impE_R hoare_drop_impE_E
(*This is unsafe, but can be very useful when supplied as a comb rule.*)
lemma hoare_drop_imp_conj[wp_unsafe]:
"\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
\<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>"
by (auto simp: valid_def)
lemmas hoare_drop_imp_conj'[wp_unsafe] = hoare_drop_imp_conj[where Q'''="\<top>\<top>", simplified]
lemmas bindE_E_wp[wp_split] = validE_validE_E[OF hoare_vcg_seqE [OF validE_E_validE]]
lemma True_E_E[wp]:
"\<lbrace>\<top>\<rbrace> f -,\<lbrace>\<top>\<top>\<rbrace>"
by (auto simp: validE_E_def validE_def valid_def split: sum.splits)
lemma hoare_vcg_set_pred_lift:
assumes "\<And>P x. m \<lbrace> \<lambda>s. P (f x s) \<rbrace>"
shows "m \<lbrace> \<lambda>s. P {x. f x s} \<rbrace>"
using assms[where P="\<lambda>x . x"] assms[where P=Not] use_valid
by (fastforce simp: valid_def elim!: subst[rotated, where P=P])
lemma hoare_vcg_set_pred_lift_mono:
assumes f: "\<And>x. m \<lbrace> f x \<rbrace>"
assumes mono: "\<And>A B. A \<subseteq> B \<Longrightarrow> P A \<Longrightarrow> P B"
shows "m \<lbrace> \<lambda>s. P {x. f x s} \<rbrace>"
by (fastforce simp: valid_def elim!: mono[rotated] dest: use_valid[OF _ f])
text \<open>If a function contains an @{term assert}, or equivalent, then it might be
possible to strengthen the precondition of an already-proven hoare triple
@{text pos}, by additionally proving a side condition @{text neg}, that
violating some condition causes failure. The stronger hoare triple produced
by this theorem allows the precondition to assume that the condition is
satisfied.\<close>
lemma hoare_strengthen_pre_via_assert_forward:
assumes pos: "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
assumes rel: "\<And>s. S s \<longrightarrow> P s \<or> N s"
assumes neg: "\<lbrace> N \<rbrace> f \<lbrace> \<bottom>\<bottom> \<rbrace>"
shows "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
apply (rule hoare_weaken_pre)
apply (rule hoare_strengthen_post)
apply (rule hoare_vcg_disj_lift[OF pos neg])
by (auto simp: rel)
text \<open>Like @{thm hoare_strengthen_pre_via_assert_forward}, strengthen a precondition
by proving a side condition that the negation of that condition would cause
failure. This version is intended for backward reasoning. Apply it to a goal to
obtain a stronger precondition after proving the side condition.\<close>
lemma hoare_strengthen_pre_via_assert_backward:
assumes neg: "\<lbrace> Not \<circ> E \<rbrace> f \<lbrace> \<bottom>\<bottom> \<rbrace>"
assumes pos: "\<lbrace> P and E \<rbrace> f \<lbrace> Q \<rbrace>"
shows "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
by (rule hoare_strengthen_pre_via_assert_forward[OF pos _ neg], simp)
subsection \<open>Strongest postcondition rules\<close>
@ -1080,4 +1343,44 @@ lemma hoare_returnOk_sp:
"\<lbrace>P\<rbrace> returnOk x \<lbrace>\<lambda>rv s. rv = x \<and> P s\<rbrace>, \<lbrace>Q\<rbrace>"
by (simp add: valid_def validE_def returnOk_def return_def mres_def)
\<comment> \<open>For forward reasoning in Hoare proofs, these lemmas allow us to step over the
left-hand-side of monadic bind, while keeping the same precondition.\<close>
named_theorems forward_inv_step_rules
lemmas hoare_forward_inv_step_nobind[forward_inv_step_rules] =
hoare_seq_ext_nobind[where B=A and A=A for A, rotated]
lemmas hoare_seq_ext_skip[forward_inv_step_rules] =
hoare_seq_ext[where B="\<lambda>_. A" and A=A for A, rotated]
lemmas hoare_forward_inv_step_nobindE_valid[forward_inv_step_rules] =
hoare_seq_ext_nobindE[where B=A and A=A and E="\<lambda>_. C" and C="\<lambda>_. C" for A C,
simplified validE_eq_valid, rotated]
lemmas hoare_forward_inv_step_valid[forward_inv_step_rules] =
hoare_vcg_seqE[where B="\<lambda>_. A" and A=A and E="\<lambda>_. C" and C="\<lambda>_. C" for A C,
simplified validE_eq_valid, rotated]
lemmas hoare_forward_inv_step_nobindE[forward_inv_step_rules] =
hoare_seq_ext_nobindE[where B=A and A=A for A, rotated]
lemmas hoare_seq_ext_skipE[forward_inv_step_rules] =
hoare_vcg_seqE[where B="\<lambda>_. A" and A=A for A, rotated]
lemmas hoare_forward_inv_step_nobindE_validE_E[forward_inv_step_rules] =
hoare_forward_inv_step_nobindE[where C="\<top>\<top>", simplified validE_E_def[symmetric]]
lemmas hoare_forward_inv_step_validE_E[forward_inv_step_rules] =
hoare_seq_ext_skipE[where C="\<top>\<top>", simplified validE_E_def[symmetric]]
lemmas hoare_forward_inv_step_nobindE_validE_R[forward_inv_step_rules] =
hoare_forward_inv_step_nobindE[where E="\<top>\<top>", simplified validE_R_def[symmetric]]
lemmas hoare_forward_inv_step_validE_R[forward_inv_step_rules] =
hoare_seq_ext_skipE[where E="\<top>\<top>", simplified validE_R_def[symmetric]]
method forward_inv_step uses wp simp =
rule forward_inv_step_rules, solves \<open>wpsimp wp: wp simp: simp\<close>
end