lib: option (reader) monad syntax and gets_map operator
This commit is contained in:
parent
7a48f4c8c7
commit
f3dca6865c
|
@ -0,0 +1,31 @@
|
|||
(*
|
||||
* Copyright 2018, Data61, CSIRO
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(DATA61_BSD)
|
||||
*)
|
||||
|
||||
theory Less_Monad_Syntax (* use instead of HOL-Library.Monad_Syntax *)
|
||||
imports "HOL-Library.Monad_Syntax"
|
||||
begin
|
||||
|
||||
(* remove >> from Monad_Syntax, clashes with word shift *)
|
||||
no_syntax
|
||||
"_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
|
||||
|
||||
(* remove input version of >>= from Monad_Syntax, avoid clash with NonDetMonad *)
|
||||
no_notation
|
||||
Monad_Syntax.bind (infixr ">>=" 54)
|
||||
|
||||
(* use ASCII >>= instead of \<bind> *)
|
||||
notation (output)
|
||||
bind_do (infixr ">>=" 54)
|
||||
|
||||
(* enable pretty printing for do { .. } syntax globally *)
|
||||
translations
|
||||
"CONST bind_do" <= "CONST bind"
|
||||
|
||||
end
|
|
@ -232,6 +232,15 @@ definition
|
|||
"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 {* The Monad Laws *}
|
||||
|
||||
text {* A more expanded definition of @{text bind} *}
|
||||
|
|
|
@ -804,6 +804,22 @@ lemma no_fail_returnOK [simp, wp]:
|
|||
"no_fail \<top> (returnOk x)"
|
||||
by (simp add: returnOk_def)
|
||||
|
||||
lemma no_fail_bind [wp]:
|
||||
assumes f: "no_fail P f"
|
||||
assumes g: "\<And>rv. no_fail (R rv) (g rv)"
|
||||
assumes v: "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>"
|
||||
shows "no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
|
||||
apply (clarsimp simp: no_fail_def bind_def)
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply (erule no_failD [OF f])
|
||||
apply clarsimp
|
||||
apply (drule (1) use_valid [OF _ v])
|
||||
apply (drule no_failD [OF g])
|
||||
apply simp
|
||||
done
|
||||
|
||||
|
||||
text {* Empty results implies non-failure *}
|
||||
|
||||
lemma empty_fail_modify [simp, wp]:
|
||||
|
@ -862,6 +878,10 @@ lemma empty_fail_mk_ef:
|
|||
"empty_fail (mk_ef o m)"
|
||||
by (simp add: empty_fail_def mk_ef_def)
|
||||
|
||||
lemma empty_fail_gets_map[simp]:
|
||||
"empty_fail (gets_map f p)"
|
||||
unfolding gets_map_def by simp
|
||||
|
||||
subsection "Failure"
|
||||
|
||||
lemma fail_wp: "\<lbrace>\<lambda>x. True\<rbrace> fail \<lbrace>Q\<rbrace>"
|
||||
|
@ -1803,6 +1823,30 @@ lemma select_throwError_wp:
|
|||
by (simp add: bind_def throwError_def return_def select_def validE_E_def
|
||||
validE_def valid_def)
|
||||
|
||||
lemma assert_opt_wp[wp]:
|
||||
"\<lbrace>\<lambda>s. x \<noteq> None \<longrightarrow> Q (the x) s\<rbrace> assert_opt x \<lbrace>Q\<rbrace>"
|
||||
by (case_tac x, (simp add: assert_opt_def | wp)+)
|
||||
|
||||
lemma gets_the_wp[wp]:
|
||||
"\<lbrace>\<lambda>s. (f s \<noteq> None) \<longrightarrow> Q (the (f s)) s\<rbrace> gets_the f \<lbrace>Q\<rbrace>"
|
||||
by (unfold gets_the_def, wp)
|
||||
|
||||
lemma gets_the_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
|
||||
|
||||
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
|
||||
|
||||
lemma gets_map_wp'[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
|
||||
|
||||
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
|
||||
|
||||
|
||||
section "validNF Rules"
|
||||
|
||||
|
|
|
@ -14,8 +14,10 @@
|
|||
* Option monad while loop formalisation.
|
||||
*)
|
||||
|
||||
theory OptionMonad
|
||||
imports "../Lib" (* FIXME: reduce dependencies *)
|
||||
theory OptionMonad (* FIXME: this is really a Reader_Option_Monad *)
|
||||
imports
|
||||
"../Lib" (* FIXME: reduce dependencies *)
|
||||
"Less_Monad_Syntax"
|
||||
begin
|
||||
|
||||
type_synonym ('s,'a) lookup = "'s \<Rightarrow> 'a option"
|
||||
|
@ -44,6 +46,10 @@ definition
|
|||
where
|
||||
"f |>> g \<equiv> \<lambda>s. case f s of None \<Rightarrow> None | Some x \<Rightarrow> g x s"
|
||||
|
||||
(* Enable "do { .. }" syntax *)
|
||||
adhoc_overloading
|
||||
Monad_Syntax.bind obind
|
||||
|
||||
definition
|
||||
"ofail = K None"
|
||||
|
||||
|
@ -331,7 +337,7 @@ lemma owhile_rule:
|
|||
assumes "wf M"
|
||||
assumes less: "\<And>r r'. \<lbrakk>I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> (r',r) \<in> M"
|
||||
assumes step: "\<And>r r'. \<lbrakk>I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> I r' s"
|
||||
assumes fail: "\<And>r r'. \<lbrakk>I r s; C r s; B r s = None\<rbrakk> \<Longrightarrow> Q None"
|
||||
assumes fail: "\<And>r. \<lbrakk>I r s; C r s; B r s = None\<rbrakk> \<Longrightarrow> Q None"
|
||||
assumes final: "\<And>r. \<lbrakk>I r s; \<not>C r s\<rbrakk> \<Longrightarrow> Q (Some r)"
|
||||
shows "Q (owhile C B r s)"
|
||||
proof -
|
||||
|
|
|
@ -16,7 +16,7 @@ imports
|
|||
NonDetMonadLemmas
|
||||
begin
|
||||
|
||||
(* FIXME: better concrete syntax? *)
|
||||
(* FIXME: remove this syntax, standardise on do {..} instead *)
|
||||
(* Syntax defined here so we can reuse NonDetMonad definitions *)
|
||||
syntax
|
||||
"_doO" :: "[dobinds, 'a] => 'a" ("(DO (_);// (_)//OD)" 100)
|
||||
|
@ -36,28 +36,24 @@ definition
|
|||
ocatch :: "('s,('e + 'a)) lookup \<Rightarrow> ('e \<Rightarrow> ('s,'a) lookup) \<Rightarrow> ('s, 'a) lookup"
|
||||
(infix "<ocatch>" 10)
|
||||
where
|
||||
"f <ocatch> handler \<equiv>
|
||||
DO x \<leftarrow> f;
|
||||
case x of
|
||||
Inr b \<Rightarrow> oreturn b
|
||||
| Inl e \<Rightarrow> handler e
|
||||
OD"
|
||||
"f <ocatch> handler \<equiv> do {
|
||||
x \<leftarrow> f;
|
||||
case x of Inr b \<Rightarrow> oreturn b | Inl e \<Rightarrow> handler e
|
||||
}"
|
||||
|
||||
|
||||
definition
|
||||
odrop :: "('s, 'e + 'a) lookup \<Rightarrow> ('s, 'a) lookup"
|
||||
where
|
||||
"odrop f \<equiv>
|
||||
DO x \<leftarrow> f;
|
||||
case x of
|
||||
Inr b \<Rightarrow> oreturn b
|
||||
| Inl e \<Rightarrow> ofail
|
||||
OD"
|
||||
"odrop f \<equiv> do {
|
||||
x \<leftarrow> f;
|
||||
case x of Inr b \<Rightarrow> oreturn b | Inl e \<Rightarrow> ofail
|
||||
}"
|
||||
|
||||
definition
|
||||
osequence_x :: "('s, 'a) lookup list \<Rightarrow> ('s, unit) lookup"
|
||||
where
|
||||
"osequence_x xs \<equiv> foldr (\<lambda>x y. DO _ <- x; y OD) xs (oreturn ())"
|
||||
"osequence_x xs \<equiv> foldr (\<lambda>x y. do { x; y }) xs (oreturn ())"
|
||||
|
||||
definition
|
||||
osequence :: "('s, 'a) lookup list \<Rightarrow> ('s, 'a list) lookup"
|
||||
|
|
|
@ -73,22 +73,6 @@ lemma hoare_vcg_if_lift:
|
|||
\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P then X rv else Y rv\<rbrace>"
|
||||
by (auto simp: valid_def split_def)
|
||||
|
||||
|
||||
lemma no_fail_bind [wp]:
|
||||
assumes f: "no_fail P f"
|
||||
assumes g: "\<And>rv. no_fail (R rv) (g rv)"
|
||||
assumes v: "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>"
|
||||
shows "no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
|
||||
apply (clarsimp simp: no_fail_def bind_def)
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply (erule no_failD [OF f])
|
||||
apply clarsimp
|
||||
apply (drule (1) use_valid [OF _ v])
|
||||
apply (drule no_failD [OF g])
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma hoare_lift_Pf2:
|
||||
assumes P: "\<And>x. \<lbrace>Q x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>"
|
||||
assumes f: "\<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>"
|
||||
|
@ -1112,13 +1096,6 @@ lemma let_into_return:
|
|||
"(let f = x in m f) = (do f \<leftarrow> return x; m f od)"
|
||||
by simp
|
||||
|
||||
lemma assert_opt_wp [wp]: "\<lbrace>\<lambda>s. (x \<noteq> None) \<longrightarrow> Q (the x) s\<rbrace> assert_opt x \<lbrace>Q\<rbrace>"
|
||||
by (case_tac x, (simp add: assert_opt_def | wp)+)
|
||||
|
||||
lemma gets_the_wp [wp]:
|
||||
"\<lbrace>\<lambda>s. (f s \<noteq> None) \<longrightarrow> Q (the (f s)) s\<rbrace> gets_the f \<lbrace>Q\<rbrace>"
|
||||
by (unfold gets_the_def, wp)
|
||||
|
||||
definition
|
||||
injection_handler :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s, 'a + 'c) nondet_monad
|
||||
\<Rightarrow> ('s, 'b + 'c) nondet_monad"
|
||||
|
|
Loading…
Reference in New Issue