1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6theory TraceMonadLemmas
7imports TraceMonadVCG
8begin
9
10lemma mapM_Cons:
11  "mapM f (x # xs) = do
12    y \<leftarrow> f x;
13    ys \<leftarrow> mapM f xs;
14    return (y # ys)
15  od"
16  and mapM_Nil:
17  "mapM f [] = return []"
18  by (simp_all add: mapM_def sequence_def)
19
20lemma mapM_x_Cons:
21  "mapM_x f (x # xs) = do
22    y \<leftarrow> f x;
23    mapM_x f xs
24  od"
25  and mapM_x_Nil:
26  "mapM_x f [] = return ()"
27  by (simp_all add: mapM_x_def sequence_x_def)
28
29lemma mapM_append:
30  "mapM f (xs @ ys) = (do
31    fxs \<leftarrow> mapM f xs;
32    fys \<leftarrow> mapM f ys;
33    return (fxs @ fys)
34  od)"
35  by (induct xs, simp_all add: mapM_Cons mapM_Nil bind_assoc)
36
37lemma mapM_x_append:
38  "mapM_x f (xs @ ys) = (do
39    x \<leftarrow> mapM_x f xs;
40    mapM_x f ys
41  od)"
42  by (induct xs, simp_all add: mapM_x_Cons mapM_x_Nil bind_assoc)
43
44lemma mapM_map:
45  "mapM f (map g xs) = mapM (f o g) xs"
46  by (induct xs; simp add: mapM_Nil mapM_Cons)
47
48lemma mapM_x_map:
49  "mapM_x f (map g xs) = mapM_x (f o g) xs"
50  by (induct xs; simp add: mapM_x_Nil mapM_x_Cons)
51
52primrec
53  repeat_n :: "nat \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad"
54where
55    "repeat_n 0 f = return ()"
56  | "repeat_n (Suc n) f = do f; repeat_n n f od"
57
58lemma repeat_n_mapM_x:
59  "repeat_n n f = mapM_x (\<lambda>_. f) (replicate n ())"
60  by (induct n, simp_all add: mapM_x_Cons mapM_x_Nil)
61
62definition
63  repeat :: "('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad"
64where
65  "repeat f = do n \<leftarrow> select UNIV; repeat_n n f od"
66
67definition
68  env_step :: "('s,unit) tmonad"
69where
70  "env_step =
71  (do
72    s' \<leftarrow> select UNIV;
73    put_trace_elem (Env, s');
74    put s'
75  od)"
76
77abbreviation
78  "env_n_steps n \<equiv> repeat_n n env_step"
79
80lemma elem_select_bind:
81  "(tr, res) \<in> (do x \<leftarrow> select S; f x od) s
82    = (\<exists>x \<in> S. (tr, res) \<in> f x s)"
83  by (simp add: bind_def select_def)
84
85lemma select_bind_UN:
86  "(do x \<leftarrow> select S; f x od) = (\<lambda>s. \<Union>x \<in> S. f x s)"
87  by (rule ext, auto simp: elem_select_bind)
88
89lemma select_early:
90  "S \<noteq> {}
91    \<Longrightarrow> do x \<leftarrow> f; y \<leftarrow> select S; g x y od
92        = do y \<leftarrow> select S; x \<leftarrow> f; g x y od"
93  apply (simp add: bind_def select_def Sigma_def)
94  apply (rule ext)
95  apply (fastforce elim: rev_bexI image_eqI[rotated] split: tmres.split_asm)
96  done
97
98lemma repeat_n_choice:
99  "S \<noteq> {}
100    \<Longrightarrow> repeat_n n (do x \<leftarrow> select S; f x od)
101        = (do xs \<leftarrow> select {xs. set xs \<subseteq> S \<and> length xs = n}; mapM_x f xs od)"
102  apply (induct n; simp?)
103   apply (simp add: select_def bind_def mapM_x_Nil cong: conj_cong)
104  apply (simp add: select_early bind_assoc)
105  apply (subst select_early)
106   apply simp
107   apply (auto intro: exI[where x="replicate n xs" for n xs])[1]
108  apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind)
109  apply (simp only: conj_comms[where Q="length xs = n" for xs n])
110  apply (simp only: ex_simps[symmetric] conj_assoc length_Suc_conv, simp)
111  apply (auto simp: mapM_x_Cons)
112  done
113
114lemma repeat_choice:
115  "S \<noteq> {}
116    \<Longrightarrow> repeat (do x \<leftarrow> select S; f x od)
117        = (do xs \<leftarrow> select {xs. set xs \<subseteq> S}; mapM_x f xs od)"
118  apply (simp add: repeat_def repeat_n_choice)
119  apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind)
120  done
121
122lemma put_trace_append:
123  "put_trace (xs @ ys) = do put_trace ys; put_trace xs od"
124  by (induct xs; simp add: bind_assoc)
125
126lemma put_trace_elem_put_comm:
127  "do y \<leftarrow> put_trace_elem x; put s od
128    = do y \<leftarrow> put s; put_trace_elem x od"
129  by (simp add: put_def put_trace_elem_def bind_def insert_commute)
130
131lemma put_trace_put_comm:
132  "do y \<leftarrow> put_trace xs; put s od
133    = do y \<leftarrow> put s; put_trace xs od"
134  apply (rule sym; induct xs; simp)
135  apply (simp add: bind_assoc put_trace_elem_put_comm)
136  apply (simp add: bind_assoc[symmetric])
137  done
138
139lemma mapM_x_comm:
140  "(\<forall>x \<in> set xs. do y \<leftarrow> g; f x od = do y \<leftarrow> f x; g od)
141    \<Longrightarrow> do y \<leftarrow> g; mapM_x f xs od = do y \<leftarrow> mapM_x f xs; g od"
142  apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons)
143  apply (simp add: bind_assoc[symmetric], simp add: bind_assoc)
144  done
145
146lemma mapM_x_split:
147  "(\<forall>x \<in> set xs. \<forall>y \<in> set xs. do z \<leftarrow> g y; f x od = do (z :: unit) \<leftarrow> f x; g y od)
148    \<Longrightarrow> mapM_x (\<lambda>x. do z \<leftarrow> f x; g x od) xs = do y \<leftarrow> mapM_x f xs; mapM_x g xs od"
149  apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons bind_assoc)
150  apply (subst bind_assoc[symmetric], subst mapM_x_comm[where f=f and g="g x" for x])
151   apply simp
152  apply (simp add: bind_assoc)
153  done
154
155lemma mapM_x_put:
156  "mapM_x put xs = unless (xs = []) (put (last xs))"
157  apply (induct xs rule: rev_induct)
158   apply (simp add: mapM_x_Nil unless_def when_def)
159  apply (simp add: mapM_x_append mapM_x_Cons mapM_x_Nil)
160  apply (simp add: bind_def unless_def when_def put_def return_def)
161  done
162
163lemma put_trace_mapM_x:
164  "put_trace xs = mapM_x put_trace_elem (rev xs)"
165  by (induct xs; simp add: mapM_x_Nil mapM_x_append mapM_x_Cons)
166
167lemma rev_surj:
168  "surj rev"
169  by (rule_tac f=rev in surjI, simp)
170
171lemma select_image:
172  "select (f ` S) = do x \<leftarrow> select S; return (f x) od"
173  by (auto simp add: bind_def select_def return_def Sigma_def)
174
175lemma env_steps_repeat:
176  "env_steps = repeat env_step"
177  apply (simp add: env_step_def repeat_choice env_steps_def
178                   select_early)
179  apply (simp add: put_trace_elem_put_comm)
180  apply (simp add: mapM_x_split put_trace_elem_put_comm put_trace_put_comm
181                   mapM_x_put)
182  apply (simp add: put_trace_mapM_x rev_map mapM_x_map o_def)
183  apply (subst rev_surj[symmetric], simp add: select_image bind_assoc)
184  apply (rule arg_cong2[where f=bind, OF refl ext])
185  apply (simp add: bind_def get_def put_def unless_def when_def return_def)
186  apply (simp add: last_st_tr_def hd_map hd_rev)
187  done
188
189lemma repeat_n_plus:
190  "repeat_n (n + m) f = do repeat_n n f; repeat_n m f od"
191  by (induct n; simp add: bind_assoc)
192
193lemma repeat_eq_twice[simp]:
194  "(do x \<leftarrow> repeat f; repeat f od) = repeat f"
195  apply (simp add: repeat_def select_early)
196  apply (simp add: bind_assoc repeat_n_plus[symmetric, simplified])
197  apply (simp add: bind_def select_def Sigma_def)
198  apply (rule ext, fastforce intro: exI[where x=0])
199  done
200
201lemmas bind_then_eq = arg_cong2[where f=bind, OF _ refl]
202lemmas repeat_eq_twice_then[simp]
203    = repeat_eq_twice[THEN bind_then_eq, simplified bind_assoc]
204
205lemmas env_steps_eq_twice[simp]
206    = repeat_eq_twice[where f=env_step, folded env_steps_repeat]
207lemmas env_steps_eq_twice_then[simp]
208    = env_steps_eq_twice[THEN bind_then_eq, simplified bind_assoc]
209
210lemmas mapM_collapse_append = mapM_append[symmetric, THEN bind_then_eq,
211    simplified bind_assoc, simplified]
212
213lemma prefix_closed_mapM[rule_format, wp_split]:
214  "(\<forall>x \<in> set xs. prefix_closed (f x)) \<Longrightarrow> prefix_closed (mapM f xs)"
215  apply (induct xs)
216   apply (simp add: mapM_def sequence_def)
217  apply (clarsimp simp: mapM_Cons)
218  apply (intro prefix_closed_bind allI; clarsimp)
219  done
220
221lemma modify_id:
222  "modify id = return ()"
223  by (simp add: modify_def get_def bind_def put_def return_def)
224
225lemma modify_modify:
226  "(do x \<leftarrow> modify f; modify (g x) od) = modify (g () o f)"
227  by (simp add: bind_def simpler_modify_def)
228
229lemmas modify_modify_bind = arg_cong2[where f=bind,
230  OF modify_modify refl, simplified bind_assoc]
231
232lemma select_single:
233  "select {x} = return x"
234  by (simp add: select_def return_def)
235
236lemma put_then_get[unfolded K_bind_def]:
237  "do put s; get od = do put s; return s od"
238  by (simp add: put_def bind_def get_def return_def)
239
240lemmas put_then_get_then
241    = put_then_get[THEN bind_then_eq, simplified bind_assoc return_bind]
242
243lemmas bind_promote_If
244    = if_distrib[where f="\<lambda>f. bind f g" for g]
245      if_distrib[where f="\<lambda>g. bind f g" for f]
246
247lemma bind_promote_If2:
248  "do x \<leftarrow> f; if P then g x else h x od
249    = (if P then bind f g else bind f h)"
250  by simp
251
252lemma exec_put_trace[unfolded K_bind_def]:
253  "(do put_trace xs; f od) s
254    = (\<Union>n \<in> {n. 0 < n \<and> n \<le> length xs}. {(drop n xs, Incomplete)})
255        \<union> ((\<lambda>(a, b). (a @ xs, b)) ` f s)"
256  apply (simp add: put_trace_eq_drop bind_def)
257  apply (safe; (clarsimp split: if_split_asm)?;
258      fastforce intro: bexI[where x=0] rev_bexI)
259  done
260
261lemma if_fun_lift:
262  "(if P then f else g) x = (if P then f x else g x)"
263  by simp
264
265lemma UN_If_distrib:
266  "(\<Union>x \<in> S. if P x then A x else B x)
267    = ((\<Union>x \<in> S \<inter> {x. P x}. A x) \<union> (\<Union>x \<in> S \<inter> {x. \<not> P x}. B x))"
268  by (fastforce split: if_split_asm)
269
270lemma Await_redef:
271  "Await P = do
272    s1 \<leftarrow> select {s. P s};
273    env_steps;
274    s \<leftarrow> get;
275    select (if P s then {()} else {})
276  od"
277  apply (simp add: Await_def env_steps_def bind_assoc)
278  apply (cases "{s. P s} = {}")
279   apply (simp add: select_def bind_def get_def)
280  apply (rule ext)
281  apply (simp add: exec_get select_bind_UN put_then_get_then)
282  apply (simp add: bind_promote_If2 if_fun_lift if_distrib[where f=select])
283  apply (simp add: exec_put_trace cong: if_cong)
284  apply (simp add: put_def bind_def select_def cong: if_cong)
285  apply (strengthen equalityI)
286  apply clarsimp
287  apply (strengthen exI[where x="s # xs" for s xs])
288  apply (strengthen exI[where x="Suc n" for n])
289  apply simp
290  apply blast
291  done
292
293lemma bind_apply_cong':
294  "f s = f' s
295    \<Longrightarrow> (\<forall>rv s'. (rv, s') \<in> mres (f s) \<longrightarrow> g rv s' = g' rv s')
296    \<Longrightarrow> bind f g s = bind f' g' s"
297  apply (simp add: bind_def)
298  apply (rule SUP_cong; simp?)
299  apply (clarsimp split: tmres.split)
300  apply (drule spec2, drule mp, erule in_mres)
301  apply simp
302  done
303
304lemmas bind_apply_cong = bind_apply_cong'[rule_format]
305
306lemma select_empty_bind[simp]:
307  "select {} >>= f = select {}"
308  by (simp add: select_def bind_def)
309
310lemma fail_bind[simp]:
311  "fail >>= f = fail"
312  by (simp add: bind_def fail_def)
313
314lemma eq_Me_neq_Env:
315  "(x = Me) = (x \<noteq> Env)"
316  by (cases x; simp)
317
318lemma validI_invariant_imp:
319  assumes v: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
320    and P: "\<forall>s0 s. P s0 s \<longrightarrow> I s0"
321    and R: "\<forall>s0 s. I s0 \<longrightarrow> R s0 s \<longrightarrow> I s"
322    and G: "\<forall>s0 s. I s0 \<longrightarrow> G s0 s \<longrightarrow> I s"
323  shows "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>,\<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace>"
324proof -
325  { fix tr s0 i
326  assume r: "rely_cond R s0 tr" and g: "guar_cond G s0 tr"
327    and I: "I s0"
328  hence imp: "\<forall>(_, s, s') \<in> trace_steps (rev tr) s0. I s \<longrightarrow> I s'"
329    apply (clarsimp simp: guar_cond_def rely_cond_def)
330    apply (drule(1) bspec)+
331    apply (clarsimp simp: eq_Me_neq_Env)
332    apply (metis R G)
333    done
334  hence "i < length tr \<longrightarrow> I (snd (rev tr ! i))"
335    using I
336    apply (induct i)
337     apply (clarsimp simp: neq_Nil_conv[where xs="rev tr" for tr, simplified])
338    apply clarsimp
339    apply (drule bspec, fastforce simp add: trace_steps_nth)
340    apply simp
341    done
342  }
343  note I = this
344  show ?thesis
345    using v
346    apply (clarsimp simp: validI_def rely_def imp_conjL)
347    apply (drule spec2, drule(1) mp)+
348    apply clarsimp
349    apply (frule P[rule_format])
350    apply (clarsimp simp: guar_cond_def trace_steps_nth I last_st_tr_def
351                          hd_append last_rev[symmetric]
352                          last_conv_nth rev_map)
353    done
354qed
355
356lemma validI_guar_post_conj_lift:
357  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G1\<rbrace>,\<lbrace>Q1\<rbrace>
358    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G2\<rbrace>,\<lbrace>Q2\<rbrace>
359    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. G1 s0 s \<and> G2 s0 s\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q1 rv s0 s \<and> Q2 rv s0 s\<rbrace>"
360  apply (frule validI_prefix_closed)
361  apply (subst validI_def, clarsimp simp: rely_def)
362  apply (drule(3) validI_D)+
363  apply (auto simp: guar_cond_def)
364  done
365
366lemmas modify_prefix_closed[simp] =
367  modify_wp[THEN valid_validI_wp[OF no_trace_all(3)], THEN validI_prefix_closed]
368lemmas await_prefix_closed[simp] = Await_sync_twp[THEN validI_prefix_closed]
369
370lemma repeat_prefix_closed[intro!]:
371  "prefix_closed f \<Longrightarrow> prefix_closed (repeat f)"
372  apply (simp add: repeat_def)
373  apply (rule prefix_closed_bind; clarsimp)
374  apply (rename_tac n)
375  apply (induct_tac n; simp)
376  apply (auto intro: prefix_closed_bind)
377  done
378
379end
380