src/HOL/UNITY/Simple/Lift.thy
changeset 13806 fd40c9d9076b
parent 13785 e2fcd88be55d
child 13812 91713a1915ee
     1.1 --- a/src/HOL/UNITY/Simple/Lift.thy	Tue Feb 04 18:12:40 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Simple/Lift.thy	Wed Feb 05 13:35:32 2003 +0100
     1.3 @@ -21,26 +21,26 @@
     1.4    Max :: "int"       (*least and greatest floors*)
     1.5  
     1.6  axioms
     1.7 -  Min_le_Max [iff]: "Min <= Max"
     1.8 +  Min_le_Max [iff]: "Min \<le> Max"
     1.9    
    1.10  constdefs
    1.11    
    1.12    (** Abbreviations: the "always" part **)
    1.13    
    1.14    above :: "state set"
    1.15 -    "above == {s. EX i. floor s < i & i <= Max & i : req s}"
    1.16 +    "above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
    1.17  
    1.18    below :: "state set"
    1.19 -    "below == {s. EX i. Min <= i & i < floor s & i : req s}"
    1.20 +    "below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
    1.21  
    1.22    queueing :: "state set"
    1.23 -    "queueing == above Un below"
    1.24 +    "queueing == above \<union> below"
    1.25  
    1.26    goingup :: "state set"
    1.27 -    "goingup   == above Int  ({s. up s}  Un -below)"
    1.28 +    "goingup   == above \<inter> ({s. up s}  \<union> -below)"
    1.29  
    1.30    goingdown :: "state set"
    1.31 -    "goingdown == below Int ({s. ~ up s} Un -above)"
    1.32 +    "goingdown == below \<inter> ({s. ~ up s} \<union> -above)"
    1.33  
    1.34    ready :: "state set"
    1.35      "ready == {s. stop s & ~ open s & move s}"
    1.36 @@ -63,7 +63,7 @@
    1.37      "atFloor n ==  {s. floor s = n}"
    1.38  
    1.39    Req :: "int => state set"
    1.40 -    "Req n ==  {s. n : req s}"
    1.41 +    "Req n ==  {s. n \<in> req s}"
    1.42  
    1.43  
    1.44    
    1.45 @@ -71,15 +71,15 @@
    1.46    
    1.47    request_act :: "(state*state) set"
    1.48      "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
    1.49 -		                  & ~ stop s & floor s : req s}"
    1.50 +		                  & ~ stop s & floor s \<in> req s}"
    1.51  
    1.52    open_act :: "(state*state) set"
    1.53      "open_act ==
    1.54           {(s,s'). s' = s (|open :=True,
    1.55  			   req  := req s - {floor s},
    1.56  			   move := True|)
    1.57 -		       & stop s & ~ open s & floor s : req s
    1.58 -	               & ~(move s & s: queueing)}"
    1.59 +		       & stop s & ~ open s & floor s \<in> req s
    1.60 +	               & ~(move s & s \<in> queueing)}"
    1.61  
    1.62    close_act :: "(state*state) set"
    1.63      "close_act == {(s,s'). s' = s (|open := False|) & open s}"
    1.64 @@ -89,24 +89,24 @@
    1.65           {(s,s'). s' = s (|stop  :=False,
    1.66  			   floor := floor s + 1,
    1.67  			   up    := True|)
    1.68 -		       & s : (ready Int goingup)}"
    1.69 +		       & s \<in> (ready \<inter> goingup)}"
    1.70  
    1.71    req_down :: "(state*state) set"
    1.72      "req_down ==
    1.73           {(s,s'). s' = s (|stop  :=False,
    1.74  			   floor := floor s - 1,
    1.75  			   up    := False|)
    1.76 -		       & s : (ready Int goingdown)}"
    1.77 +		       & s \<in> (ready \<inter> goingdown)}"
    1.78  
    1.79    move_up :: "(state*state) set"
    1.80      "move_up ==
    1.81           {(s,s'). s' = s (|floor := floor s + 1|)
    1.82 -		       & ~ stop s & up s & floor s ~: req s}"
    1.83 +		       & ~ stop s & up s & floor s \<notin> req s}"
    1.84  
    1.85    move_down :: "(state*state) set"
    1.86      "move_down ==
    1.87           {(s,s'). s' = s (|floor := floor s - 1|)
    1.88 -		       & ~ stop s & ~ up s & floor s ~: req s}"
    1.89 +		       & ~ stop s & ~ up s & floor s \<notin> req s}"
    1.90  
    1.91    (*This action is omitted from prior treatments, which therefore are
    1.92      unrealistic: nobody asks the lift to do anything!  But adding this
    1.93 @@ -114,8 +114,8 @@
    1.94      "ensures" properties fail.*)
    1.95    button_press  :: "(state*state) set"
    1.96      "button_press ==
    1.97 -         {(s,s'). EX n. s' = s (|req := insert n (req s)|)
    1.98 -		        & Min <= n & n <= Max}"
    1.99 +         {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
   1.100 +		        & Min \<le> n & n \<le> Max}"
   1.101  
   1.102  
   1.103    Lift :: "state program"
   1.104 @@ -130,7 +130,7 @@
   1.105    (** Invariants **)
   1.106  
   1.107    bounded :: "state set"
   1.108 -    "bounded == {s. Min <= floor s & floor s <= Max}"
   1.109 +    "bounded == {s. Min \<le> floor s & floor s \<le> Max}"
   1.110  
   1.111    open_stop :: "state set"
   1.112      "open_stop == {s. open s --> stop s}"
   1.113 @@ -139,15 +139,15 @@
   1.114      "open_move == {s. open s --> move s}"
   1.115    
   1.116    stop_floor :: "state set"
   1.117 -    "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
   1.118 +    "stop_floor == {s. stop s & ~ move s --> floor s \<in> req s}"
   1.119    
   1.120    moving_up :: "state set"
   1.121      "moving_up == {s. ~ stop s & up s -->
   1.122 -                   (EX f. floor s <= f & f <= Max & f : req s)}"
   1.123 +                   (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
   1.124    
   1.125    moving_down :: "state set"
   1.126      "moving_down == {s. ~ stop s & ~ up s -->
   1.127 -                     (EX f. Min <= f & f <= floor s & f : req s)}"
   1.128 +                     (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}"
   1.129    
   1.130    metric :: "[int,state] => int"
   1.131      "metric ==
   1.132 @@ -160,10 +160,10 @@
   1.133  
   1.134  locale Floor =
   1.135    fixes n
   1.136 -  assumes Min_le_n [iff]: "Min <= n"
   1.137 -      and n_le_Max [iff]: "n <= Max"
   1.138 +  assumes Min_le_n [iff]: "Min \<le> n"
   1.139 +      and n_le_Max [iff]: "n \<le> Max"
   1.140  
   1.141 -lemma not_mem_distinct: "[| x ~: A;  y : A |] ==> x ~= y"
   1.142 +lemma not_mem_distinct: "[| x \<notin> A;  y \<in> A |] ==> x \<noteq> y"
   1.143  by blast
   1.144  
   1.145  
   1.146 @@ -194,36 +194,36 @@
   1.147          moving_up_def [simp]
   1.148          moving_down_def [simp]
   1.149  
   1.150 -lemma open_stop: "Lift : Always open_stop"
   1.151 +lemma open_stop: "Lift \<in> Always open_stop"
   1.152  apply (rule AlwaysI, force) 
   1.153  apply (unfold Lift_def, constrains) 
   1.154  done
   1.155  
   1.156 -lemma stop_floor: "Lift : Always stop_floor"
   1.157 +lemma stop_floor: "Lift \<in> Always stop_floor"
   1.158  apply (rule AlwaysI, force) 
   1.159  apply (unfold Lift_def, constrains)
   1.160  done
   1.161  
   1.162  (*This one needs open_stop, which was proved above*)
   1.163 -lemma open_move: "Lift : Always open_move"
   1.164 +lemma open_move: "Lift \<in> Always open_move"
   1.165  apply (cut_tac open_stop)
   1.166  apply (rule AlwaysI, force) 
   1.167  apply (unfold Lift_def, constrains)
   1.168  done
   1.169  
   1.170 -lemma moving_up: "Lift : Always moving_up"
   1.171 +lemma moving_up: "Lift \<in> Always moving_up"
   1.172  apply (rule AlwaysI, force) 
   1.173  apply (unfold Lift_def, constrains)
   1.174  apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
   1.175  done
   1.176  
   1.177 -lemma moving_down: "Lift : Always moving_down"
   1.178 +lemma moving_down: "Lift \<in> Always moving_down"
   1.179  apply (rule AlwaysI, force) 
   1.180  apply (unfold Lift_def, constrains)
   1.181  apply (blast dest: zle_imp_zless_or_eq)
   1.182  done
   1.183  
   1.184 -lemma bounded: "Lift : Always bounded"
   1.185 +lemma bounded: "Lift \<in> Always bounded"
   1.186  apply (cut_tac moving_up moving_down)
   1.187  apply (rule AlwaysI, force) 
   1.188  apply (unfold Lift_def, constrains, auto)
   1.189 @@ -244,24 +244,24 @@
   1.190  (** The HUG'93 paper mistakenly omits the Req n from these! **)
   1.191  
   1.192  (** Lift_1 **)
   1.193 -lemma E_thm01: "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"
   1.194 +lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
   1.195  apply (cut_tac stop_floor)
   1.196  apply (unfold Lift_def, ensures_tac "open_act")
   1.197  done  (*lem_lift_1_5*)
   1.198  
   1.199 -lemma E_thm02: "Lift : (Req n Int stopped - atFloor n) LeadsTo  
   1.200 -                     (Req n Int opened - atFloor n)"
   1.201 +lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
   1.202 +                     (Req n \<inter> opened - atFloor n)"
   1.203  apply (cut_tac stop_floor)
   1.204  apply (unfold Lift_def, ensures_tac "open_act")
   1.205  done  (*lem_lift_1_1*)
   1.206  
   1.207 -lemma E_thm03: "Lift : (Req n Int opened - atFloor n) LeadsTo  
   1.208 -                     (Req n Int closed - (atFloor n - queueing))"
   1.209 +lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
   1.210 +                     (Req n \<inter> closed - (atFloor n - queueing))"
   1.211  apply (unfold Lift_def, ensures_tac "close_act")
   1.212  done  (*lem_lift_1_2*)
   1.213  
   1.214 -lemma E_thm04: "Lift : (Req n Int closed Int (atFloor n - queueing))   
   1.215 -             LeadsTo (opened Int atFloor n)"
   1.216 +lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
   1.217 +             LeadsTo (opened \<inter> atFloor n)"
   1.218  apply (unfold Lift_def, ensures_tac "open_act")
   1.219  done  (*lem_lift_1_7*)
   1.220  
   1.221 @@ -283,14 +283,14 @@
   1.222    NOT an ensures_tac property, but a mere inclusion
   1.223    don't know why script lift_2.uni says ENSURES*)
   1.224  lemma (in Floor) E_thm05c: 
   1.225 -    "Lift : (Req n Int closed - (atFloor n - queueing))    
   1.226 -             LeadsTo ((closed Int goingup Int Req n)  Un  
   1.227 -                      (closed Int goingdown Int Req n))"
   1.228 +    "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
   1.229 +             LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
   1.230 +                      (closed \<inter> goingdown \<inter> Req n))"
   1.231  by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
   1.232  
   1.233  (*lift_2*)
   1.234 -lemma (in Floor) lift_2: "Lift : (Req n Int closed - (atFloor n - queueing))    
   1.235 -             LeadsTo (moving Int Req n)"
   1.236 +lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
   1.237 +             LeadsTo (moving \<inter> Req n)"
   1.238  apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
   1.239  apply (unfold Lift_def) 
   1.240  apply (ensures_tac [2] "req_down")
   1.241 @@ -306,13 +306,13 @@
   1.242  (*lem_lift_4_1 *)
   1.243  lemma (in Floor) E_thm12a:
   1.244       "0 < N ==>  
   1.245 -      Lift : (moving Int Req n Int {s. metric n s = N} Int  
   1.246 -              {s. floor s ~: req s} Int {s. up s})    
   1.247 +      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
   1.248 +              {s. floor s \<notin> req s} \<inter> {s. up s})    
   1.249               LeadsTo  
   1.250 -               (moving Int Req n Int {s. metric n s < N})"
   1.251 +               (moving \<inter> Req n \<inter> {s. metric n s < N})"
   1.252  apply (cut_tac moving_up)
   1.253  apply (unfold Lift_def, ensures_tac "move_up", safe)
   1.254 -(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   1.255 +(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
   1.256  apply (erule linorder_leI [THEN order_antisym, symmetric])
   1.257  apply (auto simp add: metric_def)
   1.258  done
   1.259 @@ -320,21 +320,21 @@
   1.260  
   1.261  (*lem_lift_4_3 *)
   1.262  lemma (in Floor) E_thm12b: "0 < N ==>  
   1.263 -      Lift : (moving Int Req n Int {s. metric n s = N} Int  
   1.264 -              {s. floor s ~: req s} - {s. up s})    
   1.265 -             LeadsTo (moving Int Req n Int {s. metric n s < N})"
   1.266 +      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
   1.267 +              {s. floor s \<notin> req s} - {s. up s})    
   1.268 +             LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
   1.269  apply (cut_tac moving_down)
   1.270  apply (unfold Lift_def, ensures_tac "move_down", safe)
   1.271 -(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   1.272 +(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
   1.273  apply (erule linorder_leI [THEN order_antisym, symmetric])
   1.274  apply (auto simp add: metric_def)
   1.275  done
   1.276  
   1.277  (*lift_4*)
   1.278  lemma (in Floor) lift_4:
   1.279 -     "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int  
   1.280 -                            {s. floor s ~: req s}) LeadsTo      
   1.281 -                           (moving Int Req n Int {s. metric n s < N})"
   1.282 +     "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
   1.283 +                            {s. floor s \<notin> req s}) LeadsTo      
   1.284 +                           (moving \<inter> Req n \<inter> {s. metric n s < N})"
   1.285  apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   1.286                                LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
   1.287  done
   1.288 @@ -344,8 +344,8 @@
   1.289  
   1.290  (*lem_lift_5_3*)
   1.291  lemma (in Floor) E_thm16a: "0<N    
   1.292 -  ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo  
   1.293 -             (moving Int Req n Int {s. metric n s < N})"
   1.294 +  ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo  
   1.295 +             (moving \<inter> Req n \<inter> {s. metric n s < N})"
   1.296  apply (cut_tac bounded)
   1.297  apply (unfold Lift_def, ensures_tac "req_up")
   1.298  apply (auto simp add: metric_def)
   1.299 @@ -354,8 +354,8 @@
   1.300  
   1.301  (*lem_lift_5_1 has ~goingup instead of goingdown*)
   1.302  lemma (in Floor) E_thm16b: "0<N ==>    
   1.303 -      Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo  
   1.304 -                   (moving Int Req n Int {s. metric n s < N})"
   1.305 +      Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo  
   1.306 +                   (moving \<inter> Req n \<inter> {s. metric n s < N})"
   1.307  apply (cut_tac bounded)
   1.308  apply (unfold Lift_def, ensures_tac "req_down")
   1.309  apply (auto simp add: metric_def)
   1.310 @@ -365,14 +365,14 @@
   1.311  (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   1.312    i.e. the trivial disjunction, leading to an asymmetrical proof.*)
   1.313  lemma (in Floor) E_thm16c:
   1.314 -     "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"
   1.315 +     "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown"
   1.316  by (force simp add: metric_def)
   1.317  
   1.318  
   1.319  (*lift_5*)
   1.320  lemma (in Floor) lift_5:
   1.321 -     "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo    
   1.322 -                     (moving Int Req n Int {s. metric n s < N})"
   1.323 +     "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo    
   1.324 +                     (moving \<inter> Req n \<inter> {s. metric n s < N})"
   1.325  apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   1.326                                LeadsTo_Un [OF E_thm16a E_thm16b]])
   1.327  apply (drule E_thm16c, auto)
   1.328 @@ -383,37 +383,37 @@
   1.329  
   1.330  (*lemma used to prove lem_lift_3_1*)
   1.331  lemma (in Floor) metric_eq_0D [dest]:
   1.332 -     "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n"
   1.333 +     "[| metric n s = 0;  Min \<le> floor s;  floor s \<le> Max |] ==> floor s = n"
   1.334  by (force simp add: metric_def)
   1.335  
   1.336  
   1.337  (*lem_lift_3_1*)
   1.338 -lemma (in Floor) E_thm11: "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo    
   1.339 -                       (stopped Int atFloor n)"
   1.340 +lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo    
   1.341 +                       (stopped \<inter> atFloor n)"
   1.342  apply (cut_tac bounded)
   1.343  apply (unfold Lift_def, ensures_tac "request_act", auto)
   1.344  done
   1.345  
   1.346  (*lem_lift_3_5*)
   1.347  lemma (in Floor) E_thm13: 
   1.348 -  "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
   1.349 -  LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"
   1.350 +  "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
   1.351 +  LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})"
   1.352  apply (unfold Lift_def, ensures_tac "request_act")
   1.353  apply (auto simp add: metric_def)
   1.354  done
   1.355  
   1.356  (*lem_lift_3_6*)
   1.357  lemma (in Floor) E_thm14: "0 < N ==>  
   1.358 -      Lift :  
   1.359 -        (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
   1.360 -        LeadsTo (opened Int Req n Int {s. metric n s = N})"
   1.361 +      Lift \<in>  
   1.362 +        (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
   1.363 +        LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})"
   1.364  apply (unfold Lift_def, ensures_tac "open_act")
   1.365  apply (auto simp add: metric_def)
   1.366  done
   1.367  
   1.368  (*lem_lift_3_7*)
   1.369 -lemma (in Floor) E_thm15: "Lift : (opened Int Req n Int {s. metric n s = N})   
   1.370 -             LeadsTo (closed Int Req n Int {s. metric n s = N})"
   1.371 +lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})   
   1.372 +             LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})"
   1.373  apply (unfold Lift_def, ensures_tac "close_act")
   1.374  apply (auto simp add: metric_def)
   1.375  done
   1.376 @@ -422,15 +422,15 @@
   1.377  (** the final steps **)
   1.378  
   1.379  lemma (in Floor) lift_3_Req: "0 < N ==>  
   1.380 -      Lift :  
   1.381 -        (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})    
   1.382 -        LeadsTo (moving Int Req n Int {s. metric n s < N})"
   1.383 +      Lift \<in>  
   1.384 +        (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})    
   1.385 +        LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
   1.386  apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans)
   1.387  done
   1.388  
   1.389  
   1.390  (*Now we observe that our integer metric is really a natural number*)
   1.391 -lemma (in Floor) Always_nonneg: "Lift : Always {s. 0 <= metric n s}"
   1.392 +lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
   1.393  apply (rule bounded [THEN Always_weaken])
   1.394  apply (auto simp add: metric_def)
   1.395  done
   1.396 @@ -438,10 +438,10 @@
   1.397  lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
   1.398  
   1.399  lemma (in Floor) lift_3:
   1.400 -     "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"
   1.401 +     "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
   1.402  apply (rule Always_nonneg [THEN integ_0_le_induct])
   1.403  apply (case_tac "0 < z")
   1.404 -(*If z <= 0 then actually z = 0*)
   1.405 +(*If z \<le> 0 then actually z = 0*)
   1.406  prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less)
   1.407  apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])
   1.408  apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   1.409 @@ -449,7 +449,7 @@
   1.410  done
   1.411  
   1.412  
   1.413 -lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)"
   1.414 +lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
   1.415  apply (rule LeadsTo_Trans)
   1.416   prefer 2
   1.417   apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])