src/HOL/UNITY/Lift.ML
author paulson
Fri Dec 11 10:41:53 1998 +0100 (1998-12-11)
changeset 6024 cb87f103d114
parent 5783 95ac0bf10518
child 6061 e80bcb98df78
permissions -rw-r--r--
new Close_locale synatx
paulson@5277
     1
(*  Title:      HOL/UNITY/Lift
paulson@5277
     2
    ID:         $Id$
paulson@5277
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5277
     4
    Copyright   1998  University of Cambridge
paulson@5277
     5
paulson@5277
     6
The Lift-Control Example
paulson@5277
     7
*)
paulson@5277
     8
paulson@5563
     9
Goal "~ z < w ==> (z < w + #1) = (z = w)";
paulson@5563
    10
by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1);
paulson@5563
    11
qed "not_zless_zless1_eq";
paulson@5563
    12
paulson@5563
    13
paulson@5426
    14
(*split_all_tac causes a big blow-up*)
wenzelm@5706
    15
claset_ref() := claset() delSWrapper record_split_name;
paulson@5426
    16
paulson@5563
    17
Delsimps [split_paired_All];
paulson@5563
    18
paulson@5563
    19
Goal "[| x ~: A;  y : A |] ==> x ~= y";
paulson@5563
    20
by (Blast_tac 1);
paulson@5563
    21
qed "not_mem_distinct";
paulson@5563
    22
paulson@5563
    23
fun distinct_tac i =
paulson@5563
    24
    dtac zle_neq_implies_zless i THEN
paulson@5563
    25
    eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
paulson@5563
    26
    assume_tac i;
paulson@5563
    27
paulson@5426
    28
paulson@5426
    29
(** Rules to move "metric n s" out of the assumptions, for case splitting **)
paulson@5426
    30
val mov_metric1 = read_instantiate_sg (sign_of thy) 
paulson@5596
    31
                   [("P", "?x < metric ?n ?s")] rev_mp;
paulson@5426
    32
paulson@5426
    33
val mov_metric2 = read_instantiate_sg (sign_of thy) 
paulson@5596
    34
                   [("P", "?x = metric ?n ?s")] rev_mp;
paulson@5426
    35
paulson@5426
    36
val mov_metric3 = read_instantiate_sg (sign_of thy) 
paulson@5596
    37
                   [("P", "~ (?x < metric ?n ?s)")] rev_mp;
paulson@5426
    38
paulson@5563
    39
val mov_metric4 = read_instantiate_sg (sign_of thy) 
paulson@5596
    40
                   [("P", "(?x <= metric ?n ?s)")] rev_mp;
paulson@5563
    41
paulson@5426
    42
(*The order in which they are applied seems to be critical...*)
paulson@5563
    43
val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
paulson@5426
    44
paulson@5357
    45
paulson@5563
    46
val zless_zadd1_contra = zless_zadd1_imp_zless COMP rev_contrapos;
paulson@5563
    47
val zless_zadd1_contra' = zless_not_sym RS zless_zadd1_contra;
paulson@5563
    48
paulson@5563
    49
paulson@5563
    50
val metric_simps =
paulson@5563
    51
    [metric_def, vimage_def, order_less_imp_not_less, order_less_imp_triv, 
paulson@5563
    52
     order_less_imp_not_eq, order_less_imp_not_eq2,
paulson@5563
    53
     not_zless_zless1_eq, zless_not_sym RS not_zless_zless1_eq,
paulson@5563
    54
     zless_zadd1_contra, zless_zadd1_contra',
paulson@5563
    55
     zless_not_refl2, zless_not_refl3];
paulson@5563
    56
paulson@5340
    57
paulson@5648
    58
Addsimps [Lprg_def RS def_prg_Init];
paulson@5648
    59
program_defs_ref := [Lprg_def];
paulson@5426
    60
paulson@5426
    61
Addsimps (map simp_of_act
paulson@5426
    62
	  [request_act_def, open_act_def, close_act_def,
paulson@5426
    63
	   req_up_def, req_down_def, move_up_def, move_down_def,
paulson@5426
    64
	   button_press_def]);
paulson@5426
    65
paulson@5277
    66
val always_defs = [above_def, below_def, queueing_def, 
paulson@5277
    67
		   goingup_def, goingdown_def, ready_def];
