src/HOL/UNITY/Client.ML
author paulson
Mon Oct 11 10:53:39 1999 +0200 (1999-10-11)
changeset 7826 c6a8b73b6c2a
parent 7594 8a188ef6545e
child 7878 43b03d412b82
permissions -rw-r--r--
working shapshot with "projecting" and "extending"
     1 (*  Title:      HOL/UNITY/Client
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Distributed Resource Management System: the Client
     7 *)
     8 
     9 
    10 Addsimps [Cli_prg_def RS def_prg_Init];
    11 program_defs_ref := [Cli_prg_def];
    12 
    13 Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
    14 
    15 
    16 fun invariant_tac i = 
    17     rtac invariantI i  THEN
    18     constrains_tac (i+1);
    19 
    20 (*Safety property 1(a): ask is nondecreasing*)
    21 Goalw [increasing_def] "Cli_prg: increasing ask";
    22 by (Clarify_tac 1);
    23 by (constrains_tac 1);
    24 by Auto_tac;
    25 qed "increasing_ask";
    26 
    27 (*Safety property 1(b): rel is nondecreasing*)
    28 Goalw [increasing_def] "Cli_prg: increasing rel";
    29 by (Clarify_tac 1);
    30 by (constrains_tac 1);
    31 by Auto_tac;
    32 qed "increasing_rel";
    33 
    34 Addsimps [nth_append, append_one_prefix];
    35 
    36 Goal "Cli_prg: invariant {s. tok s <= Max}";
    37 by (invariant_tac 1);
    38 by Auto_tac;
    39 qed "tok_bounded";
    40 
    41 (*Safety property 3: no client requests "too many" tokens.
    42       With no Substitution Axiom, we must prove the two invariants 
    43   simultaneously.  Could combine tok_bounded, stable_constrains_stable 
    44   and a rule invariant_implies_stable...
    45 *)
    46 Goal "Cli_prg:                             \
    47 \       invariant ({s. tok s <= Max}  Int  \
    48 \                  {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})";
    49 by (invariant_tac 1);
    50 by (auto_tac (claset() addSEs [less_SucE], simpset()));
    51 qed "ask_bounded";
    52 
    53 (** Several facts used to prove Lemma 1 **)
    54 
    55 Goal "Cli_prg: stable {s. rel s <= giv s}";
    56 by (constrains_tac 1);
    57 by Auto_tac;
    58 qed "stable_rel_le_giv";
    59 
    60 Goal "Cli_prg: stable {s. size (rel s) <= size (giv s)}";
    61 by (constrains_tac 1);
    62 by Auto_tac;
    63 qed "stable_size_rel_le_giv";
    64 
    65 Goal "Cli_prg: stable {s. size (ask s) <= Suc (size (rel s))}";
    66 by (constrains_tac 1);
    67 by Auto_tac;
    68 qed "stable_size_ask_le_rel";
    69 
    70 
    71 (*We no longer need constrains_tac to expand the program definition, and 
    72   expanding it is extremely expensive!*)
    73 program_defs_ref := [];
    74 
    75 (*Safety property 2: clients return the right number of tokens*)
    76 Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
    77 \               guarantees Always {s. rel s <= giv s}";
    78 by (rtac guaranteesI 1);
    79 by (rtac AlwaysI 1);
    80 by (Force_tac 1);
    81 by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
    82 by (blast_tac (claset() addIs [Increasing_localTo_Stable, 
    83 			       stable_rel_le_giv]) 1);
    84 qed "ok_guar_rel_prefix_giv";
    85 
    86 
    87 (*** Towards proving the liveness property ***)
    88 
    89 Goal "Cli_prg Join G   \
    90 \       : transient {s. size (giv s) = Suc k &  \
    91 \                       size (rel s) = k & ask s ! k <= giv s ! k}";
    92 by (res_inst_tac [("act", "rel_act")] transient_mem 1);
    93 by (auto_tac (claset(),
    94 	      simpset() addsimps [Domain_def, Cli_prg_def]));
    95 qed "transient_lemma";
    96 
    97 
    98 
    99 val rewrite_o = rewrite_rule [o_def];
   100 
   101 val Increasing_length = mono_length RS mono_Increasing_o;
   102 
   103 Goal "Cli_prg : \
   104 \      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
   105 \      guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
   106 \                            {s. size (rel s) <= size (giv s)})";
   107 by (rtac guaranteesI 1);
   108 by (Clarify_tac 1);
   109 by (dtac (impOfSubs (rewrite_o Increasing_length)) 1);
   110 by (rtac AlwaysI 1);
   111 by (Force_tac 1);
   112 by (rtac Stable_Int 1);
   113 by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 2);
   114 by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
   115 	               addIs [Increasing_localTo_Stable, 
   116 			      stable_size_rel_le_giv]) 2);
   117 by (full_simp_tac (simpset() addsimps [Join_localTo]) 1);
   118 by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
   119 	               addIs [stable_localTo_stable2 RS stable_imp_Stable,
   120 			      stable_size_ask_le_rel]) 1);
   121 val lemma1 = result();
   122 
   123 
   124 Goal "Cli_prg : \
   125 \      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
   126 \                 Int Always giv_meets_ask) \
   127 \      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
   128 by (rtac guaranteesI 1);
   129 by (Clarify_tac 1);
   130 by (rtac Stable_transient_Always_LeadsTo 1);
   131 by (res_inst_tac [("k", "k")] transient_lemma 2);
   132 by (force_tac (claset() addDs [impOfSubs Increasing_length,
   133 			       impOfSubs Increasing_Stable_less],
   134 	       simpset()) 1);
   135 by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
   136 by (Blast_tac 1);
   137 by (force_tac (claset(), 
   138 	       simpset() addsimps [Always_eq_includes_reachable, 
   139 				  giv_meets_ask_def]) 1);
   140 qed "client_correct";