src/HOL/UNITY/Comp.thy
author wenzelm
Sat Dec 01 18:52:32 2001 +0100 (2001-12-01)
changeset 12338 de0f4a63baa5
parent 11190 44e157622cb2
child 13792 d1811693899c
permissions -rw-r--r--
renamed class "term" to "type" (actually "HOL.type");
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
ehmety@11190
     7
From Chandy and Sanders, "Reasoning About Program Composition",
ehmety@11190
     8
Technical Report 2000-003, University of Florida, 2000.
paulson@5597
     9
ehmety@11190
    10
Revised by Sidi Ehmety on January  2001 
ehmety@11190
    11
ehmety@11190
    12
Added: a strong form of the <= relation (component_of) and localize 
ehmety@11190
    13
paulson@5597
    14
*)
paulson@5597
    15
paulson@5597
    16
Comp = Union +
paulson@5597
    17
paulson@7399
    18
instance
wenzelm@12338
    19
  program :: (type) ord
paulson@5597
    20
paulson@7399
    21
defs
paulson@7399
    22
  component_def   "F <= H == EX G. F Join G = H"
paulson@7399
    23
  strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
paulson@5612
    24
ehmety@11190
    25
paulson@8055
    26
constdefs
ehmety@11190
    27
  component_of :: "'a program=>'a program=> bool"
ehmety@11190
    28
                                    (infixl "component'_of" 50)
ehmety@11190
    29
  "F component_of H == EX G. F ok G & F Join G = H"
ehmety@11190
    30
ehmety@11190
    31
  strict_component_of :: "'a program\\<Rightarrow>'a program=> bool"
ehmety@11190
    32
                                    (infixl "strict'_component'_of" 50)
ehmety@11190
    33
  "F strict_component_of H == F component_of H & F~=H"
ehmety@11190
    34
  
paulson@8055
    35
  preserves :: "('a=>'b) => 'a program set"
paulson@8055
    36
    "preserves v == INT z. stable {s. v s = z}"
paulson@8055
    37
ehmety@11190
    38
  localize  :: "('a=>'b) => 'a program => 'a program"
ehmety@11190
    39
  "localize v F == mk_program(Init F, Acts F,
ehmety@11190
    40
			      AllowedActs F Int (UN G:preserves v. Acts G))"
ehmety@11190
    41
paulson@8055
    42
  funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
ehmety@11190
    43
  "funPair f g == %x. (f x, g x)"
paulson@5597
    44
end