src/HOL/UNITY/Lift.thy

New theory Lift

(*  Title:      HOL/UNITY/Lift.thy
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

The Lift-Control Example


*)

Lift = SubstAx +

record state =
  floor :: nat		(*current position of the lift*)
  open  :: bool		(*whether the door is open at floor*)
  stop  :: bool		(*whether the lift is stopped at floor*)
  req   :: nat set	(*for each floor, whether the lift is requested*)
  up    :: bool		(*current direction of movement*)
  move  :: bool		(*whether moving takes precedence over opening*)

consts
  Min, Max :: nat       (*least and greatest floors*)

rules
  Min_le_Max  "Min <= Max"
  
  (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
  arith1      "m < fl ==> n - Suc fl < fl - m + (n - m)"
  arith2      "[| m<n;  m <= fl |] ==> n - Suc fl < fl - m + (n - m)"
  arith3      "[| Suc ix < m |] ==> ix - n < m - Suc ix + (m - n)"
  arith4      "[| ix < m;  n < ix |] ==> ix - n < m - Suc (ix) + (m - n)"

constdefs
  
  (** Abbreviations: the "always" part **)
  
  above :: state set
    "above == {s. EX i. floor s < i & i <= Max & i : req s}"

  below :: state set
    "below == {s. EX i. Min <= i & i < floor s & i : req s}"

  queueing :: state set
    "queueing == above Un below"

  goingup :: state set
    "goingup   == above Int  ({s. up s}  Un Compl below)"

  goingdown :: state set
    "goingdown == below Int ({s. ~ up s} Un Compl above)"

  ready :: state set
    "ready == {s. stop s & ~ open s & move s}"

 
  (** Further abbreviations **)

  moving :: state set
    "moving ==  {s. ~ stop s & ~ open s}"

  stopped :: state set
    "stopped == {s. stop s  & ~ open s & ~ move s}"

  opened :: state set
    "opened ==  {s. stop s  &  open s  &  move s}"

  closed :: state set  (*but this is the same as ready!!*)
    "closed ==  {s. stop s  & ~ open s &  move s}"

  atFloor :: nat => state set
    "atFloor n ==  {s. floor s = n}"

  Req :: nat => state set
    "Req n ==  {s. n : req s}"


  
  (** The program **)
  
  request_act :: "(state*state) set"
    "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
		                  & ~ stop s & floor s : req s}"

  open_act :: "(state*state) set"
    "open_act ==
         {(s,s'). s' = s (|open :=True,
			   req  := req s - {floor s},
			   move := True|)
		       & stop s & ~ open s & floor s : req s
	               & ~(move s & s: queueing)}"

  close_act :: "(state*state) set"
    "close_act == {(s,s'). s' = s (|open := False|) & open s}"

  req_up :: "(state*state) set"
    "req_up ==
         {(s,s'). s' = s (|stop  :=False,
			   floor := Suc (floor s),
			   up    := True|)
		       & s : (ready Int goingup)}"

  req_down :: "(state*state) set"
    "req_down ==
         {(s,s'). s' = s (|stop  :=False,
			   floor := floor s - 1,
			   up    := False|)
		       & s : (ready Int goingdown)}"

  move_up :: "(state*state) set"
    "move_up ==
         {(s,s'). s' = s (|floor := Suc (floor s)|)
		       & ~ stop s & up s & floor s ~: req s}"

  move_down :: "(state*state) set"
    "move_down ==
         {(s,s'). s' = s (|floor := floor s - 1|)
		       & ~ stop s & ~ up s & floor s ~: req s}"

  button_press  :: "(state*state) set"
    "button_press ==
         {(s,s'). EX n. s' = s (|req := insert n (req s)|)
		        & Min <= n & n <= Max}"


  Lprg :: state program
    (*for the moment, we OMIT button_press*)
    "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
		          ~ open s & req s = {}},
	       Acts = {id, request_act, open_act, close_act,
		       req_up, req_down, move_up, move_down}|)"


  (** Invariants **)

  bounded :: state set
    "bounded == {s. Min <= floor s & floor s <= Max}"

  open_stop :: state set
    "open_stop == {s. open s --> stop s}"
  
  open_move :: state set
    "open_move == {s. open s --> move s}"
  
  stop_floor :: state set
    "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
  
  moving_up :: state set
    "moving_up == {s. ~ stop s & up s -->
                   (EX f. floor s <= f & f <= Max & f : req s)}"
  
  moving_down :: state set
    "moving_down == {s. ~ stop s & ~ up s -->
                     (EX f. Min <= f & f <= floor s & f : req s)}"
  
  metric :: [nat,state] => nat
    "metric ==
       %n s. if up s & floor s < n then n - floor s
	     else if ~ up s & n < floor s then floor s - n
	     else if up s & n < floor s then (Max - floor s) + (Max-n)
	     else if ~ up s & floor s < n then (floor s - Min) + (n-Min)
	     else 0"

locale floor =
  fixes 
    n	:: nat
  assumes
    Min_le_n    "Min <= n"
    n_le_Max    "n <= Max"
  defines

end