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