1(* Title: HOL/UNITY/Simple/Lift.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5The Lift-Control Example. 6*) 7 8theory Lift 9imports "../UNITY_Main" 10begin 11 12record state = 13 floor :: "int" \<comment> \<open>current position of the lift\<close> 14 "open" :: "bool" \<comment> \<open>whether the door is opened at floor\<close> 15 stop :: "bool" \<comment> \<open>whether the lift is stopped at floor\<close> 16 req :: "int set" \<comment> \<open>for each floor, whether the lift is requested\<close> 17 up :: "bool" \<comment> \<open>current direction of movement\<close> 18 move :: "bool" \<comment> \<open>whether moving takes precedence over opening\<close> 19 20axiomatization 21 Min :: "int" and \<comment> \<open>least and greatest floors\<close> 22 Max :: "int" \<comment> \<open>least and greatest floors\<close> 23where 24 Min_le_Max [iff]: "Min \<le> Max" 25 26 27 \<comment> \<open>Abbreviations: the "always" part\<close> 28 29definition 30 above :: "state set" 31 where "above = {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}" 32 33definition 34 below :: "state set" 35 where "below = {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}" 36 37definition 38 queueing :: "state set" 39 where "queueing = above \<union> below" 40 41definition 42 goingup :: "state set" 43 where "goingup = above \<inter> ({s. up s} \<union> -below)" 44 45definition 46 goingdown :: "state set" 47 where "goingdown = below \<inter> ({s. ~ up s} \<union> -above)" 48 49definition 50 ready :: "state set" 51 where "ready = {s. stop s & ~ open s & move s}" 52 53 \<comment> \<open>Further abbreviations\<close> 54 55definition 56 moving :: "state set" 57 where "moving = {s. ~ stop s & ~ open s}" 58 59definition 60 stopped :: "state set" 61 where "stopped = {s. stop s & ~ open s & ~ move s}" 62 63definition 64 opened :: "state set" 65 where "opened = {s. stop s & open s & move s}" 66 67definition 68 closed :: "state set" \<comment> \<open>but this is the same as ready!!\<close> 69 where "closed = {s. stop s & ~ open s & move s}" 70 71definition 72 atFloor :: "int => state set" 73 where "atFloor n = {s. floor s = n}" 74 75definition 76 Req :: "int => state set" 77 where "Req n = {s. n \<in> req s}" 78 79 80 81 \<comment> \<open>The program\<close> 82 83definition 84 request_act :: "(state*state) set" 85 where "request_act = {(s,s'). s' = s (|stop:=True, move:=False|) 86 & ~ stop s & floor s \<in> req s}" 87 88definition 89 open_act :: "(state*state) set" 90 where "open_act = 91 {(s,s'). s' = s (|open :=True, 92 req := req s - {floor s}, 93 move := True|) 94 & stop s & ~ open s & floor s \<in> req s 95 & ~(move s & s \<in> queueing)}" 96 97definition 98 close_act :: "(state*state) set" 99 where "close_act = {(s,s'). s' = s (|open := False|) & open s}" 100 101definition 102 req_up :: "(state*state) set" 103 where "req_up = 104 {(s,s'). s' = s (|stop :=False, 105 floor := floor s + 1, 106 up := True|) 107 & s \<in> (ready \<inter> goingup)}" 108 109definition 110 req_down :: "(state*state) set" 111 where "req_down = 112 {(s,s'). s' = s (|stop :=False, 113 floor := floor s - 1, 114 up := False|) 115 & s \<in> (ready \<inter> goingdown)}" 116 117definition 118 move_up :: "(state*state) set" 119 where "move_up = 120 {(s,s'). s' = s (|floor := floor s + 1|) 121 & ~ stop s & up s & floor s \<notin> req s}" 122 123definition 124 move_down :: "(state*state) set" 125 where "move_down = 126 {(s,s'). s' = s (|floor := floor s - 1|) 127 & ~ stop s & ~ up s & floor s \<notin> req s}" 128 129definition 130 button_press :: "(state*state) set" 131 \<comment> \<open>This action is omitted from prior treatments, which therefore are 132 unrealistic: nobody asks the lift to do anything! But adding this 133 action invalidates many of the existing progress arguments: various 134 "ensures" properties fail. Maybe it should be constrained to only 135 allow button presses in the current direction of travel, like in a 136 real lift.\<close> 137 where "button_press = 138 {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|) 139 & Min \<le> n & n \<le> Max}" 140 141 142definition 143 Lift :: "state program" 144 \<comment> \<open>for the moment, we OMIT \<open>button_press\<close>\<close> 145 where "Lift = mk_total_program 146 ({s. floor s = Min & ~ up s & move s & stop s & 147 ~ open s & req s = {}}, 148 {request_act, open_act, close_act, 149 req_up, req_down, move_up, move_down}, 150 UNIV)" 151 152 153 \<comment> \<open>Invariants\<close> 154 155definition 156 bounded :: "state set" 157 where "bounded = {s. Min \<le> floor s & floor s \<le> Max}" 158 159definition 160 open_stop :: "state set" 161 where "open_stop = {s. open s --> stop s}" 162 163definition 164 open_move :: "state set" 165 where "open_move = {s. open s --> move s}" 166 167definition 168 stop_floor :: "state set" 169 where "stop_floor = {s. stop s & ~ move s --> floor s \<in> req s}" 170 171definition 172 moving_up :: "state set" 173 where "moving_up = {s. ~ stop s & up s --> 174 (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}" 175 176definition 177 moving_down :: "state set" 178 where "moving_down = {s. ~ stop s & ~ up s --> 179 (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}" 180 181definition 182 metric :: "[int,state] => int" 183 where "metric = 184 (%n s. if floor s < n then (if up s then n - floor s 185 else (floor s - Min) + (n-Min)) 186 else 187 if n < floor s then (if up s then (Max - floor s) + (Max-n) 188 else floor s - n) 189 else 0)" 190 191locale Floor = 192 fixes n 193 assumes Min_le_n [iff]: "Min \<le> n" 194 and n_le_Max [iff]: "n \<le> Max" 195 196lemma not_mem_distinct: "[| x \<notin> A; y \<in> A |] ==> x \<noteq> y" 197by blast 198 199 200declare Lift_def [THEN def_prg_Init, simp] 201 202declare request_act_def [THEN def_act_simp, simp] 203declare open_act_def [THEN def_act_simp, simp] 204declare close_act_def [THEN def_act_simp, simp] 205declare req_up_def [THEN def_act_simp, simp] 206declare req_down_def [THEN def_act_simp, simp] 207declare move_up_def [THEN def_act_simp, simp] 208declare move_down_def [THEN def_act_simp, simp] 209declare button_press_def [THEN def_act_simp, simp] 210 211(*The ALWAYS properties*) 212declare above_def [THEN def_set_simp, simp] 213declare below_def [THEN def_set_simp, simp] 214declare queueing_def [THEN def_set_simp, simp] 215declare goingup_def [THEN def_set_simp, simp] 216declare goingdown_def [THEN def_set_simp, simp] 217declare ready_def [THEN def_set_simp, simp] 218 219(*Basic definitions*) 220declare bounded_def [simp] 221 open_stop_def [simp] 222 open_move_def [simp] 223 stop_floor_def [simp] 224 moving_up_def [simp] 225 moving_down_def [simp] 226 227lemma open_stop: "Lift \<in> Always open_stop" 228apply (rule AlwaysI, force) 229apply (unfold Lift_def, safety) 230done 231 232lemma stop_floor: "Lift \<in> Always stop_floor" 233apply (rule AlwaysI, force) 234apply (unfold Lift_def, safety) 235done 236 237(*This one needs open_stop, which was proved above*) 238lemma open_move: "Lift \<in> Always open_move" 239apply (cut_tac open_stop) 240apply (rule AlwaysI, force) 241apply (unfold Lift_def, safety) 242done 243 244lemma moving_up: "Lift \<in> Always moving_up" 245apply (rule AlwaysI, force) 246apply (unfold Lift_def, safety) 247apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq) 248done 249 250lemma moving_down: "Lift \<in> Always moving_down" 251apply (rule AlwaysI, force) 252apply (unfold Lift_def, safety) 253apply (blast dest: order_le_imp_less_or_eq) 254done 255 256lemma bounded: "Lift \<in> Always bounded" 257apply (cut_tac moving_up moving_down) 258apply (rule AlwaysI, force) 259apply (unfold Lift_def, safety, auto) 260apply (drule not_mem_distinct, assumption, arith)+ 261done 262 263 264subsection\<open>Progress\<close> 265 266declare moving_def [THEN def_set_simp, simp] 267declare stopped_def [THEN def_set_simp, simp] 268declare opened_def [THEN def_set_simp, simp] 269declare closed_def [THEN def_set_simp, simp] 270declare atFloor_def [THEN def_set_simp, simp] 271declare Req_def [THEN def_set_simp, simp] 272 273 274text\<open>The HUG'93 paper mistakenly omits the Req n from these!\<close> 275 276(** Lift_1 **) 277lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)" 278apply (cut_tac stop_floor) 279apply (unfold Lift_def, ensures_tac "open_act") 280done (*lem_lift_1_5*) 281 282 283 284 285lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo 286 (Req n \<inter> opened - atFloor n)" 287apply (cut_tac stop_floor) 288apply (unfold Lift_def, ensures_tac "open_act") 289done (*lem_lift_1_1*) 290 291lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo 292 (Req n \<inter> closed - (atFloor n - queueing))" 293apply (unfold Lift_def, ensures_tac "close_act") 294done (*lem_lift_1_2*) 295 296lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing)) 297 LeadsTo (opened \<inter> atFloor n)" 298apply (unfold Lift_def, ensures_tac "open_act") 299done (*lem_lift_1_7*) 300 301 302(** Lift 2. Statements of thm05a and thm05b were wrong! **) 303 304lemmas linorder_leI = linorder_not_less [THEN iffD1] 305 306context Floor 307begin 308 309lemmas le_MinD = Min_le_n [THEN order_antisym] 310 and Max_leD = n_le_Max [THEN [2] order_antisym] 311 312declare le_MinD [dest!] 313 and linorder_leI [THEN le_MinD, dest!] 314 and Max_leD [dest!] 315 and linorder_leI [THEN Max_leD, dest!] 316 317 318(*lem_lift_2_0 319 NOT an ensures_tac property, but a mere inclusion 320 don't know why script lift_2.uni says ENSURES*) 321lemma E_thm05c: 322 "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing)) 323 LeadsTo ((closed \<inter> goingup \<inter> Req n) \<union> 324 (closed \<inter> goingdown \<inter> Req n))" 325by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff) 326 327(*lift_2*) 328lemma lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing)) 329 LeadsTo (moving \<inter> Req n)" 330apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un]) 331apply (unfold Lift_def) 332apply (ensures_tac [2] "req_down") 333apply (ensures_tac "req_up", auto) 334done 335 336 337(** Towards lift_4 ***) 338 339declare if_split_asm [split] 340 341 342(*lem_lift_4_1 *) 343lemma E_thm12a: 344 "0 < N ==> 345 Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 346 {s. floor s \<notin> req s} \<inter> {s. up s}) 347 LeadsTo 348 (moving \<inter> Req n \<inter> {s. metric n s < N})" 349apply (cut_tac moving_up) 350apply (unfold Lift_def, ensures_tac "move_up", safe) 351(*this step consolidates two formulae to the goal metric n s' \<le> metric n s*) 352apply (erule linorder_leI [THEN order_antisym, symmetric]) 353apply (auto simp add: metric_def) 354done 355 356 357(*lem_lift_4_3 *) 358lemma E_thm12b: "0 < N ==> 359 Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 360 {s. floor s \<notin> req s} - {s. up s}) 361 LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})" 362apply (cut_tac moving_down) 363apply (unfold Lift_def, ensures_tac "move_down", safe) 364(*this step consolidates two formulae to the goal metric n s' \<le> metric n s*) 365apply (erule linorder_leI [THEN order_antisym, symmetric]) 366apply (auto simp add: metric_def) 367done 368 369(*lift_4*) 370lemma lift_4: 371 "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 372 {s. floor s \<notin> req s}) LeadsTo 373 (moving \<inter> Req n \<inter> {s. metric n s < N})" 374apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo 375 LeadsTo_Un [OF E_thm12a E_thm12b]], auto) 376done 377 378 379(** towards lift_5 **) 380 381(*lem_lift_5_3*) 382lemma E_thm16a: "0<N 383 ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo 384 (moving \<inter> Req n \<inter> {s. metric n s < N})" 385apply (cut_tac bounded) 386apply (unfold Lift_def, ensures_tac "req_up") 387apply (auto simp add: metric_def) 388done 389 390 391(*lem_lift_5_1 has ~goingup instead of goingdown*) 392lemma E_thm16b: "0<N ==> 393 Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo 394 (moving \<inter> Req n \<inter> {s. metric n s < N})" 395apply (cut_tac bounded) 396apply (unfold Lift_def, ensures_tac "req_down") 397apply (auto simp add: metric_def) 398done 399 400 401(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, 402 i.e. the trivial disjunction, leading to an asymmetrical proof.*) 403lemma E_thm16c: 404 "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown" 405by (force simp add: metric_def) 406 407 408(*lift_5*) 409lemma lift_5: 410 "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo 411 (moving \<inter> Req n \<inter> {s. metric n s < N})" 412apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo 413 LeadsTo_Un [OF E_thm16a E_thm16b]]) 414apply (drule E_thm16c, auto) 415done 416 417 418(** towards lift_3 **) 419 420(*lemma used to prove lem_lift_3_1*) 421lemma metric_eq_0D [dest]: 422 "[| metric n s = 0; Min \<le> floor s; floor s \<le> Max |] ==> floor s = n" 423by (force simp add: metric_def) 424 425 426(*lem_lift_3_1*) 427lemma E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo 428 (stopped \<inter> atFloor n)" 429apply (cut_tac bounded) 430apply (unfold Lift_def, ensures_tac "request_act", auto) 431done 432 433(*lem_lift_3_5*) 434lemma E_thm13: 435 "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) 436 LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})" 437apply (unfold Lift_def, ensures_tac "request_act") 438apply (auto simp add: metric_def) 439done 440 441(*lem_lift_3_6*) 442lemma E_thm14: "0 < N ==> 443 Lift \<in> 444 (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) 445 LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})" 446apply (unfold Lift_def, ensures_tac "open_act") 447apply (auto simp add: metric_def) 448done 449 450(*lem_lift_3_7*) 451lemma E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N}) 452 LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})" 453apply (unfold Lift_def, ensures_tac "close_act") 454apply (auto simp add: metric_def) 455done 456 457 458(** the final steps **) 459 460lemma lift_3_Req: "0 < N ==> 461 Lift \<in> 462 (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) 463 LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})" 464apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans) 465done 466 467 468(*Now we observe that our integer metric is really a natural number*) 469lemma Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}" 470apply (rule bounded [THEN Always_weaken]) 471apply (auto simp add: metric_def) 472done 473 474lemmas R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11] 475 476lemma lift_3: "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)" 477apply (rule Always_nonneg [THEN integ_0_le_induct]) 478apply (case_tac "0 < z") 479(*If z \<le> 0 then actually z = 0*) 480prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less) 481apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1]) 482apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo 483 LeadsTo_Un [OF lift_4 lift_3_Req]], auto) 484done 485 486 487lemma lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)" 488apply (rule LeadsTo_Trans) 489 prefer 2 490 apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post]) 491 apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un]) 492 apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un]) 493 apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un]) 494 apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03]) 495apply (rule open_move [THEN Always_LeadsToI]) 496apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify) 497(*The case split is not essential but makes the proof much faster.*) 498apply (case_tac "open x", auto) 499done 500 501end 502 503end 504