src/HOL/UNITY/Simple/Mutex.thy
author paulson
Mon, 05 Mar 2001 15:47:11 +0100
changeset 11195 65ede8dfe304
child 11701 3d51fbf81c17
permissions -rw-r--r--
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11195
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Mutex.thy
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     2
    ID:         $Id$
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     5
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     6
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     7
*)
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     8
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     9
Mutex = SubstAx +
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    10
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    11
record state =
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    12
  p :: bool
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    13
  m :: int
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    14
  n :: int
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    15
  u :: bool
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    16
  v :: bool
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    17
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    18
types command = "(state*state) set"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    19
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    20
constdefs
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    21
  
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    22
  (** The program for process U **)
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    23
  
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    24
  U0 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    25
    "U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    26
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    27
  U1 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    28
    "U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    29
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    30
  U2 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    31
    "U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    32
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    33
  U3 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    34
    "U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    35
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    36
  U4 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    37
    "U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    38
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    39
  (** The program for process V **)
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    40
  
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    41
  V0 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    42
    "V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    43
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    44
  V1 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    45
    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    46
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    47
  V2 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    48
    "V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    49
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    50
  V3 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    51
    "V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    52
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    53
  V4 :: command
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    54
    "V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    55
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    56
  Mutex :: state program
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    57
    "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    58
		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    59
			  UNIV)"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    60
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    61
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    62
  (** The correct invariants **)
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    63
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    64
  IU :: state set
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    65
    "IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    66
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    67
  IV :: state set
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    68
    "IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    69
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    70
  (** The faulty invariant (for U alone) **)
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    71
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    72
  bad_IU :: state set
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    73
    "bad_IU == {s. (u s = (#1 <= m s & m s <= #3)) &
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    74
	           (#3 <= m s & m s <= #4 --> ~ p s)}"
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    75
65ede8dfe304 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    76
end