1(* Title: HOL/UNITY/Comp/Alloc.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Specification of Chandy and Charpentier's Allocator 6*) 7 8theory Alloc 9imports AllocBase "../PPROD" 10begin 11 12subsection\<open>State definitions. OUTPUT variables are locals\<close> 13 14record clientState = 15 giv :: "nat list" \<comment> \<open>client's INPUT history: tokens GRANTED\<close> 16 ask :: "nat list" \<comment> \<open>client's OUTPUT history: tokens REQUESTED\<close> 17 rel :: "nat list" \<comment> \<open>client's OUTPUT history: tokens RELEASED\<close> 18 19record 'a clientState_d = 20 clientState + 21 dummy :: 'a \<comment> \<open>dummy field for new variables\<close> 22 23definition 24 \<comment> \<open>DUPLICATED FROM Client.thy, but with "tok" removed\<close> 25 \<comment> \<open>Maybe want a special theory section to declare such maps\<close> 26 non_dummy :: "'a clientState_d => clientState" 27 where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s|)" 28 29definition 30 \<comment> \<open>Renaming map to put a Client into the standard form\<close> 31 client_map :: "'a clientState_d => clientState*'a" 32 where "client_map = funPair non_dummy dummy" 33 34 35record allocState = 36 allocGiv :: "nat => nat list" \<comment> \<open>OUTPUT history: source of "giv" for i\<close> 37 allocAsk :: "nat => nat list" \<comment> \<open>INPUT: allocator's copy of "ask" for i\<close> 38 allocRel :: "nat => nat list" \<comment> \<open>INPUT: allocator's copy of "rel" for i\<close> 39 40record 'a allocState_d = 41 allocState + 42 dummy :: 'a \<comment> \<open>dummy field for new variables\<close> 43 44record 'a systemState = 45 allocState + 46 client :: "nat => clientState" \<comment> \<open>states of all clients\<close> 47 dummy :: 'a \<comment> \<open>dummy field for new variables\<close> 48 49 50subsubsection \<open>Resource allocation system specification\<close> 51 52definition 53 \<comment> \<open>spec (1)\<close> 54 system_safety :: "'a systemState program set" 55 where "system_safety = 56 Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o giv o sub i o client)s) 57 \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o rel o sub i o client)s)}" 58 59definition 60 \<comment> \<open>spec (2)\<close> 61 system_progress :: "'a systemState program set" 62 where "system_progress = (INT i : lessThan Nclients. 63 INT h. 64 {s. h \<le> (ask o sub i o client)s} LeadsTo 65 {s. h pfixLe (giv o sub i o client) s})" 66 67definition 68 system_spec :: "'a systemState program set" 69 where "system_spec = system_safety Int system_progress" 70 71 72subsubsection \<open>Client specification (required)\<close> 73 74definition 75 \<comment> \<open>spec (3)\<close> 76 client_increasing :: "'a clientState_d program set" 77 where "client_increasing = UNIV guarantees Increasing ask Int Increasing rel" 78 79definition 80 \<comment> \<open>spec (4)\<close> 81 client_bounded :: "'a clientState_d program set" 82 where "client_bounded = UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}" 83 84definition 85 \<comment> \<open>spec (5)\<close> 86 client_progress :: "'a clientState_d program set" 87 where "client_progress = 88 Increasing giv guarantees 89 (INT h. {s. h \<le> giv s & h pfixGe ask s} 90 LeadsTo {s. tokens h \<le> (tokens o rel) s})" 91 92definition 93 \<comment> \<open>spec: preserves part\<close> 94 client_preserves :: "'a clientState_d program set" 95 where "client_preserves = preserves giv Int preserves clientState_d.dummy" 96 97definition 98 \<comment> \<open>environmental constraints\<close> 99 client_allowed_acts :: "'a clientState_d program set" 100 where "client_allowed_acts = 101 {F. AllowedActs F = 102 insert Id (UNION (preserves (funPair rel ask)) Acts)}" 103 104definition 105 client_spec :: "'a clientState_d program set" 106 where "client_spec = client_increasing Int client_bounded Int client_progress 107 Int client_allowed_acts Int client_preserves" 108 109 110subsubsection \<open>Allocator specification (required)\<close> 111 112definition 113 \<comment> \<open>spec (6)\<close> 114 alloc_increasing :: "'a allocState_d program set" 115 where "alloc_increasing = 116 UNIV guarantees 117 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))" 118 119definition 120 \<comment> \<open>spec (7)\<close> 121 alloc_safety :: "'a allocState_d program set" 122 where "alloc_safety = 123 (INT i : lessThan Nclients. Increasing (sub i o allocRel)) 124 guarantees 125 Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv)s) 126 \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)}" 127 128definition 129 \<comment> \<open>spec (8)\<close> 130 alloc_progress :: "'a allocState_d program set" 131 where "alloc_progress = 132 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int 133 Increasing (sub i o allocRel)) 134 Int 135 Always {s. \<forall>i<Nclients. 136 \<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT} 137 Int 138 (INT i : lessThan Nclients. 139 INT h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} 140 LeadsTo 141 {s. tokens h \<le> (tokens o sub i o allocRel)s}) 142 guarantees 143 (INT i : lessThan Nclients. 144 INT h. {s. h \<le> (sub i o allocAsk) s} 145 LeadsTo 146 {s. h pfixLe (sub i o allocGiv) s})" 147 148 (*NOTE: to follow the original paper, the formula above should have had 149 INT h. {s. h i \<le> (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s} 150 LeadsTo 151 {s. tokens h i \<le> (tokens o sub i o allocRel)s}) 152 thus h should have been a function variable. However, only h i is ever 153 looked at.*) 154 155definition 156 \<comment> \<open>spec: preserves part\<close> 157 alloc_preserves :: "'a allocState_d program set" 158 where "alloc_preserves = preserves allocRel Int preserves allocAsk Int 159 preserves allocState_d.dummy" 160 161definition 162 \<comment> \<open>environmental constraints\<close> 163 alloc_allowed_acts :: "'a allocState_d program set" 164 where "alloc_allowed_acts = 165 {F. AllowedActs F = 166 insert Id (UNION (preserves allocGiv) Acts)}" 167 168definition 169 alloc_spec :: "'a allocState_d program set" 170 where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int 171 alloc_allowed_acts Int alloc_preserves" 172 173 174subsubsection \<open>Network specification\<close> 175 176definition 177 \<comment> \<open>spec (9.1)\<close> 178 network_ask :: "'a systemState program set" 179 where "network_ask = (INT i : lessThan Nclients. 180 Increasing (ask o sub i o client) guarantees 181 ((sub i o allocAsk) Fols (ask o sub i o client)))" 182 183definition 184 \<comment> \<open>spec (9.2)\<close> 185 network_giv :: "'a systemState program set" 186 where "network_giv = (INT i : lessThan Nclients. 187 Increasing (sub i o allocGiv) 188 guarantees 189 ((giv o sub i o client) Fols (sub i o allocGiv)))" 190 191definition 192 \<comment> \<open>spec (9.3)\<close> 193 network_rel :: "'a systemState program set" 194 where "network_rel = (INT i : lessThan Nclients. 195 Increasing (rel o sub i o client) 196 guarantees 197 ((sub i o allocRel) Fols (rel o sub i o client)))" 198 199definition 200 \<comment> \<open>spec: preserves part\<close> 201 network_preserves :: "'a systemState program set" 202 where "network_preserves = 203 preserves allocGiv Int 204 (INT i : lessThan Nclients. preserves (rel o sub i o client) Int 205 preserves (ask o sub i o client))" 206 207definition 208 \<comment> \<open>environmental constraints\<close> 209 network_allowed_acts :: "'a systemState program set" 210 where "network_allowed_acts = 211 {F. AllowedActs F = 212 insert Id 213 (UNION (preserves allocRel Int 214 (INT i: lessThan Nclients. preserves(giv o sub i o client))) 215 Acts)}" 216 217definition 218 network_spec :: "'a systemState program set" 219 where "network_spec = network_ask Int network_giv Int 220 network_rel Int network_allowed_acts Int 221 network_preserves" 222 223 224subsubsection \<open>State mappings\<close> 225 226definition 227 sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState" 228 where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s 229 in (| allocGiv = allocGiv s, 230 allocAsk = allocAsk s, 231 allocRel = allocRel s, 232 client = cl, 233 dummy = xtr|))" 234 235 236definition 237 sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState" 238 where "sysOfClient = (%(cl,al). (| allocGiv = allocGiv al, 239 allocAsk = allocAsk al, 240 allocRel = allocRel al, 241 client = cl, 242 systemState.dummy = allocState_d.dummy al|))" 243 244axiomatization Alloc :: "'a allocState_d program" 245 where Alloc: "Alloc \<in> alloc_spec" 246 247axiomatization Client :: "'a clientState_d program" 248 where Client: "Client \<in> client_spec" 249 250axiomatization Network :: "'a systemState program" 251 where Network: "Network \<in> network_spec" 252 253definition System :: "'a systemState program" 254 where "System = rename sysOfAlloc Alloc \<squnion> Network \<squnion> 255 (rename sysOfClient 256 (plam x: lessThan Nclients. rename client_map Client))" 257 258 259(** 260locale System = 261 fixes 262 Alloc :: 'a allocState_d program 263 Client :: 'a clientState_d program 264 Network :: 'a systemState program 265 System :: 'a systemState program 266 267 assumes 268 Alloc "Alloc : alloc_spec" 269 Client "Client : client_spec" 270 Network "Network : network_spec" 271 272 defines 273 System_def 274 "System == rename sysOfAlloc Alloc 275 \<squnion> 276 Network 277 \<squnion> 278 (rename sysOfClient 279 (plam x: lessThan Nclients. rename client_map Client))" 280**) 281 282declare subset_preserves_o [THEN [2] rev_subsetD, intro] 283declare subset_preserves_o [THEN [2] rev_subsetD, simp] 284declare funPair_o_distrib [simp] 285declare Always_INT_distrib [simp] 286declare o_apply [simp del] 287 288(*For rewriting of specifications related by "guarantees"*) 289lemmas [simp] = 290 rename_image_constrains 291 rename_image_stable 292 rename_image_increasing 293 rename_image_invariant 294 rename_image_Constrains 295 rename_image_Stable 296 rename_image_Increasing 297 rename_image_Always 298 rename_image_leadsTo 299 rename_image_LeadsTo 300 rename_preserves 301 rename_image_preserves 302 lift_image_preserves 303 bij_image_INT 304 bij_is_inj [THEN image_Int] 305 bij_image_Collect_eq 306 307ML \<open> 308(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*) 309fun list_of_Int th = 310 (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2)) 311 handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2)) 312 handle THM _ => (list_of_Int (th RS @{thm INT_D})) 313 handle THM _ => (list_of_Int (th RS bspec)) 314 handle THM _ => [th]; 315\<close> 316 317lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec] 318 319attribute_setup normalized = \<open> 320let 321 fun normalized th = 322 normalized (th RS spec 323 handle THM _ => th RS @{thm lessThanBspec} 324 handle THM _ => th RS bspec 325 handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1)) 326 handle THM _ => th; 327in 328 Scan.succeed (Thm.rule_attribute [] (K normalized)) 329end 330\<close> 331 332(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***) 333ML \<open> 334fun record_auto_tac ctxt = 335 let val ctxt' = 336 ctxt addSWrapper Record.split_wrapper 337 addsimps 338 [@{thm sysOfAlloc_def}, @{thm sysOfClient_def}, 339 @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def}, 340 @{thm o_apply}, @{thm Let_def}] 341 in auto_tac ctxt' end; 342 343\<close> 344 345method_setup record_auto = \<open>Scan.succeed (SIMPLE_METHOD o record_auto_tac)\<close> 346 347lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc" 348 apply (unfold sysOfAlloc_def Let_def) 349 apply (rule inj_onI) 350 apply record_auto 351 done 352 353text\<open>We need the inverse; also having it simplifies the proof of surjectivity\<close> 354lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s = 355 (| allocGiv = allocGiv s, 356 allocAsk = allocAsk s, 357 allocRel = allocRel s, 358 allocState_d.dummy = (client s, dummy s) |)" 359 apply (rule inj_sysOfAlloc [THEN inv_f_eq]) 360 apply record_auto 361 done 362 363lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc" 364 apply (simp add: surj_iff_all) 365 apply record_auto 366 done 367 368lemma bij_sysOfAlloc [iff]: "bij sysOfAlloc" 369 apply (blast intro: bijI) 370 done 371 372 373subsubsection\<open>bijectivity of @{term sysOfClient}\<close> 374 375lemma inj_sysOfClient [iff]: "inj sysOfClient" 376 apply (unfold sysOfClient_def) 377 apply (rule inj_onI) 378 apply record_auto 379 done 380 381lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s = 382 (client s, 383 (| allocGiv = allocGiv s, 384 allocAsk = allocAsk s, 385 allocRel = allocRel s, 386 allocState_d.dummy = systemState.dummy s|) )" 387 apply (rule inj_sysOfClient [THEN inv_f_eq]) 388 apply record_auto 389 done 390 391lemma surj_sysOfClient [iff]: "surj sysOfClient" 392 apply (simp add: surj_iff_all) 393 apply record_auto 394 done 395 396lemma bij_sysOfClient [iff]: "bij sysOfClient" 397 apply (blast intro: bijI) 398 done 399 400 401subsubsection\<open>bijectivity of @{term client_map}\<close> 402 403lemma inj_client_map [iff]: "inj client_map" 404 apply (unfold inj_on_def) 405 apply record_auto 406 done 407 408lemma inv_client_map_eq [simp]: "!!s. inv client_map s = 409 (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, 410 clientState_d.dummy = y|)) s" 411 apply (rule inj_client_map [THEN inv_f_eq]) 412 apply record_auto 413 done 414 415lemma surj_client_map [iff]: "surj client_map" 416 apply (simp add: surj_iff_all) 417 apply record_auto 418 done 419 420lemma bij_client_map [iff]: "bij client_map" 421 apply (blast intro: bijI) 422 done 423 424 425text\<open>o-simprules for @{term client_map}\<close> 426 427lemma fst_o_client_map: "fst o client_map = non_dummy" 428 apply (unfold client_map_def) 429 apply (rule fst_o_funPair) 430 done 431 432ML \<open>ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map})\<close> 433declare fst_o_client_map' [simp] 434 435lemma snd_o_client_map: "snd o client_map = clientState_d.dummy" 436 apply (unfold client_map_def) 437 apply (rule snd_o_funPair) 438 done 439 440ML \<open>ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map})\<close> 441declare snd_o_client_map' [simp] 442 443 444subsection\<open>o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]\<close> 445 446lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy " 447 apply record_auto 448 done 449 450ML \<open>ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc})\<close> 451declare client_o_sysOfAlloc' [simp] 452 453lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv" 454 apply record_auto 455 done 456 457ML \<open>ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq})\<close> 458declare allocGiv_o_sysOfAlloc_eq' [simp] 459 460lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk" 461 apply record_auto 462 done 463 464ML \<open>ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq})\<close> 465declare allocAsk_o_sysOfAlloc_eq' [simp] 466 467lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel" 468 apply record_auto 469 done 470 471ML \<open>ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq})\<close> 472declare allocRel_o_sysOfAlloc_eq' [simp] 473 474 475subsection\<open>o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]\<close> 476 477lemma client_o_sysOfClient: "client o sysOfClient = fst" 478 apply record_auto 479 done 480 481ML \<open>ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient})\<close> 482declare client_o_sysOfClient' [simp] 483 484lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd " 485 apply record_auto 486 done 487 488ML \<open>ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq})\<close> 489declare allocGiv_o_sysOfClient_eq' [simp] 490 491lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd " 492 apply record_auto 493 done 494 495ML \<open>ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq})\<close> 496declare allocAsk_o_sysOfClient_eq' [simp] 497 498lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd " 499 apply record_auto 500 done 501 502ML \<open>ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq})\<close> 503declare allocRel_o_sysOfClient_eq' [simp] 504 505lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv" 506 apply (simp add: o_def) 507 done 508 509ML \<open>ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq})\<close> 510declare allocGiv_o_inv_sysOfAlloc_eq' [simp] 511 512lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk" 513 apply (simp add: o_def) 514 done 515 516ML \<open>ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq})\<close> 517declare allocAsk_o_inv_sysOfAlloc_eq' [simp] 518 519lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel" 520 apply (simp add: o_def) 521 done 522 523ML \<open>ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq})\<close> 524declare allocRel_o_inv_sysOfAlloc_eq' [simp] 525 526lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) = 527 rel o sub i o client" 528 apply (simp add: o_def drop_map_def) 529 done 530 531ML \<open>ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map})\<close> 532declare rel_inv_client_map_drop_map [simp] 533 534lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) = 535 ask o sub i o client" 536 apply (simp add: o_def drop_map_def) 537 done 538 539ML \<open>ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map})\<close> 540declare ask_inv_client_map_drop_map [simp] 541 542 543text\<open>Client : <unfolded specification>\<close> 544lemmas client_spec_simps = 545 client_spec_def client_increasing_def client_bounded_def 546 client_progress_def client_allowed_acts_def client_preserves_def 547 guarantees_Int_right 548 549ML \<open> 550val [Client_Increasing_ask, Client_Increasing_rel, 551 Client_Bounded, Client_Progress, Client_AllowedActs, 552 Client_preserves_giv, Client_preserves_dummy] = 553 @{thm Client} |> simplify (@{context} addsimps @{thms client_spec_simps}) 554 |> list_of_Int; 555 556ML_Thms.bind_thm ("Client_Increasing_ask", Client_Increasing_ask); 557ML_Thms.bind_thm ("Client_Increasing_rel", Client_Increasing_rel); 558ML_Thms.bind_thm ("Client_Bounded", Client_Bounded); 559ML_Thms.bind_thm ("Client_Progress", Client_Progress); 560ML_Thms.bind_thm ("Client_AllowedActs", Client_AllowedActs); 561ML_Thms.bind_thm ("Client_preserves_giv", Client_preserves_giv); 562ML_Thms.bind_thm ("Client_preserves_dummy", Client_preserves_dummy); 563\<close> 564 565declare 566 Client_Increasing_ask [iff] 567 Client_Increasing_rel [iff] 568 Client_Bounded [iff] 569 Client_preserves_giv [iff] 570 Client_preserves_dummy [iff] 571 572 573text\<open>Network : <unfolded specification>\<close> 574lemmas network_spec_simps = 575 network_spec_def network_ask_def network_giv_def 576 network_rel_def network_allowed_acts_def network_preserves_def 577 ball_conj_distrib 578 579ML \<open> 580val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs, 581 Network_preserves_allocGiv, Network_preserves_rel, 582 Network_preserves_ask] = 583 @{thm Network} |> simplify (@{context} addsimps @{thms network_spec_simps}) 584 |> list_of_Int; 585 586ML_Thms.bind_thm ("Network_Ask", Network_Ask); 587ML_Thms.bind_thm ("Network_Giv", Network_Giv); 588ML_Thms.bind_thm ("Network_Rel", Network_Rel); 589ML_Thms.bind_thm ("Network_AllowedActs", Network_AllowedActs); 590ML_Thms.bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv); 591ML_Thms.bind_thm ("Network_preserves_rel", Network_preserves_rel); 592ML_Thms.bind_thm ("Network_preserves_ask", Network_preserves_ask); 593\<close> 594 595declare Network_preserves_allocGiv [iff] 596 597declare 598 Network_preserves_rel [simp] 599 Network_preserves_ask [simp] 600 601declare 602 Network_preserves_rel [simplified o_def, simp] 603 Network_preserves_ask [simplified o_def, simp] 604 605text\<open>Alloc : <unfolded specification>\<close> 606lemmas alloc_spec_simps = 607 alloc_spec_def alloc_increasing_def alloc_safety_def 608 alloc_progress_def alloc_allowed_acts_def alloc_preserves_def 609 610ML \<open> 611val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs, 612 Alloc_preserves_allocRel, Alloc_preserves_allocAsk, 613 Alloc_preserves_dummy] = 614 @{thm Alloc} |> simplify (@{context} addsimps @{thms alloc_spec_simps}) 615 |> list_of_Int; 616 617ML_Thms.bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0); 618ML_Thms.bind_thm ("Alloc_Safety", Alloc_Safety); 619ML_Thms.bind_thm ("Alloc_Progress", Alloc_Progress); 620ML_Thms.bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs); 621ML_Thms.bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel); 622ML_Thms.bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk); 623ML_Thms.bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy); 624\<close> 625 626text\<open>Strip off the INT in the guarantees postcondition\<close> 627 628lemmas Alloc_Increasing = Alloc_Increasing_0 [normalized] 629 630declare 631 Alloc_preserves_allocRel [iff] 632 Alloc_preserves_allocAsk [iff] 633 Alloc_preserves_dummy [iff] 634 635 636subsection\<open>Components Lemmas [MUST BE AUTOMATED]\<close> 637 638lemma Network_component_System: "Network \<squnion> 639 ((rename sysOfClient 640 (plam x: (lessThan Nclients). rename client_map Client)) \<squnion> 641 rename sysOfAlloc Alloc) 642 = System" 643 by (simp add: System_def Join_ac) 644 645lemma Client_component_System: "(rename sysOfClient 646 (plam x: (lessThan Nclients). rename client_map Client)) \<squnion> 647 (Network \<squnion> rename sysOfAlloc Alloc) = System" 648 by (simp add: System_def Join_ac) 649 650lemma Alloc_component_System: "rename sysOfAlloc Alloc \<squnion> 651 ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) \<squnion> 652 Network) = System" 653 by (simp add: System_def Join_ac) 654 655declare 656 Client_component_System [iff] 657 Network_component_System [iff] 658 Alloc_component_System [iff] 659 660 661text\<open>* These preservation laws should be generated automatically *\<close> 662 663lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask" 664 by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff) 665 666lemma Network_Allowed [simp]: "Allowed Network = 667 preserves allocRel Int 668 (INT i: lessThan Nclients. preserves(giv o sub i o client))" 669 by (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff) 670 671lemma Alloc_Allowed [simp]: "Allowed Alloc = preserves allocGiv" 672 by (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff) 673 674text\<open>needed in \<open>rename_client_map_tac\<close>\<close> 675lemma OK_lift_rename_Client [simp]: "OK I (%i. lift i (rename client_map Client))" 676 apply (rule OK_lift_I) 677 apply auto 678 apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD]) 679 apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD]) 680 apply (auto simp add: o_def split_def) 681 done 682 683lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x" 684apply (insert fst_o_lift_map [of i]) 685apply (drule fun_cong [where x=x]) 686apply (simp add: o_def) 687done 688 689lemma fst_o_lift_map' [simp]: 690 "(f \<circ> sub i \<circ> fst \<circ> lift_map i \<circ> g) = f o fst o g" 691apply (subst fst_o_lift_map [symmetric]) 692apply (simp only: o_assoc) 693done 694 695 696(*The proofs of rename_Client_Increasing, rename_Client_Bounded and 697 rename_Client_Progress are similar. All require copying out the original 698 Client property. A forward proof can be constructed as follows: 699 700 Client_Increasing_ask RS 701 (bij_client_map RS rename_rename_guarantees_eq RS iffD2) 702 RS (lift_lift_guarantees_eq RS iffD2) 703 RS guarantees_PLam_I 704 RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2) 705 |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def, 706 surj_rename]) 707 708However, the "preserves" property remains to be discharged, and the unfolding 709of "o" and "sub" complicates subsequent reasoning. 710 711The following tactic works for all three proofs, though it certainly looks 712ad-hoc! 713*) 714ML 715\<open> 716fun rename_client_map_tac ctxt = 717 EVERY [ 718 simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1, 719 resolve_tac ctxt @{thms guarantees_PLam_I} 1, 720 assume_tac ctxt 2, 721 (*preserves: routine reasoning*) 722 asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2, 723 (*the guarantee for "lift i (rename client_map Client)" *) 724 asm_simp_tac 725 (ctxt addsimps [@{thm lift_guarantees_eq_lift_inv}, 726 @{thm rename_guarantees_eq_rename_inv}, 727 @{thm bij_imp_bij_inv}, @{thm surj_rename}, 728 @{thm inv_inv_eq}]) 1, 729 asm_simp_tac 730 (ctxt addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1] 731\<close> 732 733method_setup rename_client_map = \<open> 734 Scan.succeed (fn ctxt => SIMPLE_METHOD (rename_client_map_tac ctxt)) 735\<close> 736 737text\<open>Lifting \<open>Client_Increasing\<close> to @{term systemState}\<close> 738lemma rename_Client_Increasing: "i \<in> I 739 ==> rename sysOfClient (plam x: I. rename client_map Client) \<in> 740 UNIV guarantees 741 Increasing (ask o sub i o client) Int 742 Increasing (rel o sub i o client)" 743 by rename_client_map 744 745lemma preserves_sub_fst_lift_map: "[| F \<in> preserves w; i \<noteq> j |] 746 ==> F \<in> preserves (sub i o fst o lift_map j o funPair v w)" 747 apply (auto simp add: lift_map_def split_def linorder_neq_iff o_def) 748 apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD]) 749 apply (auto simp add: o_def) 750 done 751 752lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |] 753 ==> Client \<in> preserves (giv o sub i o fst o lift_map j o client_map)" 754 apply (cases "i=j") 755 apply (simp, simp add: o_def non_dummy_def) 756 apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map]) 757 apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD]) 758 apply (simp add: o_def client_map_def) 759 done 760 761lemma rename_sysOfClient_ok_Network: 762 "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) 763 ok Network" 764 by (auto simp add: ok_iff_Allowed client_preserves_giv_oo_client_map) 765 766lemma rename_sysOfClient_ok_Alloc: 767 "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) 768 ok rename sysOfAlloc Alloc" 769 by (simp add: ok_iff_Allowed) 770 771lemma rename_sysOfAlloc_ok_Network: "rename sysOfAlloc Alloc ok Network" 772 by (simp add: ok_iff_Allowed) 773 774declare 775 rename_sysOfClient_ok_Network [iff] 776 rename_sysOfClient_ok_Alloc [iff] 777 rename_sysOfAlloc_ok_Network [iff] 778 779text\<open>The "ok" laws, re-oriented. 780 But not sure this works: theorem \<open>ok_commute\<close> is needed below\<close> 781declare 782 rename_sysOfClient_ok_Network [THEN ok_sym, iff] 783 rename_sysOfClient_ok_Alloc [THEN ok_sym, iff] 784 rename_sysOfAlloc_ok_Network [THEN ok_sym] 785 786lemma System_Increasing: "i < Nclients 787 ==> System \<in> Increasing (ask o sub i o client) Int 788 Increasing (rel o sub i o client)" 789 apply (rule component_guaranteesD [OF rename_Client_Increasing Client_component_System]) 790 apply auto 791 done 792 793lemmas rename_guarantees_sysOfAlloc_I = 794 bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2] 795 796 797(*Lifting Alloc_Increasing up to the level of systemState*) 798lemmas rename_Alloc_Increasing = 799 Alloc_Increasing 800 [THEN rename_guarantees_sysOfAlloc_I, 801 simplified surj_rename o_def sub_apply 802 rename_image_Increasing bij_sysOfAlloc 803 allocGiv_o_inv_sysOfAlloc_eq'] 804 805lemma System_Increasing_allocGiv: 806 "i < Nclients \<Longrightarrow> System \<in> Increasing (sub i o allocGiv)" 807 apply (unfold System_def) 808 apply (simp add: o_def) 809 apply (rule rename_Alloc_Increasing [THEN guarantees_Join_I1, THEN guaranteesD]) 810 apply auto 811 done 812 813 814ML \<open> 815ML_Thms.bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing}) 816\<close> 817 818declare System_Increasing' [intro!] 819 820text\<open>Follows consequences. 821 The "Always (INT ...) formulation expresses the general safety property 822 and allows it to be combined using \<open>Always_Int_rule\<close> below.\<close> 823 824lemma System_Follows_rel: 825 "i < Nclients ==> System \<in> ((sub i o allocRel) Fols (rel o sub i o client))" 826 apply (auto intro!: Network_Rel [THEN component_guaranteesD]) 827 apply (simp add: ok_commute [of Network]) 828 done 829 830lemma System_Follows_ask: 831 "i < Nclients ==> System \<in> ((sub i o allocAsk) Fols (ask o sub i o client))" 832 apply (auto intro!: Network_Ask [THEN component_guaranteesD]) 833 apply (simp add: ok_commute [of Network]) 834 done 835 836lemma System_Follows_allocGiv: 837 "i < Nclients ==> System \<in> (giv o sub i o client) Fols (sub i o allocGiv)" 838 apply (auto intro!: Network_Giv [THEN component_guaranteesD] 839 rename_Alloc_Increasing [THEN component_guaranteesD]) 840 apply (simp_all add: o_def non_dummy_def ok_commute [of Network]) 841 apply (auto intro!: rename_Alloc_Increasing [THEN component_guaranteesD]) 842 done 843 844 845lemma Always_giv_le_allocGiv: "System \<in> Always (INT i: lessThan Nclients. 846 {s. (giv o sub i o client) s \<le> (sub i o allocGiv) s})" 847 apply auto 848 apply (erule System_Follows_allocGiv [THEN Follows_Bounded]) 849 done 850 851 852lemma Always_allocAsk_le_ask: "System \<in> Always (INT i: lessThan Nclients. 853 {s. (sub i o allocAsk) s \<le> (ask o sub i o client) s})" 854 apply auto 855 apply (erule System_Follows_ask [THEN Follows_Bounded]) 856 done 857 858 859lemma Always_allocRel_le_rel: "System \<in> Always (INT i: lessThan Nclients. 860 {s. (sub i o allocRel) s \<le> (rel o sub i o client) s})" 861 by (auto intro!: Follows_Bounded System_Follows_rel) 862 863 864subsection\<open>Proof of the safety property (1)\<close> 865 866text\<open>safety (1), step 1 is \<open>System_Follows_rel\<close>\<close> 867 868text\<open>safety (1), step 2\<close> 869(* i < Nclients ==> System : Increasing (sub i o allocRel) *) 870lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1] 871 872(*Lifting Alloc_safety up to the level of systemState. 873 Simplifying with o_def gets rid of the translations but it unfortunately 874 gets rid of the other "o"s too.*) 875 876text\<open>safety (1), step 3\<close> 877lemma System_sum_bounded: 878 "System \<in> Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s) 879 \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}" 880 apply (simp add: o_apply) 881 apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I]) 882 apply (simp add: o_def) 883 apply (erule component_guaranteesD) 884 apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def]) 885 done 886 887text\<open>Follows reasoning\<close> 888 889lemma Always_tokens_giv_le_allocGiv: "System \<in> Always (INT i: lessThan Nclients. 890 {s. (tokens o giv o sub i o client) s 891 \<le> (tokens o sub i o allocGiv) s})" 892 apply (rule Always_giv_le_allocGiv [THEN Always_weaken]) 893 apply (auto intro: tokens_mono_prefix simp add: o_apply) 894 done 895 896lemma Always_tokens_allocRel_le_rel: "System \<in> Always (INT i: lessThan Nclients. 897 {s. (tokens o sub i o allocRel) s 898 \<le> (tokens o rel o sub i o client) s})" 899 apply (rule Always_allocRel_le_rel [THEN Always_weaken]) 900 apply (auto intro: tokens_mono_prefix simp add: o_apply) 901 done 902 903text\<open>safety (1), step 4 (final result!)\<close> 904theorem System_safety: "System \<in> system_safety" 905 apply (unfold system_safety_def) 906 apply (tactic \<open>resolve_tac @{context} [Always_Int_rule [@{thm System_sum_bounded}, 907 @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS 908 @{thm Always_weaken}] 1\<close>) 909 apply auto 910 apply (rule sum_fun_mono [THEN order_trans]) 911 apply (drule_tac [2] order_trans) 912 apply (rule_tac [2] add_le_mono [OF order_refl sum_fun_mono]) 913 prefer 3 apply assumption 914 apply auto 915 done 916 917subsection \<open>Proof of the progress property (2)\<close> 918 919text\<open>progress (2), step 1 is \<open>System_Follows_ask\<close> and 920 \<open>System_Follows_rel\<close>\<close> 921 922text\<open>progress (2), step 2; see also \<open>System_Increasing_allocRel\<close>\<close> 923(* i < Nclients ==> System : Increasing (sub i o allocAsk) *) 924lemmas System_Increasing_allocAsk = System_Follows_ask [THEN Follows_Increasing1] 925 926text\<open>progress (2), step 3: lifting \<open>Client_Bounded\<close> to systemState\<close> 927lemma rename_Client_Bounded: "i \<in> I 928 ==> rename sysOfClient (plam x: I. rename client_map Client) \<in> 929 UNIV guarantees 930 Always {s. \<forall>elt \<in> set ((ask o sub i o client) s). elt \<le> NbT}" 931 by rename_client_map 932 933 934lemma System_Bounded_ask: "i < Nclients 935 ==> System \<in> Always 936 {s. \<forall>elt \<in> set ((ask o sub i o client) s). elt \<le> NbT}" 937 apply (rule component_guaranteesD [OF rename_Client_Bounded Client_component_System]) 938 apply auto 939 done 940 941lemma Collect_all_imp_eq: "{x. \<forall>y. P y \<longrightarrow> Q x y} = (INT y: {y. P y}. {x. Q x y})" 942 apply blast 943 done 944 945text\<open>progress (2), step 4\<close> 946lemma System_Bounded_allocAsk: "System \<in> Always {s. \<forall>i<Nclients. 947 \<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT}" 948 apply (auto simp add: Collect_all_imp_eq) 949 apply (tactic \<open>resolve_tac @{context} [Always_Int_rule [@{thm Always_allocAsk_le_ask}, 950 @{thm System_Bounded_ask}] RS @{thm Always_weaken}] 1\<close>) 951 apply (auto dest: set_mono) 952 done 953 954text\<open>progress (2), step 5 is \<open>System_Increasing_allocGiv\<close>\<close> 955 956text\<open>progress (2), step 6\<close> 957(* i < Nclients ==> System : Increasing (giv o sub i o client) *) 958lemmas System_Increasing_giv = System_Follows_allocGiv [THEN Follows_Increasing1] 959 960 961lemma rename_Client_Progress: "i \<in> I 962 ==> rename sysOfClient (plam x: I. rename client_map Client) 963 \<in> Increasing (giv o sub i o client) 964 guarantees 965 (INT h. {s. h \<le> (giv o sub i o client) s & 966 h pfixGe (ask o sub i o client) s} 967 LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})" 968 apply rename_client_map 969 apply (simp add: Client_Progress [simplified o_def]) 970 done 971 972 973text\<open>progress (2), step 7\<close> 974lemma System_Client_Progress: 975 "System \<in> (INT i : (lessThan Nclients). 976 INT h. {s. h \<le> (giv o sub i o client) s & 977 h pfixGe (ask o sub i o client) s} 978 LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})" 979 apply (rule INT_I) 980(*Couldn't have just used Auto_tac since the "INT h" must be kept*) 981 apply (rule component_guaranteesD [OF rename_Client_Progress Client_component_System]) 982 apply (auto simp add: System_Increasing_giv) 983 done 984 985(*Concludes 986 System : {s. k \<le> (sub i o allocGiv) s} 987 LeadsTo 988 {s. (sub i o allocAsk) s \<le> (ask o sub i o client) s} Int 989 {s. k \<le> (giv o sub i o client) s} *) 990 991lemmas System_lemma1 = 992 Always_LeadsToD [OF System_Follows_ask [THEN Follows_Bounded] 993 System_Follows_allocGiv [THEN Follows_LeadsTo]] 994 995lemmas System_lemma2 = 996 PSP_Stable [OF System_lemma1 997 System_Follows_ask [THEN Follows_Increasing1, THEN IncreasingD]] 998 999 1000lemma System_lemma3: "i < Nclients 1001 ==> System \<in> {s. h \<le> (sub i o allocGiv) s & 1002 h pfixGe (sub i o allocAsk) s} 1003 LeadsTo 1004 {s. h \<le> (giv o sub i o client) s & 1005 h pfixGe (ask o sub i o client) s}" 1006 apply (rule single_LeadsTo_I) 1007 apply (rule_tac k1 = h and x1 = "(sub i o allocAsk) s" 1008 in System_lemma2 [THEN LeadsTo_weaken]) 1009 apply auto 1010 apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe) 1011 done 1012 1013 1014text\<open>progress (2), step 8: Client i's "release" action is visible system-wide\<close> 1015lemma System_Alloc_Client_Progress: "i < Nclients 1016 ==> System \<in> {s. h \<le> (sub i o allocGiv) s & 1017 h pfixGe (sub i o allocAsk) s} 1018 LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel) s}" 1019 apply (rule LeadsTo_Trans) 1020 prefer 2 1021 apply (drule System_Follows_rel [THEN 1022 mono_tokens [THEN mono_Follows_o, THEN [2] rev_subsetD], 1023 THEN Follows_LeadsTo]) 1024 apply (simp add: o_assoc) 1025 apply (rule LeadsTo_Trans) 1026 apply (cut_tac [2] System_Client_Progress) 1027 prefer 2 1028 apply (blast intro: LeadsTo_Basis) 1029 apply (erule System_lemma3) 1030 done 1031 1032text\<open>Lifting \<open>Alloc_Progress\<close> up to the level of systemState\<close> 1033 1034text\<open>progress (2), step 9\<close> 1035lemma System_Alloc_Progress: 1036 "System \<in> (INT i : (lessThan Nclients). 1037 INT h. {s. h \<le> (sub i o allocAsk) s} 1038 LeadsTo {s. h pfixLe (sub i o allocGiv) s})" 1039 apply (simp only: o_apply sub_def) 1040 apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I]) 1041 apply (simp add: o_def del: INT_iff) 1042 apply (drule component_guaranteesD) 1043 apply (auto simp add: 1044 System_Increasing_allocRel [simplified sub_apply o_def] 1045 System_Increasing_allocAsk [simplified sub_apply o_def] 1046 System_Bounded_allocAsk [simplified sub_apply o_def] 1047 System_Alloc_Client_Progress [simplified sub_apply o_def]) 1048 done 1049 1050text\<open>progress (2), step 10 (final result!)\<close> 1051lemma System_Progress: "System \<in> system_progress" 1052 apply (unfold system_progress_def) 1053 apply (cut_tac System_Alloc_Progress) 1054 apply auto 1055 apply (blast intro: LeadsTo_Trans 1056 System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe] 1057 System_Follows_ask [THEN Follows_LeadsTo]) 1058 done 1059 1060 1061theorem System_correct: "System \<in> system_spec" 1062 apply (unfold system_spec_def) 1063 apply (blast intro: System_safety System_Progress) 1064 done 1065 1066 1067text\<open>Some obsolete lemmas\<close> 1068 1069lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o 1070 (funPair giv (funPair ask rel))" 1071 apply (rule ext) 1072 apply (auto simp add: o_def non_dummy_def) 1073 done 1074 1075lemma preserves_non_dummy_eq: "(preserves non_dummy) = 1076 (preserves rel Int preserves ask Int preserves giv)" 1077 apply (simp add: non_dummy_eq_o_funPair) 1078 apply auto 1079 apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD]) 1080 apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD]) 1081 apply (drule_tac [3] w1 = giv in subset_preserves_o [THEN [2] rev_subsetD]) 1082 apply (auto simp add: o_def) 1083 done 1084 1085text\<open>Could go to Extend.ML\<close> 1086lemma bij_fst_inv_inv_eq: "bij f \<Longrightarrow> fst (inv (%(x, u). inv f x) z) = f z" 1087 apply (rule fst_inv_equalityI) 1088 apply (rule_tac f = "%z. (f z, h z)" for h in surjI) 1089 apply (simp add: bij_is_inj inv_f_f) 1090 apply (simp add: bij_is_surj surj_f_inv_f) 1091 done 1092 1093end 1094