Addition of HOL/UNITY/Client
authorpaulson
Tue Oct 13 10:32:59 1998 +0200 (1998-10-13)
changeset 5636dd8f30780fa9
parent 5635 b7d6b7f66131
child 5637 a06006a320a1
Addition of HOL/UNITY/Client
src/HOL/IsaMakefile
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Client.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 09 15:28:04 1998 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 13 10:32:59 1998 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4  
     1.5  $(LOG)/HOL-UNITY.gz: $(OUT)/HOL UNITY/ROOT.ML\
     1.6    UNITY/Channel.ML UNITY/Channel.thy UNITY/Common.ML UNITY/Common.thy\
     1.7 -  UNITY/Comp.ML UNITY/Comp.thy\
     1.8 +  UNITY/Client.ML UNITY/Client.thy  UNITY/Comp.ML UNITY/Comp.thy\
     1.9    UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/FP.ML UNITY/FP.thy\
    1.10    UNITY/Union.ML UNITY/Union.thy UNITY/Handshake.ML UNITY/Handshake.thy\
    1.11    UNITY/LessThan.ML UNITY/LessThan.thy UNITY/Mutex.ML UNITY/Mutex.thy\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Client.ML	Tue Oct 13 10:32:59 1998 +0200
     2.3 @@ -0,0 +1,218 @@
     2.4 +(*  Title:      HOL/UNITY/Client
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1998  University of Cambridge
     2.8 +
     2.9 +Distributed Resource Management System: the Client
    2.10 +*)
    2.11 +
    2.12 +
    2.13 + (*MOVE higher-up: UNITY.thy or Traces.thy ???*)
    2.14 +
    2.15 +(*[| stable acts C; constrains acts (C Int A) A |] ==> stable acts (C Int A)*)
    2.16 +bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
    2.17 +
    2.18 +
    2.19 +(*"raw" notion of invariant.  Yields a SET of programs*)
    2.20 +Goal "[| Init F<=A;  stable (Acts F) A |] ==> F : invariant A";
    2.21 +by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
    2.22 +qed "invariantI";
    2.23 +
    2.24 +Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
    2.25 +     "F : invariant A ==> Invariant F A";
    2.26 +by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
    2.27 +qed "invariant_imp_Invariant";
    2.28 +
    2.29 +
    2.30 +(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
    2.31 +Goal "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)";
    2.32 +by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
    2.33 +qed "invariant_Int";
    2.34 +
    2.35 +Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
    2.36 +     "Invariant F A = (F : invariant (reachable F Int A))";
    2.37 +by (blast_tac (claset() addIs reachable.intrs) 1);
    2.38 +qed "Invariant_eq_invariant_reachable";
    2.39 +
    2.40 +
    2.41 +bind_thm ("invariant_includes_reachable",
    2.42 +	  invariant_imp_Invariant RS Invariant_includes_reachable);
    2.43 +
    2.44 +Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
    2.45 +by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
    2.46 +                               stable_reachable,
    2.47 +			       impOfSubs invariant_includes_reachable]) 1);
    2.48 +qed "always_eq_UN_invariant";
    2.49 +
    2.50 +Goal "F : always A = (EX I. F: invariant I & I <= A)";
    2.51 +by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
    2.52 +by (Blast_tac 1);
    2.53 +qed "always_iff_ex_invariant";
    2.54 +
    2.55 +
    2.56 +Goalw [increasing_def, stable_def, constrains_def]
    2.57 +     "increasing f <= increasing (length o f)";
    2.58 +by Auto_tac;
    2.59 +by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
    2.60 +qed "increasing_length";
    2.61 +
    2.62 +
    2.63 +Goalw [increasing_def]
    2.64 +     "increasing f <= {F. ALL z::nat. stable (Acts F) {s. z < f s}}";
    2.65 +by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
    2.66 +by (Blast_tac 1);
    2.67 +qed "increasing_less";
    2.68 +
    2.69 +
    2.70 +Goal "[| F Join G : f localTo F;  (s,s') : act;  \
    2.71 +\        act : Acts G; act ~: Acts F |] ==> f s' = f s";
    2.72 +by (asm_full_simp_tac 
    2.73 +    (simpset() addsimps [localTo_def, Acts_Join, stable_def, 
    2.74 +			 constrains_def]) 1);
    2.75 +by (Blast_tac 1);
    2.76 +qed "localTo_imp_equals";
    2.77 +
    2.78 +
    2.79 +Goal "[| Stable F A;  transient (Acts F) C;  \
    2.80 +\        reachable F <= (-A Un B Un C) |] ==> LeadsTo F A B";
    2.81 +by (etac reachable_LeadsTo_weaken 1);
    2.82 +by (rtac LeadsTo_Diff 1);
    2.83 +by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
    2.84 +by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
    2.85 +qed "Stable_transient_reachable_LeadsTo";
    2.86 +
    2.87 +
    2.88 +(**** things that definitely belong in Client.ML ****)
    2.89 +
    2.90 +(*split_all_tac causes a big blow-up*)
    2.91 +claset_ref() := claset() delSWrapper "split_all_tac";
    2.92 +
    2.93 +val Client_simp = Cli_prg_def RS def_prg_simps;
    2.94 +
    2.95 +Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
    2.96 +
    2.97 +DelIffs [length_Suc_conv];
    2.98 +
    2.99 +(*Simplification for records*)
   2.100 +Addsimps (thms"state.update_defs");
   2.101 +
   2.102 +
   2.103 +(*CAN THIS be generalized?
   2.104 +  Importantly, the second case considers actions that are in G
   2.105 +  and NOT in Cli_prg (needed to use localTo_imp_equals) *)
   2.106 +Goal "(act : Acts (Cli_prg Join G)) = \
   2.107 +\      (act : {Id, rel_act, tok_act, ask_act} | \
   2.108 +\       act : Acts G & act ~: Acts Cli_prg)";
   2.109 +by (asm_full_simp_tac (simpset() addsimps [Client_simp, Acts_Join]) 1);
   2.110 +(*don't unfold definitions of actions*)
   2.111 +by (blast_tac HOL_cs 1);
   2.112 +qed "Acts_Cli_Join_eq";
   2.113 +
   2.114 +
   2.115 +fun invariant_tac i = 
   2.116 +    rtac invariantI i  THEN
   2.117 +    auto_tac (claset(), simpset() addsimps [Client_simp])  THEN
   2.118 +    constrains_tac i;
   2.119 +
   2.120 +(*Safety property 1(a): ask is nondecreasing*)
   2.121 +Goalw [increasing_def] "Cli_prg: increasing ask";
   2.122 +by (auto_tac (claset(), simpset() addsimps [Client_simp]));
   2.123 +by (constrains_tac 1);
   2.124 +by Auto_tac;
   2.125 +qed "increasing_ask";
   2.126 +
   2.127 +(*Safety property 1(b): rel is nondecreasing*)
   2.128 +Goalw [increasing_def] "Cli_prg: increasing rel";
   2.129 +by (auto_tac (claset(), simpset() addsimps [Client_simp]));
   2.130 +by (constrains_tac 1);
   2.131 +by Auto_tac;
   2.132 +qed "increasing_rel";
   2.133 +
   2.134 +Addsimps [nth_append, append_one_prefix];
   2.135 +
   2.136 +Goal "Cli_prg: invariant {s. tok s <= Max}";
   2.137 +by (invariant_tac 1);
   2.138 +by Auto_tac;
   2.139 +qed "tok_bounded";
   2.140 +
   2.141 +(*Safety property 3: no client requests "too many" tokens.
   2.142 +      With no Substitution Axiom, we must prove the two invariants 
   2.143 +  simultaneously.  Could combine tok_bounded, stable_constrains_stable 
   2.144 +  and a rule invariant_implies_stable...
   2.145 +*)
   2.146 +Goal "Cli_prg:                             \
   2.147 +\       invariant ({s. tok s <= Max}  Int  \
   2.148 +\                  {s. ALL n: lessThan (length (ask s)). ask s!n <= Max})";
   2.149 +by (invariant_tac 1);
   2.150 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
   2.151 +qed "ask_bounded";
   2.152 +
   2.153 +
   2.154 +(*Safety property 2: clients return the right number of tokens*)
   2.155 +Goalw [increasing_def]
   2.156 +      "Cli_prg : (increasing giv Int (rel localTo Cli_prg))  \
   2.157 +\                guarantees invariant {s. rel s <= giv s}";
   2.158 +by (rtac guaranteesI 1);
   2.159 +by (Clarify_tac 1);
   2.160 +by (invariant_tac 1);
   2.161 +by (subgoal_tac "rel s <= giv s'" 1);
   2.162 +by (force_tac (claset(),
   2.163 +	       simpset() addsimps [stable_def, constrains_def]) 2);
   2.164 +by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
   2.165 +(*we note that "rel" is local to Client*)
   2.166 +by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
   2.167 +qed "ok_guar_rel_prefix_giv";
   2.168 +
   2.169 +
   2.170 +(*** Towards proving the liveness property ***)
   2.171 +
   2.172 +Goal "transient (Acts (Cli_prg Join G))   \
   2.173 +\               {s. length (giv s) = Suc k &  \
   2.174 +\                   length (rel s) = k & ask s ! k <= giv s ! k}";
   2.175 +by (res_inst_tac [("act", "rel_act")] transient_mem 1);
   2.176 +by (auto_tac (claset(),
   2.177 +	      simpset() addsimps [Domain_def, Acts_Join, Client_simp]));
   2.178 +qed "transient_lemma";
   2.179 +
   2.180 +Goal "Cli_prg : \
   2.181 +\      (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
   2.182 +\                 Int invariant giv_meets_ask) \
   2.183 +\      guarantees invariant {s. length (ask s) <= Suc (length (rel s)) & \
   2.184 +\                               length (rel s) <= length (giv s)}";
   2.185 +by (rtac guaranteesI 1);
   2.186 +by (Clarify_tac 1);
   2.187 +by (dtac (impOfSubs increasing_length) 1);
   2.188 +by (invariant_tac 1);
   2.189 +by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
   2.190 +by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
   2.191 +by (force_tac (claset(),
   2.192 +	       simpset() addsimps [increasing_def, Acts_Join, stable_def, 
   2.193 +				   constrains_def]) 1);
   2.194 +val lemma1 = result();
   2.195 +
   2.196 +
   2.197 +Goal "Cli_prg : \
   2.198 +\      (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
   2.199 +\                 Int invariant giv_meets_ask) \
   2.200 +\      guarantees {F. LeadsTo F {s. k < length (giv s)}    \
   2.201 +\                               {s. k < length (rel s)}}";
   2.202 +by (rtac guaranteesI 1);
   2.203 +by (Clarify_tac 1);
   2.204 +by (rtac Stable_transient_reachable_LeadsTo 1);
   2.205 +by (res_inst_tac [("k", "k")] transient_lemma 2);
   2.206 +by (rtac stable_imp_Stable 1);
   2.207 +by (dtac (impOfSubs increasing_length) 1);
   2.208 +by (force_tac (claset(),
   2.209 +	       simpset() addsimps [increasing_def, 
   2.210 +				   stable_def, constrains_def]) 1);
   2.211 +(** LEVEL 7 **)
   2.212 +(*         Invariant (Cli_prg Join G)
   2.213 +              (- {s. k < length (giv s)} Un {s. k < length (rel s)} Un
   2.214 +               {s. length (giv s) = Suc k &
   2.215 +                   length (rel s) = k & ask s ! k <= giv s ! k})
   2.216 +*)
   2.217 +by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
   2.218 +by (Blast_tac 1);
   2.219 +by (auto_tac (claset() addSDs [invariant_includes_reachable],
   2.220 +	      simpset() addsimps [giv_meets_ask_def]));
   2.221 +qed "client_correct";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Client.thy	Tue Oct 13 10:32:59 1998 +0200
     3.3 @@ -0,0 +1,80 @@
     3.4 +(*  Title:      HOL/UNITY/Client.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1998  University of Cambridge
     3.8 +
     3.9 +Distributed Resource Management System: the Client
    3.10 +*)
    3.11 +
    3.12 +Client = Comp + Prefix + 
    3.13 +
    3.14 +constdefs  (*MOVE higher-up: UNITY.thy or Traces.thy ???*)
    3.15 +  always :: "'a set => 'a program set"
    3.16 +    "always A == {F. reachable F <= A}"
    3.17 +
    3.18 +  (*The traditional word for inductive properties.  Anyway, INDUCTIVE is
    3.19 +    reserved!*)
    3.20 +  invariant :: "'a set => 'a program set"
    3.21 +    "invariant A == {F. Init F <= A & stable (Acts F) A}"
    3.22 +
    3.23 +  (*Polymorphic in both states and the meaning of <= *)
    3.24 +  increasing :: "['a => 'b::{ord}] => 'a program set"
    3.25 +    "increasing f == {F. ALL z. stable (Acts F) {s. z <= f s}}"
    3.26 +
    3.27 +  (*The set of systems that regard "f" as local to F*)
    3.28 +  localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
    3.29 +    "f localTo F == {G. ALL z. stable (Acts G - Acts F) {s. f s = z}}"
    3.30 +
    3.31 +
    3.32 +consts
    3.33 +  Max :: nat       (*Maximum number of tokens*)
    3.34 +
    3.35 +types
    3.36 +  tokbag = nat	   (*tokbags could be multisets...or any ordered type?*)
    3.37 +
    3.38 +record state =
    3.39 +  giv :: tokbag list   (*input history: tokens granted*)
    3.40 +  ask :: tokbag list   (*output history: tokens requested*)
    3.41 +  rel :: tokbag list   (*output history: tokens released*)
    3.42 +  tok :: tokbag	       (*current token request*)
    3.43 +
    3.44 +
    3.45 +(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
    3.46 +
    3.47 +constdefs
    3.48 +  
    3.49 +  (** Release some tokens **)
    3.50 +  
    3.51 +  rel_act :: "(state*state) set"
    3.52 +    "rel_act == {(s,s').
    3.53 +		  EX nrel. nrel = length (rel s) &
    3.54 +		           s' = s (| rel := rel s @ [giv s!nrel] |) &
    3.55 +		           nrel < length (giv s) &
    3.56 +		           ask s!nrel <= giv s!nrel}"
    3.57 +
    3.58 +  (** Choose a new token requirement **)
    3.59 +
    3.60 +  (** Including s'=s suppresses fairness, allowing the non-trivial part
    3.61 +      of the action to be ignored **)
    3.62 +
    3.63 +  tok_act :: "(state*state) set"
    3.64 +    "tok_act == {(s,s'). s'=s | (EX t: atMost Max. s' = s (|tok := t|))}"
    3.65 +
    3.66 +  ask_act :: "(state*state) set"
    3.67 +    "ask_act == {(s,s'). s'=s |
    3.68 +		         (s' = s (|ask := ask s @ [tok s]|) &
    3.69 +		          length (ask s) = length (rel s))}"
    3.70 +
    3.71 +  Cli_prg :: state program
    3.72 +    "Cli_prg == mk_program ({s. tok s : atMost Max &
    3.73 +			        giv s = [] &
    3.74 +			        ask s = [] &
    3.75 +			        rel s = []},
    3.76 +			    {rel_act, tok_act, ask_act})"
    3.77 +
    3.78 +  giv_meets_ask :: state set
    3.79 +    "giv_meets_ask ==
    3.80 +       {s. length (giv s) <= length (ask s) & 
    3.81 +           (ALL n: lessThan (length (giv s)). ask s!n <= giv s!n)}"
    3.82 +
    3.83 +end