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
```