src/HOL/UNITY/Union.thy
changeset 7359 98a2afab3f86
parent 6295 351b3c2b0d83
child 7826 c6a8b73b6c2a
equal deleted inserted replaced
7358:9e95b846ad42 7359:98a2afab3f86
     4     Copyright   1998  University of Cambridge
     4     Copyright   1998  University of Cambridge
     5 
     5 
     6 Unions of programs
     6 Unions of programs
     7 
     7 
     8 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
     8 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
       
     9 
       
    10 Do we need a Meet operator?  (Aka Intersection)
     9 *)
    11 *)
    10 
    12 
    11 Union = SubstAx + FP +
    13 Union = SubstAx + FP +
    12 
    14 
    13 constdefs
    15 constdefs
    30   (*Two programs with disjoint actions, except for identity actions *)
    32   (*Two programs with disjoint actions, except for identity actions *)
    31   Disjoint :: ['a program, 'a program] => bool
    33   Disjoint :: ['a program, 'a program] => bool
    32     "Disjoint F G == Acts F Int Acts G <= {Id}"
    34     "Disjoint F G == Acts F Int Acts G <= {Id}"
    33 
    35 
    34 syntax
    36 syntax
       
    37   "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)
    35   "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
    38   "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
    36 
    39 
    37 translations
    40 translations
    38   "JN x:A. B"   == "JOIN A (%x. B)"
    41   "JN x:A. B"   == "JOIN A (%x. B)"
       
    42   "JN x y. B"   == "JN x. JN y. B"
       
    43   "JN x. B"     == "JOIN UNIV (%x. B)"
    39 
    44 
    40 end
    45 end