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.
paulson@11195
     1
(*  Title:      HOL/UNITY/Lift.thy
paulson@11195
     2
    ID:         $Id$
paulson@11195
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11195
     4
    Copyright   1998  University of Cambridge
paulson@11195
     5
paulson@11195
     6
The Lift-Control Example
paulson@11195
     7
*)
paulson@11195
     8
paulson@11195
     9
Lift = SubstAx +
paulson@11195
    10
paulson@11195
    11
record state =
paulson@11195
    12
  floor :: int		(*current position of the lift*)
paulson@11195
    13
  open  :: bool		(*whether the door is open at floor*)
paulson@11195
    14
  stop  :: bool		(*whether the lift is stopped at floor*)
paulson@11195
    15
  req   :: int set	(*for each floor, whether the lift is requested*)
paulson@11195
    16
  up    :: bool		(*current direction of movement*)
paulson@11195
    17
  move  :: bool		(*whether moving takes precedence over opening*)
paulson@11195
    18
paulson@11195
    19
consts
paulson@11195
    20
  Min, Max :: int       (*least and greatest floors*)
paulson@11195
    21
paulson@11195
    22
rules
paulson@11195
    23
  Min_le_Max  "Min <= Max"
paulson@11195
    24
  
paulson@11195
    25
constdefs
paulson@11195
    26
  
paulson@11195
    27
  (** Abbreviations: the "always" part **)
paulson@11195
    28
  
paulson@11195
    29
  above :: state set
paulson@11195
    30
    "above == {s. EX i. floor s < i & i <= Max & i : req s}"
paulson@11195
    31
paulson@11195
    32
  below :: state set
paulson@11195
    33
    "below == {s. EX i. Min <= i & i < floor s & i : req s}"
paulson@11195
    34
paulson@11195
    35
  queueing :: state set
paulson@11195
    36
    "queueing == above Un below"
paulson@11195
    37
paulson@11195
    38
  goingup :: state set
paulson@11195
    39
    "goingup   == above Int  ({s. up s}  Un -below)"
paulson@11195
    40
paulson@11195
    41
  goingdown :: state set
paulson@11195
    42
    "goingdown == below Int ({s. ~ up s} Un -above)"
paulson@11195
    43
paulson@11195
    44
  ready :: state set
paulson@11195
    45
    "ready == {s. stop s & ~ open s & move s}"
paulson@11195
    46
paulson@11195
    47
 
paulson@11195
    48
  (** Further abbreviations **)
paulson@11195
    49
paulson@11195
    50
  moving :: state set
paulson@11195
    51
    "moving ==  {s. ~ stop s & ~ open s}"
paulson@11195
    52
paulson@11195
    53
  stopped :: state set
paulson@11195
    54
    "stopped == {s. stop s  & ~ open s & ~ move s}"
paulson@11195
    55
paulson@11195
    56
  opened :: state set
paulson@11195
    57
    "opened ==  {s. stop s  &  open s  &  move s}"
paulson@11195
    58
paulson@11195
    59
  closed :: state set  (*but this is the same as ready!!*)
paulson@11195
    60
    "closed ==  {s. stop s  & ~ open s &  move s}"
paulson@11195
    61
paulson@11195
    62
  atFloor :: int => state set
paulson@11195
    63
    "atFloor n ==  {s. floor s = n}"
paulson@11195
    64
paulson@11195
    65
  Req :: int => state set
paulson@11195
    66
    "Req n ==  {s. n : req s}"
paulson@11195
    67
paulson@11195
    68
paulson@11195
    69
  
paulson@11195
    70
  (** The program **)
paulson@11195
    71
  
paulson@11195
    72
  request_act :: "(state*state) set"
paulson@11195
    73
    "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
paulson@11195
    74
		                  & ~ stop s & floor s : req s}"
paulson@11195
    75
paulson@11195
    76
  open_act :: "(state*state) set"
paulson@11195
    77
    "open_act ==
