1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory SpecValid_R 8imports ExtraCorres 9begin 10 11definition 12 spec_valid :: "'s \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s, 'r) nondet_monad \<Rightarrow> ('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 13 ("_ \<turnstile> /\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>" [60,0,0,0] 100) 14where 15 "spec_valid st P f Q \<equiv> valid (\<lambda>s. s = st \<and> P s) f Q" 16 17definition 18 spec_validE :: "'s \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'r) nondet_monad \<Rightarrow> 19 ('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('e \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 20 ("_ \<turnstile> /\<lbrace>_\<rbrace>/ _ /(\<lbrace>_\<rbrace>, /\<lbrace>_\<rbrace>)" [60,0,0,0] 100) 21where 22 "spec_validE st P f Q E \<equiv> validE (\<lambda>s. s = st \<and> P s) f Q E" 23 24lemma use_spec': 25 assumes x: "\<And>s. s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 26 shows "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 27 apply (clarsimp simp: valid_def) 28 apply (cut_tac s=s in x) 29 apply (clarsimp simp: valid_def spec_valid_def) 30 apply (erule(1) my_BallE, simp) 31 done 32 33lemma use_specE': 34 "\<lbrakk> \<And>s. s \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace>" 35 apply (simp add: validE_def spec_validE_def) 36 apply (fold spec_valid_def) 37 apply (simp add: use_spec') 38 done 39 40lemmas use_spec = use_spec' use_specE' 41 42lemma drop_equalled_validE: 43 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. s = s' \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 44 by (erule hoare_pre, clarsimp) 45 46lemma drop_spec_valid[wp_split]: 47 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 48 apply (simp add: spec_valid_def) 49 apply (erule hoare_vcg_precond_imp) 50 apply clarsimp 51 done 52 53lemma drop_spec_validE[wp_split]: 54 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 55 apply (simp add: spec_validE_def) 56 apply (erule hoare_vcg_precond_impE) 57 apply clarsimp 58 done 59 60lemma split_spec_bindE[wp_split]: 61 assumes x: "\<And>rv s''. (Inr rv, s'') \<in> fst (f s') \<Longrightarrow> s'' \<turnstile> \<lbrace>B rv\<rbrace> g rv \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 62 shows "s' \<turnstile> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace> 63 \<Longrightarrow> s' \<turnstile> \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 64 apply (clarsimp simp: spec_validE_def validE_def valid_def bind_def bindE_def lift_def split_def) 65 apply (case_tac a) 66 apply (clarsimp simp add: throwError_def return_def) 67 apply (erule(1) my_BallE, simp) 68 apply clarsimp 69 apply (erule(1) my_BallE, simp) 70 apply (drule x) 71 apply (clarsimp simp: spec_validE_def validE_def valid_def split_def) 72 apply (erule(1) my_BallE, simp) 73 done 74 75lemma split_spec_bind[wp_split]: 76 assumes x: "\<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> s'' \<turnstile> \<lbrace>B rv\<rbrace> g rv \<lbrace>C\<rbrace>" 77 shows "s' \<turnstile> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace> 78 \<Longrightarrow> s' \<turnstile> \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace>" 79 apply (clarsimp simp: spec_valid_def valid_def bind_def lift_def split_def) 80 apply (erule(1) my_BallE, simp) 81 apply (drule x) 82 apply (fastforce simp: spec_valid_def valid_def split_def) 83 done 84 85lemma split_spec_if[wp_split]: 86 "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; 87 \<not> G \<Longrightarrow> s' \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace> 88 \<rbrakk> \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> if G then f else f' \<lbrace>Q\<rbrace>" 89 by (cases G, simp+) 90 91lemma split_spec_ifE[wp_split]: 92 "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; 93 \<not> G \<Longrightarrow> s' \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> 94 \<rbrakk> \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> if G then f else f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 95 by (cases G, simp+) 96 97lemma split_spec_unlessE[wp_split]: 98 "\<lbrakk> \<not> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> 99 s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> Q () s) \<and> (\<not> G \<longrightarrow> P s)\<rbrace> unlessE G f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 100 apply (cases G, simp_all add: unlessE_def) 101 apply wp 102 done 103 104lemma spec_fun_applyE [wp_split]: 105 "s \<turnstile> \<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 106 by simp 107 108lemma split_spec_K_bind[wp_split]: 109 "s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>" 110 by simp 111 112lemma split_spec_K_bindE[wp_split]: 113 "s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 114 by simp 115 116lemma fudge_hoare: 117 "s \<turnstile> \<lbrace>P\<rbrace> \<lambda>s. f s \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 118 . 119 120lemma split_spec_whenE [wp_split]: 121 "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> 122 s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> Q () s)\<rbrace> whenE G f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 123 apply (cases G, simp_all add: whenE_def) 124 apply wp 125 done 126 127lemma spec_valid_conj_lift: 128 "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> 129 \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>" 130 apply (simp add: spec_valid_def) 131 apply (drule(1) hoare_vcg_conj_lift) 132 apply (simp add: conj_comms) 133 done 134 135lemma spec_valid_conj_liftE1: 136 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk> 137 \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E'\<rbrace>" 138 apply (simp add: spec_validE_def) 139 apply (drule(1) hoare_vcg_conj_liftE1) 140 apply (simp add: conj_comms pred_conj_def) 141 done 142 143lemma spec_valid_conj_liftE2: 144 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk> 145 \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E'\<rbrace>" 146 apply (simp add: spec_validE_def) 147 apply (drule(1) hoare_vcg_conj_liftE1) 148 apply (simp add: conj_comms pred_conj_def) 149 done 150 151lemma hoare_pre_spec_valid: 152 "\<lbrakk> s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 153 apply (simp add: spec_valid_def) 154 apply (erule hoare_pre) 155 apply clarsimp 156 done 157 158lemma hoare_pre_spec_validE: 159 "\<lbrakk> s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 160 apply (simp add: spec_validE_def) 161 apply (erule hoare_pre) 162 apply clarsimp 163 done 164 165lemma spec_validE_if: 166 "\<lbrakk> G \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<not> G \<Longrightarrow> s \<turnstile> \<lbrace>P'\<rbrace> g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and P'\<rbrace> if G then f else g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 167 apply (cases G, simp_all) 168 apply (clarsimp elim!: hoare_pre_spec_validE)+ 169 done 170 171lemma spec_strengthen_post: 172 "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s r. Q' s r \<Longrightarrow> Q s r \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 173 by (simp add: spec_valid_def valid_def 174 split_def split: sum.splits) 175 176lemma spec_strengthen_postE: 177 "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>; \<And>s r. Q' s r \<Longrightarrow> Q s r \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" 178 by (simp add: spec_valid_def spec_validE_def validE_def valid_def 179 split_def split: sum.splits) 180 181end 182