src/HOL/UNITY/Comp.thy
author paulson
Fri Jan 14 12:17:53 2000 +0100 (2000-01-14)
changeset 8128 3a5864b465e2
parent 8122 b43ad07660b9
child 11190 44e157622cb2
permissions -rw-r--r--
still working; a bit of polishing
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@5597
    29
end