1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory BCorres_UL
8imports
9  NonDetMonadVCG
10  Crunch_Instances_NonDet
11begin
12
13definition s_bcorres_underlying where
14  "s_bcorres_underlying t f g s \<equiv> (\<lambda>(x,y). (x, t y)) ` (fst (f s)) \<subseteq> (fst (g (t s)))"
15
16definition bcorres_underlying where
17  "bcorres_underlying t f g \<equiv> \<forall>s. s_bcorres_underlying t f g s"
18
19lemma wpc_helper_bcorres:
20  "bcorres_underlying t f g \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (bcorres_underlying t f g)"
21  by (simp add: wpc_helper_def)
22
23lemma wpc_helper_s_bcorres:
24  "s_bcorres_underlying t f g s \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (s_bcorres_underlying t f g s)"
25  by (simp add: wpc_helper_def)
26
27wpc_setup "\<lambda>f. bcorres_underlying t f g" wpc_helper_bcorres
28wpc_setup "\<lambda>f. s_bcorres_underlying t f g s" wpc_helper_bcorres
29
30lemma s_bcorres_underlying_split[wp_split]:
31  "(\<And>r s'. (r,s') \<in> fst (f s) \<Longrightarrow>  (s_bcorres_underlying t (g r) (g' r) s')) \<Longrightarrow>
32   s_bcorres_underlying t f f' s \<Longrightarrow>
33   s_bcorres_underlying t (f >>= g) (f' >>= g') s"
34  by (clarsimp simp: s_bcorres_underlying_def bind_def) force
35
36lemma bcorres_underlying_split[wp_split]:
37  "(\<And>r. (bcorres_underlying t (g r) (g' r))) \<Longrightarrow>
38   bcorres_underlying t f f' \<Longrightarrow>
39   bcorres_underlying t (f >>= g) (f' >>= g')"
40  by (simp add: bcorres_underlying_def s_bcorres_underlying_split)
41
42lemma get_s_bcorres_underlying[wp]:
43  "s_bcorres_underlying t (f s) (f' (t s)) s \<Longrightarrow> s_bcorres_underlying t (get >>= f) (get >>= f') s"
44  by (simp add: gets_def s_bcorres_underlying_def get_def bind_def return_def)
45
46lemma get_bcorres[wp]:
47  "(\<And>x. bcorres_underlying t (f x) (f' (t x))) \<Longrightarrow> bcorres_underlying t (get >>= f) (get >>= f')"
48  by (simp add: bcorres_underlying_def get_s_bcorres_underlying)
49
50lemma gets_s_bcorres_underlying[wp]:
51  "x' (t s) = x s \<Longrightarrow>  s_bcorres_underlying t (gets x) (gets x') s"
52  by (simp add: s_bcorres_underlying_def gets_def get_def bind_def return_def)
53
54lemma gets_bcorres_underlying[wp]:
55  "(\<And>s. x' (t s) = x s) \<Longrightarrow> bcorres_underlying t (gets x) (gets x')"
56  by (simp add: bcorres_underlying_def gets_s_bcorres_underlying)
57
58lemma gets_map_bcorres_underlying[wp]:
59  "(\<And>s. f' (t s) p = f s p) \<Longrightarrow> bcorres_underlying t (gets_map f p) (gets_map f' p)"
60  by (simp add: gets_map_def bcorres_underlying_def s_bcorres_underlying_def simpler_gets_def
61                bind_def assert_opt_def fail_def return_def
62        split: option.splits)
63
64lemma gets_bcorres_underlying':
65  "(\<And>xa. bcorres_underlying t (f (x xa)) (f' (x' (t xa)))) \<Longrightarrow>
66  bcorres_underlying t (gets x >>= f) (gets x' >>= f')"
67  by (wpsimp simp: gets_def)
68
69lemma assert_bcorres_underlying[wp]:
70  "f = f' \<Longrightarrow> bcorres_underlying t (assert f) (assert f')"
71  by (simp add: assert_def bcorres_underlying_def return_def s_bcorres_underlying_def fail_def)
72
73lemma return_bcorres[wp]:
74  "bcorres_underlying t (return x) (return x)"
75  by (simp add:return_def bcorres_underlying_def s_bcorres_underlying_def)
76
77lemma drop_sbcorres_underlying:
78  "bcorres_underlying t f g \<Longrightarrow> s_bcorres_underlying t f g s"
79  by (simp add: bcorres_underlying_def)
80
81lemma use_sbcorres_underlying:
82  "(\<And>s. s_bcorres_underlying t f g s) \<Longrightarrow> bcorres_underlying t f g"
83  by (simp add: bcorres_underlying_def)
84
85lemma bcorres_underlying_throwError[wp]:
86  "bcorres_underlying t (throwError a) (throwError a)"
87  by (wpsimp simp: throwError_def)
88
89lemma s_bcorres_underlying_splitE[wp_split]:
90  "(\<And>r s'. (Inr r,s') \<in> fst (f s) \<Longrightarrow> s_bcorres_underlying t (g r) (g' r) s') \<Longrightarrow>
91   s_bcorres_underlying t f f' s \<Longrightarrow>
92   s_bcorres_underlying t (f >>=E g) (f' >>=E g') s"
93  by (wpsimp simp: bindE_def lift_def split: sum.splits | rule conjI drop_sbcorres_underlying)+
94
95lemma get_s_bcorres_underlyingE[wp]:
96  "s_bcorres_underlying t (f s) (f' (t s)) s \<Longrightarrow>
97   s_bcorres_underlying t (liftE get >>=E f) (liftE get >>=E f') s"
98  by (simp add: gets_def s_bcorres_underlying_def get_def bindE_def bind_def return_def liftE_def lift_def)
99
100lemma bcorres_underlying_splitE[wp_split]:
101  "(\<And>r. bcorres_underlying t (g r) (g' r)) \<Longrightarrow>
102   bcorres_underlying t f f' \<Longrightarrow>
103   bcorres_underlying t (f >>=E g) (f' >>=E g')"
104  by (simp add: bcorres_underlying_def s_bcorres_underlying_splitE)
105
106lemmas return_s_bcorres_underlying[wp] = drop_sbcorres_underlying[OF return_bcorres]
107
108lemma liftE_s_bcorres_underlying[wp]:
109  "s_bcorres_underlying t f f' s \<Longrightarrow> s_bcorres_underlying t (liftE f) (liftE f') s"
110  by (wpsimp simp: liftE_def)
111
112lemma liftE_bcorres_underlying[wp]:
113  "bcorres_underlying t f f' \<Longrightarrow>  bcorres_underlying t (liftE f) (liftE f')"
114  by (simp add: bcorres_underlying_def liftE_s_bcorres_underlying)
115
116lemma returnOk_bcorres_underlying[wp]:
117  "bcorres_underlying t (returnOk x) (returnOk x)"
118  by (wpsimp simp: returnOk_def)
119
120lemma whenE_s_bcorres_underlying[wp]:
121  "\<lbrakk> \<lbrakk>P = P'; P\<rbrakk> \<Longrightarrow> s_bcorres_underlying t f f' s; P = P' \<rbrakk> \<Longrightarrow>
122   s_bcorres_underlying t (whenE P f) (whenE P' f') s"
123  by (wpsimp simp: whenE_def|rule drop_sbcorres_underlying)+
124
125lemma select_s_bcorres_underlying[wp]:
126  "A \<subseteq> B \<Longrightarrow> s_bcorres_underlying t (select A) (select B) s"
127  by (simp add: s_bcorres_underlying_def select_def image_def) blast
128
129lemma fail_s_bcorres_underlying[wp]:
130  "s_bcorres_underlying t fail fail s"
131  by (simp add: s_bcorres_underlying_def fail_def)
132
133lemma fail_bcorres_underlying[wp]:
134  "bcorres_underlying t fail fail"
135  by (simp add: bcorres_underlying_def fail_s_bcorres_underlying)
136
137lemma assertE_bcorres_underlying[wp]:
138  "bcorres_underlying t (assertE P) (assertE P)"
139  by (wpsimp simp: assertE_def returnOk_def|rule conjI)+
140
141lemmas assertE_s_bcorres_underlying[wp] = drop_sbcorres_underlying[OF assertE_bcorres_underlying]
142
143lemma when_s_bcorres_underlying[wp]:
144  "(P \<Longrightarrow> s_bcorres_underlying t f f' s) \<Longrightarrow> s_bcorres_underlying t (when P f) (when P f') s"
145  by (simp add: return_s_bcorres_underlying when_def)
146
147lemma when_bcorres_underlying[wp]:
148  "(P \<Longrightarrow> bcorres_underlying t f f') \<Longrightarrow> bcorres_underlying t (when P f) (when P f')"
149  by (simp add: bcorres_underlying_def when_s_bcorres_underlying)
150
151lemma put_bcorres_underlying[wp]:
152  "t f = f' \<Longrightarrow> bcorres_underlying t (put f) (put f')"
153  by (simp add: bcorres_underlying_def s_bcorres_underlying_def put_def)
154
155lemma modify_bcorres_underlying[wp]:
156  "(\<And>x. t (f x) = f' (t x)) \<Longrightarrow> bcorres_underlying t (modify f) (modify f')"
157  by (wpsimp simp: modify_def)
158
159lemma liftM_bcorres_underlying[wp]:
160  "bcorres_underlying t m m' \<Longrightarrow> bcorres_underlying t (liftM f m) (liftM f m')"
161  by (wpsimp simp: liftM_def)
162
163lemma sequence_x_bcorres_underlying[wp]:
164  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow>
165   bcorres_underlying t (sequence_x (map f xs)) (sequence_x (map f' xs))"
166  by (induct xs; wpsimp simp: sequence_x_def)
167
168lemma sequence_bcorres_underlying[wp]:
169  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow>
170   bcorres_underlying t (sequence (map f xs)) (sequence (map f' xs))"
171  by (induct xs; wpsimp simp: sequence_def)
172
173lemma mapM_x_bcorres_underlying[wp]:
174  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapM_x f xs) (mapM_x f' xs)"
175  by (wpsimp simp: mapM_x_def)
176
177lemma mapM_bcorres_underlying[wp]:
178  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapM f xs) (mapM f' xs)"
179  by (simp add: mapM_def | wp)+
180
181lemma gets_s_bcorres_underlyingE':
182  "s_bcorres_underlying t (f (x s)) (f' (x' (t s))) s \<Longrightarrow>
183   s_bcorres_underlying t (liftE (gets x) >>=E f) (liftE (gets x') >>=E f') s"
184  by (simp add: gets_def liftE_def lift_def bindE_def) wp
185
186lemma bcorres_underlying_filterM[wp]:
187  "(\<And>x. bcorres_underlying t (a x) (a' x)) \<Longrightarrow> bcorres_underlying t (filterM a b) (filterM a' b)"
188  by (induct b; wpsimp simp: filterM_def)
189
190lemma option_rec_bcorres_underlying[wp_split]:
191  "(\<And>x y. bcorres_underlying t (g x y) (g' x y)) \<Longrightarrow>
192   (\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow>
193   bcorres_underlying t (rec_option f g a b) (rec_option f' g' a b)"
194  by (cases a, simp+)
195
196lemma bcorres_underlying_mapME[wp]:
197  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapME f r) (mapME f' r)"
198  by (induct r; wpsimp simp: mapME_def sequenceE_def)
199
200lemma handle2_bcorres_underlying[wp]:
201  "bcorres_underlying t f f' \<Longrightarrow>
202   (\<And>x. bcorres_underlying t (g x) (g' x)) \<Longrightarrow>
203   bcorres_underlying t (f <handle2> g) (f' <handle2> g')"
204  by (wpsimp simp: handleE'_def)
205
206lemma liftME_bcorres_underlying[wp]:
207  "bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (liftME a f) (liftME a f')"
208  by (wpsimp simp: liftME_def)
209
210lemma zipWithM_x_bcorres[wp]:
211  "(\<And>x y. bcorres_underlying t (f x y) (f' x y) ) \<Longrightarrow>
212   bcorres_underlying t (zipWithM_x f xs ys) (zipWithM_x f' xs ys)"
213  by (wpsimp simp: zipWithM_x_def zipWith_def split_def)
214
215lemma mapME_x_bcorres_underlying[wp]:
216  "(\<And>x. bcorres_underlying t (f x) (f' x)) \<Longrightarrow> bcorres_underlying t (mapME_x f xs) (mapME_x f' xs)"
217  by (induct xs; wpsimp simp: mapME_x_def sequenceE_x_def)
218
219lemma liftE_bind_bcorres[wp]:
220  "bcorres_underlying t (f >>= g) (f' >>= g') \<Longrightarrow>
221   bcorres_underlying t (liftE f >>=E g) (liftE f' >>=E g')"
222  by (simp add: gets_def bcorres_underlying_def s_bcorres_underlying_def get_def bind_def return_def
223                split_def liftE_def bindE_def lift_def)
224
225lemma select_f_bcorres[wp]: "bcorres_underlying t (select_f f) (select_f f)"
226  by (fastforce simp: select_f_def bcorres_underlying_def s_bcorres_underlying_def)
227
228lemma bcorres_underlying_if[wp]:
229  "(b \<Longrightarrow> bcorres_underlying t f f') \<Longrightarrow>
230   (\<not>b \<Longrightarrow> bcorres_underlying t g g') \<Longrightarrow>
231   bcorres_underlying t (if b then f else g) (if b then f' else g')"
232  by (case_tac b; simp)
233
234lemma assert_opt_bcorres_underlying[wp]:
235  "bcorres_underlying t (assert_opt f) (assert_opt f)"
236  by (wpsimp simp: assert_opt_def)
237
238lemma unlessb_corres_underlying[wp]:
239  "bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (unless a f) (unless a f')"
240  by (wpsimp simp: unless_def)
241
242lemma select_bcorres_underlying[wp]:
243  "A \<subseteq> B \<Longrightarrow> bcorres_underlying t (select A) (select B)"
244  by (fastforce simp: bcorres_underlying_def select_def s_bcorres_underlying_def)
245
246lemma catch_bcorres[wp]:
247  "bcorres_underlying t f f' \<Longrightarrow>
248   (\<And>x. bcorres_underlying t (g x) (g' x)) \<Longrightarrow>
249   bcorres_underlying t (f <catch> g) (f' <catch> g')"
250  unfolding catch_def by wpsimp
251
252lemma whenE_bcorres_underlying[wp]:
253  "\<lbrakk> \<lbrakk>P = P'; P\<rbrakk> \<Longrightarrow> bcorres_underlying t f f'; P = P' \<rbrakk> \<Longrightarrow>
254  bcorres_underlying t (whenE P f) (whenE P' f')"
255  unfolding whenE_def by wpsimp
256
257lemma unlessE_bcorres[wp]:
258  "bcorres_underlying t f f' \<Longrightarrow> bcorres_underlying t (unlessE P f) (unlessE P f')"
259  by (wpsimp simp: unlessE_def)
260
261lemma alternative_bcorres[wp]:
262  "\<lbrakk> bcorres_underlying t f f';  bcorres_underlying t g g' \<rbrakk> \<Longrightarrow>
263  bcorres_underlying t (f \<sqinter> g) (f' \<sqinter> g')"
264  by (fastforce simp: alternative_def bcorres_underlying_def s_bcorres_underlying_def)
265
266lemma gets_the_bcorres_underlying[wp]:
267  "(\<And>s. f' (t s) = f s) \<Longrightarrow> bcorres_underlying t (gets_the f) (gets_the f')"
268  by (wpsimp simp: gets_the_def)
269
270ML \<open>
271structure CrunchBCorresInstance : CrunchInstance =
272struct
273  val name = "bcorres";
274  type extra = term;
275  val eq_extra = ae_conv;
276  fun parse_extra ctxt extra
277        = case extra of
278             "" => error "bcorres needs truncate function"
279             | e =>(Syntax.parse_term ctxt "%_. True", Syntax.parse_term ctxt e);
280  val has_preconds = false;
281  fun mk_term _ body extra =
282    (Syntax.parse_term @{context} "bcorres_underlying") $ extra $ body $ body;
283  fun dest_term (Const (@{const_name "bcorres_underlying"}, _) $ extra $ body $ _)
284        = SOME (Term.dummy, body, extra)
285    | dest_term _ = NONE;
286  fun put_precond _ ((v as Const (@{const_name "bcorres_underlying"}, _)) $ extra $ body $ body')
287        = v $ extra $ body $ body'
288    | put_precond _ _ = error "put_precond: not an bcorres term";
289  val pre_thms = [];
290  val wpc_tactic = WeakestPreCases.wp_cases_tac @{thms wpc_processors};
291  fun wps_tactic _ _ _ = no_tac;
292  val magic = Syntax.parse_term @{context}
293    "\<lambda>mapp_lambda_ignore. bcorres_underlying t_free_ignore mapp_lambda_ignore g_free_ignore";
294  val get_monad_state_type = get_nondet_monad_state_type;
295end;
296
297structure CrunchBCorres : CRUNCH = Crunch(CrunchBCorresInstance);
298\<close>
299
300setup \<open>
301  add_crunch_instance "bcorres" (CrunchBCorres.crunch_x, CrunchBCorres.crunch_ignore_add_del)
302\<close>
303
304end
305