1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8 A general calculus of refinement in Isabelle. 9*) 10 11chapter "Refinement" 12 13theory Simulation 14imports Main 15begin 16 17text \<open> 18 A data type is a collection of three functions on three basic types. 19 The three basic types are the private state space @{typ 'a}, the observable 20 state space @{typ 'b} and the operations @{typ 'j}. 21 22 The three functions are the initialisation @{term "Init"} which (potentially 23 nondeterministically) produces a private state space from an observable one, 24 the finalisation @{term Fin} which projects the observable part of 25 the state space out of the private one, and finally @{term Step} that gives 26 the (potentially nondeterministic) transition relation on the private state 27 space for each operation in @{typ 'j}. 28 29 In the simple case, the private state space is something like a 30 tuple @{typ "'a \<times> 'b"} fully containing the observable part such 31 that @{term Fin} just becomes the projection @{term snd}, and @{term 32 "Init s"} constructs an additional private part, e.g. just 33 @{term "{(f x, x)}"}. 34 35 Hoare triples on the system and refinement are defined over the observable 36 part of the state. 37\<close> 38 39record ('a,'b,'j) data_type = 40 Init :: "'b \<Rightarrow> 'a set" 41 Fin :: "'a \<Rightarrow> 'b" 42 Step :: "'j \<Rightarrow> ('a \<times> 'a) set" 43 44text \<open> 45 A sequence of operations over a transition relation @{term \<delta>} is executed 46 by applying the relation repeatedly. 47\<close> 48definition 49 steps :: "('j \<Rightarrow> ('a \<times> 'a) set) \<Rightarrow> 'a set \<Rightarrow> 'j list \<Rightarrow> 'a set" where 50 "steps \<delta> \<equiv> foldl (\<lambda>S j. \<delta> j `` S)" 51 52text \<open> 53 The sequence of operations in the data type is then executed 54 in an initial state by initialising the private state, executing 55 the transition relation over this private state, and finally 56 projecting back out the set of final, observable states. 57\<close> 58definition 59 execution :: "('a,'b,'j) data_type \<Rightarrow> 'b \<Rightarrow> 'j list \<Rightarrow> 'b set" where 60 "execution A s js \<equiv> Fin A ` steps (Step A) (Init A s) js" 61 62text \<open> 63 A Hoare triple over a list of operations in the data type is 64 the usual: given a state in the pre-condition, all resulting states 65 of the execution must be in the post-condition: 66\<close> 67definition 68 hoare_triple :: "('a,'b,'j) data_type \<Rightarrow> 'b set \<Rightarrow> 'j list \<Rightarrow> 'b set \<Rightarrow> bool" 69where 70 "hoare_triple A P js Q \<equiv> \<forall>s \<in> P. execution A s js \<subseteq> Q" 71 72text \<open> 73 Refinement is defined by saying that all concrete behaviours are contained in 74 their corresponding abstract ones. Only the private state spaces of the 75 data type may differ. 76\<close> 77definition 78 refines :: "('c,'b,'j) data_type \<Rightarrow> ('a,'b,'j) data_type \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 79where 80 "C \<sqsubseteq> A \<equiv> \<forall>js s. execution C s js \<subseteq> execution A s js" 81 82text \<open> 83 Alternatively, one may say that all Hoare triples proved on the abstract data 84 type are true for the concrete one. 85\<close> 86lemma hoare_triple_refinement: 87 "C \<sqsubseteq> A = (\<forall>P Q js. hoare_triple A P js Q \<longrightarrow> hoare_triple C P js Q)" 88 by (simp add: refines_def hoare_triple_def) blast 89 90 91\<comment> \<open>composing two relations\<close> 92definition 93 rel_semi :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixl ";;;" 65) 94where 95 "A ;;; B \<equiv> A O B" 96 97text \<open> 98 Refinement is a global property over all executions and/or all 99 hoare triples. As this is hard to show, we define the weaker concept 100 of forward simulation. 101\<close> 102definition 103 fw_sim :: "('a \<times> 'c) set \<Rightarrow> ('c,'b,'j) data_type \<Rightarrow> ('a,'b,'j) data_type \<Rightarrow> bool" 104where 105 "fw_sim R C A \<equiv> (\<forall>s. Init C s \<subseteq> R `` Init A s) \<and> 106 (\<forall>j. R ;;; Step C j \<subseteq> Step A j ;;; R) \<and> 107 (\<forall>s s'. (s,s') \<in> R \<longrightarrow> Fin C s' = Fin A s)" 108 109definition 110 fw_simulates :: "('c,'b,'j) data_type \<Rightarrow> ('a,'b,'j) data_type \<Rightarrow> bool" (infixl "\<sqsubseteq>\<^sub>F" 50) 111where 112 "C \<sqsubseteq>\<^sub>F A \<equiv> \<exists>R. fw_sim R C A" 113 114lemma fw_sim_steps: 115 assumes steps: "t' \<in> steps (Step C) S' js" "S' \<subseteq> R `` S" 116 assumes sim: "fw_sim R C A" 117 shows "\<exists>t \<in> steps (Step A) S js. (t,t') \<in> R" using steps 118proof (induct js arbitrary: S' S) 119 case Nil 120 thus ?case by (simp add: steps_def) blast 121next 122 case (Cons j js) 123 hence "t' \<in> steps (Step C) (Step C j `` S') js" 124 by (clarsimp simp: steps_def) 125 moreover { 126 from Cons.prems 127 have "S' \<subseteq> R `` S" by simp 128 moreover 129 from sim 130 have "R ;;; Step C j \<subseteq> Step A j ;;; R" by (simp add: fw_sim_def) 131 ultimately 132 have "Step C j `` S' \<subseteq> R `` (Step A j `` S)" 133 by (simp add: rel_semi_def) blast 134 } 135 ultimately 136 show ?case using Cons.hyps 137 by (auto simp: steps_def) 138qed 139 140lemma sim_imp_refines: 141 "C \<sqsubseteq>\<^sub>F A \<Longrightarrow> C \<sqsubseteq> A" 142 apply (clarsimp simp: refines_def execution_def fw_simulates_def) 143 apply (rename_tac t) 144 apply (drule fw_sim_steps) 145 prefer 2 146 apply assumption 147 apply (simp add: fw_sim_def) 148 apply blast 149 apply clarsimp 150 apply (erule rev_image_eqI) 151 apply (simp add: fw_sim_def) 152 done 153 154 155text \<open> 156 To further aid proofs, we define (private) invariants on data types. 157 Private invariants are properties that are true throughout execution 158 on the private state space of the state type. The purpose is to exploit 159 these properties while showing forward simulation. 160\<close> 161definition 162 invariant_holds :: "('a,'b,'j) data_type \<Rightarrow> 'a set \<Rightarrow> bool" (infix "\<Turnstile>" 60) 163where 164 "D \<Turnstile> I \<equiv> (\<forall>s. Init D s \<subseteq> I) \<and> (\<forall>j. Step D j `` I \<subseteq> I)" 165 166lemma invariant_T [iff]: "D \<Turnstile> UNIV" 167 by (simp add: invariant_holds_def) 168 169lemma invariantI: 170 "\<lbrakk> \<forall>s. Init D s \<subseteq> I; \<forall>j. Step D j `` I \<subseteq> I \<rbrakk> \<Longrightarrow> D \<Turnstile> I" 171 by (simp add: invariant_holds_def) 172 173lemma invariant_CollectI [intro?]: 174 assumes init: "\<And>s a. s \<in> Init D a \<Longrightarrow> I s" 175 assumes step: "\<And>j s s'. \<lbrakk> I s; (s,s') \<in> Step D j \<rbrakk> \<Longrightarrow> I s'" 176 shows "D \<Turnstile> Collect I" 177proof (rule invariantI) 178 show "\<forall>a. Init D a \<subseteq> Collect I" by (fast intro: init) 179next 180 show "\<forall>j. Step D j `` Collect I \<subseteq> Collect I" 181 by (auto simp add: Image_def intro: step) 182qed 183 184lemma invariant_conjI: 185 "D \<Turnstile> P \<Longrightarrow> D \<Turnstile> Q \<Longrightarrow> D \<Turnstile> P \<inter> Q" 186 by (simp add: invariant_holds_def) blast 187 188lemma invariant_conjI2: 189 "\<lbrakk> D \<Turnstile> I; \<And>s. Init D s \<subseteq> I \<Longrightarrow> Init D s \<subseteq> J; 190 \<forall>j. Step D j `` (I \<inter> J) \<subseteq> J \<rbrakk> \<Longrightarrow> D \<Turnstile> I \<inter> J" 191 by (simp add: invariant_holds_def) blast 192 193 194text \<open> 195 We can now define forward simulation with an invariant. The proof 196 obligation for the step and final case in the correspondence proof 197 can now assume that the invariant holds. The invariant itself can be 198 shown separately. 199\<close> 200definition 201 LI :: "('a,'b,'j) data_type \<Rightarrow> ('c,'b,'j) data_type \<Rightarrow> ('a \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set \<Rightarrow> bool" 202where 203 "LI A C R I \<equiv> (\<forall>s. Init C s \<subseteq> R `` Init A s) \<and> 204 (\<forall>j. (R \<inter> I) ;;; Step C j \<subseteq> Step A j ;;; R) \<and> 205 (\<forall>s s'. (s,s') \<in> R \<inter> I \<longrightarrow> Fin C s' = Fin A s)" 206 207 208lemma LI_fw_sim: 209 assumes ia: "A \<Turnstile> I\<^sub>a" and ic: "C \<Turnstile> I\<^sub>c" and li: "LI A C r (I\<^sub>a \<times> I\<^sub>c)" 210 shows "fw_sim (r \<inter> I\<^sub>a \<times> I\<^sub>c) C A" 211proof - 212 from li have 213 init: "\<forall>s. Init C s \<subseteq> r `` Init A s" and 214 step: "\<forall>j. (r \<inter> (I\<^sub>a \<times> I\<^sub>c)) ;;; Step C j \<subseteq> Step A j ;;; r" and 215 fin: "(\<forall>s s'. (s,s') \<in> r \<inter> (I\<^sub>a \<times> I\<^sub>c) \<longrightarrow> Fin C s' = Fin A s)" 216 by (auto simp: LI_def) 217 from ia have "\<forall>s. (r \<inter> (UNIV \<times> I\<^sub>c) ) `` Init A s = (r \<inter> (I\<^sub>a \<times> I\<^sub>c)) `` Init A s" 218 by (simp add: invariant_holds_def, blast) 219 moreover from init ic have "\<forall>s. Init C s \<subseteq> (r \<inter> (UNIV \<times> I\<^sub>c)) `` Init A s" 220 by (simp add: invariant_holds_def, blast) 221 ultimately have initI: "\<forall>s. Init C s \<subseteq> (r \<inter> (I\<^sub>a \<times> I\<^sub>c)) `` Init A s" by simp 222 moreover { 223 fix j 224 from step have "r \<inter> (I\<^sub>a \<times> I\<^sub>c) ;;; Step C j \<subseteq> Step A j ;;; r".. 225 also 226 have "r \<inter> (I\<^sub>a \<times> I\<^sub>c) = ((UNIV \<times> I\<^sub>a) \<inter> Id) ;;; r ;;; ((I\<^sub>c \<times> UNIV) \<inter> Id)" 227 (is "_ = ?I\<^sub>a ;;; r ;;; ?I\<^sub>c") 228 by (simp add: rel_semi_def, blast) 229 finally 230 have "?I\<^sub>a ;;; r ;;; ?I\<^sub>c ;;; Step C j \<subseteq> ?I\<^sub>a ;;; Step A j ;;; r" 231 by (simp add: rel_semi_def, blast) 232 also 233 from ia have "\<dots> \<subseteq> Step A j ;;; ?I\<^sub>a ;;; r" 234 by (simp add: invariant_holds_def rel_semi_def, blast) 235 finally 236 have "?I\<^sub>a ;;; r ;;; ?I\<^sub>c ;;; Step C j;;; ?I\<^sub>c \<subseteq> Step A j ;;; ?I\<^sub>a ;;; r ;;; ?I\<^sub>c" 237 by (simp add: rel_semi_def, blast) 238 also 239 from ic 240 have "?I\<^sub>a ;;; r ;;; ?I\<^sub>c ;;; Step C j;;; ?I\<^sub>c = ?I\<^sub>a ;;; r ;;; ?I\<^sub>c ;;; Step C j" 241 by (simp add: invariant_holds_def rel_semi_def, blast) 242 finally 243 have "r \<inter> (I\<^sub>a \<times> I\<^sub>c) ;;; Step C j \<subseteq> Step A j ;;; r \<inter> (I\<^sub>a \<times> I\<^sub>c)" 244 by (simp add: rel_semi_def, blast) 245 } 246 ultimately show "fw_sim (r \<inter> I\<^sub>a \<times> I\<^sub>c) C A" using fin 247 by (simp add: fw_sim_def) 248qed 249 250 251lemma weaken_LI: 252 assumes LI: "LI A C R I'" and weaker: "I \<subseteq> I'" shows "LI A C R I" 253proof - 254 from weaker have step: "\<And>j. R \<inter> I ;;; Step C j \<subseteq> R \<inter> I' ;;; Step C j" 255 by (fastforce simp: rel_semi_def relcomp_def) 256 from weaker have fin: "\<And>S. S \<in> R \<inter> I \<Longrightarrow> S \<in> R \<inter> I'" by fastforce 257 from subset_trans[OF step] fin LI show ?thesis by (clarsimp simp: LI_def) 258qed 259 260lemma fw_sim_eq_LI: "fw_sim r C A = LI A C r UNIV" 261 by (simp add: fw_sim_def LI_def) 262 263lemma fw_sim_LI: "fw_sim r C A \<Longrightarrow> LI A C r I" 264 by (simp add: fw_sim_eq_LI weaken_LI[where I'=UNIV]) 265 266 267lemma L_invariantI: 268 assumes "A \<Turnstile> I\<^sub>a" and "C \<Turnstile> I\<^sub>c" and "LI A C r (I\<^sub>a \<times> I\<^sub>c)" 269 shows "C \<sqsubseteq>\<^sub>F A" 270 using assms 271 by (simp add: fw_simulates_def, rule_tac x="r \<inter> I\<^sub>a \<times> I\<^sub>c" in exI, 272 simp add: LI_fw_sim) 273 274lemma refinement_refl[simp]: 275 "A \<sqsubseteq> A" 276 by (simp add: refines_def) 277 278lemma refinement_trans [trans]: 279 "\<lbrakk>C \<sqsubseteq> B; B \<sqsubseteq> A\<rbrakk> \<Longrightarrow> C \<sqsubseteq> A" 280 by (simp add: refines_def) blast 281 282 283lemma fw_inv_transport: 284 "\<lbrakk> A \<Turnstile> I\<^sub>a; C \<Turnstile> I\<^sub>c; LI A C R (I\<^sub>a \<times> I\<^sub>c) \<rbrakk> \<Longrightarrow> C \<Turnstile> {s'. \<exists>s. (s,s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c}" 285 apply (clarsimp simp: LI_def invariant_holds_def) 286 apply (rule conjI) 287 apply (rule allI) 288 apply clarsimp 289 apply (subgoal_tac "x \<in> (R `` Init A s)") 290 prefer 2 291 apply fastforce 292 apply blast 293 apply clarsimp 294 apply (erule_tac x=j in allE)+ 295 apply (clarsimp simp: rel_semi_def) 296 apply (subgoal_tac "(s,x) \<in> Step A j O R") 297 prefer 2 298 apply blast 299 apply blast 300 done 301 302lemma fw_sim_refl: 303 "fw_sim Id A A" 304 apply (simp add: fw_sim_def rel_semi_def) 305 done 306 307lemma fw_simulates_refl[simp]: 308 "A \<sqsubseteq>\<^sub>F A" 309 apply (simp add: fw_simulates_def fw_sim_refl exI[where x="Id"]) 310 done 311 312lemma fw_sim_trans: 313 "\<lbrakk>fw_sim Q C B; fw_sim R B A\<rbrakk> \<Longrightarrow> fw_sim (R O Q) C A" 314 by (auto simp: fw_sim_def rel_semi_def; blast) 315 316lemma fw_simulates_trans: 317 "\<lbrakk>C \<sqsubseteq>\<^sub>F B; B \<sqsubseteq>\<^sub>F A\<rbrakk> \<Longrightarrow> C \<sqsubseteq>\<^sub>F A" 318 apply (auto simp: fw_simulates_def dest: fw_sim_trans) 319 done 320 321end 322