1.1 --- a/src/HOL/UNITY/Handshake.ML Fri Aug 14 12:06:34 1998 +0200
1.2 +++ b/src/HOL/UNITY/Handshake.ML Fri Aug 14 13:52:42 1998 +0200
1.3 @@ -50,7 +50,6 @@
1.4 by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
1.5 GreaterThan_bounded_induct 1);
1.6 by (auto_tac (claset(), simpset() addsimps [vimage_def]));
1.7 -by (trans_tac 2);
1.8 (*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
1.9 by (rtac LeadsTo_Diff 1);
1.10 by (rtac lemma2_2 2);
2.1 --- a/src/HOL/UNITY/LessThan.ML Fri Aug 14 12:06:34 1998 +0200
2.2 +++ b/src/HOL/UNITY/LessThan.ML Fri Aug 14 13:52:42 1998 +0200
2.3 @@ -7,6 +7,9 @@
2.4 *)
2.5
2.6
2.7 +claset_ref() := claset() addaltern ("trans_tac",trans_tac);
2.8 +
2.9 +
2.10 (*** lessThan ***)
2.11
2.12 Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
3.1 --- a/src/HOL/UNITY/Lift.ML Fri Aug 14 12:06:34 1998 +0200
3.2 +++ b/src/HOL/UNITY/Lift.ML Fri Aug 14 13:52:42 1998 +0200
3.3 @@ -33,10 +33,18 @@
3.4 moving_up_def, moving_down_def];
3.5
3.6
3.7 +val nat_exhaust_less_pred =
3.8 + read_instantiate_sg (sign_of thy) [("P", "?m < ?y-1")] nat.exhaust;
3.9 +
3.10 +val nat_exhaust_le_pred =
3.11 + read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
3.12 +
3.13 +val nat_exhaust_pred_le =
3.14 + read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
3.15 +
3.16 Goal "0 < n ==> (m <= n-1) = (m<n)";
3.17 by (exhaust_tac "n" 1);
3.18 by Auto_tac;
3.19 -by (REPEAT_FIRST trans_tac);
3.20 qed "le_pred_eq";
3.21
3.22 Goal "m < n ==> m <= n-1";
3.23 @@ -82,57 +90,44 @@
3.24 qed "moving_down";
3.25
3.26
3.27 -xxxxxxxxxxxxxxxx;
3.28 -
3.29 -Goalw [Lprg_def] "Invariant Lprg bounded";
3.30 +Goal "Invariant Lprg bounded";
3.31 by (rtac InvariantI 1);
3.32 +br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2;
3.33 +bw Lprg_def;
3.34 by (Force_tac 1);
3.35 by (constrains_tac (cmd_defs@always_defs) 1);
3.36 -by (ALLGOALS
3.37 - (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq])));
3.38 -by (REPEAT_FIRST trans_tac);
3.39 -by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1);
3.40 -by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1);
3.41 -by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3);
3.42 +by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le]));
3.43 +by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
3.44 +by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]));
3.45 qed "bounded";
3.46
3.47 -Goalw [Lprg_def] "Invariant Lprg invariantV";
3.48 -by (rtac InvariantI 1);
3.49 -by (constrains_tac cmd_defs 2);
3.50 -by Auto_tac;
3.51 -qed "invariantV";
3.52
3.53 -val invariantUV = invariant_Int_rule [invariantU, invariantV];
3.54
3.55 +(*** Progress ***)
3.56
3.57 -(*The safety property: mutual exclusion*)
3.58 -Goal "(reachable Lprg) Int {s. MM s = 3 & NN s = 3} = {}";
3.59 -by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
3.60 -by Auto_tac;
3.61 -qed "mutual_exclusion";
3.62
3.63 +val abbrev_defs = [moving_def, stopped_def,
3.64 + opened_def, closed_def, atFloor_def];
3.65
3.66 -(*** Progress for U ***)
3.67 +val defs = cmd_defs@always_defs@abbrev_defs;
3.68
3.69 -Goalw [unless_def] "unless (Acts Lprg) {s. MM s=2} {s. MM s=3}";
3.70 -by (constrains_tac cmd_defs 1);
3.71 -qed "U_F0";
3.72 +(***
3.73
3.74 -Goal "LeadsTo Lprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
3.75 -by (ensures_tac cmd_defs "cmd1U" 1);
3.76 +Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
3.77 +by (ensures_tac defs "open_act" 1);
3.78 qed "U_F1";
3.79
3.80 Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
3.81 by (cut_facts_tac [invariantUV] 1);
3.82 by (rewtac Lprg_def);
3.83 -by (ensures_tac cmd_defs "cmd2U" 1);
3.84 +by (ensures_tac defs "cmd2U" 1);
3.85 qed "U_F2";
3.86
3.87 Goal "LeadsTo Lprg {s. MM s = 3} {s. PP s}";
3.88 by (rtac leadsTo_imp_LeadsTo 1);
3.89 by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
3.90 -by (ensures_tac cmd_defs "cmd4U" 2);
3.91 -by (ensures_tac cmd_defs "cmd3U" 1);
3.92 +by (ensures_tac defs "cmd4U" 2);
3.93 +by (ensures_tac defs "cmd3U" 1);
3.94 qed "U_F3";
3.95
3.96 Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}";
3.97 @@ -142,3 +137,4 @@
3.98 by (auto_tac (claset() addSEs [less_SucE], simpset()));
3.99 val U_lemma2 = result();
3.100
3.101 +***)
4.1 --- a/src/HOL/UNITY/Lift.thy Fri Aug 14 12:06:34 1998 +0200
4.2 +++ b/src/HOL/UNITY/Lift.thy Fri Aug 14 13:52:42 1998 +0200
4.3 @@ -27,25 +27,44 @@
4.4
4.5 (** Abbreviations: the "always" part **)
4.6
4.7 - above :: "state set"
4.8 + above :: state set
4.9 "above == {s. EX i. floor s < i & i <= max & i : req s}"
4.10
4.11 - below :: "state set"
4.12 + below :: state set
4.13 "below == {s. EX i. min <= i & i < floor s & i : req s}"
4.14
4.15 - queueing :: "state set"
4.16 + queueing :: state set
4.17 "queueing == above Un below"
4.18
4.19 - goingup :: "state set"
4.20 + goingup :: state set
4.21 "goingup == above Int ({s. up s} Un Compl below)"
4.22
4.23 - goingdown :: "state set"
4.24 + goingdown :: state set
4.25 "goingdown == below Int ({s. ~ up s} Un Compl above)"
4.26
4.27 - ready :: "state set"
4.28 + ready :: state set
4.29 "ready == {s. stop s & ~ open s & move s}"
4.30
4.31 +
4.32 + (** Further abbreviations **)
4.33
4.34 + moving :: state set
4.35 + "moving == {s. ~ stop s & ~ open s}"
4.36 +
4.37 + stopped :: state set
4.38 + "stopped == {s. stop s & ~ open s & move s}"
4.39 +
4.40 + opened :: state set
4.41 + "opened == {s. stop s & open s & move s}"
4.42 +
4.43 + closed :: state set
4.44 + "closed == {s. stop s & ~ open s & move s}"
4.45 +
4.46 + atFloor :: nat => state set
4.47 + "atFloor n == {s. floor s = n}"
4.48 +
4.49 +
4.50 +
4.51 (** The program **)
4.52
4.53 request_act :: "(state*state) set"
4.54 @@ -99,11 +118,6 @@
4.55 bounded :: state set
4.56 "bounded == {s. min <= floor s & floor s <= max}"
4.57
4.58 - (** ???
4.59 - (~ stop s & up s --> floor s < max) &
4.60 - (~ stop s & ~ up s --> min < floor s)}"
4.61 - **)
4.62 -
4.63 open_stop :: state set
4.64 "open_stop == {s. open s --> stop s}"
4.65
4.66 @@ -121,7 +135,8 @@
4.67 "moving_down == {s. ~ stop s & ~ up s -->
4.68 (EX f. min <= f & f <= floor s & f : req s)}"
4.69
4.70 - valid :: "state set"
4.71 + (*intersection of all invariants: NECESSARY??*)
4.72 + valid :: state set
4.73 "valid == bounded Int open_stop Int open_move"
4.74
4.75 end
5.1 --- a/src/HOL/UNITY/Mutex.ML Fri Aug 14 12:06:34 1998 +0200
5.2 +++ b/src/HOL/UNITY/Mutex.ML Fri Aug 14 13:52:42 1998 +0200
5.3 @@ -56,7 +56,6 @@
5.4 by (rtac InvariantI 1);
5.5 by (Force_tac 1);
5.6 by (constrains_tac cmd_defs 1);
5.7 -by (REPEAT (trans_tac 1));
5.8 by (safe_tac (claset() addSEs [le_SucE]));
5.9 by (Asm_full_simp_tac 1);
5.10 (*Resulting state: n=1, p=false, m=4, u=false.