Skip to content

Commit

Permalink
lib/monads: resync trace monad with nondet
Browse files Browse the repository at this point in the history
Signed-off-by: Corey Lewis <[email protected]>
  • Loading branch information
corlewis committed Jul 17, 2024
1 parent e429ff6 commit f00bbb7
Show file tree
Hide file tree
Showing 6 changed files with 54 additions and 15 deletions.
12 changes: 6 additions & 6 deletions lib/Monads/nondet/Nondet_Reader_Option.thy
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,11 @@ lemma gets_the_obind:
"gets_the (f |>> g) = gets_the f >>= (\<lambda>x. gets_the (g x))"
by (rule ext) (simp add: monad_simps obind_def split: option.splits)

lemma gets_the_Some_get[simp]:
lemma gets_the_Some_return:
"gets_the (\<lambda>_. Some x) = return x"
by (simp add: gets_the_def assert_opt_Some)

lemma gets_the_Some_get:
"gets_the Some = get"
by (clarsimp simp: gets_the_def gets_def assert_opt_Some)

Expand Down Expand Up @@ -115,10 +119,6 @@ lemma gets_the_oapply_comp:
"gets_the (oapply x \<circ> f) = gets_map f x"
by (fastforce simp: gets_map_def gets_the_def o_def gets_def)

lemma gets_the_Some:
"gets_the (\<lambda>_. Some x) = return x"
by (simp add: gets_the_def assert_opt_Some)

lemma gets_the_oapply2_comp:
"gets_the (oapply2 y x \<circ> f) = gets_map (swp f y) x"
by (clarsimp simp: gets_map_def gets_the_def o_def gets_def)
Expand All @@ -136,7 +136,7 @@ lemma fst_assert_opt:
lemmas omonad_simps [simp] =
gets_the_opt_map assert_opt_Some gets_the_obind
gets_the_return gets_the_fail gets_the_returnOk
gets_the_throwError gets_the_assert gets_the_Some
gets_the_throwError gets_the_assert gets_the_Some_return gets_the_Some_get
gets_the_oapply_comp


Expand Down
4 changes: 2 additions & 2 deletions lib/Monads/nondet/Nondet_VCG.thy
Original file line number Diff line number Diff line change
Expand Up @@ -227,11 +227,11 @@ lemma return_inv[iff]:

lemma hoare_modifyE_var:
"\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<lambda>_ s. Q s\<rbrace>"
by(simp add: valid_def modify_def put_def get_def bind_def)
by (simp add: valid_def modify_def put_def get_def bind_def)

lemma hoare_if:
"\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> \<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> if P' then f else g \<lbrace>Q\<rbrace>"
by (simp add: valid_def)
by simp

lemma hoare_pre_subst:
"\<lbrakk> P = P'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"
Expand Down
14 changes: 14 additions & 0 deletions lib/Monads/trace/Trace_More_RG.thy
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,20 @@ lemma assertE_tsp:
"\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> assertE Q \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q \<and> P s0 s\<rbrace>,\<lbrace>E\<rbrace>"
by (wpsimp wp: assertE_wp)

lemma select_inv_rg:
"\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> select S \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
by wpsimp

lemma assert_inv_rg:
"\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> assert Q \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
unfolding assert_def
by (cases Q) wpsimp+

lemma assert_opt_inv_rg:
"\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> assert_opt Q \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
unfolding assert_opt_def
by (cases Q) (wp | simp)+

lemma case_options_weak_twp:
"\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk>
\<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
Expand Down
16 changes: 16 additions & 0 deletions lib/Monads/trace/Trace_RG.thy
Original file line number Diff line number Diff line change
Expand Up @@ -362,6 +362,22 @@ lemma rg_FalseE[simp]:
"\<lbrace>\<bottom>\<bottom>\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> = prefix_closed f"
by (simp add: validI_def validIE_def)

lemma rg_modifyE_var:
"\<lbrakk> \<And>s0 s. P s0 s \<Longrightarrow> Q s0 (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> modify f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>"
by (simp add: validI_def modify_def put_def get_def bind_def prefix_closed_def rely_def)

lemma rg_if:
"\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> if P' then f else g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
by simp

lemma rg_pre_subst:
"\<lbrakk> P = P'; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
by (erule subst)

lemma rg_post_subst:
"\<lbrakk> Q = Q'; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>"
by (erule subst)

lemma rg_post_imp:
"\<lbrakk>\<And>v s0 s. Q' v s0 s \<Longrightarrow> Q v s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
by (simp add: validI_def)
Expand Down
19 changes: 14 additions & 5 deletions lib/Monads/trace/Trace_Reader_Option.thy
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,14 @@ lemma gets_the_obind:
"gets_the (f |>> g) = gets_the f >>= (\<lambda>x. gets_the (g x))"
by (rule ext) (simp add: monad_simps obind_def split: option.splits)

lemma gets_the_Some_return:
"gets_the (\<lambda>_. Some x) = return x"
by (simp add: gets_the_def assert_opt_Some)

lemma gets_the_Some_get:
"gets_the Some = get"
by (clarsimp simp: gets_the_def gets_def assert_opt_Some)

lemma gets_the_return:
"gets_the (oreturn x) = return x"
by (simp add: monad_simps oreturn_def)
Expand All @@ -94,6 +102,11 @@ lemma gets_the_assert:
"gets_the (oassert P) = assert P"
by (simp add: oassert_def assert_def gets_the_fail gets_the_return)

lemma gets_the_ostate_assert:
"gets_the (ostate_assert P) = state_assert P"
by (clarsimp simp: ostate_assert_def state_assert_def gets_the_obind gets_the_Some_get
gets_the_assert)

lemma gets_the_assert_opt:
"gets_the (oassert_opt P) = assert_opt P"
by (simp add: oassert_opt_def assert_opt_def gets_the_return gets_the_fail split: option.splits)
Expand All @@ -106,10 +119,6 @@ lemma gets_the_oapply_comp:
"gets_the (oapply x \<circ> f) = gets_map f x"
by (fastforce simp: gets_map_def gets_the_def o_def gets_def)

lemma gets_the_Some:
"gets_the (\<lambda>_. Some x) = return x"
by (simp add: gets_the_def assert_opt_Some)

lemma gets_the_oapply2_comp:
"gets_the (oapply2 y x \<circ> f) = gets_map (swp f y) x"
by (clarsimp simp: gets_map_def gets_the_def o_def gets_def)
Expand All @@ -127,7 +136,7 @@ lemma mres_assert_opt:
lemmas omonad_simps [simp] =
gets_the_opt_map assert_opt_Some gets_the_obind
gets_the_return gets_the_fail gets_the_returnOk
gets_the_throwError gets_the_assert gets_the_Some
gets_the_throwError gets_the_assert gets_the_Some_return gets_the_Some_get
gets_the_oapply_comp


Expand Down
4 changes: 2 additions & 2 deletions lib/Monads/trace/Trace_VCG.thy
Original file line number Diff line number Diff line change
Expand Up @@ -223,11 +223,11 @@ lemma return_inv[iff]:

lemma hoare_modifyE_var:
"\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<lambda>_ s. Q s\<rbrace>"
by(simp add: valid_def modify_def put_def get_def bind_def mres_def)
by (simp add: valid_def modify_def put_def get_def bind_def mres_def)

lemma hoare_if:
"\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> \<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> if P' then f else g \<lbrace>Q\<rbrace>"
by (simp add: valid_def)
by simp

lemma hoare_pre_subst:
"\<lbrakk> P = P'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"
Expand Down

0 comments on commit f00bbb7

Please sign in to comment.