src/HOL/UNITY/Client.ML
author paulson
Mon, 07 Dec 1998 18:23:39 +0100
changeset 6018 8131f37f4ba3
parent 6012 1894bfc4aee9
child 6295 351b3c2b0d83
permissions -rw-r--r--
expandshort
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Client
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     2
    ID:         $Id$
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     5
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     6
Distributed Resource Management System: the Client
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     7
*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     8
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     9
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    10
claset_ref() := claset();
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    11
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    12
Addsimps [Cli_prg_def RS def_prg_Init];
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    13
program_defs_ref := [Cli_prg_def];
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    14
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    15
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    16
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    17
(*Simplification for records*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    18
Addsimps (thms"state.update_defs");
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    19
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    20
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    21
fun invariant_tac i = 
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    22
    rtac invariantI i  THEN
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    23
    constrains_tac (i+1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    24
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    25
(*Safety property 1(a): ask is nondecreasing*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    26
Goalw [increasing_def] "Cli_prg: increasing ask";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    27
by (Clarify_tac 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    28
by (constrains_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    29
by Auto_tac;
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    30
qed "increasing_ask";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    31
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    32
(*Safety property 1(b): rel is nondecreasing*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    33
Goalw [increasing_def] "Cli_prg: increasing rel";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    34
by (Clarify_tac 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    35
by (constrains_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    36
by Auto_tac;
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    37
qed "increasing_rel";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    38
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    39
Addsimps [nth_append, append_one_prefix];
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    40
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    41
Goal "Cli_prg: invariant {s. tok s <= Max}";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    42
by (invariant_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    43
by Auto_tac;
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    44
qed "tok_bounded";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    45
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    46
(*Safety property 3: no client requests "too many" tokens.
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    47
      With no Substitution Axiom, we must prove the two invariants 
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    48
  simultaneously.  Could combine tok_bounded, stable_constrains_stable 
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    49
  and a rule invariant_implies_stable...
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    50
*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    51
Goal "Cli_prg:                             \
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    52
\       invariant ({s. tok s <= Max}  Int  \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    53
\                  {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    54
by (invariant_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    55
by (auto_tac (claset() addSEs [less_SucE], simpset()));
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    56
qed "ask_bounded";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    57
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    58
(** Several facts used to prove Lemma 1 **)
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    59
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    60
Goal "Cli_prg: stable {s. rel s <= giv s}";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    61
by (constrains_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    62
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    63
qed "stable_rel_le_giv";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    64
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    65
Goal "Cli_prg: stable {s. size (rel s) <= size (giv s)}";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    66
by (constrains_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    67
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    68
qed "stable_size_rel_le_giv";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    69
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    70
Goal "Cli_prg: stable {s. size (ask s) <= Suc (size (rel s))}";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    71
by (constrains_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    72
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    73
qed "stable_size_ask_le_rel";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    74
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    75
5667
2df6fccf5719 fixed comment
paulson
parents: 5648
diff changeset
    76
(*We no longer need constrains_tac to expand the program definition, and 
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    77
  expanding it is extremely expensive!*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    78
program_defs_ref := [];
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    79
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    80
(*Safety property 2: clients return the right number of tokens*)
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    81
Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    82
\               guarantees Invariant {s. rel s <= giv s}";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    83
by (rtac guaranteesI 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    84
by (rtac InvariantI 1);
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    85
by (Force_tac 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    86
by (blast_tac (claset() addIs [Increasing_localTo_Stable, 
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    87
			       stable_rel_le_giv]) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    88
qed "ok_guar_rel_prefix_giv";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    89
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    90
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    91
(*** Towards proving the liveness property ***)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    92
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    93
Goal "States Cli_prg = States G \
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    94
\     ==> Cli_prg Join G   \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    95
\       : transient {s. size (giv s) = Suc k &  \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    96
\                       size (rel s) = k & ask s ! k <= giv s ! k}";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    97
by (res_inst_tac [("act", "rel_act")] transient_mem 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    98
by (auto_tac (claset(),
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    99
	      simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def]));
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   100
qed "transient_lemma";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   101
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   102
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   103
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   104
val rewrite_o = rewrite_rule [o_def];
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   105
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   106
Goal "Cli_prg : \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   107
\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   108
\      guarantees Invariant ({s. size (ask s) <= Suc (size (rel s))} Int \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   109
\                            {s. size (rel s) <= size (giv s)})";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   110
by (rtac guaranteesI 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   111
by (Clarify_tac 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   112
by (dtac (impOfSubs (rewrite_o Increasing_size)) 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   113
by (rtac InvariantI 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   114
by (Force_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   115
by (rtac Stable_Int 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   116
by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   117
	               addIs [Increasing_localTo_Stable, 
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   118
			      stable_size_rel_le_giv]) 2);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   119
by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   120
	               addIs [stable_localTo_stable2 RS stable_imp_Stable,
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   121
			      stable_size_ask_le_rel]) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   122
val lemma1 = result();
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   123
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   124
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   125
Goal "Cli_prg : \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   126
\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   127
\                 Int Invariant giv_meets_ask) \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   128
\      guarantees (LeadsTo {s. k < size (giv s)}    \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   129
\                          {s. k < size (rel s)})";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   130
by (rtac guaranteesI 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   131
by (Clarify_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   132
by (rtac Stable_transient_reachable_LeadsTo 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   133
by (res_inst_tac [("k", "k")] transient_lemma 2);
6018
8131f37f4ba3 expandshort
paulson
parents: 6012
diff changeset
   134
by (etac Disjoint_States_eq 2);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   135
by (force_tac (claset() addDs [impOfSubs Increasing_size,
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   136
			       impOfSubs Increasing_Stable_less],
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   137
	       simpset()) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   138
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
5758
27a2b36efd95 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5706
diff changeset
   139
 by (Blast_tac 1);
6018
8131f37f4ba3 expandshort
paulson
parents: 6012
diff changeset
   140
by (etac Disjoint_States_eq 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   141
by (auto_tac (claset(),
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   142
	      simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
5758
27a2b36efd95 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5706
diff changeset
   143
by (ALLGOALS Force_tac);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   144
qed "client_correct";