src/HOL/UNITY/Lift.thy
changeset 5357 6efb2b87610c
parent 5340 d75c03cf77b5
child 5426 566f47250bd0
     1.1 --- a/src/HOL/UNITY/Lift.thy	Thu Aug 20 16:58:28 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Lift.thy	Thu Aug 20 17:43:01 1998 +0200
     1.3 @@ -19,25 +19,26 @@
     1.4    move  :: bool		(*whether moving takes precedence over opening*)
     1.5  
     1.6  consts
     1.7 -  min, max :: nat       (*least and greatest floors*)
     1.8 +  Min, Max :: nat       (*least and greatest floors*)
     1.9  
    1.10  rules
    1.11 -  min_le_max  "min <= max"
    1.12 +  Min_le_Max  "Min <= Max"
    1.13    
    1.14    (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
    1.15    arith1      "m < fl ==> n - Suc fl < fl - m + (n - m)"
    1.16 -  arith2      "[| Suc fl < n; m < n |] ==> n - Suc fl < fl - m + (n - m)"
    1.17 -
    1.18 +  arith2      "[| m<n;  m <= fl |] ==> n - Suc fl < fl - m + (n - m)"
    1.19 +  arith3      "[| Suc ix < m |] ==> ix - n < m - Suc ix + (m - n)"
    1.20 +  arith4      "[| ix < m;  n < ix |] ==> ix - n < m - Suc (ix) + (m - n)"
    1.21  
    1.22  constdefs
    1.23    
    1.24    (** Abbreviations: the "always" part **)
    1.25    
    1.26    above :: state set
    1.27 -    "above == {s. EX i. floor s < i & i <= max & i : req s}"
    1.28 +    "above == {s. EX i. floor s < i & i <= Max & i : req s}"
    1.29  
    1.30    below :: state set
    1.31 -    "below == {s. EX i. min <= i & i < floor s & i : req s}"
    1.32 +    "below == {s. EX i. Min <= i & i < floor s & i : req s}"
    1.33  
    1.34    queueing :: state set
    1.35      "queueing == above Un below"
    1.36 @@ -91,15 +92,15 @@
    1.37    close_act :: "(state*state) set"
    1.38      "close_act == {(s,s'). s' = s (|open := False|) & open s}"
    1.39  
    1.40 -  req_up_act :: "(state*state) set"
    1.41 -    "req_up_act ==
    1.42 +  req_up :: "(state*state) set"
    1.43 +    "req_up ==
    1.44           {(s,s'). s' = s (|stop  :=False,
    1.45  			   floor := Suc (floor s),
    1.46  			   up    := True|)
    1.47  		       & s : (ready Int goingup)}"
    1.48  
    1.49 -  req_down_act :: "(state*state) set"
    1.50 -    "req_down_act ==
    1.51 +  req_down :: "(state*state) set"
    1.52 +    "req_down ==
    1.53           {(s,s'). s' = s (|stop  :=False,
    1.54  			   floor := floor s - 1,
    1.55  			   up    := False|)
    1.56 @@ -115,17 +116,24 @@
    1.57           {(s,s'). s' = s (|floor := floor s - 1|)
    1.58  		       & ~ stop s & ~ up s & floor s ~: req s}"
    1.59  
    1.60 +  button_press  :: "(state*state) set"
    1.61 +    "button_press ==
    1.62 +         {(s,s'). EX n. s' = s (|req := insert n (req s)|)
    1.63 +		        & Min <= n & n <= Max}"
    1.64 +
    1.65 +
    1.66    Lprg :: state program
    1.67 -    "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s &
    1.68 +    (*for the moment, we OMIT button_press*)
    1.69 +    "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
    1.70  		          ~ open s & req s = {}},
    1.71  	       Acts = {id, request_act, open_act, close_act,
    1.72 -		       req_up_act, req_down_act, move_up, move_down}|)"
    1.73 +		       req_up, req_down, move_up, move_down}|)"
    1.74  
    1.75  
    1.76    (** Invariants **)
    1.77  
    1.78    bounded :: state set
    1.79 -    "bounded == {s. min <= floor s & floor s <= max}"
    1.80 +    "bounded == {s. Min <= floor s & floor s <= Max}"
    1.81  
    1.82    open_stop :: state set
    1.83      "open_stop == {s. open s --> stop s}"
    1.84 @@ -138,25 +146,26 @@
    1.85    
    1.86    moving_up :: state set
    1.87      "moving_up == {s. ~ stop s & up s -->
    1.88 -                   (EX f. floor s <= f & f <= max & f : req s)}"
    1.89 +                   (EX f. floor s <= f & f <= Max & f : req s)}"
    1.90    
    1.91    moving_down :: state set
    1.92      "moving_down == {s. ~ stop s & ~ up s -->
    1.93 -                     (EX f. min <= f & f <= floor s & f : req s)}"
    1.94 +                     (EX f. Min <= f & f <= floor s & f : req s)}"
    1.95    
    1.96    metric :: [nat,state] => nat
    1.97 -    "metric n s == if up s & floor s < n then n - floor s
    1.98 -		   else if ~ up s & n < floor s then floor s - n
    1.99 -		   else if up s & n < floor s then (max - floor s) + (max-n)
   1.100 -		   else if ~ up s & floor s < n then (floor s - min) + (n-min)
   1.101 -		   else 0"
   1.102 +    "metric ==
   1.103 +       %n s. if up s & floor s < n then n - floor s
   1.104 +	     else if ~ up s & n < floor s then floor s - n
   1.105 +	     else if up s & n < floor s then (Max - floor s) + (Max-n)
   1.106 +	     else if ~ up s & floor s < n then (floor s - Min) + (n-Min)
   1.107 +	     else 0"
   1.108  
   1.109  locale floor =
   1.110    fixes 
   1.111      n	:: nat
   1.112    assumes
   1.113 -    min_le_n    "min <= n"
   1.114 -    n_le_max    "n <= max"
   1.115 +    Min_le_n    "Min <= n"
   1.116 +    n_le_Max    "n <= Max"
   1.117    defines
   1.118  
   1.119  end