src/HOL/UNITY/Simple/Lift.thy
changeset 13806 fd40c9d9076b
parent 13785 e2fcd88be55d
child 13812 91713a1915ee
equal deleted inserted replaced
13805:3786b2fd6808 13806:fd40c9d9076b
    19 consts
    19 consts
    20   Min :: "int"       (*least and greatest floors*)
    20   Min :: "int"       (*least and greatest floors*)
    21   Max :: "int"       (*least and greatest floors*)
    21   Max :: "int"       (*least and greatest floors*)
    22 
    22 
    23 axioms
    23 axioms
    24   Min_le_Max [iff]: "Min <= Max"
    24   Min_le_Max [iff]: "Min \<le> Max"
    25   
    25   
    26 constdefs
    26 constdefs
    27   
    27   
    28   (** Abbreviations: the "always" part **)
    28   (** Abbreviations: the "always" part **)
    29   
    29   
    30   above :: "state set"
    30   above :: "state set"
    31     "above == {s. EX i. floor s < i & i <= Max & i : req s}"
    31     "above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
    32 
    32 
    33   below :: "state set"
    33   below :: "state set"
    34     "below == {s. EX i. Min <= i & i < floor s & i : req s}"
    34     "below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
    35 
    35 
    36   queueing :: "state set"
    36   queueing :: "state set"
    37     "queueing == above Un below"
    37     "queueing == above \<union> below"
    38 
    38 
    39   goingup :: "state set"
    39   goingup :: "state set"
    40     "goingup   == above Int  ({s. up s}  Un -below)"
    40     "goingup   == above \<inter> ({s. up s}  \<union> -below)"
    41 
    41 
    42   goingdown :: "state set"
    42   goingdown :: "state set"
    43     "goingdown == below Int ({s. ~ up s} Un -above)"
    43     "goingdown == below \<inter> ({s. ~ up s} \<union> -above)"
    44 
    44 
    45   ready :: "state set"
    45   ready :: "state set"
    46     "ready == {s. stop s & ~ open s & move s}"
    46     "ready == {s. stop s & ~ open s & move s}"
    47  
    47  
    48   (** Further abbreviations **)
    48   (** Further abbreviations **)
    61 
    61 
    62   atFloor :: "int => state set"
    62   atFloor :: "int => state set"
    63     "atFloor n ==  {s. floor s = n}"
    63     "atFloor n ==  {s. floor s = n}"
    64 
    64 
    65   Req :: "int => state set"
    65   Req :: "int => state set"
    66     "Req n ==  {s. n : req s}"
    66     "Req n ==  {s. n \<in> req s}"
    67 
    67 
    68 
    68 
    69   
    69   
    70   (** The program **)
    70   (** The program **)
    71   
    71   
    72   request_act :: "(state*state) set"
    72   request_act :: "(state*state) set"
    73     "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
    73     "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
    74 		                  & ~ stop s & floor s : req s}"
    74 		                  & ~ stop s & floor s \<in> req s}"
    75 
    75 
    76   open_act :: "(state*state) set"
    76   open_act :: "(state*state) set"
    77     "open_act ==
    77     "open_act ==
    78          {(s,s'). s' = s (|open :=True,
    78          {(s,s'). s' = s (|open :=True,
    79 			   req  := req s - {floor s},
    79 			   req  := req s - {floor s},
    80 			   move := True|)
    80 			   move := True|)
    81 		       & stop s & ~ open s & floor s : req s
    81 		       & stop s & ~ open s & floor s \<in> req s
    82 	               & ~(move s & s: queueing)}"
    82 	               & ~(move s & s \<in> queueing)}"
    83 
    83 
    84   close_act :: "(state*state) set"
    84   close_act :: "(state*state) set"
    85     "close_act == {(s,s'). s' = s (|open := False|) & open s}"
    85     "close_act == {(s,s'). s' = s (|open := False|) & open s}"
    86 
    86 
    87   req_up :: "(state*state) set"
    87   req_up :: "(state*state) set"
    88     "req_up ==
    88     "req_up ==
    89          {(s,s'). s' = s (|stop  :=False,
    89          {(s,s'). s' = s (|stop  :=False,
    90 			   floor := floor s + 1,
    90 			   floor := floor s + 1,
    91 			   up    := True|)
    91 			   up    := True|)
    92 		       & s : (ready Int goingup)}"
    92 		       & s \<in> (ready \<inter> goingup)}"
    93 
    93 
    94   req_down :: "(state*state) set"
    94   req_down :: "(state*state) set"
    95     "req_down ==
    95     "req_down ==
    96          {(s,s'). s' = s (|stop  :=False,
    96          {(s,s'). s' = s (|stop  :=False,
    97 			   floor := floor s - 1,
    97 			   floor := floor s - 1,
    98 			   up    := False|)
    98 			   up    := False|)
    99 		       & s : (ready Int goingdown)}"
    99 		       & s \<in> (ready \<inter> goingdown)}"
   100 
   100 
   101   move_up :: "(state*state) set"
   101   move_up :: "(state*state) set"
   102     "move_up ==
   102     "move_up ==
   103          {(s,s'). s' = s (|floor := floor s + 1|)
   103          {(s,s'). s' = s (|floor := floor s + 1|)
   104 		       & ~ stop s & up s & floor s ~: req s}"
   104 		       & ~ stop s & up s & floor s \<notin> req s}"
   105 
   105 
   106   move_down :: "(state*state) set"
   106   move_down :: "(state*state) set"
   107     "move_down ==
   107     "move_down ==
   108          {(s,s'). s' = s (|floor := floor s - 1|)
   108          {(s,s'). s' = s (|floor := floor s - 1|)
   109 		       & ~ stop s & ~ up s & floor s ~: req s}"
   109 		       & ~ stop s & ~ up s & floor s \<notin> req s}"
   110 
   110 
   111   (*This action is omitted from prior treatments, which therefore are
   111   (*This action is omitted from prior treatments, which therefore are
   112     unrealistic: nobody asks the lift to do anything!  But adding this
   112     unrealistic: nobody asks the lift to do anything!  But adding this
   113     action invalidates many of the existing progress arguments: various
   113     action invalidates many of the existing progress arguments: various
   114     "ensures" properties fail.*)
   114     "ensures" properties fail.*)
   115   button_press  :: "(state*state) set"
   115   button_press  :: "(state*state) set"
   116     "button_press ==
   116     "button_press ==
   117          {(s,s'). EX n. s' = s (|req := insert n (req s)|)
   117          {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
   118 		        & Min <= n & n <= 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_program ({s. floor s = Min & ~ up s & move s & stop s &
   128 
   128 
   129 
   129 
   130   (** Invariants **)
   130   (** Invariants **)
   131 
   131 
   132   bounded :: "state set"
   132   bounded :: "state set"
   133     "bounded == {s. Min <= floor s & floor s <= Max}"
   133     "bounded == {s. Min \<le> floor s & floor s \<le> Max}"
   134 
   134 
   135   open_stop :: "state set"
   135   open_stop :: "state set"
   136     "open_stop == {s. open s --> stop s}"
   136     "open_stop == {s. open s --> stop s}"
   137   
   137   
   138   open_move :: "state set"
   138   open_move :: "state set"
   139     "open_move == {s. open s --> move s}"
   139     "open_move == {s. open s --> move s}"
   140   
   140   
   141   stop_floor :: "state set"
   141   stop_floor :: "state set"
   142     "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
   142     "stop_floor == {s. stop s & ~ move s --> floor s \<in> req s}"
   143   
   143   
   144   moving_up :: "state set"
   144   moving_up :: "state set"
   145     "moving_up == {s. ~ stop s & up s -->
   145     "moving_up == {s. ~ stop s & up s -->
   146                    (EX f. floor s <= f & f <= Max & f : req s)}"
   146                    (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
   147   
   147   
   148   moving_down :: "state set"
   148   moving_down :: "state set"
   149     "moving_down == {s. ~ stop s & ~ up s -->
   149     "moving_down == {s. ~ stop s & ~ up s -->
   150                      (EX f. Min <= f & f <= floor s & f : req s)}"
   150                      (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}"
   151   
   151   
   152   metric :: "[int,state] => int"
   152   metric :: "[int,state] => int"
   153     "metric ==
   153     "metric ==
   154        %n s. if floor s < n then (if up s then n - floor s
   154        %n s. if floor s < n then (if up s then n - floor s
   155 			          else (floor s - Min) + (n-Min))
   155 			          else (floor s - Min) + (n-Min))
   158 		                  else floor s - n)
   158 		                  else floor s - n)
   159              else 0"
   159              else 0"
   160 
   160 
   161 locale Floor =
   161 locale Floor =
   162   fixes n
   162   fixes n
   163   assumes Min_le_n [iff]: "Min <= n"
   163   assumes Min_le_n [iff]: "Min \<le> n"
   164       and n_le_Max [iff]: "n <= Max"
   164       and n_le_Max [iff]: "n \<le> Max"
   165 
   165 
   166 lemma not_mem_distinct: "[| x ~: A;  y : A |] ==> x ~= y"
   166 lemma not_mem_distinct: "[| x \<notin> A;  y \<in> A |] ==> x \<noteq> y"
   167 by blast
   167 by blast
   168 
   168 
   169 
   169 
   170 declare Lift_def [THEN def_prg_Init, simp]
   170 declare Lift_def [THEN def_prg_Init, simp]
   171 
   171 
   192         open_move_def [simp] 
   192         open_move_def [simp] 
   193         stop_floor_def [simp]
   193         stop_floor_def [simp]
   194         moving_up_def [simp]
   194         moving_up_def [simp]
   195         moving_down_def [simp]
   195         moving_down_def [simp]
   196 
   196 
   197 lemma open_stop: "Lift : Always open_stop"
   197 lemma open_stop: "Lift \<in> Always open_stop"
   198 apply (rule AlwaysI, force) 
   198 apply (rule AlwaysI, force) 
   199 apply (unfold Lift_def, constrains) 
   199 apply (unfold Lift_def, constrains) 
   200 done
   200 done
   201 
   201 
   202 lemma stop_floor: "Lift : Always stop_floor"
   202 lemma stop_floor: "Lift \<in> Always stop_floor"
   203 apply (rule AlwaysI, force) 
   203 apply (rule AlwaysI, force) 
   204 apply (unfold Lift_def, constrains)
   204 apply (unfold Lift_def, constrains)
   205 done
   205 done
   206 
   206 
   207 (*This one needs open_stop, which was proved above*)
   207 (*This one needs open_stop, which was proved above*)
   208 lemma open_move: "Lift : Always open_move"
   208 lemma open_move: "Lift \<in> Always open_move"
   209 apply (cut_tac open_stop)
   209 apply (cut_tac open_stop)
   210 apply (rule AlwaysI, force) 
   210 apply (rule AlwaysI, force) 
   211 apply (unfold Lift_def, constrains)
   211 apply (unfold Lift_def, constrains)
   212 done
   212 done
   213 
   213 
   214 lemma moving_up: "Lift : Always moving_up"
   214 lemma moving_up: "Lift \<in> Always moving_up"
   215 apply (rule AlwaysI, force) 
   215 apply (rule AlwaysI, force) 
   216 apply (unfold Lift_def, constrains)
   216 apply (unfold Lift_def, constrains)
   217 apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
   217 apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
   218 done
   218 done
   219 
   219 
   220 lemma moving_down: "Lift : Always moving_down"
   220 lemma moving_down: "Lift \<in> Always moving_down"
   221 apply (rule AlwaysI, force) 
   221 apply (rule AlwaysI, force) 
   222 apply (unfold Lift_def, constrains)
   222 apply (unfold Lift_def, constrains)
   223 apply (blast dest: zle_imp_zless_or_eq)
   223 apply (blast dest: zle_imp_zless_or_eq)
   224 done
   224 done
   225 
   225 
   226 lemma bounded: "Lift : Always bounded"
   226 lemma bounded: "Lift \<in> Always bounded"
   227 apply (cut_tac moving_up moving_down)
   227 apply (cut_tac moving_up moving_down)
   228 apply (rule AlwaysI, force) 
   228 apply (rule AlwaysI, force) 
   229 apply (unfold Lift_def, constrains, auto)
   229 apply (unfold Lift_def, constrains, auto)
   230 apply (drule not_mem_distinct, assumption, arith)+
   230 apply (drule not_mem_distinct, assumption, arith)+
   231 done
   231 done
   242 
   242 
   243 
   243 
   244 (** The HUG'93 paper mistakenly omits the Req n from these! **)
   244 (** The HUG'93 paper mistakenly omits the Req n from these! **)
   245 
   245 
   246 (** Lift_1 **)
   246 (** Lift_1 **)
   247 lemma E_thm01: "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"
   247 lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
   248 apply (cut_tac stop_floor)
   248 apply (cut_tac stop_floor)
   249 apply (unfold Lift_def, ensures_tac "open_act")
   249 apply (unfold Lift_def, ensures_tac "open_act")
   250 done  (*lem_lift_1_5*)
   250 done  (*lem_lift_1_5*)
   251 
   251 
   252 lemma E_thm02: "Lift : (Req n Int stopped - atFloor n) LeadsTo  
   252 lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
   253                      (Req n Int opened - atFloor n)"
   253                      (Req n \<inter> opened - atFloor n)"
   254 apply (cut_tac stop_floor)
   254 apply (cut_tac stop_floor)
   255 apply (unfold Lift_def, ensures_tac "open_act")
   255 apply (unfold Lift_def, ensures_tac "open_act")
   256 done  (*lem_lift_1_1*)
   256 done  (*lem_lift_1_1*)
   257 
   257 
   258 lemma E_thm03: "Lift : (Req n Int opened - atFloor n) LeadsTo  
   258 lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
   259                      (Req n Int closed - (atFloor n - queueing))"
   259                      (Req n \<inter> closed - (atFloor n - queueing))"
   260 apply (unfold Lift_def, ensures_tac "close_act")
   260 apply (unfold Lift_def, ensures_tac "close_act")
   261 done  (*lem_lift_1_2*)
   261 done  (*lem_lift_1_2*)
   262 
   262 
   263 lemma E_thm04: "Lift : (Req n Int closed Int (atFloor n - queueing))   
   263 lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
   264              LeadsTo (opened Int atFloor n)"
   264              LeadsTo (opened \<inter> atFloor n)"
   265 apply (unfold Lift_def, ensures_tac "open_act")
   265 apply (unfold Lift_def, ensures_tac "open_act")
   266 done  (*lem_lift_1_7*)
   266 done  (*lem_lift_1_7*)
   267 
   267 
   268 
   268 
   269 (** Lift 2.  Statements of thm05a and thm05b were wrong! **)
   269 (** Lift 2.  Statements of thm05a and thm05b were wrong! **)
   281 
   281 
   282 (*lem_lift_2_0 
   282 (*lem_lift_2_0 
   283   NOT an ensures_tac property, but a mere inclusion
   283   NOT an ensures_tac property, but a mere inclusion
   284   don't know why script lift_2.uni says ENSURES*)
   284   don't know why script lift_2.uni says ENSURES*)
   285 lemma (in Floor) E_thm05c: 
   285 lemma (in Floor) E_thm05c: 
   286     "Lift : (Req n Int closed - (atFloor n - queueing))    
   286     "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
   287              LeadsTo ((closed Int goingup Int Req n)  Un  
   287              LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
   288                       (closed Int goingdown Int Req n))"
   288                       (closed \<inter> goingdown \<inter> Req n))"
   289 by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
   289 by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
   290 
   290 
   291 (*lift_2*)
   291 (*lift_2*)
   292 lemma (in Floor) lift_2: "Lift : (Req n Int closed - (atFloor n - queueing))    
   292 lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
   293              LeadsTo (moving Int Req n)"
   293              LeadsTo (moving \<inter> Req n)"
   294 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
   294 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
   295 apply (unfold Lift_def) 
   295 apply (unfold Lift_def) 
   296 apply (ensures_tac [2] "req_down")
   296 apply (ensures_tac [2] "req_down")
   297 apply (ensures_tac "req_up", auto)
   297 apply (ensures_tac "req_up", auto)
   298 done
   298 done
   304 
   304 
   305 
   305 
   306 (*lem_lift_4_1 *)
   306 (*lem_lift_4_1 *)
   307 lemma (in Floor) E_thm12a:
   307 lemma (in Floor) E_thm12a:
   308      "0 < N ==>  
   308      "0 < N ==>  
   309       Lift : (moving Int Req n Int {s. metric n s = N} Int  
   309       Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
   310               {s. floor s ~: req s} Int {s. up s})    
   310               {s. floor s \<notin> req s} \<inter> {s. up s})    
   311              LeadsTo  
   311              LeadsTo  
   312                (moving Int Req n Int {s. metric n s < N})"
   312                (moving \<inter> Req n \<inter> {s. metric n s < N})"
   313 apply (cut_tac moving_up)
   313 apply (cut_tac moving_up)
   314 apply (unfold Lift_def, ensures_tac "move_up", safe)
   314 apply (unfold Lift_def, ensures_tac "move_up", safe)
   315 (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   315 (*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
   316 apply (erule linorder_leI [THEN order_antisym, symmetric])
   316 apply (erule linorder_leI [THEN order_antisym, symmetric])
   317 apply (auto simp add: metric_def)
   317 apply (auto simp add: metric_def)
   318 done
   318 done
   319 
   319 
   320 
   320 
   321 (*lem_lift_4_3 *)
   321 (*lem_lift_4_3 *)
   322 lemma (in Floor) E_thm12b: "0 < N ==>  
   322 lemma (in Floor) E_thm12b: "0 < N ==>  
   323       Lift : (moving Int Req n Int {s. metric n s = N} Int  
   323       Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
   324               {s. floor s ~: req s} - {s. up s})    
   324               {s. floor s \<notin> req s} - {s. up s})    
   325              LeadsTo (moving Int Req n Int {s. metric n s < N})"
   325              LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
   326 apply (cut_tac moving_down)
   326 apply (cut_tac moving_down)
   327 apply (unfold Lift_def, ensures_tac "move_down", safe)
   327 apply (unfold Lift_def, ensures_tac "move_down", safe)
   328 (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   328 (*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
   329 apply (erule linorder_leI [THEN order_antisym, symmetric])
   329 apply (erule linorder_leI [THEN order_antisym, symmetric])
   330 apply (auto simp add: metric_def)
   330 apply (auto simp add: metric_def)
   331 done
   331 done
   332 
   332 
   333 (*lift_4*)
   333 (*lift_4*)
   334 lemma (in Floor) lift_4:
   334 lemma (in Floor) lift_4:
   335      "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int  
   335      "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
   336                             {s. floor s ~: req s}) LeadsTo      
   336                             {s. floor s \<notin> req s}) LeadsTo      
   337                            (moving Int Req n Int {s. metric n s < N})"
   337                            (moving \<inter> Req n \<inter> {s. metric n s < N})"
   338 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   338 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   339                               LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
   339                               LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
   340 done
   340 done
   341 
   341 
   342 
   342 
   343 (** towards lift_5 **)
   343 (** towards lift_5 **)
   344 
   344 
   345 (*lem_lift_5_3*)
   345 (*lem_lift_5_3*)
   346 lemma (in Floor) E_thm16a: "0<N    
   346 lemma (in Floor) E_thm16a: "0<N    
   347   ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo  
   347   ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo  
   348              (moving Int Req n Int {s. metric n s < N})"
   348              (moving \<inter> Req n \<inter> {s. metric n s < N})"
   349 apply (cut_tac bounded)
   349 apply (cut_tac bounded)
   350 apply (unfold Lift_def, ensures_tac "req_up")
   350 apply (unfold Lift_def, ensures_tac "req_up")
   351 apply (auto simp add: metric_def)
   351 apply (auto simp add: metric_def)
   352 done
   352 done
   353 
   353 
   354 
   354 
   355 (*lem_lift_5_1 has ~goingup instead of goingdown*)
   355 (*lem_lift_5_1 has ~goingup instead of goingdown*)
   356 lemma (in Floor) E_thm16b: "0<N ==>    
   356 lemma (in Floor) E_thm16b: "0<N ==>    
   357       Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo  
   357       Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo  
   358                    (moving Int Req n Int {s. metric n s < N})"
   358                    (moving \<inter> Req n \<inter> {s. metric n s < N})"
   359 apply (cut_tac bounded)
   359 apply (cut_tac bounded)
   360 apply (unfold Lift_def, ensures_tac "req_down")
   360 apply (unfold Lift_def, ensures_tac "req_down")
   361 apply (auto simp add: metric_def)
   361 apply (auto simp add: metric_def)
   362 done
   362 done
   363 
   363 
   364 
   364 
   365 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   365 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   366   i.e. the trivial disjunction, leading to an asymmetrical proof.*)
   366   i.e. the trivial disjunction, leading to an asymmetrical proof.*)
   367 lemma (in Floor) E_thm16c:
   367 lemma (in Floor) E_thm16c:
   368      "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"
   368      "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown"
   369 by (force simp add: metric_def)
   369 by (force simp add: metric_def)
   370 
   370 
   371 
   371 
   372 (*lift_5*)
   372 (*lift_5*)
   373 lemma (in Floor) lift_5:
   373 lemma (in Floor) lift_5:
   374      "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo    
   374      "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo    
   375                      (moving Int Req n Int {s. metric n s < N})"
   375                      (moving \<inter> Req n \<inter> {s. metric n s < N})"
   376 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   376 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   377                               LeadsTo_Un [OF E_thm16a E_thm16b]])
   377                               LeadsTo_Un [OF E_thm16a E_thm16b]])
   378 apply (drule E_thm16c, auto)
   378 apply (drule E_thm16c, auto)
   379 done
   379 done
   380 
   380 
   381 
   381 
   382 (** towards lift_3 **)
   382 (** towards lift_3 **)
   383 
   383 
   384 (*lemma used to prove lem_lift_3_1*)
   384 (*lemma used to prove lem_lift_3_1*)
   385 lemma (in Floor) metric_eq_0D [dest]:
   385 lemma (in Floor) metric_eq_0D [dest]:
   386      "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n"
   386      "[| metric n s = 0;  Min \<le> floor s;  floor s \<le> Max |] ==> floor s = n"
   387 by (force simp add: metric_def)
   387 by (force simp add: metric_def)
   388 
   388 
   389 
   389 
   390 (*lem_lift_3_1*)
   390 (*lem_lift_3_1*)
   391 lemma (in Floor) E_thm11: "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo    
   391 lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo    
   392                        (stopped Int atFloor n)"
   392                        (stopped \<inter> atFloor n)"
   393 apply (cut_tac bounded)
   393 apply (cut_tac bounded)
   394 apply (unfold Lift_def, ensures_tac "request_act", auto)
   394 apply (unfold Lift_def, ensures_tac "request_act", auto)
   395 done
   395 done
   396 
   396 
   397 (*lem_lift_3_5*)
   397 (*lem_lift_3_5*)
   398 lemma (in Floor) E_thm13: 
   398 lemma (in Floor) E_thm13: 
   399   "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
   399   "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
   400   LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"
   400   LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})"
   401 apply (unfold Lift_def, ensures_tac "request_act")
   401 apply (unfold Lift_def, ensures_tac "request_act")
   402 apply (auto simp add: metric_def)
   402 apply (auto simp add: metric_def)
   403 done
   403 done
   404 
   404 
   405 (*lem_lift_3_6*)
   405 (*lem_lift_3_6*)
   406 lemma (in Floor) E_thm14: "0 < N ==>  
   406 lemma (in Floor) E_thm14: "0 < N ==>  
   407       Lift :  
   407       Lift \<in>  
   408         (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
   408         (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
   409         LeadsTo (opened Int Req n Int {s. metric n s = N})"
   409         LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})"
   410 apply (unfold Lift_def, ensures_tac "open_act")
   410 apply (unfold Lift_def, ensures_tac "open_act")
   411 apply (auto simp add: metric_def)
   411 apply (auto simp add: metric_def)
   412 done
   412 done
   413 
   413 
   414 (*lem_lift_3_7*)
   414 (*lem_lift_3_7*)
   415 lemma (in Floor) E_thm15: "Lift : (opened Int Req n Int {s. metric n s = N})   
   415 lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})   
   416              LeadsTo (closed Int Req n Int {s. metric n s = N})"
   416              LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})"
   417 apply (unfold Lift_def, ensures_tac "close_act")
   417 apply (unfold Lift_def, ensures_tac "close_act")
   418 apply (auto simp add: metric_def)
   418 apply (auto simp add: metric_def)
   419 done
   419 done
   420 
   420 
   421 
   421 
   422 (** the final steps **)
   422 (** the final steps **)
   423 
   423 
   424 lemma (in Floor) lift_3_Req: "0 < N ==>  
   424 lemma (in Floor) lift_3_Req: "0 < N ==>  
   425       Lift :  
   425       Lift \<in>  
   426         (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})    
   426         (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})    
   427         LeadsTo (moving Int Req n Int {s. metric n s < N})"
   427         LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
   428 apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans)
   428 apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans)
   429 done
   429 done
   430 
   430 
   431 
   431 
   432 (*Now we observe that our integer metric is really a natural number*)
   432 (*Now we observe that our integer metric is really a natural number*)
   433 lemma (in Floor) Always_nonneg: "Lift : Always {s. 0 <= metric n s}"
   433 lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
   434 apply (rule bounded [THEN Always_weaken])
   434 apply (rule bounded [THEN Always_weaken])
   435 apply (auto simp add: metric_def)
   435 apply (auto simp add: metric_def)
   436 done
   436 done
   437 
   437 
   438 lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
   438 lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
   439 
   439 
   440 lemma (in Floor) lift_3:
   440 lemma (in Floor) lift_3:
   441      "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"
   441      "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
   442 apply (rule Always_nonneg [THEN integ_0_le_induct])
   442 apply (rule Always_nonneg [THEN integ_0_le_induct])
   443 apply (case_tac "0 < z")
   443 apply (case_tac "0 < z")
   444 (*If z <= 0 then actually z = 0*)
   444 (*If z \<le> 0 then actually z = 0*)
   445 prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less)
   445 prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less)
   446 apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])
   446 apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])
   447 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   447 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
   448                               LeadsTo_Un [OF lift_4 lift_3_Req]], auto)
   448                               LeadsTo_Un [OF lift_4 lift_3_Req]], auto)
   449 done
   449 done
   450 
   450 
   451 
   451 
   452 lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)"
   452 lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
   453 apply (rule LeadsTo_Trans)
   453 apply (rule LeadsTo_Trans)
   454  prefer 2
   454  prefer 2
   455  apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
   455  apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
   456  apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un])
   456  apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un])
   457  apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un])
   457  apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un])