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