--- a/src/HOL/UNITY/Lift.ML Thu Aug 20 16:58:28 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML Thu Aug 20 17:43:01 1998 +0200
@@ -6,19 +6,21 @@
The Lift-Control Example
*)
-(*ARITH.ML??*)
-Goal "m-1 < n ==> m <= n";
-by (exhaust_tac "m" 1);
-by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
-qed "pred_less_imp_le";
+(*To move 0 < metric n s out of the assumptions for case splitting*)
+val rev_mp' = read_instantiate_sg (sign_of thy)
+ [("P", "0 < metric ?n ?s")] rev_mp;
+
+val Suc_lessD_contra = Suc_lessD COMP rev_contrapos;
+val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra;
val always_defs = [above_def, below_def, queueing_def,
goingup_def, goingdown_def, ready_def];
val cmd_defs = [Lprg_def,
request_act_def, open_act_def, close_act_def,
- req_up_act_def, req_down_act_def, move_up_def, move_down_def];
+ req_up_def, req_down_def, move_up_def, move_down_def,
+ button_press_def];
Goalw [Lprg_def] "id : Acts Lprg";
by (Simp_tac 1);
@@ -26,6 +28,19 @@
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 *)
+
+
+val metric_simps =
+ [metric_def, vimage_def,
+ not_less_less_Suc_eq, less_not_sym RS not_less_less_Suc_eq,
+ Suc_lessD_contra, Suc_lessD_contra',
+ less_not_refl2, less_not_refl3];
+
+
+
(*split_all_tac causes a big blow-up*)
claset_ref() := claset() delSWrapper "split_all_tac";
@@ -37,7 +52,7 @@
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
moving_up_def, moving_down_def];
-AddIffs [min_le_max];
+AddIffs [Min_le_Max];
val nat_exhaust_le_pred =
@@ -60,7 +75,6 @@
by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
qed "less_imp_le_pred";
-
Goalw [Lprg_def] "Invariant Lprg open_stop";
by (rtac InvariantI 1);
by (Force_tac 1);
@@ -123,35 +137,53 @@
(** The HUG'93 paper mistakenly omits the Req n from these! **)
+(** Lift_1 **)
+
+(*lem_lift_1_5*)
Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
by (cut_facts_tac [stop_floor] 1);
by (ensures_tac defs "open_act" 1);
qed "E_thm01";
+(*lem_lift_1_1*)
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 defs "open_act" 1);
qed "E_thm02";
+(*lem_lift_1_2*)
Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
\ (Req n Int closed - (atFloor n - queueing))";
by (ensures_tac defs "close_act" 1);
qed "E_thm03";
+
+(*lem_lift_1_7*)
Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
\ (opened Int atFloor n)";
by (ensures_tac defs "open_act" 1);
qed "E_thm04";
-(** Theorem 5. Statements of thm05a and thm05b were wrong! **)
+(** Lift 2. Statements of thm05a and thm05b were wrong! **)
Open_locale "floor";
-AddIffs [thm "min_le_n", thm "n_le_max"];
+val Min_le_n = thm "Min_le_n";
+val n_le_Max = thm "n_le_Max";
+
+AddIffs [Min_le_n, n_le_Max];
-(*NOT an ensures property, but a mere inclusion*)
+val le_MinD = Min_le_n RS le_anti_sym;
+val Max_leD = n_le_Max RSN (2,le_anti_sym);
+
+AddSDs [le_MinD, leI RS le_MinD,
+ Max_leD, leI 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))";
@@ -159,21 +191,248 @@
by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
qed "E_thm05c";
+(*lift_2*)
Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
\ (moving Int Req n)";
br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
-by (ensures_tac defs "req_down_act" 2);
-by (ensures_tac defs "req_up_act" 1);
+by (ensures_tac defs "req_down" 2);
+by (ensures_tac defs "req_up" 1);
qed "lift_2";
+(** Towards lift_4 ***)
-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 *)
+Goal "[| x ~: A; y : A |] ==> x ~= y";
+by (Blast_tac 1);
+qed "not_mem_distinct";
+
+fun distinct_tac i =
+ dtac le_neq_implies_less i THEN
+ eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
+ assume_tac i;
+
+
+(*lem_lift_4_1 *)
+Goal "0 < N ==> \
+\ LeadsTo Lprg \
+\ (moving Int Req n Int (metric n -`` {N}) Int \
+\ {s. floor s ~: req s} Int {s. up s}) \
+\ (moving Int Req n Int (metric n -`` lessThan N))";
+by (cut_facts_tac [moving_up] 1);
+by (ensures_tac defs "move_up" 1);
+(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
+be (leI RS le_anti_sym RS sym) 1;
+by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
+by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
+by (REPEAT_FIRST (etac rev_mp'));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+by (distinct_tac 1);
+by (auto_tac
+ (claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)]
+ addIs [diff_Suc_less_diff],
+ simpset()));
+qed "E_thm12a";
+
+
+(*This rule helps eliminate occurrences of (floor s - 1) *)
+val less_floor_imp = read_instantiate_sg (sign_of thy)
+ [("n", "floor ?s")] less_eq_Suc_add RS exE;
+
+(*lem_lift_4_3 *)
+Goal "0 < N ==> \
+\ LeadsTo Lprg \
+\ (moving Int Req n Int (metric n -`` {N}) Int \
+\ {s. floor s ~: req s} - {s. up s}) \
+\ (moving Int Req n Int (metric n -`` lessThan N))";
+by (cut_facts_tac [moving_down] 1);
+by (ensures_tac defs "move_down" 1);
+by (ALLGOALS distinct_tac);
+by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
+(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
+be (leI RS le_anti_sym RS sym) 1;
+by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
+by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
+by (REPEAT_FIRST (etac rev_mp'));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+by (auto_tac
+ (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
+ addIs [diff_le_Suc_diff, diff_less_Suc_diff],
+ simpset() addsimps [trans_le_add1]));
+qed "E_thm12b";
+
+
+(*lift_4*)
+Goal "0<N ==> LeadsTo Lprg (moving Int Req n Int (metric n -`` {N}) Int \
+\ {s. floor s ~: req s}) \
+\ (moving Int Req n Int (metric n -`` lessThan N))";
+br ([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 (metric n -`` {N}) Int goingup) \
+\ (moving Int Req n Int (metric n -`` lessThan N))";
+by (cut_facts_tac [bounded] 1);
+by (ensures_tac defs "req_up" 1);
+by (REPEAT_FIRST (etac rev_mp'));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+by (auto_tac (claset() addIs [diff_Suc_less_diff],
+ simpset() addsimps [arith1, arith2]));
+qed "E_thm16a";
+
+ (*arith1 comes from
+ 1. !!s i.
+ [| n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
+ i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
+ ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
+ Suc (floor s) < n; 0 < floor s - Min |]
+ ==> n - Suc (floor s) < floor s - Min + (n - Min)
+ *)
+
+ (*arith2 comes from
+ 2. !!s i.
+ [| Min <= floor s; ...
+ n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
+ i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
+ ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
+ Suc (floor s) < n; Min < n |]
+ ==> n - Suc (floor s) < floor s - Min + (n - Min)
+ *)
-val [lift_3] =
-goal thy "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n) ==> LeadsTo Lprg (Req n) (opened Int atFloor n)";
+(*lem_lift_5_1 has ~goingup instead of goingdown*)
+Goal "0<N ==> \
+\ LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingdown) \
+\ (moving Int Req n Int (metric n -`` lessThan N))";
+by (cut_facts_tac [bounded] 1);
+by (ensures_tac defs "req_down" 1);
+by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
+by (REPEAT_FIRST (etac rev_mp'));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff],
+ simpset() addsimps [trans_le_add1, arith3, arith4]));
+qed "E_thm16b";
+
+ (*arith3 comes from
+ 1. !!s i x.
+ [| floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max;
+ ~ open s; n : req s; move s; Min <= i; i : req s;
+ ALL ia. ia <= Max --> Suc (i + x) < ia --> ia ~: req s;
+ ~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x;
+ Suc (i + x) < Max |]
+ ==> i + x - n < Max - Suc (i + x) + (Max - n)
+ *)
+
+ (*arith4 comes from
+ 2. !!s i x.
+ [| floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max;
+ ~ open s; n : req s; move s; Min <= i; i : req s;
+ ALL ia. ia <= Max --> Suc (i + x) < ia --> ia ~: req s;
+ ~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x;
+ n < Max |]
+ ==> i + x - n < Max - Suc (i + x) + (Max - n)
+ *)
+
+
+
+(*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 (metric n -``{N}) <= goingup Un goingdown";
+by (asm_simp_tac (simpset() addsimps (defs@metric_simps)) 1);
+by (Blast_tac 1);
+qed "E_thm16c";
+
+
+(*lift_5*)
+Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N})) \
+\ (moving Int Req n Int (metric n -`` lessThan N))";
+br ([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);
+bd 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";
+be rev_mp 1;
+by (asm_simp_tac (simpset() addsimps metric_simps) 1);
+auto();
+qed "metric_eq_0D";
+
+AddDs [metric_eq_0D];
+
+
+(*lem_lift_3_1*)
+Goal "LeadsTo Lprg (moving Int Req n Int (metric n -`` {0})) \
+\ (stopped Int atFloor n)";
+by (cut_facts_tac [bounded] 1);
+by (ensures_tac defs "request_act" 1);
+qed "E_thm11";
+
+(*lem_lift_3_5*)
+Goal "LeadsTo Lprg \
+\ (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
+\ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})";
+by (ensures_tac defs "request_act" 1);
+by (asm_simp_tac (simpset() addsimps metric_simps) 1);
+qed "E_thm13";
+
+(*lem_lift_3_6*)
+Goal "0 < N ==> \
+\ LeadsTo Lprg \
+\ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
+\ (opened Int Req n Int (metric n -`` {N}))";
+by (ensures_tac defs "open_act" 1);
+by (REPEAT_FIRST (etac rev_mp'));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
+qed "E_thm14";
+
+(*lem_lift_3_7*)
+Goal "LeadsTo Lprg \
+\ (opened Int Req n Int (metric n -`` {N})) \
+\ (closed Int Req n Int (metric n -`` {N}))";
+by (ensures_tac defs "close_act" 1);
+by (asm_simp_tac (simpset() addsimps metric_simps) 1);
+qed "E_thm15";
+
+
+(** the final steps **)
+
+Goal "0 < N ==> \
+\ LeadsTo Lprg \
+\ (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
+\ (moving Int Req n Int (metric n -`` lessThan N))";
+(*Blast_tac: PROOF FAILED*)
+by (best_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
+ addIs [LeadsTo_Trans]) 1);
+qed "lift_3_Req";
+
+
+Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
+br (allI RS LessThan_induct) 1;
+by (exhaust_tac "m" 1);
+auto();
+br E_thm11 1;
+br ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1;
+br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
+br lift_3_Req 4;
+br lift_4 3;
+auto();
+qed "lift_3";
+
+
+Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
br LeadsTo_Trans 1;
br (E_thm04 RS LeadsTo_Un) 2;
br LeadsTo_Un_post' 2;
@@ -189,230 +448,10 @@
bws defs;
by (Clarify_tac 1);
(*stops simplification from looping*)
-by (asm_full_simp_tac (simpset() setsubgoaler simp_tac) 1);
+by (Full_simp_tac 1);
by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
qed "lift_1";
-
-val rev_mp' = read_instantiate_sg (sign_of thy)
- [("P", "0 < metric ?n ?s")] rev_mp;
-
-
-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 (ensures_tac defs "req_up_act" 1);
-by (REPEAT_FIRST (etac rev_mp'));
-by (auto_tac (claset() addIs [diff_Suc_less_diff],
- simpset() addsimps [arith1, arith2, metric_def]));
-qed "E_thm16a";
-
-
-(*arith1 comes from
- 1. !!s i.
- [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
- i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
- ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
- Suc (floor s) < n; 0 < floor s - min |]
- ==> n - Suc (floor s) < floor s - min + (n - min)
-*)
-
-(*arith2 comes from
- 2. !!s i.
- [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
- i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
- ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
- Suc (floor s) < n; min < n |]
- ==> n - Suc (floor s) < floor s - min + (n - min)
-*)
-
-
-xxxxxxxxxxxxxxxx;
-
-Goal "j<=i ==> i - j < Suc i - j";
-by (REPEAT (etac rev_mp 1));
-by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
-by Auto_tac;
-qed "diff_less_Suc_diff";
-
-
-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 (ensures_tac defs "req_down_act" 1);
-be rev_mp 2;
-be rev_mp 1;
-by (dtac less_eq_Suc_add 2);
-by (Clarify_tac 2);
-by (Asm_full_simp_tac 2);
-by (dtac less_eq_Suc_add 1);
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-
-by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
-by (REPEAT (Safe_step_tac 1));
-by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
-by (REPEAT (Safe_step_tac 1));
-by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
-by (REPEAT (Safe_step_tac 1));
-
-
-
-
-
-
-
-Goal "[| i + k < n; Suc (i + k) < n |] ==> i + k - m < Suc (i + k) - m";
-by (REPEAT (etac rev_mp 1));
-by (arith_oracle_tac 1);
-
-
-by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
-by (REPEAT (Safe_step_tac 2));
-by(Blast_tac 2);
-by(Blast_tac 2);
-by(Blast_tac 2);
-by (REPEAT (Safe_step_tac 2));
-by(Blast_tac 2);
-by(blast_tac (claset() addEs [less_asym]) 2);
-by (REPEAT (Safe_step_tac 2));
-by(blast_tac (claset() addEs [less_asym]) 2);
-by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
-by (REPEAT (Safe_step_tac 2));
-by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
-
-
-by (asm_simp_tac (simpset() addsimps [less_not_sym] setsubgoaler simp_tac) 1);
-
-
-by (REPEAT (Safe_step_tac 2));
-by (REPEAT (Safe_step_tac 2 THEN Blast_tac 2));
-
-by (auto_tac (claset() addIs [diff_Suc_less_diff],
- simpset() addsimps [metric_def]));
-qed "E_thm16b";
-
-
-
-Goal "[| m <= i; i < fl; ~ fl < n; fl - 1 < n |] ==> ~ n < fl - 1 --> n < fl --> fl - 1 - m + (n - m) < fl - n";
-
-
-not_less_iff_le
-
-Goal "[| ~ m < n; m - 1 < n |] ==> n = m";
-by (cut_facts_tac [less_linear] 1);
-by (blast_tac (claset() addSEs [less_irrefl]) 1);
- by (REPEAT (etac rev_mp 1));
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (arith_oracle_tac 1);
+Close_locale;
-
-
-
-
-
-(**in the postscript file, but too horrible**)
-
-Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} - goingup) \
-\ (moving Int Req n Int {s. metric n s < N})";
-by (ensures_tac defs "req_down_act" 1);
-by (REPEAT_FIRST (etac rev_mp'));
-
-by (dtac less_eq_Suc_add 2);
-by (Clarify_tac 2);
-by (Asm_full_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
-
-
-yyyyyyyyyyyyyyyy;
-
-by (REPEAT (Safe_step_tac 2));
-by(blast_tac (claset() addEs [less_asym]) 2);
-by (REPEAT (Safe_step_tac 2));
-by(Blast_tac 2);
-by(Blast_tac 2);
-by (REPEAT (Safe_step_tac 2));
-by(Blast_tac 2);
-by(Blast_tac 2);
-by (REPEAT (Safe_step_tac 2));
-by(blast_tac (claset() addEs [less_asym]) 2);
-by(blast_tac (claset() addDs [le_anti_sym]
- addSDs [leI, pred_less_imp_le]) 2);
-by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
-
-
-by(Blast_tac 3);
-
-
-
-
-
-
-
-Goal "m < fl ==> n - Suc (fl) < fl - m + (n - m)";
-fe rev_mp;
-by (res_inst_tac [("m","MIN"),("n","fl")] diff_induct 1);
- by (ALLGOALS Asm_simp_tac);
-
-by (arith_oracle_tac 1);
-
-
-Goal "[| Suc (fl) < n; m < n |] ==> n - Suc (fl) < fl - m + (n - m)";
-by (REPEAT (etac rev_mp 1));
-by (arith_oracle_tac 1);
-
-
-
-
-
-
-
-infixr TRANS;
-fun th1 TRANS th2 = [th1, th2] MRS LeadsTo_Trans_Un';
-
-E_thm02 TRANS E_thm03 TRANS (lift_2 RS LeadsTo_Un_post');
-
-
-
-[E_thm02,
- E_thm03 RS LeadsTo_Un_post'] MRS LeadsTo_Trans_Un';
-
-
-val sact = "open_act";
-val sact = "move_up_act";
-
-val (main_def::CDEFS) = defs;
-
-by (REPEAT (Invariant_Int_tac 1));
-
-by (etac Invariant_LeadsTo_Basis 1
- ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1));
-
-by (res_inst_tac [("act", sact)] transient_mem 2);
-by (simp_tac (simpset() addsimps (Domain_partial_func::CDEFS)) 3);
-by (force_tac (claset(), simpset() addsimps [main_def]) 2);
-by (constrains_tac (main_def::CDEFS) 1);
-by (rewrite_goals_tac CDEFS);
-by (ALLGOALS Clarify_tac);
-by (Auto_tac);
-
-by(Force_tac 2);
-
-
-
-yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
-
-
-
-Goalw [transient_def]
- "transient acts A = (EX act:acts. A <= act^-1 ^^ (Compl A))";
-by Safe_tac;
-by (ALLGOALS (rtac bexI));
-by (TRYALL assume_tac);
-by (Blast_tac 1);
-br conjI 1;
-by (Blast_tac 1);
-(*remains to show
- [| act : acts; A <= act^-1 ^^ Compl A |] ==> act ^^ A <= Compl A
-*)
-
--- a/src/HOL/UNITY/Lift.thy Thu Aug 20 16:58:28 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy Thu Aug 20 17:43:01 1998 +0200
@@ -19,25 +19,26 @@
move :: bool (*whether moving takes precedence over opening*)
consts
- min, max :: nat (*least and greatest floors*)
+ Min, Max :: nat (*least and greatest floors*)
rules
- min_le_max "min <= max"
+ Min_le_Max "Min <= Max"
(** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
arith1 "m < fl ==> n - Suc fl < fl - m + (n - m)"
- arith2 "[| Suc fl < n; m < n |] ==> n - Suc fl < fl - m + (n - m)"
-
+ arith2 "[| m<n; m <= fl |] ==> n - Suc fl < fl - m + (n - m)"
+ arith3 "[| Suc ix < m |] ==> ix - n < m - Suc ix + (m - n)"
+ arith4 "[| ix < m; n < ix |] ==> ix - n < m - Suc (ix) + (m - n)"
constdefs
(** Abbreviations: the "always" part **)
above :: state set
- "above == {s. EX i. floor s < i & i <= max & i : req s}"
+ "above == {s. EX i. floor s < i & i <= Max & i : req s}"
below :: state set
- "below == {s. EX i. min <= i & i < floor s & i : req s}"
+ "below == {s. EX i. Min <= i & i < floor s & i : req s}"
queueing :: state set
"queueing == above Un below"
@@ -91,15 +92,15 @@
close_act :: "(state*state) set"
"close_act == {(s,s'). s' = s (|open := False|) & open s}"
- req_up_act :: "(state*state) set"
- "req_up_act ==
+ req_up :: "(state*state) set"
+ "req_up ==
{(s,s'). s' = s (|stop :=False,
floor := Suc (floor s),
up := True|)
& s : (ready Int goingup)}"
- req_down_act :: "(state*state) set"
- "req_down_act ==
+ req_down :: "(state*state) set"
+ "req_down ==
{(s,s'). s' = s (|stop :=False,
floor := floor s - 1,
up := False|)
@@ -115,17 +116,24 @@
{(s,s'). s' = s (|floor := floor s - 1|)
& ~ stop s & ~ up s & floor s ~: req s}"
+ button_press :: "(state*state) set"
+ "button_press ==
+ {(s,s'). EX n. s' = s (|req := insert n (req s)|)
+ & Min <= n & n <= Max}"
+
+
Lprg :: state program
- "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s &
+ (*for the moment, we OMIT button_press*)
+ "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
~ open s & req s = {}},
Acts = {id, request_act, open_act, close_act,
- req_up_act, req_down_act, move_up, move_down}|)"
+ req_up, req_down, move_up, move_down}|)"
(** Invariants **)
bounded :: state set
- "bounded == {s. min <= floor s & floor s <= max}"
+ "bounded == {s. Min <= floor s & floor s <= Max}"
open_stop :: state set
"open_stop == {s. open s --> stop s}"
@@ -138,25 +146,26 @@
moving_up :: state set
"moving_up == {s. ~ stop s & up s -->
- (EX f. floor s <= f & f <= max & f : req s)}"
+ (EX f. floor s <= f & f <= Max & f : req s)}"
moving_down :: state set
"moving_down == {s. ~ stop s & ~ up s -->
- (EX f. min <= f & f <= floor s & f : req s)}"
+ (EX f. Min <= f & f <= floor s & f : req s)}"
metric :: [nat,state] => nat
- "metric n s == if up s & floor s < n then n - floor s
- else if ~ up s & n < floor s then floor s - n
- else if up s & n < floor s then (max - floor s) + (max-n)
- else if ~ up s & floor s < n then (floor s - min) + (n-min)
- else 0"
+ "metric ==
+ %n s. if up s & floor s < n then n - floor s
+ else if ~ up s & n < floor s then floor s - n
+ else if up s & n < floor s then (Max - floor s) + (Max-n)
+ else if ~ up s & floor s < n then (floor s - Min) + (n-Min)
+ else 0"
locale floor =
fixes
n :: nat
assumes
- min_le_n "min <= n"
- n_le_max "n <= max"
+ Min_le_n "Min <= n"
+ n_le_Max "n <= Max"
defines
end