src/HOL/UNITY/Simple/Lift.thy
changeset 13812 91713a1915ee
parent 13806 fd40c9d9076b
child 14378 69c4d5997669
equal deleted inserted replaced
13811:f39f67982854 13812:91713a1915ee
   118 		        & Min \<le> n & n \<le> Max}"
   118 		        & Min \<le> n & n \<le> Max}"
   119 
   119 
   120 
   120 
   121   Lift :: "state program"
   121   Lift :: "state program"
   122     (*for the moment, we OMIT button_press*)
   122     (*for the moment, we OMIT button_press*)
   123     "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
   123     "Lift == mk_total_program
       
   124                 ({s. floor s = Min & ~ up s & move s & stop s &
   124 		          ~ open s & req s = {}},
   125 		          ~ open s & req s = {}},
   125 			 {request_act, open_act, close_act,
   126 		 {request_act, open_act, close_act,
   126 			  req_up, req_down, move_up, move_down},
   127  		  req_up, req_down, move_up, move_down},
   127 			 UNIV)"
   128 		 UNIV)"
   128 
   129 
   129 
   130 
   130   (** Invariants **)
   131   (** Invariants **)
   131 
   132 
   132   bounded :: "state set"
   133   bounded :: "state set"
   194         moving_up_def [simp]
   195         moving_up_def [simp]
   195         moving_down_def [simp]
   196         moving_down_def [simp]
   196 
   197 
   197 lemma open_stop: "Lift \<in> Always open_stop"
   198 lemma open_stop: "Lift \<in> Always open_stop"
   198 apply (rule AlwaysI, force) 
   199 apply (rule AlwaysI, force) 
   199 apply (unfold Lift_def, constrains) 
   200 apply (unfold Lift_def, constrains)
   200 done
   201 done
   201 
   202 
   202 lemma stop_floor: "Lift \<in> Always stop_floor"
   203 lemma stop_floor: "Lift \<in> Always stop_floor"
   203 apply (rule AlwaysI, force) 
   204 apply (rule AlwaysI, force) 
   204 apply (unfold Lift_def, constrains)
   205 apply (unfold Lift_def, constrains)
   247 lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
   248 lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
   248 apply (cut_tac stop_floor)
   249 apply (cut_tac stop_floor)
   249 apply (unfold Lift_def, ensures_tac "open_act")
   250 apply (unfold Lift_def, ensures_tac "open_act")
   250 done  (*lem_lift_1_5*)
   251 done  (*lem_lift_1_5*)
   251 
   252 
       
   253 
       
   254 
       
   255 
   252 lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
   256 lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
   253                      (Req n \<inter> opened - atFloor n)"
   257                        (Req n \<inter> opened - atFloor n)"
   254 apply (cut_tac stop_floor)
   258 apply (cut_tac stop_floor)
   255 apply (unfold Lift_def, ensures_tac "open_act")
   259 apply (unfold Lift_def, ensures_tac "open_act")
   256 done  (*lem_lift_1_1*)
   260 done  (*lem_lift_1_1*)
   257 
   261 
   258 lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
   262 lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
   259                      (Req n \<inter> closed - (atFloor n - queueing))"
   263                        (Req n \<inter> closed - (atFloor n - queueing))"
   260 apply (unfold Lift_def, ensures_tac "close_act")
   264 apply (unfold Lift_def, ensures_tac "close_act")
   261 done  (*lem_lift_1_2*)
   265 done  (*lem_lift_1_2*)
   262 
   266 
   263 lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
   267 lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
   264              LeadsTo (opened \<inter> atFloor n)"
   268                        LeadsTo (opened \<inter> atFloor n)"
   265 apply (unfold Lift_def, ensures_tac "open_act")
   269 apply (unfold Lift_def, ensures_tac "open_act")
   266 done  (*lem_lift_1_7*)
   270 done  (*lem_lift_1_7*)
   267 
   271 
   268 
   272 
   269 (** Lift 2.  Statements of thm05a and thm05b were wrong! **)
   273 (** Lift 2.  Statements of thm05a and thm05b were wrong! **)