src/HOL/UNITY/Comp.thy
changeset 11190 44e157622cb2
parent 8128 3a5864b465e2
child 12338 de0f4a63baa5
     1.1 --- a/src/HOL/UNITY/Comp.thy	Fri Mar 02 13:18:31 2001 +0100
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Fri Mar 02 13:18:56 2001 +0100
     1.3 @@ -4,8 +4,13 @@
     1.4      Copyright   1998  University of Cambridge
     1.5  
     1.6  Composition
     1.7 +From Chandy and Sanders, "Reasoning About Program Composition",
     1.8 +Technical Report 2000-003, University of Florida, 2000.
     1.9  
    1.10 -From Chandy and Sanders, "Reasoning About Program Composition"
    1.11 +Revised by Sidi Ehmety on January  2001 
    1.12 +
    1.13 +Added: a strong form of the <= relation (component_of) and localize 
    1.14 +
    1.15  *)
    1.16  
    1.17  Comp = Union +
    1.18 @@ -14,16 +19,26 @@
    1.19    program :: (term)ord
    1.20  
    1.21  defs
    1.22 -
    1.23    component_def   "F <= H == EX G. F Join G = H"
    1.24 -
    1.25    strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
    1.26  
    1.27 +
    1.28  constdefs
    1.29 +  component_of :: "'a program=>'a program=> bool"
    1.30 +                                    (infixl "component'_of" 50)
    1.31 +  "F component_of H == EX G. F ok G & F Join G = H"
    1.32 +
    1.33 +  strict_component_of :: "'a program\\<Rightarrow>'a program=> bool"
    1.34 +                                    (infixl "strict'_component'_of" 50)
    1.35 +  "F strict_component_of H == F component_of H & F~=H"
    1.36 +  
    1.37    preserves :: "('a=>'b) => 'a program set"
    1.38      "preserves v == INT z. stable {s. v s = z}"
    1.39  
    1.40 +  localize  :: "('a=>'b) => 'a program => 'a program"
    1.41 +  "localize v F == mk_program(Init F, Acts F,
    1.42 +			      AllowedActs F Int (UN G:preserves v. Acts G))"
    1.43 +
    1.44    funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
    1.45 -    "funPair f g == %x. (f x, g x)"
    1.46 -
    1.47 +  "funPair f g == %x. (f x, g x)"
    1.48  end