--- a/src/HOL/UNITY/Client.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Client.ML Wed Feb 09 11:45:10 2000 +0100
@@ -6,9 +6,8 @@
Distributed Resource Management System: the Client
*)
-
-Addsimps [Cli_prg_def RS def_prg_Init];
-program_defs_ref := [Cli_prg_def];
+Addsimps [Client_def RS def_prg_Init];
+program_defs_ref := [Client_def];
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
@@ -17,121 +16,150 @@
rtac invariantI i THEN
constrains_tac (i+1);
-(*Safety property 1(a): ask is nondecreasing*)
-Goalw [increasing_def] "Cli_prg: increasing ask";
-by (Clarify_tac 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "increasing_ask";
-(*Safety property 1(b): rel is nondecreasing*)
-Goalw [increasing_def] "Cli_prg: increasing rel";
-by (Clarify_tac 1);
-by (constrains_tac 1);
+(*Safety property 1: ask, rel are increasing*)
+Goal "Client: UNIV guarantees[funPair rel ask] \
+\ Increasing ask Int Increasing rel";
+by (safe_tac (claset() addSIs [guaranteesI,increasing_imp_Increasing]));
+by (auto_tac
+ (claset(),
+ simpset() addsimps [impOfSubs preserves_subset_increasing,
+ Join_increasing]));
+by (auto_tac (claset(), simpset() addsimps [increasing_def]));
+by (ALLGOALS constrains_tac);
by Auto_tac;
-qed "increasing_rel";
+qed "increasing_ask_rel";
+
Addsimps [nth_append, append_one_prefix];
-Goal "Cli_prg: invariant {s. tok s <= Max}";
-by (invariant_tac 1);
-by Auto_tac;
-qed "tok_bounded";
-(*Safety property 3: no client requests "too many" tokens.
+(*Safety property 2: the client never requests too many tokens.
With no Substitution Axiom, we must prove the two invariants
- simultaneously. Could combine tok_bounded, stable_constrains_stable
- and a rule invariant_implies_stable...
+ simultaneously.
*)
-Goal "Cli_prg: \
-\ invariant ({s. tok s <= Max} Int \
-\ {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})";
-by (invariant_tac 1);
-by (auto_tac (claset() addSEs [less_SucE], simpset()));
+Goal "G : preserves (funPair ask tok) \
+\ ==> Client Join G : \
+\ Always ({s. tok s <= NbT} Int \
+\ {s. ALL elt : set (ask s). elt <= NbT})";
+by (rtac (invariantI RS stable_Join_Always2) 1);
+by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
+ addSIs [stable_Int]) 3);
+by (constrains_tac 2);
+by Auto_tac;
+qed "ask_bounded_lemma";
+
+(*export version, with no mention of tok*)
+Goal "Client: UNIV guarantees[funPair ask tok] \
+\ Always {s. ALL elt : set (ask s). elt <= NbT}";
+by (rtac guaranteesI 1);
+by (etac (ask_bounded_lemma RS Always_weaken) 1);
+by (rtac Int_lower2 1);
qed "ask_bounded";
-(** Several facts used to prove Lemma 1 **)
-Goal "Cli_prg: stable {s. rel s <= giv s}";
+(*** Towards proving the liveness property ***)
+
+Goal "Client: stable {s. rel s <= giv s}";
by (constrains_tac 1);
by Auto_tac;
qed "stable_rel_le_giv";
-Goal "Cli_prg: stable {s. size (rel s) <= size (giv s)}";
+Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
+\ ==> Client Join G : Stable {s. rel s <= giv s}";
+by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1);
+by Auto_tac;
+qed "Join_Stable_rel_le_giv";
+
+Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
+\ ==> Client Join G : Always {s. rel s <= giv s}";
+by (rtac AlwaysI 1);
+by (rtac Join_Stable_rel_le_giv 2);
+by Auto_tac;
+qed "Join_Always_rel_le_giv";
+
+Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
+by (res_inst_tac [("act", "rel_act")] transientI 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Domain_def, Client_def]));
+by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
+ strict_prefix_length_less]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
+by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
+qed "transient_lemma";
+
+
+
+Goal "[| Client Join G : Increasing giv; G : preserves (funPair rel ask) |] \
+\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s} \
+\ LeadsTo {s. k < rel s & rel s <= giv s & \
+\ h <= giv s & h pfixGe ask s}";
+by (rtac single_LeadsTo_I 1);
+by (ftac (increasing_ask_rel RS guaranteesD) 1);
+by Auto_tac;
+by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS
+ leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
+by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
+by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
+by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
+by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
+by (etac Join_Stable_rel_le_giv 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addIs [sym, order_less_le RS iffD2,
+ order_trans, prefix_imp_pfixGe,
+ pfixGe_trans]) 2);
+by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
+qed "induct_lemma";
+
+
+Goal "[| Client Join G : Increasing giv; G : preserves (funPair rel ask) |] \
+\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s} \
+\ LeadsTo {s. h <= rel s}";
+by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
+by (auto_tac (claset(), simpset() addsimps [vimage_def]));
+by (rtac single_LeadsTo_I 1);
+by (rtac (induct_lemma RS LeadsTo_weaken) 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [order_less_le RS iffD2]
+ addDs [common_prefix_linear]) 1);
+by (REPEAT (dtac strict_prefix_length_less 1));
+by (arith_tac 1);
+qed "rel_progress_lemma";
+
+
+Goal "[| Client Join G : Increasing giv; G : preserves (funPair rel ask) |] \
+\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s} \
+\ LeadsTo {s. h <= rel s}";
+by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
+by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS
+ LeadsTo_Un RS LeadsTo_weaken_L) 3);
+by Auto_tac;
+by (blast_tac (claset() addIs [order_less_le RS iffD2]
+ addDs [common_prefix_linear]) 1);
+qed "client_progress_lemma";
+
+Goal "Client : \
+\ Increasing giv guarantees[funPair rel ask] \
+\ (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
+by (rtac guaranteesI 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [client_progress_lemma]) 1);
+qed "client_progress";
+
+
+(** Obsolete lemmas from first version of the Client **)
+
+Goal "Client: stable {s. size (rel s) <= size (giv s)}";
by (constrains_tac 1);
by Auto_tac;
qed "stable_size_rel_le_giv";
-Goal "Cli_prg: stable {s. size (ask s) <= Suc (size (rel s))}";
-by (constrains_tac 1);
-by Auto_tac;
-qed "stable_size_ask_le_rel";
-
-
-(*We no longer need constrains_tac to expand the program definition, and
- expanding it is extremely expensive!*)
-program_defs_ref := [];
-
-(*Safety property 2: clients return the right number of tokens*)
-Goal "Cli_prg : Increasing giv guarantees[rel] Always {s. rel s <= giv s}";
+(*clients return the right number of tokens*)
+Goal "Client : Increasing giv guarantees[rel] Always {s. rel s <= giv s}";
by (rtac guaranteesI 1);
by (rtac AlwaysI 1);
by (Force_tac 1);
by (blast_tac (claset() addIs [Increasing_preserves_Stable,
stable_rel_le_giv]) 1);
qed "ok_guar_rel_prefix_giv";
-
-
-(*** Towards proving the liveness property ***)
-
-Goal "Cli_prg Join G \
-\ : transient {s. size (giv s) = Suc k & \
-\ size (rel s) = k & ask s ! k <= giv s ! k}";
-by (res_inst_tac [("act", "rel_act")] transientI 1);
-by (auto_tac (claset(),
- simpset() addsimps [Domain_def, Cli_prg_def]));
-qed "transient_lemma";
-
-
-
-val rewrite_o = rewrite_rule [o_def];
-
-val Increasing_length = mono_length RS mono_Increasing_o;
-
-Goal "Cli_prg : \
-\ Increasing giv guarantees[funPair rel ask] \
-\ Always ({s. size (ask s) <= Suc (size (rel s))} Int \
-\ {s. size (rel s) <= size (giv s)})";
-by (rtac guaranteesI 1);
-by (dtac (impOfSubs (rewrite_o Increasing_length)) 1);
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (rtac Stable_Int 1);
-by (fast_tac (claset() addEs [rewrite_o (impOfSubs subset_preserves_o)]
- addIs [Increasing_preserves_Stable,
- stable_size_rel_le_giv]) 2);
-by (res_inst_tac [("v1", "ask"), ("w1", "rel")]
- (stable_localTo_stable2 RS stable_imp_Stable) 1);
-by (ALLGOALS
- (fast_tac (claset() addEs [rewrite_o (impOfSubs subset_preserves_o)]
- addIs [stable_size_ask_le_rel])));
-val lemma1 = result();
-
-
-Goal "Cli_prg : \
-\ Increasing giv Int Always giv_meets_ask \
-\ guarantees[funPair rel ask] \
-\ ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
-by (rtac guaranteesI 1);
-by (Clarify_tac 1);
-by (rtac Stable_transient_Always_LeadsTo 1);
-by (res_inst_tac [("k", "k")] transient_lemma 2);
-by (force_tac (claset() addDs [impOfSubs Increasing_length,
- impOfSubs Increasing_Stable_less],
- simpset()) 1);
-by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
-by Auto_tac;
-by (force_tac (claset(),
- simpset() addsimps [Always_eq_includes_reachable,
- giv_meets_ask_def]) 1);
-qed "client_correct";
--- a/src/HOL/UNITY/Client.thy Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Client.thy Wed Feb 09 11:45:10 2000 +0100
@@ -6,10 +6,10 @@
Distributed Resource Management System: the Client
*)
-Client = Guar +
+Client = Extend +
consts
- Max :: nat (*Maximum number of tokens*)
+ NbT :: nat (*Maximum number of tokens*)
types
tokbag = nat (*tokbags could be multisets...or any ordered type?*)
@@ -40,19 +40,21 @@
of the action to be ignored **)
tok_act :: "(state*state) set"
- "tok_act == {(s,s'). s'=s | (EX t: atMost Max. s' = s (|tok := t|))}"
+ "tok_act == {(s,s'). s'=s | (EX t: atMost NbT. s' = s (|tok := t|))}"
+ (*
+ "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
+ *)
+
+
ask_act :: "(state*state) set"
"ask_act == {(s,s'). s'=s |
- (s' = s (|ask := ask s @ [tok s]|) &
- size (ask s) = size (rel s))}"
+ (s' = s (|ask := ask s @ [tok s]|))}"
- Cli_prg :: state program
- "Cli_prg == mk_program ({s. tok s : atMost Max &
- giv s = [] &
- ask s = [] &
- rel s = []},
- {rel_act, tok_act, ask_act})"
+ Client :: state program
+ "Client == mk_program ({s. tok s : atMost NbT &
+ giv s = [] & ask s = [] & rel s = []},
+ {rel_act, tok_act, ask_act})"
giv_meets_ask :: state set
"giv_meets_ask ==
--- a/src/HOL/UNITY/Comp.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Comp.ML Wed Feb 09 11:45:10 2000 +0100
@@ -132,6 +132,12 @@
by (ALLGOALS Force_tac);
qed "preserves_subset_stable";
+Goal "preserves v <= increasing v";
+by (auto_tac (claset(),
+ simpset() addsimps [impOfSubs preserves_subset_stable,
+ increasing_def]));
+qed "preserves_subset_increasing";
+
Goal "preserves id <= stable A";
by (force_tac (claset(),
simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
--- a/src/HOL/UNITY/Constrains.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Constrains.ML Wed Feb 09 11:45:10 2000 +0100
@@ -203,6 +203,11 @@
(*** Increasing ***)
+Goalw [Increasing_def]
+ "F : Increasing f ==> F : Stable {s. x <= f s}";
+by (Blast_tac 1);
+qed "IncreasingD";
+
Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
"mono g ==> Increasing f <= Increasing (g o f)";
by Auto_tac;
@@ -210,10 +215,10 @@
qed "mono_Increasing_o";
Goalw [Increasing_def]
- "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}";
+ "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}";
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
by (Blast_tac 1);
-qed "Increasing_Stable_less";
+qed "strict_IncreasingD";
Goalw [increasing_def, Increasing_def]
"F : increasing f ==> F : Increasing f";
--- a/src/HOL/UNITY/Extend.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Extend.ML Wed Feb 09 11:45:10 2000 +0100
@@ -203,6 +203,9 @@
(*** extend_act ***)
+(*Can't strengthen it to
+ ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y')
+ because h doesn't have to be injective in the 2nd argument*)
Goalw [extend_act_def]
"((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)";
by Auto_tac;
--- a/src/HOL/UNITY/Follows.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Follows.ML Wed Feb 09 11:45:10 2000 +0100
@@ -110,11 +110,6 @@
by (Blast_tac 1);
qed "Always_Un";
-Goalw [Increasing_def]
- "F : Increasing f ==> F : Stable {s. x <= f s}";
-by (Blast_tac 1);
-qed "IncreasingD";
-
(*Lemma to re-use the argument that one variable increases (progress)
while the other variable doesn't decrease (safety)*)
Goal "[| F : Increasing f; F : Increasing g; \
--- a/src/HOL/UNITY/GenPrefix.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/GenPrefix.ML Wed Feb 09 11:45:10 2000 +0100
@@ -278,6 +278,15 @@
by (etac genPrefix_length_le 1);
qed "prefix_length_le";
+Goalw [prefix_def] "xs<=ys ==> xs~=ys --> length xs < length ys";
+by (etac genPrefix.induct 1);
+by Auto_tac;
+val lemma = result();
+
+Goalw [strict_prefix_def] "xs < ys ==> length xs < length ys";
+by (blast_tac (claset() addIs [lemma RS mp]) 1);
+qed "strict_prefix_length_less";
+
Goal "mono length";
by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1);
qed "mono_length";
@@ -313,6 +322,13 @@
by (Force_tac 1);
qed "prefix_append_iff";
+(*Although the prefix ordering is not linear, the prefixes of a list
+ are linearly ordered.*)
+Goal "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs";
+by (rev_induct_tac "zs" 1);
+by Auto_tac;
+qed_spec_mp "common_prefix_linear";
+
Goal "r<=s ==> genPrefix r <= genPrefix s";
by (Clarify_tac 1);
by (etac genPrefix.induct 1);
--- a/src/HOL/UNITY/Lift_prog.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML Wed Feb 09 11:45:10 2000 +0100
@@ -122,7 +122,7 @@
fun lift_export0 th =
good_map_lift_map RS export th
- |> simplify (simpset() addsimps [fold_o_sub]);;
+ |> simplify (simpset() addsimps [fold_o_sub]);
Goal "fst (inv (lift_map i) g) = g i";
by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
--- a/src/HOL/UNITY/SubstAx.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/SubstAx.ML Wed Feb 09 11:45:10 2000 +0100
@@ -129,7 +129,7 @@
(** Two theorems for "proof lattices" **)
-Goal "[| F : A LeadsTo B |] ==> F : (A Un B) LeadsTo B";
+Goal "F : A LeadsTo B ==> F : (A Un B) LeadsTo B";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
qed "LeadsTo_Un_post";
@@ -334,11 +334,11 @@
qed "Bounded_induct";
-Goal "[| ALL m. F : (A Int f-``{m}) LeadsTo \
-\ ((A Int f-``(lessThan m)) Un B) |] \
+val prems =
+Goal "(!! m. F : (A Int f-``{m}) LeadsTo ((A Int f-``(lessThan m)) Un B)) \
\ ==> F : A LeadsTo B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
-by (Asm_simp_tac 1);
+by (auto_tac (claset() addIs prems, simpset()));
qed "LessThan_induct";
(*Integer version. Could generalize from #0 to any lower bound*)
@@ -347,7 +347,7 @@
\ !! z. F : (A Int {s. f s = z}) LeadsTo \
\ ((A Int {s. f s < z}) Un B) |] \
\ ==> F : A LeadsTo B";
-by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
+by (res_inst_tac [("f", "nat o f")] LessThan_induct 1);
by (simp_tac (simpset() addsimps [vimage_def]) 1);
by (rtac ([reach, prem] MRS Always_LeadsTo_weaken) 1);
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
--- a/src/HOL/UNITY/UNITY.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/UNITY.ML Wed Feb 09 11:45:10 2000 +0100
@@ -306,17 +306,23 @@
(*** increasing ***)
+Goalw [increasing_def]
+ "F : increasing f ==> F : stable {s. z <= f s}";
+by (Blast_tac 1);
+qed "increasingD";
+
Goalw [increasing_def, stable_def, constrains_def]
"mono g ==> increasing f <= increasing (g o f)";
by Auto_tac;
by (blast_tac (claset() addIs [monoD, order_trans]) 1);
qed "mono_increasing_o";
+(*Holds by the theorem (Suc m <= n) = (m < n) *)
Goalw [increasing_def]
- "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}";
+ "!!z::nat. F : increasing f ==> F: stable {s. z < f s}";
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
by (Blast_tac 1);
-qed "increasing_stable_less";
+qed "strict_increasingD";
(** The Elimination Theorem. The "free" m has become universally quantified!
--- a/src/HOL/UNITY/Union.ML Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Union.ML Wed Feb 09 11:45:10 2000 +0100
@@ -250,6 +250,14 @@
Join_def]));
qed "Join_transient";
+Goal "F : transient A ==> F Join G : transient A";
+by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
+qed "Join_transient_I1";
+
+Goal "G : transient A ==> F Join G : transient A";
+by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
+qed "Join_transient_I2";
+
Goal "i : I ==> \
\ (JN i:I. F i) : A ensures B = \
\ ((ALL i:I. F i : (A-B) co (A Un B)) & \
@@ -279,7 +287,13 @@
by (full_simp_tac (simpset() addsimps [Always_def, invariant_def,
Stable_eq_stable, Join_stable]) 1);
by (force_tac(claset() addIs [stable_Int], simpset()) 1);
-qed "stable_Join_Always";
+qed "stable_Join_Always1";
+
+(*As above, but exchanging the roles of F and G*)
+Goal "[| F : invariant A; G : stable A |] ==> F Join G : Always A";
+by (stac Join_commute 1);
+by (blast_tac (claset() addIs [stable_Join_Always1]) 1);
+qed "stable_Join_Always2";
Goal "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B";
by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1);