1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Option monad syntax plus the connection between the option monad and the nondet monad *) 8 9theory OptionMonadND 10imports 11 NonDetMonadLemmas 12 OptionMonad 13begin 14 15(* FIXME: remove this syntax, standardise on do {..} instead *) 16(* Syntax defined here so we can reuse NonDetMonad definitions *) 17syntax 18 "_doO" :: "[dobinds, 'a] => 'a" ("(DO (_);// (_)//OD)" 100) 19 20translations 21 "_doO (_dobinds b bs) e" == "_doO b (_doO bs e)" 22 "_doO (_nobind b) e" == "b |>> (CONST K_bind e)" 23 "DO x <- a; e OD" == "a |>> (\<lambda>x. e)" 24 25 26definition 27 ogets :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b option)" 28where 29 "ogets f \<equiv> (\<lambda>s. Some (f s))" 30 31definition 32 ocatch :: "('s,('e + 'a)) lookup \<Rightarrow> ('e \<Rightarrow> ('s,'a) lookup) \<Rightarrow> ('s, 'a) lookup" 33 (infix "<ocatch>" 10) 34where 35 "f <ocatch> handler \<equiv> do { 36 x \<leftarrow> f; 37 case x of Inr b \<Rightarrow> oreturn b | Inl e \<Rightarrow> handler e 38 }" 39 40 41definition 42 odrop :: "('s, 'e + 'a) lookup \<Rightarrow> ('s, 'a) lookup" 43where 44 "odrop f \<equiv> do { 45 x \<leftarrow> f; 46 case x of Inr b \<Rightarrow> oreturn b | Inl e \<Rightarrow> ofail 47 }" 48 49definition 50 osequence_x :: "('s, 'a) lookup list \<Rightarrow> ('s, unit) lookup" 51where 52 "osequence_x xs \<equiv> foldr (\<lambda>x y. do { x; y }) xs (oreturn ())" 53 54definition 55 osequence :: "('s, 'a) lookup list \<Rightarrow> ('s, 'a list) lookup" 56where 57 "osequence xs \<equiv> let mcons = (\<lambda>p q. p |>> (\<lambda>x. q |>> (\<lambda>y. oreturn (x#y)))) 58 in foldr mcons xs (oreturn [])" 59 60definition 61 omap :: "('a \<Rightarrow> ('s,'b) lookup) \<Rightarrow> 'a list \<Rightarrow> ('s, 'b list) lookup" 62where 63 "omap f xs \<equiv> osequence (map f xs)" 64 65definition 66 opt_cons :: "'a option \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "o#" 65) 67where 68 "opt_cons x xs \<equiv> case x of None \<Rightarrow> xs | Some x' \<Rightarrow> x' # xs" 69 70lemmas monad_simps = 71 gets_the_def bind_def assert_def assert_opt_def 72 simpler_gets_def fail_def return_def 73 74lemma gets_the_opt_map: 75 "gets_the (f |> g) = do x \<leftarrow> gets_the f; assert_opt (g x) od" 76 by (rule ext) (simp add: monad_simps opt_map_def split: option.splits) 77 78lemma gets_the_opt_o: 79 "gets_the (f |> Some o g) = do x \<leftarrow> gets_the f; return (g x) od" 80 by (simp add: gets_the_opt_map assert_opt_Some) 81 82lemma gets_the_obind: 83 "gets_the (f |>> g) = gets_the f >>= (\<lambda>x. gets_the (g x))" 84 by (rule ext) (simp add: monad_simps obind_def split: option.splits) 85 86lemma gets_the_return: 87 "gets_the (oreturn x) = return x" 88 by (simp add: monad_simps oreturn_def K_def) 89 90lemma gets_the_fail: 91 "gets_the ofail = fail" 92 by (simp add: monad_simps ofail_def K_def) 93 94lemma gets_the_returnOk: 95 "gets_the (oreturnOk x) = returnOk x" 96 by (simp add: monad_simps K_def oreturnOk_def returnOk_def) 97 98lemma gets_the_throwError: 99 "gets_the (othrow e) = throwError e" 100 by (simp add: monad_simps othrow_def throwError_def K_def) 101 102lemma gets_the_assert: 103 "gets_the (oassert P) = assert P" 104 by (simp add: oassert_def assert_def gets_the_fail gets_the_return) 105 106lemma gets_the_if_distrib: 107 "gets_the (if P then f else g) = (if P then gets_the f else gets_the g)" 108 by simp 109 110lemma gets_the_oapply_comp: 111 "gets_the (oapply x \<circ> f) = gets_map f x" 112 by (fastforce simp: gets_map_def gets_the_def o_def gets_def) 113 114lemma gets_the_Some: 115 "gets_the (\<lambda>_. Some x) = return x" 116 by (simp add: gets_the_def assert_opt_Some) 117 118lemma fst_assert_opt: 119 "fst (assert_opt opt s) = (if opt = None then {} else {(the opt,s)})" 120 by (clarsimp simp: assert_opt_def fail_def return_def split: option.split) 121 122 123lemmas omonad_simps [simp] = 124 gets_the_opt_map assert_opt_Some gets_the_obind 125 gets_the_return gets_the_fail gets_the_returnOk 126 gets_the_throwError gets_the_assert gets_the_Some 127 gets_the_oapply_comp 128 129lemmas in_omonad = bind_eq_Some_conv in_obind_eq in_opt_map_eq Let_def 130 131 132section "Relation between option monad loops and non-deterministic monad loops." 133 134(* Option monad whileLoop formalisation thanks to Lars Noschinski <noschinl@in.tum.de>. *) 135 136lemma gets_the_conv: 137 "(gets_the B s) = (case B s of Some r' \<Rightarrow> ({(r', s)}, False) | _ \<Rightarrow> ({}, True))" 138 by (auto simp: gets_the_def gets_def get_def bind_def return_def fail_def assert_opt_def split: option.splits) 139 140lemma gets_the_loop_terminates: 141 "whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s 142 \<longleftrightarrow> (\<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s))" (is "?L \<longleftrightarrow> ?R") 143proof 144 assume ?L then show ?R 145 proof (induct rule: whileLoop_terminates.induct[case_names 1 2]) 146 case (2 r s) then show ?case 147 by (cases "B r s") (auto simp: gets_the_conv intro: option_while'.intros) 148 qed (auto intro: option_while'.intros) 149next 150 assume ?R then show ?L 151 proof (elim exE) 152 fix rs' assume "(Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" 153 then have "whileLoop_terminates C (\<lambda>a. gets_the (B a)) (the (Some r)) s" 154 by induct (auto intro: whileLoop_terminates.intros simp: gets_the_conv) 155 then show ?thesis by simp 156 qed 157qed 158 159lemma gets_the_whileLoop: 160 fixes C :: "'a \<Rightarrow> 's \<Rightarrow> bool" 161 shows "whileLoop C (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r)" 162proof - 163 { fix r s r' s' assume "(Some (r,s), Some (r', s')) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" 164 then have "s = s' \<and> (Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" 165 by (induct "Some (r, s)" "Some (r', s')" arbitrary: r s) 166 (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } 167 note wl'_Inl = this 168 169 { fix r s assume "(Some (r,s), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" 170 then have "(Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" 171 by (induct "Some (r, s)" "None :: (('a \<times> 's) option)" arbitrary: r s) 172 (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } 173 note wl'_Inr = this 174 175 { fix r s r' assume "(Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" 176 then have "(Some (r,s), Some (r',s)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" 177 by (induct "Some r" "Some r'" arbitrary: r) 178 (auto intro: whileLoop_results.intros simp: gets_the_conv) } 179 note option_while'_Some = this 180 181 { fix r s assume "(Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" 182 then have "(Some (r,s), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" 183 by (induct "Some r" "None :: 'a option" arbitrary: r) 184 (auto intro: whileLoop_results.intros simp: gets_the_conv) } 185 note option_while'_None = this 186 187 have "\<And>s. owhile C B r s = None 188 \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = ({}, True)" 189 by (auto simp: whileLoop_def owhile_def option_while_def option_while'_THE gets_the_loop_terminates 190 split: if_split_asm dest: option_while'_None wl'_Inl option_while'_inj) 191 moreover 192 have "\<And>s r'. owhile C B r s = Some r' 193 \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = ({(r', s)}, False)" 194 by (auto simp: whileLoop_def owhile_def option_while_def option_while'_THE gets_the_loop_terminates 195 split: if_split_asm dest: wl'_Inl wl'_Inr option_while'_inj intro: option_while'_Some) 196 ultimately 197 show ?thesis 198 by (auto simp: fun_eq_iff gets_the_conv split: option.split) 199qed 200 201end 202