paulson@11195
    78
         {(s,s'). s' = s (|open :=True,
paulson@11195
    79
			   req  := req s - {floor s},
paulson@11195
    80
			   move := True|)
paulson@11195
    81
		       & stop s & ~ open s & floor s : req s
paulson@11195
    82
	               & ~(move s & s: queueing)}"
paulson@11195
    83
paulson@11195
    84
  close_act :: "(state*state) set"
paulson@11195
    85
    "close_act == {(s,s'). s' = s (|open := False|) & open s}"
paulson@11195
    86
paulson@11195
    87
  req_up :: "(state*state) set"
paulson@11195
    88
    "req_up ==
paulson@11195
    89
         {(s,s'). s' = s (|stop  :=False,
paulson@11868
    90
			   floor := floor s + 1,
paulson@11195
    91
			   up    := True|)
paulson@11195
    92
		       & s : (ready Int goingup)}"
paulson@11195
    93
paulson@11195
    94
  req_down :: "(state*state) set"
paulson@11195
    95
    "req_down ==
paulson@11195
    96
         {(s,s'). s' = s (|stop  :=False,
paulson@11868
    97
			   floor := floor s - 1,
paulson@11195
    98
			   up    := False|)
paulson@11195
    99
		       & s : (ready Int goingdown)}"
paulson@11195
   100
paulson@11195
   101
  move_up :: "(state*state) set"
paulson@11195
   102
    "move_up ==
paulson@11868
   103
         {(s,s'). s' = s (|floor := floor s + 1|)
paulson@11195
   104
		       & ~ stop s & up s & floor s ~: req s}"
paulson@11195
   105
paulson@11195
   106
  move_down :: "(state*state) set"
paulson@11195
   107
    "move_down ==
paulson@11868
   108
         {(s,s'). s' = s (|floor := floor s - 1|)
paulson@11195
   109
		       & ~ stop s & ~ up s & floor s ~: req s}"
paulson@11195
   110
paulson@11195
   111
  (*This action is omitted from prior treatments, which therefore are
paulson@11195
   112
    unrealistic: nobody asks the lift to do anything!  But adding this
paulson@11195
   113
    action invalidates many of the existing progress arguments: various
paulson@11195
   114
    "ensures" properties fail.*)
paulson@11195
   115
  button_press  :: "(state*state) set"
paulson@11195
   116
    "button_press ==
paulson@11195
   117
         {(s,s'). EX n. s' = s (|req := insert n (req s)|)
paulson@11195
   118
		        & Min <= n & n <= Max}"
paulson@11195
   119
paulson@11195
   120
paulson@11195
   121
  Lift :: state program
paulson@11195
   122
    (*for the moment, we OMIT button_press*)
paulson@11195
   123
    "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
paulson@11195
   124
		          ~ open s & req s = {}},
paulson@11195
   125
			 {request_act, open_act, close_act,
paulson@11195
   126
			  req_up, req_down, move_up, move_down},
paulson@11195
   127
			 UNIV)"
paulson@11195
   128
paulson@11195
   129
paulson@11195
   130
  (** Invariants **)
paulson@11195
   131
paulson@11195
   132
  bounded :: state set
paulson@11195
   133
    "bounded == {s. Min <= floor s & floor s <= Max}"
paulson@11195
   134
paulson@11195
   135
  open_stop :: state set
paulson@11195
   136
    "open_stop == {s. open s --> stop s}"
paulson@11195
   137
  
paulson@11195
   138
  open_move :: state set
paulson@11195
   139
    "open_move == {s. open s --> move s}"
paulson@11195
   140
  
paulson@11195
   141
  stop_floor :: state set
paulson@11195
   142
    "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
paulson@11195
   143
  
paulson@11195
   144
  moving_up :: state set
paulson@11195
   145
    "moving_up == {s. ~ stop s & up s -->
paulson@11195
   146
                   (EX f. floor s <= f & f <= Max & f : req s)}"
paulson@11195
   147
  
paulson@11195
   148
  moving_down :: state set
paulson@11195
   149
    "moving_down == {s. ~ stop s & ~ up s -->
paulson@11195
   150
                     (EX f. Min <= f & f <= floor s & f : req s)}"
paulson@11195
   151
  
paulson@11195
   152
  metric :: [int,state] => int
paulson@11195
   153
    "metric ==
paulson@11195
   154
       %n s. if floor s < n then (if up s then n - floor s
paulson@11195
   155
			          else (floor s - Min) + (n-Min))
paulson@11195
   156
             else
paulson@11195
   157
             if n < floor s then (if up s then (Max - floor s) + (Max-n)
paulson@11195
   158
		                  else floor s - n)
paulson@11868
   159
             else 0"
paulson@11195
   160
paulson@11195
   161
locale floor =
paulson@11195
   162
  fixes 
paulson@11195
   163
    n	:: int
paulson@11195
   164
  assumes
paulson@11195
   165
    Min_le_n    "Min <= n"
paulson@11195
   166
    n_le_Max    "n <= Max"
paulson@11195
   167
  defines
paulson@11195
   168
paulson@11195
   169
end