src/HOL/UNITY/Channel.thy
author wenzelm
Tue, 17 Nov 1998 14:07:25 +0100
changeset 5906 1f58694fc3e2
parent 5648 fe887910e32e
child 6536 281d44905cab
permissions -rw-r--r--
Drule.rev_triv_goal;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Channel
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
Unordered Channel
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     9
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
Channel = WFair + Option + 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    13
types state = nat set
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
    15
consts
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
    16
  F :: state program
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
    17
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    18
constdefs
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    19
  minSet :: nat set => nat option
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    20
    "minSet A == if A={} then None else Some (LEAST x. x:A)"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
rules
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    23
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
    24
  UC1  "F : constrains (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    25
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
    26
  (*  UC1  "F : constrains {s. minSet s = x} {s. x <= minSet s}"  *)
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    27
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
    28
  UC2  "F : leadsTo (minSet -`` {Some x}) {s. x ~: s}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    29
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    30
end