src/HOL/UNITY/Lift.thy
changeset 5320 79b326bceafb
parent 5277 e4297d03e5d2
child 5340 d75c03cf77b5
     1.1 --- a/src/HOL/UNITY/Lift.thy	Fri Aug 14 12:06:34 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Lift.thy	Fri Aug 14 13:52:42 1998 +0200
     1.3 @@ -27,25 +27,44 @@
     1.4    
     1.5    (** Abbreviations: the "always" part **)
     1.6    
     1.7 -  above :: "state set"
     1.8 +  above :: state set
     1.9      "above == {s. EX i. floor s < i & i <= max & i : req s}"
    1.10  
    1.11 -  below :: "state set"
    1.12 +  below :: state set
    1.13      "below == {s. EX i. min <= i & i < floor s & i : req s}"
    1.14  
    1.15 -  queueing :: "state set"
    1.16 +  queueing :: state set
    1.17      "queueing == above Un below"
    1.18  
    1.19 -  goingup :: "state set"
    1.20 +  goingup :: state set
    1.21      "goingup == above Int ({s. up s} Un Compl below)"
    1.22  
    1.23 -  goingdown :: "state set"
    1.24 +  goingdown :: state set
    1.25      "goingdown == below Int ({s. ~ up s} Un Compl above)"
    1.26  
    1.27 -  ready :: "state set"
    1.28 +  ready :: state set
    1.29      "ready == {s. stop s & ~ open s & move s}"
    1.30  
    1.31 + 
    1.32 +  (** Further abbreviations **)
    1.33  
    1.34 +  moving :: state set
    1.35 +    "moving ==  {s. ~ stop s & ~ open s}"
    1.36 +
    1.37 +  stopped :: state set
    1.38 +    "stopped == {s. stop s  & ~ open s &  move s}"
    1.39 +
    1.40 +  opened :: state set
    1.41 +    "opened ==  {s. stop s  &  open s  &  move s}"
    1.42 +
    1.43 +  closed :: state set
    1.44 +    "closed ==  {s. stop s  & ~ open s &  move s}"
    1.45 +
    1.46 +  atFloor :: nat => state set
    1.47 +    "atFloor n ==  {s. floor s = n}"
    1.48 +
    1.49 +
    1.50 +  
    1.51    (** The program **)
    1.52    
    1.53    request_act :: "(state*state) set"
    1.54 @@ -99,11 +118,6 @@
    1.55    bounded :: state set
    1.56      "bounded == {s. min <= floor s & floor s <= max}"
    1.57  
    1.58 -  (** ???
    1.59 -		    (~ stop s & up s --> floor s < max) &
    1.60 -		    (~ stop s & ~ up s --> min < floor s)}"
    1.61 -  **)
    1.62 -
    1.63    open_stop :: state set
    1.64      "open_stop == {s. open s --> stop s}"
    1.65    
    1.66 @@ -121,7 +135,8 @@
    1.67      "moving_down == {s. ~ stop s & ~ up s -->
    1.68                       (EX f. min <= f & f <= floor s & f : req s)}"
    1.69    
    1.70 -  valid :: "state set"
    1.71 +  (*intersection of all invariants: NECESSARY??*)
    1.72 +  valid :: state set
    1.73      "valid == bounded Int open_stop Int open_move"
    1.74  
    1.75  end