Theory Transport_Syntax

✐‹creator "Kevin Kappelmann"›
section ‹Syntax Bundles for Transport›
theory Transport_Syntax
  imports
    Transport_Base
begin

abbreviation "Galois_infix x L R r y ≡ galois_rel.Galois L R r x y"
abbreviation (input) "ge_Galois R r L ≡ galois_rel.ge_Galois_left L R r"
abbreviation (input) "ge_Galois_infix y R r L x ≡ ge_Galois R r L y x"

bundle galois_rel_syntax
begin
  notation galois_rel.Galois (‹'((⇘_⇙)⪅(⇘(_) (_)⇙)')›)
  notation Galois_infix (‹(_) (⇘_⇙)⪅(⇘(_) (_)⇙) (_)› [51,51,51,51,51] 50)
  notation ge_Galois (‹'((⇘(_) (_)⇙)⪆(⇘_⇙)')›)
  notation ge_Galois_infix (‹(_) (⇘(_) (_)⇙)⪆(⇘_⇙) (_)› [51,51,51,51,51] 50)
end

bundle transport_syntax
begin
  notation transport.preorder_equivalence (infix ‹≡⇘pre⇙› 50)
  notation transport.partial_equivalence_rel_equivalence (infix ‹≡⇘PER⇙› 50)
end

end