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