paulson@5277
    68
paulson@5426
    69
Addsimps (map simp_of_set always_defs);
paulson@5277
    70
paulson@5277
    71
paulson@5583
    72
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
paulson@5648
    73
(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *)
paulson@5357
    74
paulson@5357
    75
paulson@5277
    76
(*Simplification for records*)
paulson@5277
    77
Addsimps (thms"state.update_defs");
paulson@5277
    78
paulson@5277
    79
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
paulson@5277
    80
	  moving_up_def, moving_down_def];
paulson@5277
    81
paulson@5357
    82
AddIffs [Min_le_Max];
paulson@5277
    83
paulson@5320
    84
paulson@5320
    85
val nat_exhaust_le_pred = 
paulson@5320
    86
    read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
paulson@5320
    87
paulson@5320
    88
val nat_exhaust_pred_le = 
paulson@5320
    89
    read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
paulson@5320
    90
paulson@5648
    91
Goal "Lprg : Invariant open_stop";
paulson@5313
    92
by (rtac InvariantI 1);
paulson@5277
    93
by (Force_tac 1);
paulson@5426
    94
by (constrains_tac 1);
paulson@5277
    95
qed "open_stop";
paulson@5277
    96
paulson@5648
    97
Goal "Lprg : Invariant stop_floor";
paulson@5313
    98
by (rtac InvariantI 1);
paulson@5277
    99
by (Force_tac 1);
paulson@5426
   100
by (constrains_tac 1);
paulson@5277
   101
qed "stop_floor";
paulson@5277
   102
paulson@5313
   103
(*This one needs open_stop, which was proved above*)
paulson@5648
   104
Goal "Lprg : Invariant open_move";
paulson@5313
   105
by (rtac InvariantI 1);
paulson@5426
   106
by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
paulson@5277
   107
by (Force_tac 1);
paulson@5426
   108
by (constrains_tac 1);
paulson@5277
   109
qed "open_move";
paulson@5277
   110
paulson@5648
   111
Goal "Lprg : Invariant moving_up";
paulson@5313
   112
by (rtac InvariantI 1);
paulson@5277
   113
by (Force_tac 1);
paulson@5426
   114
by (constrains_tac 1);
paulson@5563
   115
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
paulson@5277
   116
qed "moving_up";
paulson@5277
   117
paulson@5648
   118
Goal "Lprg : Invariant moving_down";
paulson@5313
   119
by (rtac InvariantI 1);
paulson@5277
   120
by (Force_tac 1);
paulson@5426
   121
by (constrains_tac 1);
paulson@5563
   122
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
paulson@5277
   123
qed "moving_down";
paulson@5277
   124
paulson@5648
   125
Goal "Lprg : Invariant bounded";
paulson@5313
   126
by (rtac InvariantI 1);
paulson@5426
   127
by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
paulson@5277
   128
by (Force_tac 1);
paulson@5426
   129
by (constrains_tac 1);
paulson@5563
   130
by (ALLGOALS Clarify_tac);
paulson@5563
   131
by (REPEAT_FIRST distinct_tac);
paulson@5563
   132
by (ALLGOALS 
paulson@5563
   133
    (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]@zcompare_rls)));
paulson@5563
   134
by (ALLGOALS 
paulson@5563
   135
    (blast_tac (claset() addDs [zle_imp_zless_or_eq] 
paulson@5563
   136
                         addIs [zless_trans])));
paulson@5277
   137
qed "bounded";
paulson@5277
   138
paulson@5320
   139
paulson@5277
   140
paulson@5320
   141
(*** Progress ***)
paulson@5277
   142
paulson@5277
   143
paulson@5320
   144
val abbrev_defs = [moving_def, stopped_def, 
paulson@5340
   145
		   opened_def, closed_def, atFloor_def, Req_def];
paulson@5277
   146
paulson@5426
   147
Addsimps (map simp_of_set abbrev_defs);
paulson@5277
   148
paulson@5340
   149
paulson@5340
   150
