src/HOL/UNITY/Lift.thy
changeset 5563 228b92552d1f
parent 5426 566f47250bd0
child 5584 aad639e56d4e
     1.1 --- a/src/HOL/UNITY/Lift.thy	Fri Sep 25 13:57:01 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Lift.thy	Fri Sep 25 13:58:24 1998 +0200
     1.3 @@ -9,25 +9,19 @@
     1.4  Lift = SubstAx +
     1.5  
     1.6  record state =
     1.7 -  floor :: nat		(*current position of the lift*)
     1.8 +  floor :: int		(*current position of the lift*)
     1.9    open  :: bool		(*whether the door is open at floor*)
    1.10    stop  :: bool		(*whether the lift is stopped at floor*)
    1.11 -  req   :: nat set	(*for each floor, whether the lift is requested*)
    1.12 +  req   :: int set	(*for each floor, whether the lift is requested*)
    1.13    up    :: bool		(*current direction of movement*)
    1.14    move  :: bool		(*whether moving takes precedence over opening*)
    1.15  
    1.16  consts
    1.17 -  Min, Max :: nat       (*least and greatest floors*)
    1.18 +  Min, Max :: int       (*least and greatest floors*)
    1.19  
    1.20  rules
    1.21    Min_le_Max  "Min <= Max"
    1.22    
    1.23 -  (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
    1.24 -  arith1      "m < fl ==> n - Suc fl < fl - m + (n - m)"
    1.25 -  arith2      "[| m<n;  m <= fl |] ==> n - Suc fl < fl - m + (n - m)"
    1.26 -  arith3      "[| Suc ix < m |] ==> ix - n < m - Suc ix + (m - n)"
    1.27 -  arith4      "[| ix < m;  n < ix |] ==> ix - n < m - Suc (ix) + (m - n)"
    1.28 -
    1.29  constdefs
    1.30    
    1.31    (** Abbreviations: the "always" part **)
    1.32 @@ -65,10 +59,10 @@
    1.33    closed :: state set  (*but this is the same as ready!!*)
    1.34      "closed ==  {s. stop s  & ~ open s &  move s}"
    1.35  
    1.36 -  atFloor :: nat => state set
    1.37 +  atFloor :: int => state set
    1.38      "atFloor n ==  {s. floor s = n}"
    1.39  
    1.40 -  Req :: nat => state set
    1.41 +  Req :: int => state set
    1.42      "Req n ==  {s. n : req s}"
    1.43  
    1.44  
    1.45 @@ -93,25 +87,25 @@
    1.46    req_up :: "(state*state) set"
    1.47      "req_up ==
    1.48           {(s,s'). s' = s (|stop  :=False,
    1.49 -			   floor := Suc (floor s),
    1.50 +			   floor := floor s + #1,
    1.51  			   up    := True|)
    1.52  		       & s : (ready Int goingup)}"
    1.53  
    1.54    req_down :: "(state*state) set"
    1.55      "req_down ==
    1.56           {(s,s'). s' = s (|stop  :=False,
    1.57 -			   floor := floor s - 1,
    1.58 +			   floor := floor s - #1,
    1.59  			   up    := False|)
    1.60  		       & s : (ready Int goingdown)}"
    1.61  
    1.62    move_up :: "(state*state) set"
    1.63      "move_up ==
    1.64 -         {(s,s'). s' = s (|floor := Suc (floor s)|)
    1.65 +         {(s,s'). s' = s (|floor := floor s + #1|)
    1.66  		       & ~ stop s & up s & floor s ~: req s}"
    1.67  
    1.68    move_down :: "(state*state) set"
    1.69      "move_down ==
    1.70 -         {(s,s'). s' = s (|floor := floor s - 1|)
    1.71 +         {(s,s'). s' = s (|floor := floor s - #1|)
    1.72  		       & ~ stop s & ~ up s & floor s ~: req s}"
    1.73  
    1.74    button_press  :: "(state*state) set"
    1.75 @@ -150,17 +144,18 @@
    1.76      "moving_down == {s. ~ stop s & ~ up s -->
    1.77                       (EX f. Min <= f & f <= floor s & f : req s)}"
    1.78    
    1.79 -  metric :: [nat,state] => nat
    1.80 +  metric :: [int,state] => int
    1.81      "metric ==
    1.82 -       %n s. if up s & floor s < n then n - floor s
    1.83 -	     else if ~ up s & n < floor s then floor s - n
    1.84 -	     else if up s & n < floor s then (Max - floor s) + (Max-n)
    1.85 -	     else if ~ up s & floor s < n then (floor s - Min) + (n-Min)
    1.86 -	     else 0"
    1.87 +       %n s. if floor s < n then (if up s then n - floor s
    1.88 +			          else (floor s - Min) + (n-Min))
    1.89 +             else
    1.90 +             if n < floor s then (if up s then (Max - floor s) + (Max-n)
    1.91 +		                  else floor s - n)
    1.92 +             else #0"
    1.93  
    1.94  locale floor =
    1.95    fixes 
    1.96 -    n	:: nat
    1.97 +    n	:: int
    1.98    assumes
    1.99      Min_le_n    "Min <= n"
   1.100      n_le_Max    "n <= Max"