src/HOL/UNITY/Client.ML
author paulson
Mon, 11 Oct 1999 10:53:39 +0200
changeset 7826 c6a8b73b6c2a
parent 7594 8a188ef6545e
child 7878 43b03d412b82
permissions -rw-r--r--
working shapshot with "projecting" and "extending"
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
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    10
Addsimps [Cli_prg_def RS def_prg_Init];
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    11
program_defs_ref := [Cli_prg_def];
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    12
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    13
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    14
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    15
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    16
fun invariant_tac i = 
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    17
    rtac invariantI i  THEN
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    18
    constrains_tac (i+1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    19
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    20
(*Safety property 1(a): ask is nondecreasing*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    21
Goalw [increasing_def] "Cli_prg: increasing ask";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    22
by (Clarify_tac 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    23
by (constrains_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    24
by Auto_tac;
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    25
qed "increasing_ask";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    26
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    27
(*Safety property 1(b): rel is nondecreasing*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    28
Goalw [increasing_def] "Cli_prg: increasing rel";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    29
by (Clarify_tac 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    30
by (constrains_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    31
by Auto_tac;
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    32
qed "increasing_rel";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    33
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    34
Addsimps [nth_append, append_one_prefix];
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    35
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    36
Goal "Cli_prg: invariant {s. tok s <= Max}";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    37
by (invariant_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    38
by Auto_tac;
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    39
qed "tok_bounded";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    40
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    41
(*Safety property 3: no client requests "too many" tokens.
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    42
      With no Substitution Axiom, we must prove the two invariants 
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    43
  simultaneously.  Could combine tok_bounded, stable_constrains_stable 
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    44
  and a rule invariant_implies_stable...
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    45
*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    46
Goal "Cli_prg:                             \
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    47
\       invariant ({s. tok s <= Max}  Int  \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    48
\                  {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    49
by (invariant_tac 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    50
by (auto_tac (claset() addSEs [less_SucE], simpset()));
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    51
qed "ask_bounded";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    52
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    53
(** Several facts used to prove Lemma 1 **)
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    54
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    55
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
    56
by (constrains_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    57
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    58
qed "stable_rel_le_giv";
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. size (rel s) <= size (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_size_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 (ask s) <= Suc (size (rel 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_ask_le_rel";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    69
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    70
5667
2df6fccf5719 fixed comment
paulson
parents: 5648
diff changeset
    71
(*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
    72
  expanding it is extremely expensive!*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    73
program_defs_ref := [];
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    74
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    75
(*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
    76
Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7179
diff changeset
    77
\               guarantees Always {s. rel s <= giv s}";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    78
by (rtac guaranteesI 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
    79
by (rtac AlwaysI 1);
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    80
by (Force_tac 1);
7594
8a188ef6545e working version with co-guarantees-leadsto results
paulson
parents: 7537
diff changeset
    81
by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    82
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
    83
			       stable_rel_le_giv]) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    84
qed "ok_guar_rel_prefix_giv";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    85
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    86
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    87
(*** Towards proving the liveness property ***)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    88
6295
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6018
diff changeset
    89
Goal "Cli_prg Join G   \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    90
\       : transient {s. size (giv s) = Suc k &  \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    91
\                       size (rel s) = k & ask s ! k <= giv s ! k}";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    92
by (res_inst_tac [("act", "rel_act")] transient_mem 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    93
by (auto_tac (claset(),
7537
875754b599df working snapshot
paulson
parents: 7361
diff changeset
    94
	      simpset() addsimps [Domain_def, Cli_prg_def]));
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    95
qed "transient_lemma";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    96
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    97
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    98
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    99
val rewrite_o = rewrite_rule [o_def];
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   100
6701
e84a0b941beb now uses mono_Increasing_o
paulson
parents: 6570
diff changeset
   101
val Increasing_length = mono_length RS mono_Increasing_o;
e84a0b941beb now uses mono_Increasing_o
paulson
parents: 6570
diff changeset
   102
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   103
Goal "Cli_prg : \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   104
\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7179
diff changeset
   105
\      guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   106
\                            {s. size (rel s) <= size (giv s)})";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   107
by (rtac guaranteesI 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   108
by (Clarify_tac 1);
6701
e84a0b941beb now uses mono_Increasing_o
paulson
parents: 6570
diff changeset
   109
by (dtac (impOfSubs (rewrite_o Increasing_length)) 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   110
by (rtac AlwaysI 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   111
by (Force_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   112
by (rtac Stable_Int 1);
7594
8a188ef6545e working version with co-guarantees-leadsto results
paulson
parents: 7537
diff changeset
   113
by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 2);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   114
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
   115
	               addIs [Increasing_localTo_Stable, 
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   116
			      stable_size_rel_le_giv]) 2);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7594
diff changeset
   117
by (full_simp_tac (simpset() addsimps [Join_localTo]) 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   118
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
   119
	               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
   120
			      stable_size_ask_le_rel]) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   121
val lemma1 = result();
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   122
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   123
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   124
Goal "Cli_prg : \
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   125
\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   126
\                 Int Always giv_meets_ask) \
7361
477e1bdf230f changed "guar" back to "guarantees" (sorry)
paulson
parents: 7179
diff changeset
   127
\      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   128
by (rtac guaranteesI 1);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   129
by (Clarify_tac 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   130
by (rtac Stable_transient_Always_LeadsTo 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   131
by (res_inst_tac [("k", "k")] transient_lemma 2);
6701
e84a0b941beb now uses mono_Increasing_o
paulson
parents: 6570
diff changeset
   132
by (force_tac (claset() addDs [impOfSubs Increasing_length,
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   133
			       impOfSubs Increasing_Stable_less],
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   134
	       simpset()) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   135
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   136
by (Blast_tac 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7594
diff changeset
   137
by (force_tac (claset(), 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7594
diff changeset
   138
	       simpset() addsimps [Always_eq_includes_reachable, 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7594
diff changeset
   139
				  giv_meets_ask_def]) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   140
qed "client_correct";