(** The HUG'93 paper mistakenly omits the Req n from these! **)
paulson@5277
   151
paulson@5357
   152
(** Lift_1 **)
paulson@5357
   153
paulson@5648
   154
Goal "Lprg : LeadsTo (stopped Int atFloor n) (opened Int atFloor n)";
paulson@5340
   155
by (cut_facts_tac [stop_floor] 1);
paulson@5426
   156
by (ensures_tac "open_act" 1);
paulson@5426
   157
qed "E_thm01";  (*lem_lift_1_5*)
paulson@5340
   158
paulson@5648
   159
Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \
paulson@5340
   160
\                  (Req n Int opened - atFloor n)";
paulson@5340
   161
by (cut_facts_tac [stop_floor] 1);
paulson@5426
   162
by (ensures_tac "open_act" 1);
paulson@5426
   163
qed "E_thm02";  (*lem_lift_1_1*)
paulson@5340
   164
paulson@5648
   165
Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \
paulson@5340
   166
\                  (Req n Int closed - (atFloor n - queueing))";
paulson@5426
   167
by (ensures_tac "close_act" 1);
paulson@5426
   168
qed "E_thm03";  (*lem_lift_1_2*)
paulson@5340
   169
paulson@5648
   170
Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \
paulson@5340
   171
\                  (opened Int atFloor n)";
paulson@5426
   172
by (ensures_tac "open_act" 1);
paulson@5426
   173
qed "E_thm04";  (*lem_lift_1_7*)
paulson@5340
   174
paulson@5340
   175
paulson@5357
   176
(** Lift 2.  Statements of thm05a and thm05b were wrong! **)
paulson@5340
   177
paulson@5340
   178
Open_locale "floor"; 
paulson@5340
   179
paulson@5357
   180
val Min_le_n = thm "Min_le_n";
paulson@5357
   181
val n_le_Max = thm "n_le_Max";
paulson@5357
   182
paulson@5357
   183
AddIffs [Min_le_n, n_le_Max];
paulson@5340
   184
paulson@5563
   185
val le_MinD = Min_le_n RS zle_anti_sym;
paulson@5563
   186
val Max_leD = n_le_Max RSN (2,zle_anti_sym);
paulson@5357
   187
paulson@5563
   188
AddSDs [le_MinD, zleI RS le_MinD,
paulson@5563
   189
	Max_leD, zleI RS Max_leD];
paulson@5357
   190
paulson@5357
   191
(*lem_lift_2_0 
paulson@5357
   192
  NOT an ensures property, but a mere inclusion;
paulson@5357
   193
  don't know why script lift_2.uni says ENSURES*)
paulson@5648
   194
Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
paulson@5340
   195
\                  ((closed Int goingup Int Req n)  Un \
paulson@5340
   196
\                   (closed Int goingdown Int Req n))";
paulson@5426
   197
by (rtac subset_imp_LeadsTo 1);
paulson@5563
   198
by (auto_tac (claset() addSEs [int_neqE], simpset()));
paulson@5340
   199
qed "E_thm05c";
paulson@5340
   200
paulson@5357
   201
(*lift_2*)
paulson@5648
   202
Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
paulson@5340
   203
\                  (moving Int Req n)";
paulson@5426
   204
by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
paulson@5426
   205
by (ensures_tac "req_down" 2);
paulson@5426
   206
by (ensures_tac "req_up" 1);
paulson@5424
   207
by Auto_tac;
paulson@5340
   208
qed "lift_2";
paulson@5340
   209
paulson@5340
   210
paulson@5357
   211
(** Towards lift_4 ***)
paulson@5563
   212
 
paulson@5357
   213
paulson@5357
   214
(*lem_lift_4_1 *)
paulson@5563
   215
Goal "#0 < N ==> \
paulson@5648
   216
\     Lprg : LeadsTo \
paulson@5563
   217
\       (moving Int Req n Int {s. metric n s = N} Int \
paulson@5426
   218
\         {s. floor s ~: req s} Int {s. up s})   \
paulson@5563
   219
\       (moving Int Req n Int {s. metric n s < N})";
paulson@5357
   220
by (cut_facts_tac [moving_up] 1);
paulson@5426
   221
by (ensures_tac "move_up" 1);
paulson@5426
   222
by Safe_tac;
paulson@5357
   223
(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
paulson@5563
   224
by (etac (zleI RS zle_anti_sym RS sym) 1);
paulson@5426
   225
by (REPEAT_FIRST (eresolve_tac mov_metrics));
paulson@5426
   226
by (REPEAT_FIRST distinct_tac);
paulson@5563
   227
(** LEVEL 6 **)
paulson@5583
   228
by (ALLGOALS (asm_simp_tac (simpset() addsimps 
paulson@5583
   229
			    [zle_def] @ metric_simps @ zcompare_rls)));
paulson@5357
   230
qed "E_thm12a";
paulson@5357
   231
paulson@5357
   232
paulson@5357
   233
paulson@5357
   234
(*lem_lift_4_3 *)
paulson@5563
   235
Goal "#0 < N ==> \
paulson@5648
   236
\     Lprg : LeadsTo \
paulson@5563
   237
\       (moving Int Req n Int {s. metric n s = N} Int \
paulson@5357
   238
\        {s. floor s ~: req s} - {s. up s})   \
paulson@5563
   239
\       (moving Int Req n Int {s. metric n s < N})";
paulson@5357
   240
by (cut_facts_tac [moving_down] 1);
paulson@5426
   241
by (ensures_tac "move_down" 1);
paulson@5426
   242
by Safe_tac;
paulson@5357
   243
(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
paulson@5563
   244
by (etac (zleI RS zle_anti_sym RS sym) 1);
paulson@5426
   245
by (REPEAT_FIRST (eresolve_tac mov_metrics));
paulson@5563
   246
by (REPEAT_FIRST distinct_tac);
paulson@5563
   247
(** LEVEL 6 **)
paulson@5583
   248
by (ALLGOALS (asm_simp_tac (simpset() addsimps 
paulson@5583
   249
			    [zle_def] @ metric_simps @ zcompare_rls)));
paulson@5783
   250
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
paulson@5357
   251
qed "E_thm12b";
paulson@5357
   252
paulson@5357
   253
(*lift_4*)
paulson@5648
   254
Goal "#0<N ==> Lprg : LeadsTo (moving Int Req n Int {s. metric n s = N} Int \
paulson@5357
   255
\                           {s. floor s ~: req s})     \
paulson@5563
   256
\                          (moving Int Req n Int {s. metric n s < N})";
paulson@5426
   257
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
paulson@5583
   258
by (etac E_thm12b 3);
paulson@5583
   259
by (etac E_thm12a 2);
paulson@5357
   260
by (Blast_tac 1);
paulson@5357
   261
qed "lift_4";
paulson@5357
   262
paulson@5357
   263
paulson@5357
   264
(** towards lift_5 **)
paulson@5357
   265
paulson@5357
   266
(*lem_lift_5_3*)
paulson@5563
   267
Goal "#0<N   \
paulson@5648
   268
\     ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \
paulson@5563
   269
\                      (moving Int Req n Int {s. metric n s < N})";
paulson@5357
   270
by (cut_facts_tac [bounded] 1);
paulson@5426
   271
by (ensures_tac "req_up" 1);
paulson@5424
   272
by Auto_tac;
paulson@5426
   273
by (REPEAT_FIRST (eresolve_tac mov_metrics));
paulson@5563
   274
by (ALLGOALS
paulson@5563
   275
    (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
paulson@5563
   276
(** LEVEL 5 **)
paulson@5563
   277
by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
paulson@5563
   278
by Auto_tac;
paulson@5583
   279
by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1);
paulson@5357
   280
qed "E_thm16a";
paulson@5357
   281
paulson@5357
   282
(*lem_lift_5_1 has ~goingup instead of goingdown*)
paulson@5563
   283
Goal "#0<N ==>   \
paulson@5648
   284
\     Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \
paulson@5563
   285
\                  (moving Int Req n Int {s. metric n s < N})";
paulson@5357
   286
by (cut_facts_tac [bounded] 1);
paulson@5426
   287
by (ensures_tac "req_down" 1);
paulson@5424
   288
by Auto_tac;
paulson@5426
   289
by (REPEAT_FIRST (eresolve_tac mov_metrics));
paulson@5563
   290
by (ALLGOALS
paulson@5783
   291
    (asm_simp_tac (simpset() addsimps [zle_def] @ 
paulson@5596
   292
		                      metric_simps @ zcompare_rls)));
paulson@5563
   293
(** LEVEL 5 **)
paulson@5583
   294
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
paulson@5583
   295
by (etac exE 1);  
paulson@5583
   296
by (etac ssubst 1);
paulson@5583
   297
by Auto_tac;
paulson@5583
   298
by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1);
paulson@5357
   299
qed "E_thm16b";
paulson@5357
   300
paulson@5357
   301
paulson@5357
   302
paulson@5357
   303
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
paulson@5357
   304
  i.e. the trivial disjunction, leading to an asymmetrical proof.*)
paulson@5563
   305
Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
paulson@5563
   306
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
oheimb@5758
   307
by (force_tac (claset() delrules [impCE] addEs [impCE], 
oheimb@5758
   308
	      simpset() addsimps conj_comms) 1);
paulson@5357
   309
qed "E_thm16c";
paulson@5357
   310
paulson@5357
   311
paulson@5357
   312
(*lift_5*)
paulson@5648
   313
Goal "#0<N ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N})   \
paulson@5563
   314
\                          (moving Int Req n Int {s. metric n s < N})";
paulson@5426
   315
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
paulson@5583
   316
by (etac E_thm16b 3);
paulson@5583
   317
by (etac E_thm16a 2);
paulson@5426
   318
by (dtac E_thm16c 1);
paulson@5357
   319
by (Blast_tac 1);
paulson@5357
   320
qed "lift_5";
paulson@5357
   321
paulson@5357
   322
paulson@5357
   323
(** towards lift_3 **)
paulson@5357
   324
paulson@5357
   325
(*lemma used to prove lem_lift_3_1*)
paulson@5563
   326
Goal "[| metric n s = #0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
paulson@5426
   327
by (etac rev_mp 1);
paulson@5563
   328
(*force simplification of "metric..." while in conclusion part*)
paulson@5563
   329
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
paulson@5563
   330
by (auto_tac (claset() addIs [zleI, zle_anti_sym], 
paulson@5583
   331
	      simpset() addsimps zcompare_rls@[zadd_int, integ_of_Min]));
paulson@5563
   332
(*trans_tac (or decision procedures) could do the rest*)
paulson@5563
   333
by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 2);
paulson@5563
   334
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
paulson@5563
   335
by (ALLGOALS (clarify_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1])));
paulson@5563
   336
