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"
```