src/HOL/UNITY/Simple/Lift.thy
 author paulson Mon Oct 22 11:54:22 2001 +0200 (2001-10-22) changeset 11868 56db9f3a6b3e parent 11701 3d51fbf81c17 child 13785 e2fcd88be55d permissions -rw-r--r--
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
to their abstract counterparts, while other binary numerals work correctly.
```     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 Lift = SubstAx +
```
```    10
```
```    11 record state =
```
```    12   floor :: int		(*current position of the lift*)
```
```    13   open  :: bool		(*whether the door is open 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, Max :: int       (*least and greatest floors*)
```
```    21
```
```    22 rules
```
```    23   Min_le_Max  "Min <= Max"
```
```    24
```
```    25 constdefs
```
```    26
```
```    27   (** Abbreviations: the "always" part **)
```
```    28
```
```    29   above :: state set
```
```    30     "above == {s. EX i. floor s < i & i <= Max & i : req s}"
```
```    31
```
```    32   below :: state set
```
```    33     "below == {s. EX i. Min <= i & i < floor s & i : req s}"
```
```    34
```
```    35   queueing :: state set
```
```    36     "queueing == above Un below"
```
```    37
```
```    38   goingup :: state set
```
```    39     "goingup   == above Int  ({s. up s}  Un -below)"
```
```    40
```
```    41   goingdown :: state set
```
```    42     "goingdown == below Int ({s. ~ up s} Un -above)"
```
```    43
```
```    44   ready :: state set
```
```    45     "ready == {s. stop s & ~ open s & move s}"
```
```    46
```
```    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 : 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 : 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 : req s
```
```    82 	               & ~(move s & s: 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 : (ready Int 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 : (ready Int 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 ~: 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 ~: 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'). EX n. s' = s (|req := insert n (req s)|)
```
```   118 		        & Min <= n & n <= Max}"
```
```   119
```
```   120
```
```   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)"
```
```   128
```
```   129
```
```   130   (** Invariants **)
```
```   131
```
```   132   bounded :: state set
```
```   133     "bounded == {s. Min <= floor s & floor s <= Max}"
```
```   134
```
```   135   open_stop :: state set
```
```   136     "open_stop == {s. open s --> stop s}"
```
```   137
```
```   138   open_move :: state set
```
```   139     "open_move == {s. open s --> move s}"
```
```   140
```
```   141   stop_floor :: state set
```
```   142     "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
```
```   143
```
```   144   moving_up :: state set
```
```   145     "moving_up == {s. ~ stop s & up s -->
```
```   146                    (EX f. floor s <= f & f <= Max & f : req s)}"
```
```   147
```
```   148   moving_down :: state set
```
```   149     "moving_down == {s. ~ stop s & ~ up s -->
```
```   150                      (EX f. Min <= f & f <= floor s & f : req s)}"
```
```   151
```
```   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"
```
```   160
```
```   161 locale floor =
```
```   162   fixes
```
```   163     n	:: int
```
```   164   assumes
```
```   165     Min_le_n    "Min <= n"
```
```   166     n_le_Max    "n <= Max"
```
```   167   defines
```
```   168
```
```   169 end
```