by (REPEAT_FIRST (eres_inst_tac [("P", "?x+?y = ?z")] rev_mp));
paulson@5563
   337
by (REPEAT_FIRST (etac ssubst));
paulson@5583
   338
by (auto_tac (claset(), simpset() addsimps [zadd_int]));
paulson@5357
   339
qed "metric_eq_0D";
paulson@5357
   340
paulson@5357
   341
AddDs [metric_eq_0D];
paulson@5357
   342
paulson@5357
   343
paulson@5357
   344
(*lem_lift_3_1*)
paulson@5648
   345
Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0})   \
paulson@5357
   346
\                  (stopped Int atFloor n)";
paulson@5357
   347
by (cut_facts_tac [bounded] 1);
paulson@5426
   348
by (ensures_tac "request_act" 1);
paulson@5424
   349
by Auto_tac;
paulson@5357
   350
qed "E_thm11";
paulson@5357
   351
paulson@5357
   352
(*lem_lift_3_5*)
paulson@5648
   353
Goal "Lprg : LeadsTo \
paulson@5563
   354
\       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
paulson@5563
   355
\       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
paulson@5426
   356
by (ensures_tac "request_act" 1);
paulson@5424
   357
by (auto_tac (claset(), simpset() addsimps metric_simps));
paulson@5357
   358
