# HG changeset patch # User paulson # Date 903095562 -7200 # Node ID 79b326bceafb00a59daa8e47e18d4036e33a908a # Parent 7356d0c88b1b394737c843e3670dc86a029fe861 now trans_tac is part of the claset... diff -r 7356d0c88b1b -r 79b326bceafb src/HOL/UNITY/Handshake.ML --- a/src/HOL/UNITY/Handshake.ML Fri Aug 14 12:06:34 1998 +0200 +++ b/src/HOL/UNITY/Handshake.ML Fri Aug 14 13:52:42 1998 +0200 @@ -50,7 +50,6 @@ by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] GreaterThan_bounded_induct 1); by (auto_tac (claset(), simpset() addsimps [vimage_def])); -by (trans_tac 2); (*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*) by (rtac LeadsTo_Diff 1); by (rtac lemma2_2 2); diff -r 7356d0c88b1b -r 79b326bceafb src/HOL/UNITY/LessThan.ML --- a/src/HOL/UNITY/LessThan.ML Fri Aug 14 12:06:34 1998 +0200 +++ b/src/HOL/UNITY/LessThan.ML Fri Aug 14 13:52:42 1998 +0200 @@ -7,6 +7,9 @@ *) +claset_ref() := claset() addaltern ("trans_tac",trans_tac); + + (*** lessThan ***) Goalw [lessThan_def] "(i: lessThan k) = (i (m <= n-1) = (m m <= n-1"; @@ -82,57 +90,44 @@ qed "moving_down"; -xxxxxxxxxxxxxxxx; - -Goalw [Lprg_def] "Invariant Lprg bounded"; +Goal "Invariant Lprg bounded"; by (rtac InvariantI 1); +br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2; +bw Lprg_def; by (Force_tac 1); by (constrains_tac (cmd_defs@always_defs) 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]))); -by (REPEAT_FIRST trans_tac); -by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1); -by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1); -by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3); +by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le])); +by (auto_tac (claset(), simpset() addsimps [less_Suc_eq])); +by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq])); qed "bounded"; -Goalw [Lprg_def] "Invariant Lprg invariantV"; -by (rtac InvariantI 1); -by (constrains_tac cmd_defs 2); -by Auto_tac; -qed "invariantV"; + -val invariantUV = invariant_Int_rule [invariantU, invariantV]; +(*** Progress ***) -(*The safety property: mutual exclusion*) -Goal "(reachable Lprg) Int {s. MM s = 3 & NN s = 3} = {}"; -by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1); -by Auto_tac; -qed "mutual_exclusion"; +val abbrev_defs = [moving_def, stopped_def, + opened_def, closed_def, atFloor_def]; +val defs = cmd_defs@always_defs@abbrev_defs; -(*** Progress for U ***) +(*** -Goalw [unless_def] "unless (Acts Lprg) {s. MM s=2} {s. MM s=3}"; -by (constrains_tac cmd_defs 1); -qed "U_F0"; - -Goal "LeadsTo Lprg {s. MM s=1} {s. PP s = VV s & MM s = 2}"; -by (ensures_tac cmd_defs "cmd1U" 1); +Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)"; +by (ensures_tac defs "open_act" 1); qed "U_F1"; Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}"; by (cut_facts_tac [invariantUV] 1); by (rewtac Lprg_def); -by (ensures_tac cmd_defs "cmd2U" 1); +by (ensures_tac defs "cmd2U" 1); qed "U_F2"; Goal "LeadsTo Lprg {s. MM s = 3} {s. PP s}"; by (rtac leadsTo_imp_LeadsTo 1); by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1); -by (ensures_tac cmd_defs "cmd4U" 2); -by (ensures_tac cmd_defs "cmd3U" 1); +by (ensures_tac defs "cmd4U" 2); +by (ensures_tac defs "cmd3U" 1); qed "U_F3"; Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}"; @@ -142,3 +137,4 @@ by (auto_tac (claset() addSEs [less_SucE], simpset())); val U_lemma2 = result(); +***) diff -r 7356d0c88b1b -r 79b326bceafb src/HOL/UNITY/Lift.thy --- a/src/HOL/UNITY/Lift.thy Fri Aug 14 12:06:34 1998 +0200 +++ b/src/HOL/UNITY/Lift.thy Fri Aug 14 13:52:42 1998 +0200 @@ -27,25 +27,44 @@ (** Abbreviations: the "always" part **) - above :: "state set" + above :: state set "above == {s. EX i. floor s < i & i <= max & i : req s}" - below :: "state set" + below :: state set "below == {s. EX i. min <= i & i < floor s & i : req s}" - queueing :: "state set" + queueing :: state set "queueing == above Un below" - goingup :: "state set" + goingup :: state set "goingup == above Int ({s. up s} Un Compl below)" - goingdown :: "state set" + goingdown :: state set "goingdown == below Int ({s. ~ up s} Un Compl above)" - ready :: "state set" + ready :: state set "ready == {s. stop s & ~ open s & move s}" + + (** Further abbreviations **) + moving :: state set + "moving == {s. ~ stop s & ~ open s}" + + stopped :: state set + "stopped == {s. stop s & ~ open s & move s}" + + opened :: state set + "opened == {s. stop s & open s & move s}" + + closed :: state set + "closed == {s. stop s & ~ open s & move s}" + + atFloor :: nat => state set + "atFloor n == {s. floor s = n}" + + + (** The program **) request_act :: "(state*state) set" @@ -99,11 +118,6 @@ bounded :: state set "bounded == {s. min <= floor s & floor s <= max}" - (** ??? - (~ stop s & up s --> floor s < max) & - (~ stop s & ~ up s --> min < floor s)}" - **) - open_stop :: state set "open_stop == {s. open s --> stop s}" @@ -121,7 +135,8 @@ "moving_down == {s. ~ stop s & ~ up s --> (EX f. min <= f & f <= floor s & f : req s)}" - valid :: "state set" + (*intersection of all invariants: NECESSARY??*) + valid :: state set "valid == bounded Int open_stop Int open_move" end diff -r 7356d0c88b1b -r 79b326bceafb src/HOL/UNITY/Mutex.ML --- a/src/HOL/UNITY/Mutex.ML Fri Aug 14 12:06:34 1998 +0200 +++ b/src/HOL/UNITY/Mutex.ML Fri Aug 14 13:52:42 1998 +0200 @@ -56,7 +56,6 @@ by (rtac InvariantI 1); by (Force_tac 1); by (constrains_tac cmd_defs 1); -by (REPEAT (trans_tac 1)); by (safe_tac (claset() addSEs [le_SucE])); by (Asm_full_simp_tac 1); (*Resulting state: n=1, p=false, m=4, u=false.