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