src/HOL/UNITY/Simple/Lift.thy
 changeset 13806 fd40c9d9076b parent 13785 e2fcd88be55d child 13812 91713a1915ee
equal 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  "req_down")`
`   296 apply (ensures_tac  "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  LeadsTo_Trans_Un])`
`   456  apply (rule E_thm01 [THEN  LeadsTo_Trans_Un])`
`   457  apply (rule lift_3 [THEN  LeadsTo_Trans_Un])`
`   457  apply (rule lift_3 [THEN  LeadsTo_Trans_Un])`