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");
     1 (*  Title:      HOL/UNITY/Comp.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Composition
     7 From Chandy and Sanders, "Reasoning About Program Composition",
     8 Technical Report 2000-003, University of Florida, 2000.
     9 
    10 Revised by Sidi Ehmety on January  2001 
    11 
    12 Added: a strong form of the <= relation (component_of) and localize 
    13 
    14 *)
    15 
    16 Comp = Union +
    17 
    18 instance
    19   program :: (type) ord
    20 
    21 defs
    22   component_def   "F <= H == EX G. F Join G = H"
    23   strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
    24 
    25 
    26 constdefs
    27   component_of :: "'a program=>'a program=> bool"
    28                                     (infixl "component'_of" 50)
    29   "F component_of H == EX G. F ok G & F Join G = H"
    30 
    31   strict_component_of :: "'a program\\<Rightarrow>'a program=> bool"
    32                                     (infixl "strict'_component'_of" 50)
    33   "F strict_component_of H == F component_of H & F~=H"
    34   
    35   preserves :: "('a=>'b) => 'a program set"
    36     "preserves v == INT z. stable {s. v s = z}"
    37 
    38   localize  :: "('a=>'b) => 'a program => 'a program"
    39   "localize v F == mk_program(Init F, Acts F,
    40 			      AllowedActs F Int (UN G:preserves v. Acts G))"
    41 
    42   funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
    43   "funPair f g == %x. (f x, g x)"
    44 end