qed "E_thm13";
paulson@5357
   359
paulson@5357
   360
(*lem_lift_3_6*)
paulson@5563
   361
Goal "#0 < N ==> \
paulson@5648
   362
\     Lprg : LeadsTo \
paulson@5563
   363
\       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
paulson@5563
   364
\       (opened Int Req n Int {s. metric n s = N})";
paulson@5426
   365
by (ensures_tac "open_act" 1);
paulson@5426
   366
by (REPEAT_FIRST (eresolve_tac mov_metrics));
paulson@5424
   367
by (auto_tac (claset(), simpset() addsimps metric_simps));
paulson@5357
   368
qed "E_thm14";
paulson@5357
   369
paulson@5357
   370
(*lem_lift_3_7*)
paulson@5648
   371
Goal "Lprg : LeadsTo \
paulson@5563
   372
\       (opened Int Req n Int {s. metric n s = N})  \
paulson@5563
   373
\       (closed Int Req n Int {s. metric n s = N})";
paulson@5426
   374
by (ensures_tac "close_act" 1);
paulson@5424
   375
by (auto_tac (claset(), simpset() addsimps metric_simps));
paulson@5357
   376
qed "E_thm15";
paulson@5357
   377
paulson@5357
   378
paulson@5357
   379
(** the final steps **)
paulson@5357
   380
