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