src/HOL/UNITY/Comp.thy
author paulson
Thu Jan 13 17:30:23 2000 +0100 (2000-01-13)
changeset 8122 b43ad07660b9
parent 8055 bb15396278fb
child 8128 3a5864b465e2
permissions -rw-r--r--
working version, with Alloc now working on the same state space as the whole
system. Partial removal of ELT.
paulson@5597
     1
(*  Title:      HOL/UNITY/Comp.thy
paulson@5597
     2
    ID:         $Id$
paulson@5597
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5597
     4
    Copyright   1998  University of Cambridge
paulson@5597
     5
paulson@5597
     6
Composition
paulson@5597
     7
paulson@5597
     8
From Chandy and Sanders, "Reasoning About Program Composition"
paulson@5597
     9
*)
paulson@5597
    10
paulson@5597
    11
Comp = Union +
paulson@5597
    12
paulson@7399
    13
instance
paulson@7399
    14
  program :: (term)ord
paulson@5597
    15
paulson@7399
    16
defs
paulson@5597
    17
paulson@7399
    18
  component_def   "F <= H == EX G. F Join G = H"
paulson@5597
    19
paulson@7399
    20
  strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
paulson@5612
    21
paulson@8055
    22
constdefs
paulson@8055
    23
  preserves :: "('a=>'b) => 'a program set"
paulson@8055
    24
    "preserves v == INT z. stable {s. v s = z}"
paulson@8055
    25
paulson@8055
    26
  funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
paulson@8055
    27
    "funPair f g == %x. (f x, g x)"
paulson@8055
    28
paulson@8122
    29
  (*the set of all sets determined by f alone*)
paulson@8122
    30
  givenBy :: "['a => 'b] => 'a set set"
paulson@8122
    31
    "givenBy f == range (%B. f-`` B)"
paulson@8122
    32
paulson@5597
    33
end