--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Client.ML Tue Oct 13 10:32:59 1998 +0200
@@ -0,0 +1,218 @@
+(* Title: HOL/UNITY/Client
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Distributed Resource Management System: the Client
+*)
+
+
+ (*MOVE higher-up: UNITY.thy or Traces.thy ???*)
+
+(*[| stable acts C; constrains acts (C Int A) A |] ==> stable acts (C Int A)*)
+bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
+
+
+(*"raw" notion of invariant. Yields a SET of programs*)
+Goal "[| Init F<=A; stable (Acts F) A |] ==> F : invariant A";
+by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
+qed "invariantI";
+
+Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
+ "F : invariant A ==> Invariant F A";
+by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
+qed "invariant_imp_Invariant";
+
+
+(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
+Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)";
+by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
+qed "invariant_Int";
+
+Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
+ "Invariant F A = (F : invariant (reachable F Int A))";
+by (blast_tac (claset() addIs reachable.intrs) 1);
+qed "Invariant_eq_invariant_reachable";
+
+
+bind_thm ("invariant_includes_reachable",
+ invariant_imp_Invariant RS Invariant_includes_reachable);
+
+Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
+by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable,
+ stable_reachable,
+ impOfSubs invariant_includes_reachable]) 1);
+qed "always_eq_UN_invariant";
+
+Goal "F : always A = (EX I. F: invariant I & I <= A)";
+by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
+by (Blast_tac 1);
+qed "always_iff_ex_invariant";
+
+
+Goalw [increasing_def, stable_def, constrains_def]
+ "increasing f <= increasing (length o f)";
+by Auto_tac;
+by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
+qed "increasing_length";
+
+
+Goalw [increasing_def]
+ "increasing f <= {F. ALL z::nat. stable (Acts F) {s. z < f s}}";
+by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
+by (Blast_tac 1);
+qed "increasing_less";
+
+
+Goal "[| F Join G : f localTo F; (s,s') : act; \
+\ act : Acts G; act ~: Acts F |] ==> f s' = f s";
+by (asm_full_simp_tac
+ (simpset() addsimps [localTo_def, Acts_Join, stable_def,
+ constrains_def]) 1);
+by (Blast_tac 1);
+qed "localTo_imp_equals";
+
+
+Goal "[| Stable F A; transient (Acts F) C; \
+\ reachable F <= (-A Un B Un C) |] ==> LeadsTo F A B";
+by (etac reachable_LeadsTo_weaken 1);
+by (rtac LeadsTo_Diff 1);
+by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
+by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
+qed "Stable_transient_reachable_LeadsTo";
+
+
+(**** things that definitely belong in Client.ML ****)
+
+(*split_all_tac causes a big blow-up*)
+claset_ref() := claset() delSWrapper "split_all_tac";
+
+val Client_simp = Cli_prg_def RS def_prg_simps;
+
+Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
+
+DelIffs [length_Suc_conv];
+
+(*Simplification for records*)
+Addsimps (thms"state.update_defs");
+
+
+(*CAN THIS be generalized?
+ Importantly, the second case considers actions that are in G
+ and NOT in Cli_prg (needed to use localTo_imp_equals) *)
+Goal "(act : Acts (Cli_prg Join G)) = \
+\ (act : {Id, rel_act, tok_act, ask_act} | \
+\ act : Acts G & act ~: Acts Cli_prg)";
+by (asm_full_simp_tac (simpset() addsimps [Client_simp, Acts_Join]) 1);
+(*don't unfold definitions of actions*)
+by (blast_tac HOL_cs 1);
+qed "Acts_Cli_Join_eq";
+
+
+fun invariant_tac i =
+ rtac invariantI i THEN
+ auto_tac (claset(), simpset() addsimps [Client_simp]) THEN
+ constrains_tac i;
+
+(*Safety property 1(a): ask is nondecreasing*)
+Goalw [increasing_def] "Cli_prg: increasing ask";
+by (auto_tac (claset(), simpset() addsimps [Client_simp]));
+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 (auto_tac (claset(), simpset() addsimps [Client_simp]));
+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);
+by Auto_tac;
+qed "tok_bounded";
+
+(*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 (length (ask s)). ask s!n <= Max})";
+by (invariant_tac 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+qed "ask_bounded";
+
+
+(*Safety property 2: clients return the right number of tokens*)
+Goalw [increasing_def]
+ "Cli_prg : (increasing giv Int (rel localTo Cli_prg)) \
+\ guarantees invariant {s. rel s <= giv s}";
+by (rtac guaranteesI 1);
+by (Clarify_tac 1);
+by (invariant_tac 1);
+by (subgoal_tac "rel s <= giv s'" 1);
+by (force_tac (claset(),
+ simpset() addsimps [stable_def, constrains_def]) 2);
+by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
+(*we note that "rel" is local to Client*)
+by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
+qed "ok_guar_rel_prefix_giv";
+
+
+(*** Towards proving the liveness property ***)
+
+Goal "transient (Acts (Cli_prg Join G)) \
+\ {s. length (giv s) = Suc k & \
+\ length (rel s) = k & ask s ! k <= giv s ! k}";
+by (res_inst_tac [("act", "rel_act")] transient_mem 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Domain_def, Acts_Join, Client_simp]));
+qed "transient_lemma";
+
+Goal "Cli_prg : \
+\ (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
+\ Int invariant giv_meets_ask) \
+\ guarantees invariant {s. length (ask s) <= Suc (length (rel s)) & \
+\ length (rel s) <= length (giv s)}";
+by (rtac guaranteesI 1);
+by (Clarify_tac 1);
+by (dtac (impOfSubs increasing_length) 1);
+by (invariant_tac 1);
+by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
+by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
+by (force_tac (claset(),
+ simpset() addsimps [increasing_def, Acts_Join, stable_def,
+ constrains_def]) 1);
+val lemma1 = result();
+
+
+Goal "Cli_prg : \
+\ (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
+\ Int invariant giv_meets_ask) \
+\ guarantees {F. LeadsTo F {s. k < length (giv s)} \
+\ {s. k < length (rel s)}}";
+by (rtac guaranteesI 1);
+by (Clarify_tac 1);
+by (rtac Stable_transient_reachable_LeadsTo 1);
+by (res_inst_tac [("k", "k")] transient_lemma 2);
+by (rtac stable_imp_Stable 1);
+by (dtac (impOfSubs increasing_length) 1);
+by (force_tac (claset(),
+ simpset() addsimps [increasing_def,
+ stable_def, constrains_def]) 1);
+(** LEVEL 7 **)
+(* Invariant (Cli_prg Join G)
+ (- {s. k < length (giv s)} Un {s. k < length (rel s)} Un
+ {s. length (giv s) = Suc k &
+ length (rel s) = k & ask s ! k <= giv s ! k})
+*)
+by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
+by (Blast_tac 1);
+by (auto_tac (claset() addSDs [invariant_includes_reachable],
+ simpset() addsimps [giv_meets_ask_def]));
+qed "client_correct";