src/HOL/UNITY/Simple/Lift.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 16184 80617b8d33c5
child 32960 69916a850301
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
paulson@11195
     1
(*  Title:      HOL/UNITY/Lift.thy
paulson@11195
     2
    ID:         $Id$
paulson@11195
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11195
     4
    Copyright   1998  University of Cambridge
paulson@11195
     5
paulson@11195
     6
The Lift-Control Example
paulson@11195
     7
*)
paulson@11195
     8
paulson@16184
     9
theory Lift
paulson@16184
    10
imports "../UNITY_Main"
paulson@16184
    11
paulson@16184
    12
begin
paulson@11195
    13
paulson@11195
    14
record state =
paulson@16184
    15
  floor :: "int"	    --{*current position of the lift*}
paulson@16184
    16
  "open" :: "bool"	    --{*whether the door is opened at floor*}
paulson@16184
    17
  stop  :: "bool"	    --{*whether the lift is stopped at floor*}
paulson@16184
    18
  req   :: "int set"	    --{*for each floor, whether the lift is requested*}
paulson@16184
    19
  up    :: "bool"	    --{*current direction of movement*}
paulson@16184
    20
  move  :: "bool"	    --{*whether moving takes precedence over opening*}
paulson@11195
    21
paulson@11195
    22
consts
paulson@16184
    23
  Min :: "int"       --{*least and greatest floors*}
paulson@16184
    24
  Max :: "int"       --{*least and greatest floors*}
paulson@11195
    25
paulson@13785
    26
axioms
paulson@13806
    27
  Min_le_Max [iff]: "Min \<le> Max"
paulson@11195
    28
  
paulson@11195
    29
constdefs
paulson@11195
    30
  
paulson@16184
    31
  --{*Abbreviations: the "always" part*}
paulson@11195
    32
  
paulson@13785
    33
  above :: "state set"
paulson@13806
    34
    "above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
paulson@11195
    35
paulson@13785
    36
  below :: "state set"
paulson@13806
    37
    "below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
paulson@11195
    38
paulson@13785
    39
  queueing :: "state set"
paulson@13806
    40
    "queueing == above \<union> below"
paulson@11195
    41
paulson@13785
    42
  goingup :: "state set"
paulson@13806
    43
    "goingup   == above \<inter> ({s. up s}  \<union> -below)"
paulson@11195
    44
paulson@13785
    45
  goingdown :: "state set"
paulson@13806
    46
    "goingdown == below \<inter> ({s. ~ up s} \<union> -above)"
paulson@11195
    47
paulson@13785
    48
  ready :: "state set"
paulson@11195
    49
    "ready == {s. stop s & ~ open s & move s}"
paulson@11195
    50
 
paulson@16184
    51
  --{*Further abbreviations*}
paulson@11195
    52
paulson@13785
    53
  moving :: "state set"
paulson@11195
    54
    "moving ==  {s. ~ stop s & ~ open s}"
paulson@11195
    55
paulson@13785
    56
  stopped :: "state set"
paulson@11195
    57
    "stopped == {s. stop s  & ~ open s & ~ move s}"
paulson@11195
    58
paulson@13785
    59
  opened :: "state set"
paulson@11195
    60
    "opened ==  {s. stop s  &  open s  &  move s}"
paulson@11195
    61
paulson@16184
    62
  closed :: "state set"  --{*but this is the same as ready!!*}
paulson@11195
    63
    "closed ==  {s. stop s  & ~ open s &  move s}"
paulson@11195
    64
paulson@13785
    65
  atFloor :: "int => state set"
paulson@11195
    66
    "atFloor n ==  {s. floor s = n}"
paulson@11195
    67
paulson@13785
    68
  Req :: "int => state set"
paulson@13806
    69
    "Req n ==  {s. n \<in> req s}"
paulson@11195
    70
paulson@11195
    71
paulson@11195
    72
  
paulson@16184
    73
  --{*The program*}
paulson@11195
    74
  
paulson@11195
    75
  request_act :: "(state*state) set"
paulson@11195
    76
    "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
paulson@13806
    77
		                  & ~ stop s & floor s \<in> req s}"
paulson@11195
    78
paulson@11195
    79
  open_act :: "(state*state) set"
paulson@11195
    80
    "open_act ==
