src/HOL/UNITY/Comp/Client.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 11194 ea13ff5a26d1
child 14089 7b34f58b1b81
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
paulson@11194
     1
(*  Title:      HOL/UNITY/Client.thy
paulson@11194
     2
    ID:         $Id$
paulson@11194
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11194
     4
    Copyright   1998  University of Cambridge
paulson@11194
     5
paulson@11194
     6
Distributed Resource Management System: the Client
paulson@11194
     7
*)
paulson@11194
     8
paulson@11194
     9
Client = Rename + AllocBase +
paulson@11194
    10
paulson@11194
    11
types
paulson@11194
    12
  tokbag = nat	   (*tokbags could be multisets...or any ordered type?*)
paulson@11194
    13
paulson@11194
    14
record state =
paulson@11194
    15
  giv :: tokbag list   (*input history: tokens granted*)
paulson@11194
    16
  ask :: tokbag list   (*output history: tokens requested*)
paulson@11194
    17
  rel :: tokbag list   (*output history: tokens released*)
paulson@11194
    18
  tok :: tokbag	       (*current token request*)
paulson@11194
    19
paulson@11194
    20
record 'a state_d =
paulson@11194
    21
  state +  
paulson@11194
    22
  dummy :: 'a          (*new variables*)
paulson@11194
    23
paulson@11194
    24
paulson@11194
    25
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
paulson@11194
    26
paulson@11194
    27
constdefs
paulson@11194
    28
  
paulson@11194
    29
  (** Release some tokens **)
paulson@11194
    30
  
paulson@11194
    31
  rel_act :: "('a state_d * 'a state_d) set"
paulson@11194
    32
    "rel_act == {(s,s').
paulson@13812
    33
		  \\<exists>nrel. nrel = size (rel s) &
paulson@13812
    34
		         s' = s (| rel := rel s @ [giv s!nrel] |) &
paulson@13812
    35
		         nrel < size (giv s) &
paulson@13812
    36
		         ask s!nrel <= giv s!nrel}"
paulson@11194
    37
paulson@11194
    38
  (** Choose a new token requirement **)
paulson@11194
    39
paulson@11194
    40
  (** Including s'=s suppresses fairness, allowing the non-trivial part
paulson@11194
    41
      of the action to be ignored **)
paulson@11194
    42
paulson@11194
    43
  tok_act :: "('a state_d * 'a state_d) set"
paulson@11194
    44
     "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
paulson@11194
    45
  
paulson@11194
    46
  ask_act :: "('a state_d * 'a state_d) set"
paulson@11194
    47
    "ask_act == {(s,s'). s'=s |
paulson@11194
    48
		         (s' = s (|ask := ask s @ [tok s]|))}"
paulson@11194
    49
paulson@11194
    50
  Client :: 'a state_d program
paulson@11194
    51
    "Client ==
paulson@13812
    52
       mk_total_program
paulson@13812
    53
            ({s. tok s : atMost NbT &
paulson@13812
    54
		 giv s = [] & ask s = [] & rel s = []},
paulson@13812
    55
	     {rel_act, tok_act, ask_act},
paulson@13812
    56
	     \\<Union>G \\<in> preserves rel Int preserves ask Int preserves tok.
paulson@11194
    57
		   Acts G)"
paulson@11194
    58
paulson@11194
    59
  (*Maybe want a special theory section to declare such maps*)
paulson@11194
    60
  non_dummy :: 'a state_d => state
paulson@11194
    61
    "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
paulson@11194
    62
paulson@11194
    63
  (*Renaming map to put a Client into the standard form*)
paulson@11194
    64
  client_map :: "'a state_d => state*'a"
paulson@11194
    65
    "client_map == funPair non_dummy dummy"
paulson@11194
    66
paulson@11194
    67
end