1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8 * Contributions by: 9 * 2012 Lars Noschinski <noschinl@in.tum.de> 10 * Option monad while loop formalisation. 11 *) 12 13theory OptionMonad (* FIXME: this is really a Reader_Option_Monad *) 14 imports 15 Lib (* FIXME: reduce dependencies *) 16 Less_Monad_Syntax 17begin 18 19type_synonym ('s,'a) lookup = "'s \<Rightarrow> 'a option" 20 21text \<open>Similar to map_option but the second function returns option as well\<close> 22definition 23 opt_map :: "('s,'a) lookup \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> ('s,'b) lookup" (infixl "|>" 54) 24where 25 "f |> g \<equiv> \<lambda>s. case f s of None \<Rightarrow> None | Some x \<Rightarrow> g x" 26 27abbreviation opt_map_Some :: "('s \<rightharpoonup> 'a) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 's \<rightharpoonup> 'b" (infixl "||>" 54) where 28 "f ||> g \<equiv> f |> (Some \<circ> g)" 29lemmas opt_map_Some_def = opt_map_def 30 31lemma opt_map_cong [fundef_cong]: 32 "\<lbrakk> f = f'; \<And>v s. f s = Some v \<Longrightarrow> g v = g' v\<rbrakk> \<Longrightarrow> f |> g = f' |> g'" 33 by (rule ext) (simp add: opt_map_def split: option.splits) 34 35lemma in_opt_map_eq: 36 "((f |> g) s = Some v) = (\<exists>v'. f s = Some v' \<and> g v' = Some v)" 37 by (simp add: opt_map_def split: option.splits) 38 39lemma opt_mapE: 40 "\<lbrakk> (f |> g) s = Some v; \<And>v'. \<lbrakk>f s = Some v'; g v' = Some v \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 41 by (auto simp: in_opt_map_eq) 42 43lemma opt_map_upd_None: 44 "f(x := None) |> g = (f |> g)(x := None)" 45 by (auto simp: opt_map_def) 46 47lemma opt_map_upd_Some: 48 "f(x \<mapsto> v) |> g = (f |> g)(x := g v)" 49 by (auto simp: opt_map_def) 50 51lemmas opt_map_upd[simp] = opt_map_upd_None opt_map_upd_Some 52 53declare None_upd_eq[simp] 54 55(* None_upd_eq[simp] so that this pattern is by simp. Hopefully not too much slowdown. *) 56lemma "\<lbrakk> (f |> g) x = None; g v = None \<rbrakk> \<Longrightarrow> f(x \<mapsto> v) |> g = f |> g" 57 by simp 58 59definition 60 obind :: "('s,'a) lookup \<Rightarrow> ('a \<Rightarrow> ('s,'b) lookup) \<Rightarrow> ('s,'b) lookup" (infixl "|>>" 53) 61where 62 "f |>> g \<equiv> \<lambda>s. case f s of None \<Rightarrow> None | Some x \<Rightarrow> g x s" 63 64(* Enable "do { .. }" syntax *) 65adhoc_overloading 66 Monad_Syntax.bind obind 67 68definition 69 "ofail = K None" 70 71definition 72 "oreturn = K o Some" 73 74definition 75 "oassert P \<equiv> if P then oreturn () else ofail" 76 77definition oapply :: "'a \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" 78 where 79 "oapply x \<equiv> \<lambda>s. s x" 80 81text \<open> 82 If the result can be an exception. 83 Corresponding bindE would be analogous to lifting in NonDetMonad. 84\<close> 85 86definition 87 "oreturnOk x = K (Some (Inr x))" 88 89definition 90 "othrow e = K (Some (Inl e))" 91 92definition 93 "oguard G \<equiv> (\<lambda>s. if G s then Some () else None)" 94 95definition 96 "ocondition c L R \<equiv> (\<lambda>s. if c s then L s else R s)" 97 98definition 99 "oskip \<equiv> oreturn ()" 100 101text \<open>Monad laws\<close> 102lemma oreturn_bind [simp]: "(oreturn x |>> f) = f x" 103 by (auto simp add: oreturn_def obind_def K_def) 104 105lemma obind_return [simp]: "(m |>> oreturn) = m" 106 by (auto simp add: oreturn_def obind_def K_def split: option.splits) 107 108lemma obind_assoc: 109 "(m |>> f) |>> g = m |>> (\<lambda>x. f x |>> g)" 110 by (auto simp add: oreturn_def obind_def K_def split: option.splits) 111 112 113text \<open>Binding fail\<close> 114 115lemma obind_fail [simp]: 116 "f |>> (\<lambda>_. ofail) = ofail" 117 by (auto simp add: ofail_def obind_def K_def split: option.splits) 118 119lemma ofail_bind [simp]: 120 "ofail |>> m = ofail" 121 by (auto simp add: ofail_def obind_def K_def split: option.splits) 122 123 124 125text \<open>Function package setup\<close> 126lemma opt_bind_cong [fundef_cong]: 127 "\<lbrakk> f = f'; \<And>v s. f' s = Some v \<Longrightarrow> g v s = g' v s \<rbrakk> \<Longrightarrow> f |>> g = f' |>> g'" 128 by (rule ext) (simp add: obind_def split: option.splits) 129 130lemma opt_bind_cong_apply [fundef_cong]: 131 "\<lbrakk> f s = f' s; \<And>v. f' s = Some v \<Longrightarrow> g v s = g' v s \<rbrakk> \<Longrightarrow> (f |>> g) s = (f' |>> g') s" 132 by (simp add: obind_def split: option.splits) 133 134lemma oassert_bind_cong [fundef_cong]: 135 "\<lbrakk> P = P'; P' \<Longrightarrow> m = m' \<rbrakk> \<Longrightarrow> oassert P |>> m = oassert P' |>> m'" 136 by (auto simp: oassert_def) 137 138lemma oassert_bind_cong_apply [fundef_cong]: 139 "\<lbrakk> P = P'; P' \<Longrightarrow> m () s = m' () s \<rbrakk> \<Longrightarrow> (oassert P |>> m) s = (oassert P' |>> m') s" 140 by (auto simp: oassert_def) 141 142lemma oreturn_bind_cong [fundef_cong]: 143 "\<lbrakk> x = x'; m x' = m' x' \<rbrakk> \<Longrightarrow> oreturn x |>> m = oreturn x' |>> m'" 144 by simp 145 146lemma oreturn_bind_cong_apply [fundef_cong]: 147 "\<lbrakk> x = x'; m x' s = m' x' s \<rbrakk> \<Longrightarrow> (oreturn x |>> m) s = (oreturn x' |>> m') s" 148 by simp 149 150lemma oreturn_bind_cong2 [fundef_cong]: 151 "\<lbrakk> x = x'; m x' = m' x' \<rbrakk> \<Longrightarrow> (oreturn $ x) |>> m = (oreturn $ x') |>> m'" 152 by simp 153 154lemma oreturn_bind_cong2_apply [fundef_cong]: 155 "\<lbrakk> x = x'; m x' s = m' x' s \<rbrakk> \<Longrightarrow> ((oreturn $ x) |>> m) s = ((oreturn $ x') |>> m') s" 156 by simp 157 158lemma ocondition_cong [fundef_cong]: 159"\<lbrakk>c = c'; \<And>s. c' s \<Longrightarrow> l s = l' s; \<And>s. \<not>c' s \<Longrightarrow> r s = r' s\<rbrakk> 160 \<Longrightarrow> ocondition c l r = ocondition c' l' r'" 161 by (auto simp: ocondition_def) 162 163 164text \<open>Decomposition\<close> 165 166lemma ocondition_K_true [simp]: 167 "ocondition (\<lambda>_. True) T F = T" 168 by (simp add: ocondition_def) 169 170lemma ocondition_K_false [simp]: 171 "ocondition (\<lambda>_. False) T F = F" 172 by (simp add: ocondition_def) 173 174lemma ocondition_False: 175 "\<lbrakk> \<And>s. \<not> P s \<rbrakk> \<Longrightarrow> ocondition P L R = R" 176 by (rule ext, clarsimp simp: ocondition_def) 177 178lemma ocondition_True: 179 "\<lbrakk> \<And>s. P s \<rbrakk> \<Longrightarrow> ocondition P L R = L" 180 by (rule ext, clarsimp simp: ocondition_def) 181 182lemma in_oreturn [simp]: 183 "(oreturn x s = Some v) = (v = x)" 184 by (auto simp: oreturn_def K_def) 185 186lemma oreturnE: 187 "\<lbrakk>oreturn x s = Some v; v = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 188 by simp 189 190lemma in_ofail [simp]: 191 "ofail s \<noteq> Some v" 192 by (auto simp: ofail_def K_def) 193 194lemma ofailE: 195 "ofail s = Some v \<Longrightarrow> P" 196 by simp 197 198lemma in_oassert_eq [simp]: 199 "(oassert P s = Some v) = P" 200 by (simp add: oassert_def) 201 202lemma oassert_True [simp]: 203 "oassert True = oreturn ()" 204 by (simp add: oassert_def) 205 206lemma oassert_False [simp]: 207 "oassert False = ofail" 208 by (simp add: oassert_def) 209 210lemma oassertE: 211 "\<lbrakk> oassert P s = Some v; P \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" 212 by simp 213 214lemma in_obind_eq: 215 "((f |>> g) s = Some v) = (\<exists>v'. f s = Some v' \<and> g v' s = Some v)" 216 by (simp add: obind_def split: option.splits) 217 218lemma obind_eqI: 219 "\<lbrakk> f s = f s' ; \<And>x. f s = Some x \<Longrightarrow> g x s = g' x s' \<rbrakk> \<Longrightarrow> obind f g s = obind f g' s'" 220 by (simp add: obind_def split: option.splits) 221 222(* full form of obind_eqI; the second equality makes more sense flipped here, as we end up 223 with "f s = Some x ; f s' = f s" preventing "Some x = ..." *) 224lemma obind_eqI_full: 225 "\<lbrakk> f s = f s' ; \<And>x. \<lbrakk> f s = Some x; f s' = f s \<rbrakk> \<Longrightarrow> g x s = g' x s' \<rbrakk> 226 \<Longrightarrow> obind f g s = obind f g' s'" 227 by (drule sym[where s="f s"]) (* prevent looping *) 228 (clarsimp simp: obind_def split: option.splits) 229 230lemma obindE: 231 "\<lbrakk> (f |>> g) s = Some v; 232 \<And>v'. \<lbrakk>f s = Some v'; g v' s = Some v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 233 by (auto simp: in_obind_eq) 234 235lemma in_othrow_eq [simp]: 236 "(othrow e s = Some v) = (v = Inl e)" 237 by (auto simp: othrow_def K_def) 238 239lemma othrowE: 240 "\<lbrakk>othrow e s = Some v; v = Inl e \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 241 by simp 242 243lemma in_oreturnOk_eq [simp]: 244 "(oreturnOk x s = Some v) = (v = Inr x)" 245 by (auto simp: oreturnOk_def K_def) 246 247lemma oreturnOkE: 248 "\<lbrakk>oreturnOk x s = Some v; v = Inr x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 249 by simp 250 251lemmas omonadE [elim!] = 252 opt_mapE obindE oreturnE ofailE othrowE oreturnOkE oassertE 253 254lemma in_opt_map_Some_eq: 255 "((f ||> g) x = Some y) = (\<exists>v. f x = Some v \<and> g v = y)" 256 by (simp add: in_opt_map_eq) 257 258lemma in_opt_map_None_eq[simp]: 259 "((f ||> g) x = None) = (f x = None)" 260 by (simp add: opt_map_def split: option.splits) 261 262lemma oreturn_comp[simp]: 263 "oreturn x \<circ> f = oreturn x" 264 by (simp add: oreturn_def K_def o_def) 265 266lemma ofail_comp[simp]: 267 "ofail \<circ> f = ofail" 268 by (auto simp: ofail_def K_def) 269 270lemma oassert_comp[simp]: 271 "oassert P \<circ> f = oassert P" 272 by (simp add: oassert_def) 273 274lemma fail_apply[simp]: 275 "ofail s = None" 276 by (simp add: ofail_def K_def) 277 278lemma oassert_apply[simp]: 279 "oassert P s = (if P then Some () else None)" 280 by (simp add: oassert_def) 281 282lemma oreturn_apply[simp]: 283 "oreturn x s = Some x" 284 by simp 285 286lemma oapply_apply[simp]: 287 "oapply x s = s x" 288 by (simp add: oapply_def) 289 290lemma obind_comp_dist: 291 "obind f g o h = obind (f o h) (\<lambda>x. g x o h)" 292 by (auto simp: obind_def split: option.splits) 293 294lemma if_comp_dist: 295 "(if P then f else g) o h = (if P then f o h else g o h)" 296 by auto 297 298 299section \<open>"While" loops over option monad.\<close> 300 301text \<open> 302 This is an inductive definition of a while loop over the plain option monad 303 (without passing through a state) 304\<close> 305 306inductive_set 307 option_while' :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a option) \<Rightarrow> 'a option rel" 308 for C B 309where 310 final: "\<not> C r \<Longrightarrow> (Some r, Some r) \<in> option_while' C B" 311 | fail: "\<lbrakk> C r; B r = None \<rbrakk> \<Longrightarrow> (Some r, None) \<in> option_while' C B" 312 | step: "\<lbrakk> C r; B r = Some r'; (Some r', sr'') \<in> option_while' C B \<rbrakk> 313 \<Longrightarrow> (Some r, sr'') \<in> option_while' C B" 314 315definition 316 "option_while C B r \<equiv> 317 (if (\<exists>s. (Some r, s) \<in> option_while' C B) then 318 (THE s. (Some r, s) \<in> option_while' C B) else None)" 319 320lemma option_while'_inj: 321 assumes "(s,s') \<in> option_while' C B" "(s, s'') \<in> option_while' C B" 322 shows "s' = s''" 323 using assms by (induct rule: option_while'.induct) (auto elim: option_while'.cases) 324 325lemma option_while'_inj_step: 326 "\<lbrakk> C s; B s = Some s'; (Some s, t) \<in> option_while' C B ; (Some s', t') \<in> option_while' C B \<rbrakk> \<Longrightarrow> t = t'" 327 by (metis option_while'.step option_while'_inj) 328 329lemma option_while'_THE: 330 assumes "(Some r, sr') \<in> option_while' C B" 331 shows "(THE s. (Some r, s) \<in> option_while' C B) = sr'" 332 using assms by (blast dest: option_while'_inj) 333 334lemma option_while_simps: 335 "\<not> C s \<Longrightarrow> option_while C B s = Some s" 336 "C s \<Longrightarrow> B s = None \<Longrightarrow> option_while C B s = None" 337 "C s \<Longrightarrow> B s = Some s' \<Longrightarrow> option_while C B s = option_while C B s'" 338 "(Some s, ss') \<in> option_while' C B \<Longrightarrow> option_while C B s = ss'" 339 using option_while'_inj_step[of C s B s'] 340 by (auto simp: option_while_def option_while'_THE 341 intro: option_while'.intros 342 dest: option_while'_inj 343 elim: option_while'.cases) 344 345lemma option_while_rule: 346 assumes "option_while C B s = Some s'" 347 assumes "I s" 348 assumes istep: "\<And>s s'. C s \<Longrightarrow> I s \<Longrightarrow> B s = Some s' \<Longrightarrow> I s'" 349 shows "I s' \<and> \<not> C s'" 350proof - 351 { fix ss ss' assume "(ss, ss') \<in> option_while' C B" "ss = Some s" "ss' = Some s'" 352 then have ?thesis using \<open>I s\<close> 353 by (induct arbitrary: s) (auto intro: istep) } 354 then show ?thesis using assms(1) 355 by (auto simp: option_while_def option_while'_THE split: if_split_asm) 356qed 357 358lemma option_while'_term: 359 assumes "I r" 360 assumes "wf M" 361 assumes step_less: "\<And>r r'. \<lbrakk>I r; C r; B r = Some r'\<rbrakk> \<Longrightarrow> (r',r) \<in> M" 362 assumes step_I: "\<And>r r'. \<lbrakk>I r; C r; B r = Some r'\<rbrakk> \<Longrightarrow> I r'" 363 obtains sr' where "(Some r, sr') \<in> option_while' C B" 364 apply atomize_elim 365 using assms(2,1) 366proof induct 367 case (less r) 368 show ?case 369 proof (cases "C r" "B r" rule: bool.exhaust[case_product option.exhaust]) 370 case (True_Some r') 371 then have "(r',r) \<in> M" "I r'" 372 by (auto intro: less step_less step_I) 373 then obtain sr' where "(Some r', sr') \<in> option_while' C B" 374 by atomize_elim (rule less) 375 then have "(Some r, sr') \<in> option_while' C B" 376 using True_Some by (auto intro: option_while'.intros) 377 then show ?thesis .. 378 qed (auto intro: option_while'.intros) 379qed 380 381lemma option_while_rule': 382 assumes "option_while C B s = ss'" 383 assumes "wf M" 384 assumes "I (Some s)" 385 assumes less: "\<And>s s'. C s \<Longrightarrow> I (Some s) \<Longrightarrow> B s = Some s' \<Longrightarrow> (s', s) \<in> M" 386 assumes step: "\<And>s s'. C s \<Longrightarrow> I (Some s) \<Longrightarrow> B s = Some s' \<Longrightarrow> I (Some s')" 387 assumes final: "\<And>s. C s \<Longrightarrow> I (Some s) \<Longrightarrow> B s = None \<Longrightarrow> I None" 388 shows "I ss' \<and> (case ss' of Some s' \<Rightarrow> \<not> C s' | _ \<Rightarrow> True)" 389proof - 390 define ss where "ss \<equiv> Some s" 391 obtain ss1' where "(Some s, ss1') \<in> option_while' C B" 392 using assms(3,2,4,5) by (rule option_while'_term) 393 then have *: "(ss, ss') \<in> option_while' C B" using \<open>option_while C B s = ss'\<close> 394 by (auto simp: option_while_simps ss_def) 395 show ?thesis 396 proof (cases ss') 397 case (Some s') with * ss_def show ?thesis using \<open>I _\<close> 398 by (induct arbitrary:s) (auto intro: step) 399 next 400 case None with * ss_def show ?thesis using \<open>I _\<close> 401 by (induct arbitrary:s) (auto intro: step final) 402 qed 403qed 404 405section \<open>Lift @{term option_while} to the @{typ "('a,'s) lookup"} monad\<close> 406 407definition 408 owhile :: "('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('s,'a) lookup) \<Rightarrow> 'a \<Rightarrow> ('s,'a) lookup" 409where 410 "owhile c b a \<equiv> \<lambda>s. option_while (\<lambda>a. c a s) (\<lambda>a. b a s) a" 411 412lemma owhile_unroll: 413 "owhile C B r = ocondition (C r) (B r |>> owhile C B) (oreturn r)" 414 by (auto simp: ocondition_def obind_def oreturn_def owhile_def 415 option_while_simps K_def split: option.split) 416 417text \<open>rule for terminating loops\<close> 418 419lemma owhile_rule: 420 assumes "I r s" 421 assumes "wf M" 422 assumes less: "\<And>r r'. \<lbrakk>I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> (r',r) \<in> M" 423 assumes step: "\<And>r r'. \<lbrakk>I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> I r' s" 424 assumes fail: "\<And>r. \<lbrakk>I r s; C r s; B r s = None\<rbrakk> \<Longrightarrow> Q None" 425 assumes final: "\<And>r. \<lbrakk>I r s; \<not>C r s\<rbrakk> \<Longrightarrow> Q (Some r)" 426 shows "Q (owhile C B r s)" 427proof - 428 let ?rs' = "owhile C B r s" 429 have "(case ?rs' of Some r \<Rightarrow> I r s | _ \<Rightarrow> Q None) 430 \<and> (case ?rs' of Some r' \<Rightarrow> \<not> C r' s | _ \<Rightarrow> True)" 431 by (rule option_while_rule'[where B="\<lambda>r. B r s" and s=r, OF _ \<open>wf _\<close>]) 432 (auto simp: owhile_def intro: assms) 433 then show ?thesis by (auto intro: final split: option.split_asm) 434qed 435 436end 437