Theory Transport_Via_Partial_Galois_Connections_Equivalences_Paper

✐‹creator "Kevin Kappelmann"›
section ‹Transport Paper Guide›
theory Transport_Via_Partial_Galois_Connections_Equivalences_Paper
  imports
    Transport_Black_Box
    Transport_Natural_Functors
    Transport_Partial_Quotient_Types
    Transport_Prototype
    Transport_Lists_Sets_Examples
    Transport_Dep_Fun_Rel_Examples
    Transport_Typedef_Base
begin

text ‹

▪ Section 3.1: Order basics can be found in
  @{theory "Transport.Binary_Relation_Properties"},
  @{theory "Transport.Preorders"},
  @{theory "Transport.Partial_Equivalence_Relations"},
  @{theory "Transport.Equivalence_Relations"}, and
  @{theory "Transport.Order_Functions_Base"}.
Theorem

▪ Section 3.2: Function relators and monotonicity can be found in
  @{theory "Transport.Function_Relators"} and
  @{theory "Transport.Functions_Monotone"}

▪ Section 3.3: Galois relator can be found in
  @{theory "Transport.Galois_Relator_Base"}.

  ▪ Lemma 1: @{theory "Transport.Transport_Partial_Quotient_Types"}
  (*results from Appendix*)

  ▪ Lemma 3: @{thm "galois_prop.Galois_right_iff_left_Galois_if_galois_prop"}

▪ Section 3.4: Partial Galois Connections and Equivalences can be found in
  @{theory "Transport.Half_Galois_Property"},
  @{theory "Transport.Galois_Property"},
  @{theory "Transport.Galois_Connections"},
  @{theory "Transport.Galois_Equivalences"}, and
  @{theory "Transport.Order_Equivalences"}.

  ▪ Lemma 2: @{theory "Transport.Transport_Partial_Quotient_Types"}
  (*results from Appendix*)

  ▪ Lemma 4: @{thm "galois.galois_equivalence_left_right_if_transitive_if_order_equivalence"}

  ▪ Lemma 5: @{thm "galois.order_equivalence_if_reflexive_on_in_field_if_galois_equivalence"}

▪ Section 4.1: Closure (Dependent) Function Relator can be found in
  @{dir "Black_Box/Functions"}.

  ▪ Monotone function relator @{theory "Transport.Monotone_Function_Relator"}.

  ▪ Setup of construction @{theory "Transport.Transport_Functions_Base"}.

  ▪ Theorem 1: see @{theory "Transport.Transport_Functions"}

  ▪ Theorem 2: see @{thm "transport_Mono_Dep_Fun_Rel.left_Galois_iff_Dep_Fun_Rel_left_Galois_if_preorder_equivalenceI'"}
  (*results from Appendix*)

  ▪ Lemma 6: @{thm "transport_Mono_Fun_Rel.galois_connection_left_rightI"}

  ▪ Lemma 7: @{thm "transport_Mono_Fun_Rel.left_Galois_iff_Fun_Rel_left_GaloisI"}

  ▪ Theorem 7: @{thm "transport_Mono_Dep_Fun_Rel.galois_connection_left_right_if_mono_if_galois_connectionI'"}

  ▪ Theorem 8: @{thm "transport_Mono_Dep_Fun_Rel.left_Galois_iff_Dep_Fun_Rel_left_Galois_if_mono_if_galois_connectionI'"}

  ▪ Lemma 8 @{thm "transport_Mono_Dep_Fun_Rel.left_rel_eq_tdfr_leftI_if_equivalencesI"}

  ▪ Lemma 9: @{thm "transport_Mono_Fun_Rel.left_rel_eq_tfr_leftI"}

▪ Section 4.2: Closure Natural Functors can be found in
  @{dir "Black_Box/Natural_Functors"}.
  ▪ Theorem 3: see @{theory "Transport.Transport_Natural_Functors"}

  ▪ Theorem 4: @{thm "transport_natural_functor.left_Galois_eq_Frel_left_Galois"}


▪ Section 4.3: Closure Compositions can be found in @{dir "Black_Box/Compositions"}.

  ▪ Setup for simple case in @{theory "Transport.Transport_Compositions_Agree_Base"}

  ▪ Setup for generic case in @{theory "Transport.Transport_Compositions_Generic_Base"}

  ▪ Theorem 5: @{thm "transport_comp.preorder_equivalenceI"} and

    @{thm "transport_comp.partial_equivalence_rel_equivalenceI"}
  ▪ Theorem 6: @{thm "transport_comp.left_Galois_eq_comp_left_GaloisI"}

  (*results from Appendix*)
  ▪ Theorem 9: see @{dir "Black_Box/Compositions/Agree"}, results in

    @{locale transport_comp_same}.
  ▪ Theorem 10: @{thm "transport_comp.galois_connection_left_right_if_galois_equivalenceI"}

  ▪ Theorem 11: @{thm "transport_comp.left_Galois_eq_comp_left_GaloisI'"}

▪ Section 5:

  ▪ Implementation @{theory "Transport.Transport_Prototype"}:
    Note: the command "trp" from the paper is called @{command trp_term} and the
    method "trprover" is called "trp\_term\_prover".

  ▪ Example 1: @{theory "Transport.Transport_Lists_Sets_Examples"}

  ▪ Example 2: @{theory "Transport.Transport_Dep_Fun_Rel_Examples"}

  ▪ Example 3: 🌐‹https://github.com/kappelmann/Isabelle-Set/blob/fdf59444d9a53b5279080fb4d24893c9efa31160/Isabelle_Set/Integers/Integers_Transport.thy›

▪ Proof: Partial Quotient Types are a special case:
  @{theory "Transport.Transport_Partial_Quotient_Types"}

▪ Proof: Typedefs are a special case:
  @{theory "Transport.Transport_Typedef_Base"}

▪ Proof: Set-Extensions are a special case: 🌐‹https://github.com/kappelmann/Isabelle-Set/blob/fdf59444d9a53b5279080fb4d24893c9efa31160/Isabelle_Set/Set_Extensions/Set_Extensions_Transport.thy›

▪ Proof: Bijections as special case:
  @{theory "Transport.Transport_Bijections"}
›

end