(* Title: HOL/UNITY/Lift
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
The Lift-Control Example
*)
Goal "~ z < w ==> (z < w + #1) = (z = w)";
by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1);
qed "not_zless_zless1_eq";
(*split_all_tac causes a big blow-up*)
claset_ref() := claset() delSWrapper "split_all_tac";
Delsimps [split_paired_All];
Goal "[| x ~: A; y : A |] ==> x ~= y";
by (Blast_tac 1);
qed "not_mem_distinct";
fun distinct_tac i =
dtac zle_neq_implies_zless i THEN
eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
assume_tac i;
(** Rules to move "metric n s" out of the assumptions, for case splitting **)
val mov_metric1 = read_instantiate_sg (sign_of thy)
[("P", "?x < metric ?n ?s")] rev_mp;
val mov_metric2 = read_instantiate_sg (sign_of thy)
[("P", "?x = metric ?n ?s")] rev_mp;
val mov_metric3 = read_instantiate_sg (sign_of thy)
[("P", "~ (?x < metric ?n ?s)")] rev_mp;
val mov_metric4 = read_instantiate_sg (sign_of thy)
[("P", "(?x <= metric ?n ?s)")] rev_mp;
(*The order in which they are applied seems to be critical...*)
val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
val zless_zadd1_contra = zless_zadd1_imp_zless COMP rev_contrapos;
val zless_zadd1_contra' = zless_not_sym RS zless_zadd1_contra;
val metric_simps =
[metric_def, vimage_def, order_less_imp_not_less, order_less_imp_triv,
order_less_imp_not_eq, order_less_imp_not_eq2,
not_zless_zless1_eq, zless_not_sym RS not_zless_zless1_eq,
zless_zadd1_contra, zless_zadd1_contra',
zless_not_refl2, zless_not_refl3];
Addsimps [Lprg_def RS def_prg_simps];
Addsimps (map simp_of_act
[request_act_def, open_act_def, close_act_def,
req_up_def, req_down_def, move_up_def, move_down_def,
button_press_def]);
val always_defs = [above_def, below_def, queueing_def,
goingup_def, goingdown_def, ready_def];
Addsimps (map simp_of_set always_defs);
Goalw [Lprg_def] "id : Acts Lprg";
by (Simp_tac 1);
qed "id_in_Acts";
AddIffs [id_in_Acts];
val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post
and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un);
(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
(*Simplification for records*)
Addsimps (thms"state.update_defs");
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
moving_up_def, moving_down_def];
AddIffs [Min_le_Max];
val nat_exhaust_le_pred =
read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
val nat_exhaust_pred_le =
read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
Goal "Invariant Lprg open_stop";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
qed "open_stop";
Goal "Invariant Lprg stop_floor";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
qed "stop_floor";
(*This one needs open_stop, which was proved above*)
Goal "Invariant Lprg open_move";
by (rtac InvariantI 1);
by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
by (Force_tac 1);
by (constrains_tac 1);
qed "open_move";
Goal "Invariant Lprg moving_up";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_up";
Goal "Invariant Lprg moving_down";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_down";
Goal "Invariant Lprg bounded";
by (rtac InvariantI 1);
by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
by (Force_tac 1);
by (constrains_tac 1);
by (ALLGOALS Clarify_tac);
by (REPEAT_FIRST distinct_tac);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]@zcompare_rls)));
by (ALLGOALS
(blast_tac (claset() addDs [zle_imp_zless_or_eq]
addIs [zless_trans])));
qed "bounded";
(*** Progress ***)
val abbrev_defs = [moving_def, stopped_def,
opened_def, closed_def, atFloor_def, Req_def];
Addsimps (map simp_of_set abbrev_defs);
(** The HUG'93 paper mistakenly omits the Req n from these! **)
(** Lift_1 **)
Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
by (cut_facts_tac [stop_floor] 1);
by (ensures_tac "open_act" 1);
qed "E_thm01"; (*lem_lift_1_5*)
Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
\ (Req n Int opened - atFloor n)";
by (cut_facts_tac [stop_floor] 1);
by (ensures_tac "open_act" 1);
qed "E_thm02"; (*lem_lift_1_1*)
Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
\ (Req n Int closed - (atFloor n - queueing))";
by (ensures_tac "close_act" 1);
qed "E_thm03"; (*lem_lift_1_2*)
Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
\ (opened Int atFloor n)";
by (ensures_tac "open_act" 1);
qed "E_thm04"; (*lem_lift_1_7*)
(** Lift 2. Statements of thm05a and thm05b were wrong! **)
Open_locale "floor";
val Min_le_n = thm "Min_le_n";
val n_le_Max = thm "n_le_Max";
AddIffs [Min_le_n, n_le_Max];
val le_MinD = Min_le_n RS zle_anti_sym;
val Max_leD = n_le_Max RSN (2,zle_anti_sym);
AddSDs [le_MinD, zleI RS le_MinD,
Max_leD, zleI RS Max_leD];
(*lem_lift_2_0
NOT an ensures property, but a mere inclusion;
don't know why script lift_2.uni says ENSURES*)
Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
\ ((closed Int goingup Int Req n) Un \
\ (closed Int goingdown Int Req n))";
by (rtac subset_imp_LeadsTo 1);
by (auto_tac (claset() addSEs [int_neqE], simpset()));
qed "E_thm05c";
(*lift_2*)
Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
\ (moving Int Req n)";
by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (ensures_tac "req_down" 2);
by (ensures_tac "req_up" 1);
by Auto_tac;
qed "lift_2";
(** Towards lift_4 ***)
(*lem_lift_4_1 *)
Goal "#0 < N ==> \
\ LeadsTo Lprg \
\ (moving Int Req n Int {s. metric n s = N} Int \
\ {s. floor s ~: req s} Int {s. up s}) \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [moving_up] 1);
by (ensures_tac "move_up" 1);
by Safe_tac;
(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
by (etac (zleI RS zle_anti_sym RS sym) 1);
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (REPEAT_FIRST distinct_tac);
(** LEVEL 6 **)
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [zle_def]@ metric_simps @ zcompare_rls)));
qed "E_thm12a";
(*lem_lift_4_3 *)
Goal "#0 < N ==> \
\ LeadsTo Lprg \
\ (moving Int Req n Int {s. metric n s = N} Int \
\ {s. floor s ~: req s} - {s. up s}) \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [moving_down] 1);
by (ensures_tac "move_down" 1);
by Safe_tac;
(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
by (etac (zleI RS zle_anti_sym RS sym) 1);
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (REPEAT_FIRST distinct_tac);
(** LEVEL 6 **)
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [zle_def] @
metric_simps @ zcompare_rls)));
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls)));
qed "E_thm12b";
(*lift_4*)
Goal "#0<N ==> LeadsTo Lprg (moving Int Req n Int {s. metric n s = N} Int \
\ {s. floor s ~: req s}) \
\ (moving Int Req n Int {s. metric n s < N})";
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (etac E_thm12b 4);
by (etac E_thm12a 3);
by (rtac id_in_Acts 2);
by (Blast_tac 1);
qed "lift_4";
(** towards lift_5 **)
(*lem_lift_5_3*)
Goal "#0<N \
\ ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "req_up" 1);
by Auto_tac;
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
(** LEVEL 5 **)
by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
by Auto_tac;
by (asm_simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls) 1);
by (full_simp_tac (no_neg_ss addsimps [add_nat, integ_of_Min]) 1);
qed "E_thm16a";
(*lem_lift_5_1 has ~goingup instead of goingdown*)
Goal "#0<N ==> \
\ LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "req_down" 1);
by Auto_tac;
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
(** LEVEL 5 **)
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 2);
by (etac exE 2);
by (etac ssubst 2);
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls)));
by (auto_tac (claset(), no_neg_ss addsimps [add_nat, integ_of_Min]));
qed "E_thm16b";
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
i.e. the trivial disjunction, leading to an asymmetrical proof.*)
Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
by (auto_tac (claset() delrules [impCE] addEs [impCE],
simpset() addsimps conj_comms));
qed "E_thm16c";
(*lift_5*)
Goal "#0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N}) \
\ (moving Int Req n Int {s. metric n s < N})";
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (etac E_thm16b 4);
by (etac E_thm16a 3);
by (rtac id_in_Acts 2);
by (dtac E_thm16c 1);
by (Blast_tac 1);
qed "lift_5";
(** towards lift_3 **)
(*lemma used to prove lem_lift_3_1*)
Goal "[| metric n s = #0; Min <= floor s; floor s <= Max |] ==> floor s = n";
by (etac rev_mp 1);
(*force simplification of "metric..." while in conclusion part*)
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
by (auto_tac (claset() addIs [zleI, zle_anti_sym],
simpset() addsimps zcompare_rls@[add_nat, integ_of_Min]));
(*trans_tac (or decision procedures) could do the rest*)
by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 2);
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
by (ALLGOALS (clarify_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1])));
by (REPEAT_FIRST (eres_inst_tac [("P", "?x+?y = ?z")] rev_mp));
by (REPEAT_FIRST (etac ssubst));
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls)));
by (auto_tac (claset(), no_neg_ss addsimps [add_nat]));
qed "metric_eq_0D";
AddDs [metric_eq_0D];
(*lem_lift_3_1*)
Goal "LeadsTo Lprg (moving Int Req n Int {s. metric n s = #0}) \
\ (stopped Int atFloor n)";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "request_act" 1);
by Auto_tac;
qed "E_thm11";
(*lem_lift_3_5*)
Goal "LeadsTo Lprg \
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
by (ensures_tac "request_act" 1);
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm13";
(*lem_lift_3_6*)
Goal "#0 < N ==> \
\ LeadsTo Lprg \
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
\ (opened Int Req n Int {s. metric n s = N})";
by (ensures_tac "open_act" 1);
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm14";
(*lem_lift_3_7*)
Goal "LeadsTo Lprg \
\ (opened Int Req n Int {s. metric n s = N}) \
\ (closed Int Req n Int {s. metric n s = N})";
by (ensures_tac "close_act" 1);
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm15";
(** the final steps **)
Goal "#0 < N ==> \
\ LeadsTo Lprg \
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
\ (moving Int Req n Int {s. metric n s < N})";
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
addIs [LeadsTo_Trans]) 1);
qed "lift_3_Req";
(*Now we observe that our integer metric is really a natural number*)
Goal "reachable Lprg <= {s. #0 <= metric n s}";
by (rtac (bounded RS Invariant_includes_reachable RS subset_trans) 1);
by (simp_tac (simpset() addsimps metric_simps @ zcompare_rls) 1);
by (auto_tac (claset(),
simpset() addsimps [zless_iff_Suc_zadd, zle_iff_zadd]));
by (REPEAT_FIRST (etac ssubst));
by (auto_tac (claset(),
simpset() addsimps zadd_ac@zcompare_0_rls));
by (auto_tac (claset(),
no_neg_ss addsimps [add_nat]));
qed "reach_nonneg";
val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
by (rtac (reach_nonneg RS integ_0_le_induct) 1);
by (case_tac "#0 < z" 1);
(*If z <= #0 then actually z = #0*)
by (fold_tac [zle_def]);
by (force_tac (claset() addIs [R_thm11, zle_anti_sym], simpset()) 2);
by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (rtac lift_3_Req 4);
by (rtac lift_4 3);
by Auto_tac;
qed "lift_3";
Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
by (rtac LeadsTo_Trans 1);
by (rtac (E_thm04 RS LeadsTo_Un) 2);
by (rtac LeadsTo_Un_post' 2);
by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2);
by (rtac E_thm02 2);
by (rtac (open_move RS Invariant_LeadsToI) 1);
by (rtac (open_stop RS Invariant_LeadsToI) 1);
by (rtac subset_imp_LeadsTo 1);
by (rtac id_in_Acts 2);
by (Clarify_tac 1);
(*The case split is not essential but makes Blast_tac much faster.
Must also be careful to prevent simplification from looping*)
by (case_tac "open x" 1);
by (ALLGOALS (rotate_tac ~1));
by (ALLGOALS Asm_full_simp_tac);
by (Blast_tac 1);
qed "lift_1";
Close_locale;