Theory Var_Fun_Composite

theory Var_Fun_Composite
  imports Main
begin          

text ‹
  A compositional type for the reduction algorithm,
  to ensure uniqueness of variables in the generated MLSS formulae
›

datatype ('v, 'f) Composite =
  Solo 'v |
  VennRegion "'v set" (‹v⇘_⇙›) |
  FunOfUnionOfVennRegions 'f "'v set set" (‹w⇘_⇙⇘_⇙›) |
  InterOfWAux 'f "'v set set" "'v set set" |
  UnionOfVars "'v list" |
  InterOfVarsAux "'v list" |
  InterOfVars "'v list" |
  UnionOfVennRegions "'v set list" |
  MemAux 'v

end