src/HOL/UNITY/Lift.thy
author paulson
Thu Sep 03 16:40:02 1998 +0200 (1998-09-03)
changeset 5426 566f47250bd0
parent 5357 6efb2b87610c
child 5563 228b92552d1f
permissions -rw-r--r--
A new approach, using simp_of_act and simp_of_set to activate definitions when
necessary
paulson@5277
     1
(*  Title:      HOL/UNITY/Lift.thy
paulson@5277
     2
    ID:         $Id$
paulson@5277
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5277
     4
    Copyright   1998  University of Cambridge
paulson@5277
     5
paulson@5277
     6
The Lift-Control Example
paulson@5277
     7
*)
paulson@5277
     8
paulson@5277
     9
Lift = SubstAx +
paulson@5277
    10
paulson@5277
    11
record state =
paulson@5277
    12
  floor :: nat		(*current position of the lift*)
paulson@5277
    13
  open  :: bool		(*whether the door is open at floor*)
paulson@5277
    14
  stop  :: bool		(*whether the lift is stopped at floor*)
paulson@5277
    15
  req   :: nat set	(*for each floor, whether the lift is requested*)
paulson@5277
    16
  up    :: bool		(*current direction of movement*)
paulson@5277
    17
  move  :: bool		(*whether moving takes precedence over opening*)
paulson@5277
    18
paulson@5277
    19
consts
paulson@5357
    20
  Min, Max :: nat       (*least and greatest floors*)
paulson@5277
    21
paulson@5277
    22
rules
paulson@5357
    23
  Min_le_Max  "Min <= Max"
paulson@5277
    24
  
paulson@5340
    25
  (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
paulson@5340
    26
  arith1      "m < fl ==> n - Suc fl < fl - m + (n - m)"
paulson@5357
    27
  arith2      "[| m<n;  m <= fl |] ==> n - Suc fl < fl - m + (n - m)"
paulson@5357
    28
  arith3      "[| Suc ix < m |] ==> ix - n < m - Suc ix + (m - n)"
paulson@5357
    29
  arith4      "[| ix < m;  n < ix |] ==> ix - n < m - Suc (ix) + (m - n)"
paulson@5277
    30
paulson@5277
    31
constdefs
paulson@5277
    32
  
paulson@5277
    33
  (** Abbreviations: the "always" part **)
paulson@5277
    34
  
paulson@5320
    35
  above :: state set
paulson@5357
    36
    "above == {s. EX i. floor s < i & i <= Max & i : req s}"
paulson@5277
    37
paulson@5320
    38
  below :: state set
paulson@5357
    39
    "below == {s. EX i. Min <= i & i < floor s & i : req s}"
paulson@5277
    40
paulson@5320
    41
  queueing :: state set
paulson@5277
    42
    "queueing == above Un below"
paulson@5277
    43
paulson@5320
    44
  goingup :: state set
paulson@5340
    45
    "goingup   == above Int  ({s. up s}  Un Compl below)"
paulson@5277
    46
paulson@5320
    47
  goingdown :: state set
paulson@5277
    48
    "goingdown == below Int ({s. ~ up s} Un Compl above)"
paulson@5277
    49
paulson@5320
    50
  ready :: state set
paulson@5277
    51
    "ready == {s. stop s & ~ open s & move s}"
paulson@5277
    52
paulson@5320
    53
 
paulson@5320
    54
  (** Further abbreviations **)
paulson@5277
    55
paulson@5320
    56
  moving :: state set
paulson@5320
    57
    "moving ==  {s. ~ stop s & ~ open s}"
paulson@5320
    58
paulson@5320
    59
  stopped :: state set
paulson@5340
    60
    "stopped == {s. stop s  & ~ open s & ~ move s}"
paulson@5320
    61
paulson@5320
    62
  opened :: state set
paulson@5320
    63
    "opened ==  {s. stop s  &  open s  &  move s}"
paulson@5320
    64
paulson@5340
    65
  closed :: state set  (*but this is the same as ready!!*)
paulson@5320
    66
    "closed ==  {s. stop s  & ~ open s &  move s}"
paulson@5320
    67
paulson@5320
    68
  atFloor :: nat => state set
paulson@5320
    69
    "atFloor n ==  {s. floor s = n}"
paulson@5320
    70
paulson@5340
    71
  Req :: nat => state set
paulson@5340
    72
    "Req n ==  {s. n : req s}"
paulson@5340
    73
paulson@5320
    74
paulson@5320
    75
  
paulson@5277
    76
  (** The program **)
paulson@5277
    77
  
paulson@5277
    78
  request_act :: "(state*state) set"
paulson@5277
    79
    "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
paulson@5277
    80
		                  & ~ stop s & floor s : req s}"
paulson@5277
    81
paulson@5277
    82
  open_act :: "(state*state) set"
paulson@5277
    83
    "open_act ==
