From f3dca6865cd1541fa25af15ee48c822709ea4373 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 11 Oct 2018 14:50:00 +1100 Subject: [PATCH] lib: option (reader) monad syntax and gets_map operator --- lib/Monad_WP/Less_Monad_Syntax.thy | 31 +++++++++++++++++++++ lib/Monad_WP/NonDetMonad.thy | 9 ++++++ lib/Monad_WP/NonDetMonadVCG.thy | 44 ++++++++++++++++++++++++++++++ lib/Monad_WP/OptionMonad.thy | 12 ++++++-- lib/Monad_WP/OptionMonadND.thy | 24 +++++++--------- lib/NonDetMonadLemmaBucket.thy | 23 ---------------- 6 files changed, 103 insertions(+), 40 deletions(-) create mode 100644 lib/Monad_WP/Less_Monad_Syntax.thy diff --git a/lib/Monad_WP/Less_Monad_Syntax.thy b/lib/Monad_WP/Less_Monad_Syntax.thy new file mode 100644 index 000000000..fe1b02009 --- /dev/null +++ b/lib/Monad_WP/Less_Monad_Syntax.thy @@ -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] \ '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 \ *) +notation (output) + bind_do (infixr ">>=" 54) + +(* enable pretty printing for do { .. } syntax globally *) +translations + "CONST bind_do" <= "CONST bind" + +end diff --git a/lib/Monad_WP/NonDetMonad.thy b/lib/Monad_WP/NonDetMonad.thy index f7ac442aa..9548c845b 100644 --- a/lib/Monad_WP/NonDetMonad.thy +++ b/lib/Monad_WP/NonDetMonad.thy @@ -232,6 +232,15 @@ definition "gets_the f \ gets f >>= assert_opt" +text \ + 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. +\ +definition + gets_map :: "('s \ 'a \ 'b option) \ 'a \ ('s, 'b) nondet_monad" where + "gets_map f p \ gets f >>= (\m. assert_opt (m p))" + + subsection {* The Monad Laws *} text {* A more expanded definition of @{text bind} *} diff --git a/lib/Monad_WP/NonDetMonadVCG.thy b/lib/Monad_WP/NonDetMonadVCG.thy index 6d47d93ac..fb8e5535a 100644 --- a/lib/Monad_WP/NonDetMonadVCG.thy +++ b/lib/Monad_WP/NonDetMonadVCG.thy @@ -804,6 +804,22 @@ lemma no_fail_returnOK [simp, wp]: "no_fail \ (returnOk x)" by (simp add: returnOk_def) +lemma no_fail_bind [wp]: + assumes f: "no_fail P f" + assumes g: "\rv. no_fail (R rv) (g rv)" + assumes v: "\Q\ f \R\" + shows "no_fail (P and Q) (f >>= (\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: "\\x. True\ fail \Q\" @@ -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]: + "\\s. x \ None \ Q (the x) s\ assert_opt x \Q\" + by (case_tac x, (simp add: assert_opt_def | wp)+) + +lemma gets_the_wp[wp]: + "\\s. (f s \ None) \ Q (the (f s)) s\ gets_the f \Q\" + by (unfold gets_the_def, wp) + +lemma gets_the_wp': + "\\s. \rv. f s = Some rv \ Q rv s\ gets_the f \Q\" + unfolding gets_the_def by wpsimp + +lemma gets_map_wp: + "\\s. f s p \ None \ Q (the (f s p)) s\ gets_map f p \Q\" + unfolding gets_map_def by wpsimp + +lemma gets_map_wp'[wp]: + "\\s. \rv. f s p = Some rv \ Q rv s\ gets_map f p \Q\" + unfolding gets_map_def by wpsimp + +lemma no_fail_gets_map[wp]: + "no_fail (\s. f s p \ None) (gets_map f p)" + unfolding gets_map_def by wpsimp + section "validNF Rules" diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monad_WP/OptionMonad.thy index b7fe29470..9906819d4 100644 --- a/lib/Monad_WP/OptionMonad.thy +++ b/lib/Monad_WP/OptionMonad.thy @@ -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 \ 'a option" @@ -44,6 +46,10 @@ definition where "f |>> g \ \s. case f s of None \ None | Some x \ 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: "\r r'. \I r s; C r s; B r s = Some r'\ \ (r',r) \ M" assumes step: "\r r'. \I r s; C r s; B r s = Some r'\ \ I r' s" - assumes fail: "\r r'. \I r s; C r s; B r s = None\ \ Q None" + assumes fail: "\r. \I r s; C r s; B r s = None\ \ Q None" assumes final: "\r. \I r s; \C r s\ \ Q (Some r)" shows "Q (owhile C B r s)" proof - diff --git a/lib/Monad_WP/OptionMonadND.thy b/lib/Monad_WP/OptionMonadND.thy index d962982cf..340f5dab8 100644 --- a/lib/Monad_WP/OptionMonadND.thy +++ b/lib/Monad_WP/OptionMonadND.thy @@ -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 \ ('e \ ('s,'a) lookup) \ ('s, 'a) lookup" (infix "" 10) where - "f handler \ - DO x \ f; - case x of - Inr b \ oreturn b - | Inl e \ handler e - OD" + "f handler \ do { + x \ f; + case x of Inr b \ oreturn b | Inl e \ handler e + }" definition odrop :: "('s, 'e + 'a) lookup \ ('s, 'a) lookup" where - "odrop f \ - DO x \ f; - case x of - Inr b \ oreturn b - | Inl e \ ofail - OD" + "odrop f \ do { + x \ f; + case x of Inr b \ oreturn b | Inl e \ ofail + }" definition osequence_x :: "('s, 'a) lookup list \ ('s, unit) lookup" where - "osequence_x xs \ foldr (\x y. DO _ <- x; y OD) xs (oreturn ())" + "osequence_x xs \ foldr (\x y. do { x; y }) xs (oreturn ())" definition osequence :: "('s, 'a) lookup list \ ('s, 'a list) lookup" diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index 64a7e9a26..2bde7be74 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/lib/NonDetMonadLemmaBucket.thy @@ -73,22 +73,6 @@ lemma hoare_vcg_if_lift: \R\ f \\rv. if P then X rv else Y rv\" by (auto simp: valid_def split_def) - -lemma no_fail_bind [wp]: - assumes f: "no_fail P f" - assumes g: "\rv. no_fail (R rv) (g rv)" - assumes v: "\Q\ f \R\" - shows "no_fail (P and Q) (f >>= (\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: "\x. \Q x\ m \\_. P x\" assumes f: "\P. \\s. P (f s)\ m \\_ s. P (f s)\" @@ -1112,13 +1096,6 @@ lemma let_into_return: "(let f = x in m f) = (do f \ return x; m f od)" by simp -lemma assert_opt_wp [wp]: "\\s. (x \ None) \ Q (the x) s\ assert_opt x \Q\" - by (case_tac x, (simp add: assert_opt_def | wp)+) - -lemma gets_the_wp [wp]: - "\\s. (f s \ None) \ Q (the (f s)) s\ gets_the f \Q\" - by (unfold gets_the_def, wp) - definition injection_handler :: "('a \ 'b) \ ('s, 'a + 'c) nondet_monad \ ('s, 'b + 'c) nondet_monad"