src/HOL/UNITY/Lift.thy
author paulson
Fri Aug 14 13:52:42 1998 +0200 (1998-08-14)
changeset 5320 79b326bceafb
parent 5277 e4297d03e5d2
child 5340 d75c03cf77b5
permissions -rw-r--r--
now trans_tac is part of the claset...
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@5277
    20
  min, max :: nat	(*least and greatest floors*)
paulson@5277
    21
paulson@5277
    22
rules
paulson@5277
    23
  min_le_max  "min <= max"
paulson@5277
    24
  
paulson@5277
    25
paulson@5277
    26
constdefs
paulson@5277
    27
  
paulson@5277
    28
  (** Abbreviations: the "always" part **)
paulson@5277
    29
  
paulson@5320
    30
  above :: state set
paulson@5277
    31
    "above == {s. EX i. floor s < i & i <= max & i : req s}"
paulson@5277
    32
paulson@5320
    33
  below :: state set
paulson@5277
    34
    "below == {s. EX i. min <= i & i < floor s & i : req s}"
paulson@5277
    35
paulson@5320
    36
  queueing :: state set
paulson@5277
    37
    "queueing == above Un below"
paulson@5277
    38
paulson@5320
    39
  goingup :: state set
paulson@5277
    40
    "goingup == above Int ({s. up s} Un Compl below)"
paulson@5277
    41
paulson@5320
    42
  goingdown :: state set
paulson@5277
    43
    "goingdown == below Int ({s. ~ up s} Un Compl above)"
paulson@5277
    44
paulson@5320
    45
  ready :: state set
paulson@5277
    46
    "ready == {s. stop s & ~ open s & move s}"
paulson@5277
    47
paulson@5320
    48
 
paulson@5320
    49
  (** Further abbreviations **)
paulson@5277
    50
paulson@5320
    51
  moving :: state set
paulson@5320
    52
    "moving ==  {s. ~ stop s & ~ open s}"
paulson@5320
    53
paulson@5320
    54
  stopped :: state set
paulson@5320
    55
    "stopped == {s. stop s  & ~ open s &  move s}"
paulson@5320
    56
paulson@5320
    57
  opened :: state set
paulson@5320
    58
    "opened ==  {s. stop s  &  open s  &  move s}"
paulson@5320
    59
paulson@5320
    60
  closed :: state set
paulson@5320
    61
    "closed ==  {s. stop s  & ~ open s &  move s}"
paulson@5320
    62
paulson@5320
    63
  atFloor :: nat => state set
paulson@5320
    64
    "atFloor n ==  {s. floor s = n}"
paulson@5320
    65
paulson@5320
    66
paulson@5320
    67
  
paulson@5277
    68
  (** The program **)
paulson@5277
    69
  
paulson@5277
    70
  request_act :: "(state*state) set"
paulson@5277
    71
    "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
paulson@5277
    72
		                  & ~ stop s & floor s : req s}"
paulson@5277
    73
paulson@5277
    74
  open_act :: "(state*state) set"
paulson@5277
    75
    "open_act ==
paulson@5277
    76
         {(s,s'). s' = s (|open :=True,
paulson@5277
    77
			   req  := req s - {floor s},
paulson@5277
    78
			   move := True|)
paulson@5277
    79
		       & stop s & ~ open s & floor s : req s
paulson@5277
    80
	               & ~(move s & s: queueing)}"
paulson@5277
    81
paulson@5277
    82
  close_act :: "(state*state) set"
paulson@5277
    83
    "close_act == {(s,s'). s' = s (|open := False|) & open s}"
paulson@5277
    84
paulson@5277
    85
  req_up_act :: "(state*state) set"
paulson@5277
    86
    "req_up_act ==
paulson@5277
    87
         {(s,s'). s' = s (|stop  :=False,
paulson@5277
    88
			   floor := Suc (floor s),
paulson@5277
    89
			   up    := True|)
paulson@5277
    90
		       & s : (ready Int goingup)}"
paulson@5277
    91
paulson@5277
    92
  req_down_act :: "(state*state) set"
paulson@5277
    93
    "req_down_act ==
paulson@5277
    94
         {(s,s'). s' = s (|stop  :=False,
paulson@5277
    95
			   floor := floor s - 1,
paulson@5277
    96
			   up    := False|)
paulson@5277
    97
		       & s : (ready Int goingdown)}"
paulson@5277
    98
paulson@5277
    99
  move_up :: "(state*state) set"
paulson@5277
   100
    "move_up ==
paulson@5277
   101
         {(s,s'). s' = s (|floor := Suc (floor s)|)
paulson@5277
   102
		       & ~ stop s & up s & floor s ~: req s}"
paulson@5277
   103
paulson@5277
   104
  move_down :: "(state*state) set"
paulson@5277
   105
    "move_down ==
paulson@5277
   106
         {(s,s'). s' = s (|floor := floor s - 1|)
paulson@5277
   107
		       & ~ stop s & ~ up s & floor s ~: req s}"
paulson@5277
   108
paulson@5277
   109
  Lprg :: state program
paulson@5277
   110
    "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s &
paulson@5277
   111
		          ~ open s & req s = {}},
paulson@5277
   112
	       Acts = {id, request_act, open_act, close_act,
paulson@5277
   113
		       req_up_act, req_down_act, move_up, move_down}|)"
paulson@5277
   114
paulson@5277
   115
paulson@5277
   116
  (** Invariants **)
paulson@5277
   117
paulson@5277
   118
  bounded :: state set
paulson@5277
   119
    "bounded == {s. min <= floor s & floor s <= max}"
paulson@5277
   120
paulson@5277
   121
  open_stop :: state set
paulson@5277
   122
    "open_stop == {s. open s --> stop s}"
paulson@5277
   123
  
paulson@5277
   124
  open_move :: state set
paulson@5277
   125
    "open_move == {s. open s --> move s}"
paulson@5277
   126
  
paulson@5277
   127
  stop_floor :: state set
paulson@5277
   128
    "stop_floor == {s. open s & ~ move s --> floor s : req s}"
paulson@5277
   129
  
paulson@5277
   130
  moving_up :: state set
paulson@5277
   131
    "moving_up == {s. ~ stop s & up s -->
paulson@5277
   132
                   (EX f. floor s <= f & f <= max & f : req s)}"
paulson@5277
   133
  
paulson@5277
   134
  moving_down :: state set
paulson@5277
   135
    "moving_down == {s. ~ stop s & ~ up s -->
paulson@5277
   136
                     (EX f. min <= f & f <= floor s & f : req s)}"
paulson@5277
   137
  
paulson@5320
   138
  (*intersection of all invariants: NECESSARY??*)
paulson@5320
   139
  valid :: state set
paulson@5277
   140
    "valid == bounded Int open_stop Int open_move"
paulson@5277
   141
paulson@5277
   142
end