src/HOL/UNITY/Client.ML

     Copyright   1998  University of Cambridge
 
 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]);
 
 
 fun invariant_tac i = 
     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);
+
+(*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_ask";
+qed "increasing_ask_rel";
 
-(*Safety property 1(b): rel is nondecreasing*)
-Goalw [increasing_def] "Cli_prg: increasing rel";
-by (Clarify_tac 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "increasing_rel";
 
 Addsimps [nth_append, append_one_prefix];
 
-Goal "Cli_prg: invariant {s. tok s <= Max}";
-by (invariant_tac 1);
+
+(*Safety property 2: the client never requests too many tokens.
+      With no Substitution Axiom, we must prove the two invariants 
+  simultaneously.
+*)
+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 "tok_bounded";
+qed "ask_bounded_lemma";
 
-(*Safety property 3: no client 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...
-*)
-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()));
+(*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";