src/HOL/UNITY/Comp/AllocImpl.thy
author nipkow
Thu, 22 Jul 2004 17:37:31 +0200
changeset 15074 277b3a4da341
parent 14114 e97ca1034caa
child 16417 9bc16273c2d4
permissions -rw-r--r--
Modified \<Sum> syntax a little.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/AllocImpl
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     2
    ID:         $Id$
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     5
*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     6
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
     7
header{*Implementation of a multiple-client allocator from a single-client allocator*}
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
     8
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
     9
theory AllocImpl = AllocBase + Follows + PPROD:
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    10
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    11
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    12
(** State definitions.  OUTPUT variables are locals **)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    13
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    14
(*Type variable 'b is the type of items being merged*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    15
record 'b merge =
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
    16
  In   :: "nat => 'b list"  (*merge's INPUT histories: streams to merge*)
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
    17
  Out  :: "'b list"         (*merge's OUTPUT history: merged items*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    18
  iOut :: "nat list"        (*merge's OUTPUT history: origins of merged items*)
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    19
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    20
record ('a,'b) merge_d =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    21
  "'b merge" +
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    22
  dummy :: 'a       (*dummy field for new variables*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    23
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    24
constdefs
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    25
  non_dummy :: "('a,'b) merge_d => 'b merge"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    26
    "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    27
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    28
record 'b distr =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    29
  In  :: "'b list"          (*items to distribute*)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    30
  iIn :: "nat list"         (*destinations of items to distribute*)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    31
  Out :: "nat => 'b list"   (*distributed items*)
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    32
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    33
record ('a,'b) distr_d =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    34
  "'b distr" +
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    35
  dummy :: 'a       (*dummy field for new variables*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    36
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    37
record allocState =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    38
  giv :: "nat list"   (*OUTPUT history: source of tokens*)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    39
  ask :: "nat list"   (*INPUT: tokens requested from allocator*)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    40
  rel :: "nat list"   (*INPUT: tokens released to allocator*)
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    41
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    42
record 'a allocState_d =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    43
  allocState +
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    44
  dummy    :: 'a                (*dummy field for new variables*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    45
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    46
record 'a systemState =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    47
  allocState +
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    48
  mergeRel :: "nat merge"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    49
  mergeAsk :: "nat merge"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    50
  distr    :: "nat distr"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    51
  dummy    :: 'a                  (*dummy field for new variables*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    52
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    53
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    54
constdefs
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    55
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    56
(** Merge specification (the number of inputs is Nclients) ***)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    57
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    58
  (*spec (10)*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    59
  merge_increasing :: "('a,'b) merge_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    60
    "merge_increasing ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    61
         UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    62
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    63
  (*spec (11)*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    64
  merge_eqOut :: "('a,'b) merge_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    65
    "merge_eqOut ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    66
         UNIV guarantees
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    67
         Always {s. length (merge.Out s) = length (merge.iOut s)}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    68
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    69
  (*spec (12)*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    70
  merge_bounded :: "('a,'b) merge_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    71
    "merge_bounded ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    72
         UNIV guarantees
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    73
         Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    74
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    75
  (*spec (13)*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    76
  merge_follows :: "('a,'b) merge_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    77
    "merge_follows ==
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    78
	 (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    79
	 guarantees
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
    80
	 (\<Inter>i \<in> lessThan Nclients.
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
    81
	  (%s. sublist (merge.Out s)
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    82
                       {k. k < size(merge.iOut s) & merge.iOut s! k = i})
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    83
	  Fols (sub i o merge.In))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    84
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    85
  (*spec: preserves part*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    86
  merge_preserves :: "('a,'b) merge_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    87
    "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    88
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    89
  (*environmental constraints*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    90
  merge_allowed_acts :: "('a,'b) merge_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    91
    "merge_allowed_acts ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    92
       {F. AllowedActs F =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    93
	    insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    94
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
    95
  merge_spec :: "('a,'b) merge_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    96
    "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    97
                   merge_follows Int merge_allowed_acts Int merge_preserves"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    98
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    99
(** Distributor specification (the number of outputs is Nclients) ***)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   100
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   101
  (*spec (14)*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   102
  distr_follows :: "('a,'b) distr_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   103
    "distr_follows ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   104
	 Increasing distr.In Int Increasing distr.iIn Int
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   105
	 Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   106
	 guarantees
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   107
	 (\<Inter>i \<in> lessThan Nclients.
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   108
	  (sub i o distr.Out) Fols
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   109
	  (%s. sublist (distr.In s)
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   110
                       {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   111
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   112
  distr_allowed_acts :: "('a,'b) distr_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   113
    "distr_allowed_acts ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   114
       {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   115
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   116
  distr_spec :: "('a,'b) distr_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   117
    "distr_spec == distr_follows Int distr_allowed_acts"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   118
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   119
(** Single-client allocator specification (required) ***)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   120
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   121
  (*spec (18)*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   122
  alloc_increasing :: "'a allocState_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   123
    "alloc_increasing == UNIV  guarantees  Increasing giv"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   124
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   125
  (*spec (19)*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   126
  alloc_safety :: "'a allocState_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   127
    "alloc_safety ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   128
	 Increasing rel
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   129
         guarantees  Always {s. tokens (giv s) \<le> NbT + tokens (rel s)}"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   130
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   131
  (*spec (20)*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   132
  alloc_progress :: "'a allocState_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   133
    "alloc_progress ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   134
	 Increasing ask Int Increasing rel Int
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   135
         Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   136
         Int
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   137
         (\<Inter>h. {s. h \<le> giv s & h pfixGe (ask s)}
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   138
		 LeadsTo
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   139
	         {s. tokens h \<le> tokens (rel s)})
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   140
         guarantees  (\<Inter>h. {s. h \<le> ask s} LeadsTo {s. h pfixLe giv s})"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   141
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   142
  (*spec: preserves part*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   143
  alloc_preserves :: "'a allocState_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   144
    "alloc_preserves == preserves rel Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   145
                        preserves ask Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   146
                        preserves allocState_d.dummy"
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   147
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   148
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   149
  (*environmental constraints*)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   150
  alloc_allowed_acts :: "'a allocState_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   151
    "alloc_allowed_acts ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   152
       {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   153
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   154
  alloc_spec :: "'a allocState_d program set"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   155
    "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   156
                   alloc_allowed_acts Int alloc_preserves"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   157
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   158
locale Merge =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   159
  fixes M :: "('a,'b::order) merge_d program"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   160
  assumes
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   161
    Merge_spec:  "M  \<in> merge_spec"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   162
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   163
locale Distrib =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   164
  fixes D :: "('a,'b::order) distr_d program"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   165
  assumes
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   166
    Distrib_spec:  "D \<in> distr_spec"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   167
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   168
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   169
(****
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   170
#  {** Network specification ***}
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   171
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   172
#    {*spec (9.1)*}
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   173
#    network_ask :: "'a systemState program set
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   174
#	"network_ask == \<Inter>i \<in> lessThan Nclients.
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   175
#			    Increasing (ask o sub i o client)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   176
#			    guarantees[ask]
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   177
#			    (ask  Fols (ask o sub i o client))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   178
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   179
#    {*spec (9.2)*}
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   180
#    network_giv :: "'a systemState program set
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   181
#	"network_giv == \<Inter>i \<in> lessThan Nclients.
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   182
#			    Increasing giv
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   183
#			    guarantees[giv o sub i o client]
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   184
#			    ((giv o sub i o client) Fols giv)"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   185
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   186
#    {*spec (9.3)*}
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   187
#    network_rel :: "'a systemState program set
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   188
#	"network_rel == \<Inter>i \<in> lessThan Nclients.
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   189
#			    Increasing (rel o sub i o client)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   190
#			    guarantees[rel]
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   191
#			    (rel  Fols (rel o sub i o client))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   192
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   193
#    {*spec: preserves part*}
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   194
#	network_preserves :: "'a systemState program set
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   195
#	"network_preserves == preserves giv  Int
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   196
#			      (\<Inter>i \<in> lessThan Nclients.
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   197
#			       preserves (funPair rel ask o sub i o client))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   198
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   199
#    network_spec :: "'a systemState program set
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   200
#	"network_spec == network_ask Int network_giv Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   201
#			 network_rel Int network_preserves"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   202
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   203
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   204
#  {** State mappings **}
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   205
#    sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   206
#	"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   207
#			   in (| giv = giv s,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   208
#				 ask = ask s,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   209
#				 rel = rel s,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   210
#				 client   = cl,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   211
#				 dummy    = xtr|)"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   212
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   213
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   214
#    sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   215
#	"sysOfClient == %(cl,al). (| giv = giv al,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   216
#				     ask = ask al,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   217
#				     rel = rel al,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   218
#				     client   = cl,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   219
#				     systemState.dummy = allocState_d.dummy al|)"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   220
****)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   221
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   222
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   223
declare subset_preserves_o [THEN subsetD, intro]
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   224
declare funPair_o_distrib [simp]
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   225
declare Always_INT_distrib [simp]
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   226
declare o_apply [simp del]
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   227
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   228
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   229
subsection{*Theorems for Merge*}
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   230
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   231
lemma (in Merge) Merge_Allowed:
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   232
     "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   233
apply (cut_tac Merge_spec)
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   234
apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   235
                      safety_prop_Acts_iff)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   236
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   237
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   238
lemma (in Merge) M_ok_iff [iff]:
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   239
     "M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut &
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   240
                     M \<in> Allowed G)"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   241
by (auto simp add: Merge_Allowed ok_iff_Allowed)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   242
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   243
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   244
lemma (in Merge) Merge_Always_Out_eq_iOut:
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   245
     "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   246
      ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   247
apply (cut_tac Merge_spec)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   248
apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   249
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   250
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   251
lemma (in Merge) Merge_Bounded:
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   252
     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   253
      ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   254
apply (cut_tac Merge_spec)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   255
apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   256
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   257
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   258
lemma (in Merge) Merge_Bag_Follows_lemma:
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   259
     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   260
  ==> M Join G \<in> Always
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   261
          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s)
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   262
                                  {k. k < length (iOut s) & iOut s ! k = i})) =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   263
              (bag_of o merge.Out) s}"
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   264
apply (rule Always_Compl_Un_eq [THEN iffD1])
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   265
apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   266
apply (rule UNIV_AlwaysI, clarify)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   267
apply (subst bag_of_sublist_UN_disjoint [symmetric])
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   268
  apply (simp)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   269
 apply blast
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   270
apply (simp add: set_conv_nth)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   271
apply (subgoal_tac
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   272
       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) =
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   273
       lessThan (length (iOut x))")
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   274
 apply (simp (no_asm_simp) add: o_def)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   275
apply blast
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   276
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   277
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   278
lemma (in Merge) Merge_Bag_Follows:
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   279
     "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   280
          guarantees
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   281
             (bag_of o merge.Out) Fols
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   282
             (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o merge.In) s)"
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   283
apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   284
apply (rule Follows_setsum)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   285
apply (cut_tac Merge_spec)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   286
apply (auto simp add: merge_spec_def merge_follows_def o_def)
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   287
apply (drule guaranteesD)
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   288
  prefer 3
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   289
  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   290
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   291
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   292
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   293
subsection{*Theorems for Distributor*}
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   294
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   295
lemma (in Distrib) Distr_Increasing_Out:
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   296
     "D \<in> Increasing distr.In Int Increasing distr.iIn Int
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   297
          Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   298
          guarantees
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   299
          (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o distr.Out))"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   300
apply (cut_tac Distrib_spec)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   301
apply (simp add: distr_spec_def distr_follows_def)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   302
apply clarify
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   303
apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   304
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   305
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   306
lemma (in Distrib) Distr_Bag_Follows_lemma:
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   307
     "[| G \<in> preserves distr.Out;
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   308
         D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   309
  ==> D Join G \<in> Always
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   310
          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   311
                                  {k. k < length (iIn s) & iIn s ! k = i})) =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   312
              bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   313
apply (erule Always_Compl_Un_eq [THEN iffD1])
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   314
apply (rule UNIV_AlwaysI, clarify)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   315
apply (subst bag_of_sublist_UN_disjoint [symmetric])
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   316
  apply (simp (no_asm))
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   317
 apply blast
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   318
apply (simp add: set_conv_nth)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   319
apply (subgoal_tac
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   320
       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) =
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   321
        lessThan (length (iIn x))")
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   322
 apply (simp (no_asm_simp))
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   323
apply blast
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   324
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   325
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   326
lemma (in Distrib) D_ok_iff [iff]:
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   327
     "D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   328
apply (cut_tac Distrib_spec)
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   329
apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   330
                      safety_prop_Acts_iff ok_iff_Allowed)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   331
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   332
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   333
lemma (in Distrib) Distr_Bag_Follows:
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   334
 "D \<in> Increasing distr.In Int Increasing distr.iIn Int
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   335
      Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   336
      guarantees
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   337
       (\<Inter>i \<in> lessThan Nclients.
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   338
        (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s)
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   339
        Fols
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   340
        (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   341
apply (rule guaranteesI, clarify)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   342
apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   343
apply (rule Follows_setsum)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   344
apply (cut_tac Distrib_spec)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   345
apply (auto simp add: distr_spec_def distr_follows_def o_def)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   346
apply (drule guaranteesD)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   347
  prefer 3
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   348
  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   349
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   350
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   351
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   352
subsection{*Theorems for Allocator*}
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   353
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   354
lemma alloc_refinement_lemma:
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   355
     "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
15074
277b3a4da341 Modified \<Sum> syntax a little.
nipkow
parents: 14114
diff changeset
   356
      \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}"
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   357
apply (induct_tac "n")
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   358
apply (auto simp add: lessThan_Suc)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   359
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   360
14114
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   361
lemma alloc_refinement:
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   362
"(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   363
                           Increasing (sub i o allocRel))
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   364
  Int
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   365
  Always {s. \<forall>i. i<Nclients -->
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   366
              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)}
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   367
  Int
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   368
  (\<Inter>i \<in> lessThan Nclients.
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   369
   \<Inter>h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   370
        LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel)s})
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   371
  \<subseteq>
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   372
 (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   373
                           Increasing (sub i o allocRel))
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   374
  Int
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   375
  Always {s. \<forall>i. i<Nclients -->
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   376
              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)}
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   377
  Int
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   378
  (\<Inter>hf. (\<Inter>i \<in> lessThan Nclients.
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   379
         {s. hf i \<le> (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   380
  LeadsTo {s. (\<Sum>i \<in> lessThan Nclients. tokens (hf i)) \<le>
e97ca1034caa tidying
paulson
parents: 14089
diff changeset
   381
              (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)})"
14089
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   382
apply (auto simp add: ball_conj_distrib)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   383
apply (rename_tac F hf)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   384
apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   385
apply (subgoal_tac "F \<in> Increasing (tokens o (sub i o allocRel))")
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   386
 apply (simp add: Increasing_def o_assoc)
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   387
apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   388
done
7b34f58b1b81 converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents: 11194
diff changeset
   389
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   390
end