Theory Transport_Syntax

✐‹creator "Kevin Kappelmann"›
section ‹Syntax Bundles for Transport›
theory Transport_Syntax
  imports
    Transport
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 no_galois_rel_syntax
begin
  no_notation galois_rel.Galois ("'((⇘_⇙)⪅(⇘(_) (_)⇙)')")
  no_notation Galois_infix ("(_) (⇘_⇙)⪅(⇘(_) (_)⇙) (_)" [51,51,51,51,51] 50)
  no_notation ge_Galois ("'((⇘(_) (_)⇙)⪆(⇘_⇙)')")
  no_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
bundle no_transport_syntax
begin
  no_notation transport.preorder_equivalence (infix "≡⇘pre⇙" 50)
  no_notation transport.partial_equivalence_rel_equivalence (infix "≡⇘PER⇙" 50)
end


end