paulson@5563
   381
Goal "#0 < N ==> \
paulson@5648
   382
\     Lprg : LeadsTo \
paulson@5563
   383
\       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
paulson@5563
   384
\       (moving Int Req n Int {s. metric n s < N})";
paulson@5479
   385
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
paulson@5479
   386
	                addIs [LeadsTo_Trans]) 1);
paulson@5357
   387
qed "lift_3_Req";
paulson@5357
   388
paulson@5357
   389
paulson@5563
   390
paulson@5563
   391
(*Now we observe that our integer metric is really a natural number*)
paulson@5563
   392
Goal "reachable Lprg <= {s. #0 <= metric n s}";
paulson@5563
   393
by (rtac (bounded RS Invariant_includes_reachable RS subset_trans) 1);
paulson@5563
   394
by (simp_tac (simpset() addsimps metric_simps @ zcompare_rls) 1);
paulson@5563
   395
by (auto_tac (claset(),
paulson@5563
   396
	      simpset() addsimps [zless_iff_Suc_zadd, zle_iff_zadd]));
paulson@5563
   397
by (REPEAT_FIRST (etac ssubst));
paulson@5583
   398
by (auto_tac (claset(), simpset() addsimps [zadd_int]));
paulson@5563
   399
qed "reach_nonneg";
paulson@5563
   400
paulson@5563
   401
val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
paulson@5563
   402
paulson@5648
   403
Goal "Lprg : LeadsTo (moving Int Req n) (stopped Int atFloor n)";
paulson@5563
   404
by (rtac (reach_nonneg RS integ_0_le_induct) 1);
paulson@5563
   405
by (case_tac "#0 < z" 1);
paulson@5563
   406
(*If z <= #0 then actually z = #0*)
paulson@5563
   407
by (fold_tac [zle_def]);
paulson@5563
   408
by (force_tac (claset() addIs [R_thm11, zle_anti_sym], simpset()) 2);
paulson@5426
   409
by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
paulson@5426
   410
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
paulson@5583
   411
by (rtac lift_3_Req 3);
paulson@5583
   412
by (rtac lift_4 2);
paulson@5426
   413
by Auto_tac;
paulson@5357
   414
qed "lift_3";
paulson@5357
   415
paulson@5357
   416
paulson@5648
   417
Goal "Lprg : LeadsTo (Req n) (opened Int atFloor n)";
paulson@5426
   418
by (rtac LeadsTo_Trans 1);
paulson@5426
   419
by (rtac (E_thm04 RS LeadsTo_Un) 2);
paulson@5583
   420
by (rtac LeadsTo_Un_post 2);
paulson@5426
   421
by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
paulson@5426
   422
by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
paulson@5426
   423
by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
paulson@5426
   424
by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2);
paulson@5426
   425
by (rtac E_thm02 2);
paulson@5426
   426
by (rtac (open_move RS Invariant_LeadsToI) 1);
paulson@5426
   427
by (rtac (open_stop RS Invariant_LeadsToI) 1);
paulson@5426
   428
by (rtac subset_imp_LeadsTo 1);
paulson@5340
   429
by (Clarify_tac 1);
paulson@5484
   430
(*The case split is not essential but makes Blast_tac much faster.
paulson@5484
   431
  Must also be careful to prevent simplification from looping*)
paulson@5484
   432
by (case_tac "open x" 1);
paulson@5484
   433
by (ALLGOALS (rotate_tac ~1));
paulson@5484
   434
by (ALLGOALS Asm_full_simp_tac);
paulson@5426
   435
by (Blast_tac 1);
paulson@5340
   436
qed "lift_1";
paulson@5340
   437
paulson@6024
   438
Close_locale "floor";