paulson@11195
    81
         {(s,s'). s' = s (|open :=True,
paulson@11195
    82
			   req  := req s - {floor s},
paulson@11195
    83
			   move := True|)
paulson@13806
    84
		       & stop s & ~ open s & floor s \<in> req s
paulson@13806
    85
	               & ~(move s & s \<in> queueing)}"
paulson@11195
    86
paulson@11195
    87
  close_act :: "(state*state) set"
paulson@11195
    88
    "close_act == {(s,s'). s' = s (|open := False|) & open s}"
paulson@11195
    89
paulson@11195
    90
  req_up :: "(state*state) set"
paulson@11195
    91
    "req_up ==
paulson@11195
    92
         {(s,s'). s' = s (|stop  :=False,
paulson@11868
    93
			   floor := floor s + 1,
paulson@11195
    94
			   up    := True|)
paulson@13806
    95
		       & s \<in> (ready \<inter> goingup)}"
paulson@11195
    96
paulson@11195
    97
  req_down :: "(state*state) set"
paulson@11195
    98
    "req_down ==
paulson@11195
    99
         {(s,s'). s' = s (|stop  :=False,
paulson@11868
   100
			   floor := floor s - 1,
paulson@11195
   101
			   up    := False|)
paulson@13806
   102
		       & s \<in> (ready \<inter> goingdown)}"
paulson@11195
   103
paulson@11195
   104
  move_up :: "(state*state) set"
paulson@11195
   105
    "move_up ==
paulson@11868
   106
         {(s,s'). s' = s (|floor := floor s + 1|)
paulson@13806
   107
		       & ~ stop s & up s & floor s \<notin> req s}"
paulson@11195
   108
paulson@11195
   109
  move_down :: "(state*state) set"
paulson@11195
   110
    "move_down ==
paulson@11868
   111
         {(s,s'). s' = s (|floor := floor s - 1|)
paulson@13806
   112
		       & ~ stop s & ~ up s & floor s \<notin> req s}"
paulson@11195
   113
paulson@11195
   114
  button_press  :: "(state*state) set"
paulson@16184
   115
      --{*This action is omitted from prior treatments, which therefore are
paulson@16184
   116
	unrealistic: nobody asks the lift to do anything!  But adding this
paulson@16184
   117
	action invalidates many of the existing progress arguments: various
paulson@16184
   118
	"ensures" properties fail. Maybe it should be constrained to only
paulson@16184
   119
        allow button presses in the current direction of travel, like in a
paulson@16184
   120
        real lift.*}
paulson@11195
   121
    "button_press ==
paulson@13806
   122
         {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
paulson@13806
   123
		        & Min \<le> n & n \<le> Max}"
paulson@11195
   124
paulson@11195
   125
paulson@13785
   126
  Lift :: "state program"
paulson@16184
   127
    --{*for the moment, we OMIT @{text button_press}*}
paulson@13812
   128
    "Lift == mk_total_program
paulson@13812
   129
                ({s. floor s = Min & ~ up s & move s & stop s &
paulson@11195
   130
		          ~ open s & req s = {}},
paulson@13812
   131
		 {request_act, open_act, close_act,
paulson@13812
   132
 		  req_up, req_down, move_up, move_down},
paulson@13812
   133
		 UNIV)"
paulson@11195
   134
paulson@11195
   135
paulson@16184
   136
  --{*Invariants*}
paulson@11195
   137
paulson@13785
   138
  bounded :: "state set"
paulson@13806
   139
    "bounded == {s. Min \<le> floor s & floor s \<le> Max}"
paulson@11195
   140
paulson@13785
   141
  open_stop :: "state set"
paulson@11195
   142
    "open_stop == {s. open s --> stop s}"
paulson@11195
   143
  
paulson@13785
   144
  open_move :: "state set"
paulson@11195
   145
    "open_move == {s. open s --> move s}"
paulson@11195
   146
  
paulson@13785
   147
  stop_floor :: "state set"
paulson@13806
   148
    "stop_floor == {s. stop s & ~ move s --> floor s \<in> req s}"
paulson@11195
   149
  
paulson@13785
   150
  moving_up :: "state set"
paulson@11195
   151
    "moving_up == {s. ~ stop s & up s -->
paulson@13806
   152
                   (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
paulson@11195
   153
  
paulson@13785
   154
  moving_down :: "state set"
paulson@11195
   155
    "moving_down == {s. ~ stop s & ~ up s -->
paulson@13806
   156
                     (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}"
paulson@11195
   157
  
paulson@13785
   158
  metric :: "[int,state] => int"
paulson@11195
   159
    "metric ==
paulson@11195
   160
       %n s. if floor s < n then (if up s then n - floor s
paulson@11195
   161
			          else (floor s - Min) + (n-Min))
paulson@11195
   162
             else
paulson@11195
   163
             if n < floor s then (if up s then (Max - floor s) + (Max-n)
paulson@11195
   164
		                  else floor s - n)
paulson@11868
   165
             else 0"
paulson@11195
   166
paulson@13785
   167
locale Floor =
paulson@13785
   168
  fixes n
paulson@13806
   169
  assumes Min_le_n [iff]: "Min \<le> n"
paulson@13806
   170
      and n_le_Max [iff]: "n \<le> Max"
paulson@13785
   171
paulson@13806
   172
lemma not_mem_distinct: "[| x \<notin> A;  y \<in> A |] ==> x \<noteq> y"
paulson@13785
   173
by blast
paulson@13785
   174
paulson@13785
   175
paulson@13785
   176
declare Lift_def [THEN def_prg_Init, simp]
paulson@13785
   177
paulson@13785
   178
declare request_act_def [THEN def_act_simp, simp]
paulson@13785
   179
declare open_act_def [THEN def_act_simp, simp]
paulson@13785
   180
declare close_act_def [THEN def_act_simp, simp]
paulson@13785
   181
declare req_up_def [THEN def_act_simp, simp]
paulson@13785
   182
declare req_down_def [THEN def_act_simp, simp]
paulson@13785
   183
declare move_up_def [THEN def_act_simp, simp]
paulson@13785
   184
declare move_down_def [THEN def_act_simp, simp]
paulson@13785
   185
declare button_press_def [THEN def_act_simp, simp]
paulson@13785
   186
paulson@13785
   187
(*The ALWAYS properties*)
paulson@13785
   188
declare above_def [THEN def_set_simp, simp]
paulson@13785
   189
declare below_def [THEN def_set_simp, simp]
paulson@13785
   190
declare queueing_def [THEN def_set_simp, simp]
paulson@13785
   191
declare goingup_def [THEN def_set_simp, simp]
paulson@13785
   192
declare goingdown_def [THEN def_set_simp, simp]
paulson@13785
   193
declare ready_def [THEN def_set_simp, simp]
paulson@13785
   194
paulson@13785
   195
(*Basic definitions*)
paulson@13785
   196
declare bounded_def [simp] 
paulson@13785
   197
        open_stop_def [simp] 
paulson@13785
   198
        open_move_def [simp] 
paulson@13785
   199
        stop_floor_def [simp]
paulson@13785
   200
        moving_up_def [simp]
paulson@13785
   201
        moving_down_def [simp]
paulson@13785
   202
paulson@13806
   203
lemma open_stop: "Lift \<in> Always open_stop"
paulson@13785
   204
apply (rule AlwaysI, force) 
paulson@16184
   205
apply (unfold Lift_def, safety)
paulson@13785
   206
done
paulson@13785
   207
paulson@13806
   208
lemma stop_floor: "Lift \<in> Always stop_floor"
paulson@13785
   209
apply (rule AlwaysI, force) 
paulson@16184
   210
apply (unfold Lift_def, safety)
paulson@13785
   211
done
paulson@13785
   212
paulson@13785
   213
(*This one needs open_stop, which was proved above*)
paulson@13806
   214
lemma open_move: "Lift \<in> Always open_move"
paulson@13785
   215
apply (cut_tac open_stop)
paulson@13785
   216
apply (rule AlwaysI, force) 
paulson@16184
   217
apply (unfold Lift_def, safety)
paulson@13785
   218
done
paulson@13785
   219
paulson@13806
   220
lemma moving_up: "Lift \<in> Always moving_up"
paulson@13785
   221
apply (rule AlwaysI, force) 
paulson@16184
   222
apply (unfold Lift_def, safety)
paulson@14378
   223
apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq)
paulson@13785
   224
done
paulson@13785
   225
paulson@13806
   226
lemma moving_down: "Lift \<in> Always moving_down"
paulson@13785
   227
apply (rule AlwaysI, force) 
paulson@16184
   228
apply (unfold Lift_def, safety)
paulson@14378
   229
apply (blast dest: order_le_imp_less_or_eq)
paulson@13785
   230
done
paulson@13785
   231
paulson@13806
   232
lemma bounded: "Lift \<in> Always bounded"
paulson@13785
   233
apply (cut_tac moving_up moving_down)
paulson@13785
   234
apply (rule AlwaysI, force) 
paulson@16184
   235
apply (unfold Lift_def, safety, auto)
paulson@13785
   236
apply (drule not_mem_distinct, assumption, arith)+
paulson@13785
   237
done
paulson@13785
   238
paulson@13785
   239
paulson@13785
   240
subsection{*Progress*}
paulson@13785
   241
paulson@13785
   242
declare moving_def [THEN def_set_simp, simp]
paulson@13785
   243
declare stopped_def [THEN def_set_simp, simp]
paulson@13785
   244
declare opened_def [THEN def_set_simp, simp]
paulson@13785
   245
declare closed_def [THEN def_set_simp, simp]
paulson@13785
   246
declare atFloor_def [THEN def_set_simp, simp]
paulson@13785
   247
declare Req_def [THEN def_set_simp, simp]
paulson@13785
   248
paulson@13785
   249
paulson@16184
   250
text{*The HUG'93 paper mistakenly omits the Req n from these!*}
paulson@13785
   251
paulson@13785
   252
(** Lift_1 **)
paulson@13806
   253
lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
paulson@13785
   254
apply (cut_tac stop_floor)
paulson@13785
   255
apply (unfold Lift_def, ensures_tac "open_act")
paulson@13785
   256
done  (*lem_lift_1_5*)
paulson@13785
   257
paulson@13812
   258
paulson@13812
   259
paulson@13812
   260
paulson@13806
   261
lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
paulson@13812
   262
                       (Req n \<inter> opened - atFloor n)"
paulson@13785
   263
apply (cut_tac stop_floor)
paulson@13785
   264
apply (unfold Lift_def, ensures_tac "open_act")
paulson@13785
   265
done  (*lem_lift_1_1*)
paulson@13785
   266
paulson@13806
   267
lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
paulson@13812
   268
                       (Req n \<inter> closed - (atFloor n - queueing))"
paulson@13785
   269
apply (unfold Lift_def, ensures_tac "close_act")
paulson@13785
   270
done  (*lem_lift_1_2*)
paulson@13785
   271
paulson@13806
   272
lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
paulson@13812
   273
                       LeadsTo (opened \<inter> atFloor n)"
paulson@13785
   274
apply (unfold Lift_def, ensures_tac "open_act")
paulson@13785
   275
done  (*lem_lift_1_7*)
paulson@13785
   276
paulson@13785
   277
paulson@13785
   278
(** Lift 2.  Statements of thm05a and thm05b were wrong! **)
paulson@13785
   279
paulson@13785
   280
lemmas linorder_leI = linorder_not_less [THEN iffD1]
paulson@13785
   281
paulson@13785
   282
lemmas (in Floor) le_MinD = Min_le_n [THEN order_antisym]
paulson@13785
   283
              and Max_leD = n_le_Max [THEN [2] order_antisym]
paulson@13785
   284
paulson@13785
   285
declare (in Floor) le_MinD [dest!]
paulson@13785
   286
               and linorder_leI [THEN le_MinD, dest!]
paulson@13785
   287
               and Max_leD [dest!]
paulson@13785
   288
               and linorder_leI [THEN Max_leD, dest!]
paulson@13785
   289
paulson@13785
   290
paulson@13785
   291
(*lem_lift_2_0 
paulson@13785
   292
  NOT an ensures_tac property, but a mere inclusion
paulson@13785
   293
  don't know why script lift_2.uni says ENSURES*)
paulson@13785
   294
lemma (in Floor) E_thm05c: 
paulson@13806
   295
    "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
paulson@13806
   296
             LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
paulson@13806
   297
                      (closed \<inter> goingdown \<inter> Req n))"
paulson@14378
   298
by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff)
paulson@13785
   299
paulson@13785
   300
(*lift_2*)
paulson@13806
   301
lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
paulson@13806
   302
             LeadsTo (moving \<inter> Req n)"
paulson@13785
   303
apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
paulson@13785
   304
apply (unfold Lift_def) 
paulson@13785
   305
apply (ensures_tac [2] "req_down")
paulson@13785
   306
apply (ensures_tac "req_up", auto)
paulson@13785
   307
done
paulson@13785
   308
paulson@13785
   309
paulson@13785
   310
(** Towards lift_4 ***)
paulson@13785
   311
 
paulson@13785
   312
declare split_if_asm [split]
paulson@13785
   313
paulson@13785
   314
paulson@13785
   315
(*lem_lift_4_1 *)
paulson@13785
   316
lemma (in Floor) E_thm12a:
paulson@13785
   317
     "0 < N ==>  
paulson@13806
   318
      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
paulson@13806
   319
              {s. floor s \<notin> req s} \<inter> {s. up s})    
paulson@13785
   320
             LeadsTo  
paulson@13806
   321
               (moving \<inter> Req n \<inter> {s. metric n s < N})"
paulson@13785
   322
apply (cut_tac moving_up)
paulson@13785
   323
apply (unfold Lift_def, ensures_tac "move_up", safe)
paulson@13806
   324
(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
paulson@13785
   325
apply (erule linorder_leI [THEN order_antisym, symmetric])
paulson@13785
   326
apply (auto simp add: metric_def)
paulson@13785
   327
done
paulson@13785
   328
paulson@13785
   329
paulson@13785
   330
(*lem_lift_4_3 *)
paulson@13785
   331
lemma (in Floor) E_thm12b: "0 < N ==>  
paulson@13806
   332
      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
paulson@13806
   333
              {s. floor s \<notin> req s} - {s. up s})    
paulson@13806
   334
             LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
paulson@13785
   335
apply (cut_tac moving_down)
paulson@13785
   336
apply (unfold Lift_def, ensures_tac "move_down", safe)
paulson@13806
   337
(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
paulson@13785
   338
apply (erule linorder_leI [THEN order_antisym, symmetric])
paulson@13785
   339
apply (auto simp add: metric_def)
paulson@13785
   340
done
paulson@13785
   341
paulson@13785
   342
(*lift_4*)
paulson@13785
   343
lemma (in Floor) lift_4:
paulson@13806
   344
     "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
paulson@13806
   345
                            {s. floor s \<notin> req s}) LeadsTo      
paulson@13806
   346
                           (moving \<inter> Req n \<inter> {s. metric n s < N})"
paulson@13785
   347
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
paulson@13785
   348
                              LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
paulson@13785
   349
done
paulson@13785
   350
paulson@13785
   351
paulson@13785
   352
(** towards lift_5 **)
paulson@13785
   353
paulson@13785
   354
(*lem_lift_5_3*)
paulson@13785
   355
lemma (in Floor) E_thm16a: "0<N    
paulson@13806
   356
  ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo  
paulson@13806
   357
             (moving \<inter> Req n \<inter> {s. metric n s < N})"
paulson@13785
   358
apply (cut_tac bounded)
paulson@13785
   359
apply (unfold Lift_def, ensures_tac "req_up")
paulson@13785
   360
apply (auto simp add: metric_def)
paulson@13785
   361
done
paulson@13785
   362
paulson@13785
   363
paulson@13785
   364
(*lem_lift_5_1 has ~goingup instead of goingdown*)
paulson@13785
   365
lemma (in Floor) E_thm16b: "0<N ==>    
paulson@13806
   366
      Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo  
paulson@13806
   367
                   (moving \<inter> Req n \<inter> {s. metric n s < N})"
paulson@13785
   368
apply (cut_tac bounded)
paulson@13785
   369
apply (unfold Lift_def, ensures_tac "req_down")
paulson@13785
   370
apply (auto simp add: metric_def)
paulson@13785
   371
done
paulson@13785
   372
paulson@13785
   373
paulson@13785
   374
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
paulson@13785
   375
  i.e. the trivial disjunction, leading to an asymmetrical proof.*)
paulson@13785
   376
lemma (in Floor) E_thm16c:
paulson@13806
   377
     "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown"
paulson@13785
   378
by (force simp add: metric_def)
paulson@13785
   379
paulson@13785
   380
paulson@13785
   381
(*lift_5*)
paulson@13785
   382
lemma (in Floor) lift_5:
paulson@13806
   383
     "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo    
paulson@13806
   384
                     (moving \<inter> Req n \<inter> {s. metric n s < N})"
paulson@13785
   385
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
paulson@13785
   386
                              LeadsTo_Un [OF E_thm16a E_thm16b]])
paulson@13785
   387
apply (drule E_thm16c, auto)
paulson@13785
   388
done
paulson@13785
   389
paulson@13785
   390
paulson@13785
   391
(** towards lift_3 **)
paulson@13785
   392
paulson@13785
   393
(*lemma used to prove lem_lift_3_1*)
paulson@13785
   394
lemma (in Floor) metric_eq_0D [dest]:
paulson@13806
   395
     "[| metric n s = 0;  Min \<le> floor s;  floor s \<le> Max |] ==> floor s = n"
paulson@13785
   396
by (force simp add: metric_def)
paulson@13785
   397
paulson@13785
   398
paulson@13785
   399
(*lem_lift_3_1*)
paulson@13806
   400
lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo    
paulson@13806
   401
                       (stopped \<inter> atFloor n)"
paulson@13785
   402
apply (cut_tac bounded)
paulson@13785
   403
apply (unfold Lift_def, ensures_tac "request_act", auto)
paulson@13785
   404
done
paulson@13785
   405
paulson@13785
   406
(*lem_lift_3_5*)
paulson@13785
   407
lemma (in Floor) E_thm13: 
paulson@13806
   408
  "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
paulson@13806
   409
  LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})"
