Theory Transport_White_Box

✐‹creator "Kevin Kappelmann"›
theory Transport_White_Box
  imports
    Transport_Equality
    Transport_Existential_Quantifier
    Transport_Galois_Relator_Properties
    Transport_Implies
    Transport_Universal_Quantifier
begin

paragraph ‹Summary›
text ‹Theorems for white-box transports.›

context galois
begin
(*TODO: for the Galois relator, many assumptions needed for the white-box transport theorems of the
logical connectives become vacuous. Example:*)

notepad
begin
  print_statement Fun_Rel_imp_eq_restrict_if_right_unique_onI
    [of "in_field (≤⇘L⇙)" "(⇘L⇙⪅)" "in_field (≤⇘R⇙)"]

  have "((⇘L⇙⪅) ⇛ (⟶)) (in_field (≤⇘L⇙)) (in_field (≤⇘R⇙))" by (intro Fun_Rel_relI) auto
end

end

end