src/HOL/UNITY/Simple/Lift.thy
changeset 13812 91713a1915ee
parent 13806 fd40c9d9076b
child 14378 69c4d5997669
     1.1 --- a/src/HOL/UNITY/Simple/Lift.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Simple/Lift.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -120,11 +120,12 @@
     1.4  
     1.5    Lift :: "state program"
     1.6      (*for the moment, we OMIT button_press*)
     1.7 -    "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
     1.8 +    "Lift == mk_total_program
     1.9 +                ({s. floor s = Min & ~ up s & move s & stop s &
    1.10  		          ~ open s & req s = {}},
    1.11 -			 {request_act, open_act, close_act,
    1.12 -			  req_up, req_down, move_up, move_down},
    1.13 -			 UNIV)"
    1.14 +		 {request_act, open_act, close_act,
    1.15 + 		  req_up, req_down, move_up, move_down},
    1.16 +		 UNIV)"
    1.17  
    1.18  
    1.19    (** Invariants **)
    1.20 @@ -196,7 +197,7 @@
    1.21  
    1.22  lemma open_stop: "Lift \<in> Always open_stop"
    1.23  apply (rule AlwaysI, force) 
    1.24 -apply (unfold Lift_def, constrains) 
    1.25 +apply (unfold Lift_def, constrains)
    1.26  done
    1.27  
    1.28  lemma stop_floor: "Lift \<in> Always stop_floor"
    1.29 @@ -249,19 +250,22 @@
    1.30  apply (unfold Lift_def, ensures_tac "open_act")
    1.31  done  (*lem_lift_1_5*)
    1.32  
    1.33 +
    1.34 +
    1.35 +
    1.36  lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
    1.37 -                     (Req n \<inter> opened - atFloor n)"
    1.38 +                       (Req n \<inter> opened - atFloor n)"
    1.39  apply (cut_tac stop_floor)
    1.40  apply (unfold Lift_def, ensures_tac "open_act")
    1.41  done  (*lem_lift_1_1*)
    1.42  
    1.43  lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
    1.44 -                     (Req n \<inter> closed - (atFloor n - queueing))"
    1.45 +                       (Req n \<inter> closed - (atFloor n - queueing))"
    1.46  apply (unfold Lift_def, ensures_tac "close_act")
    1.47  done  (*lem_lift_1_2*)
    1.48  
    1.49  lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
    1.50 -             LeadsTo (opened \<inter> atFloor n)"
    1.51 +                       LeadsTo (opened \<inter> atFloor n)"
    1.52  apply (unfold Lift_def, ensures_tac "open_act")
    1.53  done  (*lem_lift_1_7*)
    1.54