paulson@13785
   410
apply (unfold Lift_def, ensures_tac "request_act")
paulson@13785
   411
apply (auto simp add: metric_def)
paulson@13785
   412
done
paulson@13785
   413
paulson@13785
   414
(*lem_lift_3_6*)
paulson@13785
   415
lemma (in Floor) E_thm14: "0 < N ==>  
paulson@13806
   416
      Lift \<in>  
paulson@13806
   417
        (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
paulson@13806
   418
        LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})"
paulson@13785
   419
apply (unfold Lift_def, ensures_tac "open_act")
paulson@13785
   420
apply (auto simp add: metric_def)
paulson@13785
   421
done
paulson@13785
   422
paulson@13785
   423
(*lem_lift_3_7*)
paulson@13806
   424
lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})   
paulson@13806
   425
             LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})"
paulson@13785
   426
apply (unfold Lift_def, ensures_tac "close_act")
paulson@13785
   427
apply (auto simp add: metric_def)
paulson@13785
   428
done
paulson@13785
   429
paulson@13785
   430
paulson@13785
   431
(** the final steps **)
paulson@13785
   432
paulson@13785
   433
lemma (in Floor) lift_3_Req: "0 < N ==>  
paulson@13806
   434
      Lift \<in>  
paulson@13806
   435
        (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})    
