--- 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";