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