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