src/HOL/UNITY/Simple/Lift.thy
changeset 14378 69c4d5997669
parent 13812 91713a1915ee
child 16184 80617b8d33c5
equal deleted inserted replaced
14377:f454b3004f8f 14378:69c4d5997669
   213 done
   213 done
   214 
   214 
   215 lemma moving_up: "Lift \<in> Always moving_up"
   215 lemma moving_up: "Lift \<in> Always moving_up"
   216 apply (rule AlwaysI, force) 
   216 apply (rule AlwaysI, force) 
   217 apply (unfold Lift_def, constrains)
   217 apply (unfold Lift_def, constrains)
   218 apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
   218 apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq)
   219 done
   219 done
   220 
   220 
   221 lemma moving_down: "Lift \<in> Always moving_down"
   221 lemma moving_down: "Lift \<in> Always moving_down"
   222 apply (rule AlwaysI, force) 
   222 apply (rule AlwaysI, force) 
   223 apply (unfold Lift_def, constrains)
   223 apply (unfold Lift_def, constrains)
   224 apply (blast dest: zle_imp_zless_or_eq)
   224 apply (blast dest: order_le_imp_less_or_eq)
   225 done
   225 done
   226 
   226 
   227 lemma bounded: "Lift \<in> Always bounded"
   227 lemma bounded: "Lift \<in> Always bounded"
   228 apply (cut_tac moving_up moving_down)
   228 apply (cut_tac moving_up moving_down)
   229 apply (rule AlwaysI, force) 
   229 apply (rule AlwaysI, force) 
   288   don't know why script lift_2.uni says ENSURES*)
   288   don't know why script lift_2.uni says ENSURES*)
   289 lemma (in Floor) E_thm05c: 
   289 lemma (in Floor) E_thm05c: 
   290     "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
   290     "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
   291              LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
   291              LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
   292                       (closed \<inter> goingdown \<inter> Req n))"
   292                       (closed \<inter> goingdown \<inter> Req n))"
   293 by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
   293 by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff)
   294 
   294 
   295 (*lift_2*)
   295 (*lift_2*)
   296 lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
   296 lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
   297              LeadsTo (moving \<inter> Req n)"
   297              LeadsTo (moving \<inter> Req n)"
   298 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
   298 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])