isabelle: src/HOL/UNITY/Simple/Lift.thy@e2fcd88be55d

     1 (*  Title:      HOL/UNITY/Lift.thy

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1998  University of Cambridge

     6 The Lift-Control Example

     7 *)

     9 theory Lift = UNITY_Main:

    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*)

    19 consts

    20   Min :: "int"       (*least and greatest floors*)

    21   Max :: "int"       (*least and greatest floors*)

    23 axioms

    24   Min_le_Max [iff]: "Min <= Max"

    26 constdefs

    28   (** Abbreviations: the "always" part **)

    30   above :: "state set"

    31     "above == {s. EX i. floor s < i & i <= Max & i : req s}"

    33   below :: "state set"

    34     "below == {s. EX i. Min <= i & i < floor s & i : req s}"

    36   queueing :: "state set"

    37     "queueing == above Un below"

    39   goingup :: "state set"

    40     "goingup   == above Int  ({s. up s}  Un -below)"

    42   goingdown :: "state set"

    43     "goingdown == below Int ({s. ~ up s} Un -above)"

    45   ready :: "state set"

    46     "ready == {s. stop s & ~ open s & move s}"

    48   (** Further abbreviations **)

    50   moving :: "state set"

    51     "moving ==  {s. ~ stop s & ~ open s}"

    53   stopped :: "state set"

    54     "stopped == {s. stop s  & ~ open s & ~ move s}"

    56   opened :: "state set"

    57     "opened ==  {s. stop s  &  open s  &  move s}"

    59   closed :: "state set"  (*but this is the same as ready!!*)

    60     "closed ==  {s. stop s  & ~ open s &  move s}"

    62   atFloor :: "int => state set"

    63     "atFloor n ==  {s. floor s = n}"

    65   Req :: "int => state set"

    66     "Req n ==  {s. n : req s}"

    70   (** The program **)

    72   request_act :: "(state*state) set"

    73     "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)

    74 		                  & ~ stop s & floor s : req s}"

    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 : req s

    82 	               & ~(move s & s: queueing)}"

    84   close_act :: "(state*state) set"

    85     "close_act == {(s,s'). s' = s (|open := False|) & open s}"

    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 : (ready Int goingup)}"

    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 : (ready Int goingdown)}"

   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 ~: req s}"

   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 ~: req s}"

   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'). EX n. s' = s (|req := insert n (req s)|)

   118 		        & Min <= n & n <= Max}"

   121   Lift :: "state program"

   122     (*for the moment, we OMIT button_press*)

   123     "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &

   124 		          ~ open s & req s = {}},

   125 			 {request_act, open_act, close_act,

   126 			  req_up, req_down, move_up, move_down},

   127 			 UNIV)"

   130   (** Invariants **)

   132   bounded :: "state set"

   133     "bounded == {s. Min <= floor s & floor s <= Max}"

   135   open_stop :: "state set"

   136     "open_stop == {s. open s --> stop s}"

   138   open_move :: "state set"

   139     "open_move == {s. open s --> move s}"

   141   stop_floor :: "state set"

   142     "stop_floor == {s. stop s & ~ move s --> floor s : req s}"

   144   moving_up :: "state set"

   145     "moving_up == {s. ~ stop s & up s -->

   146                    (EX f. floor s <= f & f <= Max & f : req s)}"

   148   moving_down :: "state set"

   149     "moving_down == {s. ~ stop s & ~ up s -->

   150                      (EX f. Min <= f & f <= floor s & f : req s)}"

   152   metric :: "[int,state] => int"

   153     "metric ==

   154        %n s. if floor s < n then (if up s then n - floor s

   155 			          else (floor s - Min) + (n-Min))

   156              else

   157              if n < floor s then (if up s then (Max - floor s) + (Max-n)

   158 		                  else floor s - n)

   159              else 0"

   161 locale Floor =

   162   fixes n

   163   assumes Min_le_n [iff]: "Min <= n"

   164       and n_le_Max [iff]: "n <= Max"

   166 lemma not_mem_distinct: "[| x ~: A;  y : A |] ==> x ~= y"

   167 by blast

   170 declare Lift_def [THEN def_prg_Init, simp]

   172 declare request_act_def [THEN def_act_simp, simp]

   173 declare open_act_def [THEN def_act_simp, simp]

   174 declare close_act_def [THEN def_act_simp, simp]

   175 declare req_up_def [THEN def_act_simp, simp]

   176 declare req_down_def [THEN def_act_simp, simp]

   177 declare move_up_def [THEN def_act_simp, simp]

   178 declare move_down_def [THEN def_act_simp, simp]

   179 declare button_press_def [THEN def_act_simp, simp]

   181 (*The ALWAYS properties*)

   182 declare above_def [THEN def_set_simp, simp]

   183 declare below_def [THEN def_set_simp, simp]

   184 declare queueing_def [THEN def_set_simp, simp]

   185 declare goingup_def [THEN def_set_simp, simp]

   186 declare goingdown_def [THEN def_set_simp, simp]

   187 declare ready_def [THEN def_set_simp, simp]

   189 (*Basic definitions*)

   190 declare bounded_def [simp]

   191         open_stop_def [simp]

   192         open_move_def [simp]

   193         stop_floor_def [simp]

   194         moving_up_def [simp]

   195         moving_down_def [simp]

   197 lemma open_stop: "Lift : Always open_stop"

   198 apply (rule AlwaysI, force)

   199 apply (unfold Lift_def, constrains)

   200 done

   202 lemma stop_floor: "Lift : Always stop_floor"

   203 apply (rule AlwaysI, force)

   204 apply (unfold Lift_def, constrains)

   205 done

   207 (*This one needs open_stop, which was proved above*)

   208 lemma open_move: "Lift : Always open_move"

   209 apply (cut_tac open_stop)

   210 apply (rule AlwaysI, force)

   211 apply (unfold Lift_def, constrains)

   212 done

   214 lemma moving_up: "Lift : Always moving_up"

   215 apply (rule AlwaysI, force)

   216 apply (unfold Lift_def, constrains)

   217 apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)

   218 done

   220 lemma moving_down: "Lift : Always moving_down"

   221 apply (rule AlwaysI, force)

   222 apply (unfold Lift_def, constrains)

   223 apply (blast dest: zle_imp_zless_or_eq)

   224 done

   226 lemma bounded: "Lift : Always bounded"

   227 apply (cut_tac moving_up moving_down)

   228 apply (rule AlwaysI, force)

   229 apply (unfold Lift_def, constrains, auto)

   230 apply (drule not_mem_distinct, assumption, arith)+

   231 done

   234 subsection{*Progress*}

   236 declare moving_def [THEN def_set_simp, simp]

   237 declare stopped_def [THEN def_set_simp, simp]

   238 declare opened_def [THEN def_set_simp, simp]

   239 declare closed_def [THEN def_set_simp, simp]

   240 declare atFloor_def [THEN def_set_simp, simp]

   241 declare Req_def [THEN def_set_simp, simp]

   244 (** The HUG'93 paper mistakenly omits the Req n from these! **)

   246 (** Lift_1 **)

   247 lemma E_thm01: "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"

   248 apply (cut_tac stop_floor)

   249 apply (unfold Lift_def, ensures_tac "open_act")

   250 done  (*lem_lift_1_5*)

   252 lemma E_thm02: "Lift : (Req n Int stopped - atFloor n) LeadsTo

   253                      (Req n Int opened - atFloor n)"

   254 apply (cut_tac stop_floor)

   255 apply (unfold Lift_def, ensures_tac "open_act")

   256 done  (*lem_lift_1_1*)

   258 lemma E_thm03: "Lift : (Req n Int opened - atFloor n) LeadsTo

   259                      (Req n Int closed - (atFloor n - queueing))"

   260 apply (unfold Lift_def, ensures_tac "close_act")

   261 done  (*lem_lift_1_2*)

   263 lemma E_thm04: "Lift : (Req n Int closed Int (atFloor n - queueing))

   264              LeadsTo (opened Int atFloor n)"

   265 apply (unfold Lift_def, ensures_tac "open_act")

   266 done  (*lem_lift_1_7*)

   269 (** Lift 2.  Statements of thm05a and thm05b were wrong! **)

   271 lemmas linorder_leI = linorder_not_less [THEN iffD1]

   273 lemmas (in Floor) le_MinD = Min_le_n [THEN order_antisym]

   274               and Max_leD = n_le_Max [THEN [2] order_antisym]

   276 declare (in Floor) le_MinD [dest!]

   277                and linorder_leI [THEN le_MinD, dest!]

   278                and Max_leD [dest!]

   279                and linorder_leI [THEN Max_leD, dest!]

   282 (*lem_lift_2_0

   283   NOT an ensures_tac property, but a mere inclusion

   284   don't know why script lift_2.uni says ENSURES*)

   285 lemma (in Floor) E_thm05c:

   286     "Lift : (Req n Int closed - (atFloor n - queueing))

   287              LeadsTo ((closed Int goingup Int Req n)  Un

   288                       (closed Int goingdown Int Req n))"

   289 by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)

   291 (*lift_2*)

   292 lemma (in Floor) lift_2: "Lift : (Req n Int closed - (atFloor n - queueing))

   293              LeadsTo (moving Int Req n)"

   294 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])

   295 apply (unfold Lift_def)

   296 apply (ensures_tac [2] "req_down")

   297 apply (ensures_tac "req_up", auto)

   298 done

   301 (** Towards lift_4 ***)

   303 declare split_if_asm [split]

   306 (*lem_lift_4_1 *)

   307 lemma (in Floor) E_thm12a:

   308      "0 < N ==>

   309       Lift : (moving Int Req n Int {s. metric n s = N} Int

   310               {s. floor s ~: req s} Int {s. up s})

   311              LeadsTo

   312                (moving Int Req n Int {s. metric n s < N})"

   313 apply (cut_tac moving_up)

   314 apply (unfold Lift_def, ensures_tac "move_up", safe)

   315 (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)

   316 apply (erule linorder_leI [THEN order_antisym, symmetric])

   317 apply (auto simp add: metric_def)

   318 done

   321 (*lem_lift_4_3 *)

   322 lemma (in Floor) E_thm12b: "0 < N ==>

   323       Lift : (moving Int Req n Int {s. metric n s = N} Int

   324               {s. floor s ~: req s} - {s. up s})

   325              LeadsTo (moving Int Req n Int {s. metric n s < N})"

   326 apply (cut_tac moving_down)

   327 apply (unfold Lift_def, ensures_tac "move_down", safe)

   328 (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)

   329 apply (erule linorder_leI [THEN order_antisym, symmetric])

   330 apply (auto simp add: metric_def)

   331 done

   333 (*lift_4*)

   334 lemma (in Floor) lift_4:

   335      "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int

   336                             {s. floor s ~: req s}) LeadsTo

   337                            (moving Int Req n Int {s. metric n s < N})"

   338 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo

   339                               LeadsTo_Un [OF E_thm12a E_thm12b]], auto)

   340 done

   343 (** towards lift_5 **)

   345 (*lem_lift_5_3*)

   346 lemma (in Floor) E_thm16a: "0<N

   347   ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo

   348              (moving Int Req n Int {s. metric n s < N})"

   349 apply (cut_tac bounded)

   350 apply (unfold Lift_def, ensures_tac "req_up")

   351 apply (auto simp add: metric_def)

   352 done

   355 (*lem_lift_5_1 has ~goingup instead of goingdown*)

   356 lemma (in Floor) E_thm16b: "0<N ==>

   357       Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo

   358                    (moving Int Req n Int {s. metric n s < N})"

   359 apply (cut_tac bounded)

   360 apply (unfold Lift_def, ensures_tac "req_down")

   361 apply (auto simp add: metric_def)

   362 done

   365 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,

   366   i.e. the trivial disjunction, leading to an asymmetrical proof.*)

   367 lemma (in Floor) E_thm16c:

   368      "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"

   369 by (force simp add: metric_def)

   372 (*lift_5*)

   373 lemma (in Floor) lift_5:

   374      "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo

   375                      (moving Int Req n Int {s. metric n s < N})"

   376 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo

   377                               LeadsTo_Un [OF E_thm16a E_thm16b]])

   378 apply (drule E_thm16c, auto)

   379 done

   382 (** towards lift_3 **)

   384 (*lemma used to prove lem_lift_3_1*)

   385 lemma (in Floor) metric_eq_0D [dest]:

   386      "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n"

   387 by (force simp add: metric_def)

   390 (*lem_lift_3_1*)

   391 lemma (in Floor) E_thm11: "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo

   392                        (stopped Int atFloor n)"

   393 apply (cut_tac bounded)

   394 apply (unfold Lift_def, ensures_tac "request_act", auto)

   395 done

   397 (*lem_lift_3_5*)

   398 lemma (in Floor) E_thm13:

   399   "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})

   400   LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"

   401 apply (unfold Lift_def, ensures_tac "request_act")

   402 apply (auto simp add: metric_def)

   403 done

   405 (*lem_lift_3_6*)

   406 lemma (in Floor) E_thm14: "0 < N ==>

   407       Lift :

   408         (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})

   409         LeadsTo (opened Int Req n Int {s. metric n s = N})"

   410 apply (unfold Lift_def, ensures_tac "open_act")

   411 apply (auto simp add: metric_def)

   412 done

   414 (*lem_lift_3_7*)

   415 lemma (in Floor) E_thm15: "Lift : (opened Int Req n Int {s. metric n s = N})

   416              LeadsTo (closed Int Req n Int {s. metric n s = N})"

   417 apply (unfold Lift_def, ensures_tac "close_act")

   418 apply (auto simp add: metric_def)

   419 done

   422 (** the final steps **)

   424 lemma (in Floor) lift_3_Req: "0 < N ==>

   425       Lift :

   426         (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})

   427         LeadsTo (moving Int Req n Int {s. metric n s < N})"

   428 apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans)

   429 done

   432 (*Now we observe that our integer metric is really a natural number*)

   433 lemma (in Floor) Always_nonneg: "Lift : Always {s. 0 <= metric n s}"

   434 apply (rule bounded [THEN Always_weaken])

   435 apply (auto simp add: metric_def)

   436 done

   438 lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]

   440 lemma (in Floor) lift_3:

   441      "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"

   442 apply (rule Always_nonneg [THEN integ_0_le_induct])

   443 apply (case_tac "0 < z")

   444 (*If z <= 0 then actually z = 0*)

   445 prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less)

   446 apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])

   447 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo

   448                               LeadsTo_Un [OF lift_4 lift_3_Req]], auto)

   449 done

   452 lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)"

   453 apply (rule LeadsTo_Trans)

   454  prefer 2

   455  apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])

   456  apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un])

   457  apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un])

   458  apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un])

   459  apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03])

   460 apply (rule open_move [THEN Always_LeadsToI])

   461 apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify)

   462 (*The case split is not essential but makes the proof much faster.*)

   463 apply (case_tac "open x", auto)

   464 done

   467 end

author	paulson
	Fri Jan 24 14:06:49 2003 +0100 (2003-01-24)
changeset 13785	e2fcd88be55d
parent 11868	56db9f3a6b3e
child 13806	fd40c9d9076b
permissions	-rw-r--r--