paulson@5277
    84
         {(s,s'). s' = s (|open :=True,
paulson@5277
    85
			   req  := req s - {floor s},
paulson@5277
    86
			   move := True|)
paulson@5277
    87
		       & stop s & ~ open s & floor s : req s
paulson@5277
    88
	               & ~(move s & s: queueing)}"
paulson@5277
    89
paulson@5277
    90
  close_act :: "(state*state) set"
paulson@5277
    91
    "close_act == {(s,s'). s' = s (|open := False|) & open s}"
paulson@5277
    92
paulson@5357
    93
  req_up :: "(state*state) set"
paulson@5357
    94
    "req_up ==
paulson@5277
    95
         {(s,s'). s' = s (|stop  :=False,
paulson@5277
    96
			   floor := Suc (floor s),
paulson@5277
    97
			   up    := True|)
paulson@5277
    98
		       & s : (ready Int goingup)}"
paulson@5277
    99
paulson@5357
   100
  req_down :: "(state*state) set"
paulson@5357
   101
    "req_down ==
paulson@5277
   102
         {(s,s'). s' = s (|stop  :=False,
paulson@5277
   103
			   floor := floor s - 1,
paulson@5277
   104
			   up    := False|)
paulson@5277
   105
		       & s : (ready Int goingdown)}"
paulson@5277
   106
paulson@5277
   107
  move_up :: "(state*state) set"
paulson@5277
   108
    "move_up ==
paulson@5277
   109
         {(s,s'). s' = s (|floor := Suc (floor s)|)
paulson@5277
   110
		       & ~ stop s & up s & floor s ~: req s}"
paulson@5277
   111
paulson@5277
   112
  move_down :: "(state*state) set"
paulson@5277
   113
    "move_down ==
paulson@5277
   114
         {(s,s'). s' = s (|floor := floor s - 1|)
paulson@5277
   115
		       & ~ stop s & ~ up s & floor s ~: req s}"
paulson@5277
   116
paulson@5357
   117
  button_press  :: "(state*state) set"
paulson@5357
   118
    "button_press ==
paulson@5357
   119
         {(s,s'). EX n. s' = s (|req := insert n (req s)|)
paulson@5357
   120
		        & Min <= n & n <= Max}"
paulson@5357
   121
paulson@5357
   122
paulson@5277
   123
  Lprg :: state program
paulson@5357
   124
    (*for the moment, we OMIT button_press*)
paulson@5357
   125
    "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
paulson@5277
   126
		          ~ open s & req s = {}},
paulson@5277
   127
	       Acts = {id, request_act, open_act, close_act,
paulson@5357
   128
		       req_up, req_down, move_up, move_down}|)"
paulson@5277
   129
paulson@5277
   130
paulson@5277
   131
  (** Invariants **)
paulson@5277
   132
paulson@5277
   133
  bounded :: state set
paulson@5357
   134
    "bounded == {s. Min <= floor s & floor s <= Max}"
paulson@5277
   135
paulson@5277
   136
  open_stop :: state set
paulson@5277
   137
    "open_stop == {s. open s --> stop s}"
paulson@5277
   138
  
paulson@5277
   139
  open_move :: state set
paulson@5277
   140
    "open_move == {s. open s --> move s}"
paulson@5277
   141
  
paulson@5277
   142
  stop_floor :: state set
paulson@5340
   143
    "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
paulson@5277
   144
  
paulson@5277
   145
  moving_up :: state set
paulson@5277
   146
    "moving_up == {s. ~ stop s & up s -->
paulson@5357
   147
                   (EX f. floor s <= f & f <= Max & f : req s)}"
paulson@5277
   148
  
paulson@5277
   149
  moving_down :: state set
paulson@5277
   150
    "moving_down == {s. ~ stop s & ~ up s -->
paulson@5357
   151
                     (EX f. Min <= f & f <= floor s & f : req s)}"
paulson@5277
   152
  
paulson@5340
   153
  metric :: [nat,state] => nat
paulson@5357
   154
    "metric ==
paulson@5357
   155
       %n s. if up s & floor s < n then n - floor s
paulson@5357
   156
	     else if ~ up s & n < floor s then floor s - n
paulson@5357
   157
	     else if up s & n < floor s then (Max - floor s) + (Max-n)
paulson@5357
   158
	     else if ~ up s & floor s < n then (floor s - Min) + (n-Min)
paulson@5357
   159
	     else 0"
paulson@5340
   160
paulson@5340
   161
locale floor =
paulson@5340
   162
  fixes 
paulson@5340
   163
    n	:: nat
paulson@5340
   164
  assumes
paulson@5357
   165
    Min_le_n    "Min <= n"
paulson@5357
   166
    n_le_Max    "n <= Max"
paulson@5340
   167
  defines
paulson@5277
   168
paulson@5277
   169
end