paulson@13806
   436
        LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
paulson@13785
   437
apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans)
paulson@13785
   438
done
paulson@13785
   439
paulson@13785
   440
paulson@13785
   441
(*Now we observe that our integer metric is really a natural number*)
paulson@13806
   442
lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
paulson@13785
   443
apply (rule bounded [THEN Always_weaken])
paulson@13785
   444
apply (auto simp add: metric_def)
paulson@13785
   445
done
paulson@13785
   446
paulson@13785
   447
lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
paulson@13785
   448
paulson@13785
   449
lemma (in Floor) lift_3:
paulson@13806
   450
     "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
paulson@13785
   451
apply (rule Always_nonneg [THEN integ_0_le_induct])
paulson@13785
   452
apply (case_tac "0 < z")
paulson@13806
   453
(*If z \<le> 0 then actually z = 0*)
paulson@13785
   454
prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less)
paulson@13785
   455
apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])
paulson@13785
   456
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
paulson@13785
   457
                              LeadsTo_Un [OF lift_4 lift_3_Req]], auto)
paulson@13785
   458
done
paulson@13785
   459
paulson@13785
   460
paulson@13806
   461
lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
paulson@13785
   462
apply (rule LeadsTo_Trans)
paulson@13785
   463
 prefer 2
paulson@13785
   464
 apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
paulson@13785
   465
 apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un])
paulson@13785
   466
 apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un])
paulson@13785
   467
 apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un])
paulson@13785
   468
 apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03])
paulson@13785
   469
apply (rule open_move [THEN Always_LeadsToI])
paulson@13785
   470
apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify)
paulson@13785
   471
(*The case split is not essential but makes the proof much faster.*)
paulson@13785
   472
apply (case_tac "open x", auto)
paulson@13785
   473
done
paulson@13785
   474
paulson@11195
   475
paulson@11195
   476
end