# HG changeset patch # User paulson # Date 903627781 -7200 # Node ID 6efb2b87610ceaea73ff06411e9d93241b5c076d # Parent 6ef114ba5b551ad29d964e6c1bd7dcffbe8bdef4 New theory Lift diff -r 6ef114ba5b55 -r 6efb2b87610c src/HOL/UNITY/Lift.ML --- 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 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 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 \ +\ 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 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 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 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 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 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 -*) - diff -r 6ef114ba5b55 -r 6efb2b87610c src/HOL/UNITY/Lift.thy --- 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 - 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 diff -r 6ef114ba5b55 -r 6efb2b87610c src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Thu Aug 20 16:58:28 1998 +0200 +++ b/src/HOL/UNITY/ROOT.ML Thu Aug 20 17:43:01 1998 +0200 @@ -20,3 +20,4 @@ time_use_thy "FP"; time_use_thy "Reach"; time_use_thy "Handshake"; +time_use_thy "Lift";