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