src/HOL/UNITY/Lift.thy
 author paulson Wed Aug 19 10:34:31 1998 +0200 (1998-08-19) changeset 5340 d75c03cf77b5 parent 5320 79b326bceafb child 5357 6efb2b87610c permissions -rw-r--r--
Misc changes
```     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 *)
```
```    10
```
```    11 Lift = SubstAx +
```
```    12
```
```    13 record state =
```
```    14   floor :: nat		(*current position of the lift*)
```
```    15   open  :: bool		(*whether the door is open at floor*)
```
```    16   stop  :: bool		(*whether the lift is stopped at floor*)
```
```    17   req   :: nat set	(*for each floor, whether the lift is requested*)
```
```    18   up    :: bool		(*current direction of movement*)
```
```    19   move  :: bool		(*whether moving takes precedence over opening*)
```
```    20
```
```    21 consts
```
```    22   min, max :: nat       (*least and greatest floors*)
```
```    23
```
```    24 rules
```
```    25   min_le_max  "min <= max"
```
```    26
```
```    27   (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
```
```    28   arith1      "m < fl ==> n - Suc fl < fl - m + (n - m)"
```
```    29   arith2      "[| Suc fl < n; m < n |] ==> n - Suc fl < fl - m + (n - m)"
```
```    30
```
```    31
```
```    32 constdefs
```
```    33
```
```    34   (** Abbreviations: the "always" part **)
```
```    35
```
```    36   above :: state set
```
```    37     "above == {s. EX i. floor s < i & i <= max & i : req s}"
```
```    38
```
```    39   below :: state set
```
```    40     "below == {s. EX i. min <= i & i < floor s & i : req s}"
```
```    41
```
```    42   queueing :: state set
```
```    43     "queueing == above Un below"
```
```    44
```
```    45   goingup :: state set
```
```    46     "goingup   == above Int  ({s. up s}  Un Compl below)"
```
```    47
```
```    48   goingdown :: state set
```
```    49     "goingdown == below Int ({s. ~ up s} Un Compl above)"
```
```    50
```
```    51   ready :: state set
```
```    52     "ready == {s. stop s & ~ open s & move s}"
```
```    53
```
```    54
```
```    55   (** Further abbreviations **)
```
```    56
```
```    57   moving :: state set
```
```    58     "moving ==  {s. ~ stop s & ~ open s}"
```
```    59
```
```    60   stopped :: state set
```
```    61     "stopped == {s. stop s  & ~ open s & ~ move s}"
```
```    62
```
```    63   opened :: state set
```
```    64     "opened ==  {s. stop s  &  open s  &  move s}"
```
```    65
```
```    66   closed :: state set  (*but this is the same as ready!!*)
```
```    67     "closed ==  {s. stop s  & ~ open s &  move s}"
```
```    68
```
```    69   atFloor :: nat => state set
```
```    70     "atFloor n ==  {s. floor s = n}"
```
```    71
```
```    72   Req :: nat => state set
```
```    73     "Req n ==  {s. n : req s}"
```
```    74
```
```    75
```
```    76
```
```    77   (** The program **)
```
```    78
```
```    79   request_act :: "(state*state) set"
```
```    80     "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
```
```    81 		                  & ~ stop s & floor s : req s}"
```
```    82
```
```    83   open_act :: "(state*state) set"
```
```    84     "open_act ==
```
```    85          {(s,s'). s' = s (|open :=True,
```
```    86 			   req  := req s - {floor s},
```
```    87 			   move := True|)
```
```    88 		       & stop s & ~ open s & floor s : req s
```
```    89 	               & ~(move s & s: queueing)}"
```
```    90
```
```    91   close_act :: "(state*state) set"
```
```    92     "close_act == {(s,s'). s' = s (|open := False|) & open s}"
```
```    93
```
```    94   req_up_act :: "(state*state) set"
```
```    95     "req_up_act ==
```
```    96          {(s,s'). s' = s (|stop  :=False,
```
```    97 			   floor := Suc (floor s),
```
```    98 			   up    := True|)
```
```    99 		       & s : (ready Int goingup)}"
```
```   100
```
```   101   req_down_act :: "(state*state) set"
```
```   102     "req_down_act ==
```
```   103          {(s,s'). s' = s (|stop  :=False,
```
```   104 			   floor := floor s - 1,
```
```   105 			   up    := False|)
```
```   106 		       & s : (ready Int goingdown)}"
```
```   107
```
```   108   move_up :: "(state*state) set"
```
```   109     "move_up ==
```
```   110          {(s,s'). s' = s (|floor := Suc (floor s)|)
```
```   111 		       & ~ stop s & up s & floor s ~: req s}"
```
```   112
```
```   113   move_down :: "(state*state) set"
```
```   114     "move_down ==
```
```   115          {(s,s'). s' = s (|floor := floor s - 1|)
```
```   116 		       & ~ stop s & ~ up s & floor s ~: req s}"
```
```   117
```
```   118   Lprg :: state program
```
```   119     "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s &
```
```   120 		          ~ open s & req s = {}},
```
```   121 	       Acts = {id, request_act, open_act, close_act,
```
```   122 		       req_up_act, req_down_act, move_up, move_down}|)"
```
```   123
```
```   124
```
```   125   (** Invariants **)
```
```   126
```
```   127   bounded :: state set
```
```   128     "bounded == {s. min <= floor s & floor s <= max}"
```
```   129
```
```   130   open_stop :: state set
```
```   131     "open_stop == {s. open s --> stop s}"
```
```   132
```
```   133   open_move :: state set
```
```   134     "open_move == {s. open s --> move s}"
```
```   135
```
```   136   stop_floor :: state set
```
```   137     "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
```
```   138
```
```   139   moving_up :: state set
```
```   140     "moving_up == {s. ~ stop s & up s -->
```
```   141                    (EX f. floor s <= f & f <= max & f : req s)}"
```
```   142
```
```   143   moving_down :: state set
```
```   144     "moving_down == {s. ~ stop s & ~ up s -->
```
```   145                      (EX f. min <= f & f <= floor s & f : req s)}"
```
```   146
```
```   147   metric :: [nat,state] => nat
```
```   148     "metric n s == if up s & floor s < n then n - floor s
```
```   149 		   else if ~ up s & n < floor s then floor s - n
```
```   150 		   else if up s & n < floor s then (max - floor s) + (max-n)
```
```   151 		   else if ~ up s & floor s < n then (floor s - min) + (n-min)
```
```   152 		   else 0"
```
```   153
```
```   154 locale floor =
```
```   155   fixes
```
```   156     n	:: nat
```
```   157   assumes
```
```   158     min_le_n    "min <= n"
```
```   159     n_le_max    "n <= max"
```
```   160   defines
```
```   161
```
```   162 end
```