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