diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Simple/Lift.thy --- a/src/HOL/UNITY/Simple/Lift.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Simple/Lift.thy Sat Feb 08 16:05:33 2003 +0100 @@ -120,11 +120,12 @@ Lift :: "state program" (*for the moment, we OMIT button_press*) - "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s & + "Lift == mk_total_program + ({s. floor s = Min & ~ up s & move s & stop s & ~ open s & req s = {}}, - {request_act, open_act, close_act, - req_up, req_down, move_up, move_down}, - UNIV)" + {request_act, open_act, close_act, + req_up, req_down, move_up, move_down}, + UNIV)" (** Invariants **) @@ -196,7 +197,7 @@ lemma open_stop: "Lift \ Always open_stop" apply (rule AlwaysI, force) -apply (unfold Lift_def, constrains) +apply (unfold Lift_def, constrains) done lemma stop_floor: "Lift \ Always stop_floor" @@ -249,19 +250,22 @@ apply (unfold Lift_def, ensures_tac "open_act") done (*lem_lift_1_5*) + + + lemma E_thm02: "Lift \ (Req n \ stopped - atFloor n) LeadsTo - (Req n \ opened - atFloor n)" + (Req n \ opened - atFloor n)" apply (cut_tac stop_floor) apply (unfold Lift_def, ensures_tac "open_act") done (*lem_lift_1_1*) lemma E_thm03: "Lift \ (Req n \ opened - atFloor n) LeadsTo - (Req n \ closed - (atFloor n - queueing))" + (Req n \ closed - (atFloor n - queueing))" apply (unfold Lift_def, ensures_tac "close_act") done (*lem_lift_1_2*) lemma E_thm04: "Lift \ (Req n \ closed \ (atFloor n - queueing)) - LeadsTo (opened \ atFloor n)" + LeadsTo (opened \ atFloor n)" apply (unfold Lift_def, ensures_tac "open_act") done (*lem_lift_1_7*)