Diffusion afp-devel 46cc27ac91e4

New submission Transport
46cc27ac91e4
Actions

Tags

None

Subscribers

None

Description

New submission Transport

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFP2cd51acba0cf: update S_Finite_Measure_Monad to Isabelle2023

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFP46cc27ac91e4: New submission Transport.Oct 13 2023, 1:13 PM

Changes (145)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

Binary_Relations

Binary_Relation_Functions.thy

Binary_Relations_Lattice.thy

LBinary_Relations.thy

Binary_Relations_Order.thy

Binary_Relations_Order_Base.thy

Binary_Relation_Properties.thy

Binary_Relations_Antisymmetric.thy

Binary_Relations_Injective.thy

Binary_Relations_Irreflexive.thy

Binary_Relations_Left_Total.thy

Binary_Relations_Reflexive.thy

Binary_Relations_Right_Unique.thy

Binary_Relations_Surjective.thy

Binary_Relations_Symmetric.thy

Binary_Relations_Transitive.thy

Restricted_Equality.thy

Function_Relators.thy

Functions_Base.thy

Function_Properties.thy

Functions_Bijection.thy

Functions_Injective.thy

Functions_Inverse.thy

Functions_Monotone.thy

Functions_Surjective.thy

Galois_Base.thy

Galois_Connections.thy

Galois_Equivalences.thy

Galois_Property.thy

Galois_Relator.thy

Galois_Relator_Base.thy

Half_Galois_Property.thy

HOL_Algebra_Alignment_Galois.thy

HOL_Algebra_Alignment_Orders.thy

HOL_Algebra_Alignments.thy

HOL_Alignment_Binary_Relations.thy

HOL_Alignment_Functions.thy

HOL_Alignment_Orders.thy

HOL_Alignments.thy

HOL_Basics_Base.thy

HOL_Syntax_Bundles

HOL_Syntax_Bundles.thy

HOL_Syntax_Bundles_Base.thy

HOL_Syntax_Bundles_Functions.thy

HOL_Syntax_Bundles_Groups.thy

HOL_Syntax_Bundles_Lattices.thy

HOL_Syntax_Bundles_Orders.thy

HOL_Syntax_Bundles_Relations.thy

Equivalence_Relations.thy

Closure_Operators.thy

Order_Functions.thy

Order_Functions_Base.thy

Order_Equivalences.thy

Order_Functors.thy

Order_Functors_Base.thy

Partial_Equivalence_Relations.thy

Partial_Orders.thy

Predicates_Lattice.thy

Predicates_Order.thy

Transport_Compositions_Agree.thy

Transport_Compositions_Agree_Base.thy

Transport_Compositions_Agree_Galois_Connection.thy

Transport_Compositions_Agree_Galois_Equivalence.thy

Transport_Compositions_Agree_Galois_Property.thy

Transport_Compositions_Agree_Galois_Relator.thy

Transport_Compositions_Agree_Monotone.thy

Transport_Compositions_Agree_Order_Equivalence.thy

Transport_Compositions_Generic.thy

Transport_Compositions_Generic_Base.thy

Transport_Compositions_Generic_Galois_Connection.thy

Transport_Compositions_Generic_Galois_Equivalence.thy

Transport_Compositions_Generic_Galois_Property.thy

Transport_Compositions_Generic_Galois_Relator.thy

Transport_Compositions_Generic_Monotone.thy

Transport_Compositions_Generic_Order_Base.thy

Transport_Compositions_Generic_Order_Equivalence.thy

Transport_Compositions.thy

Transport_Prototype.thy

Transport_Rel_If.thy

transport_util.ML

Transport_Dep_Fun_Rel_Examples.thy

Transport_Lists_Sets_Examples.thy

Transport_Partial_Quotient_Types.thy

Transport_Syntax.thy

Transport_Typedef.thy

Transport_Typedef_Base.thy

Monotone_Function_Relator.thy

Reflexive_Relator.thy

Transport_Functions.thy

Transport_Functions_Base.thy

Transport_Functions_Galois_Connection.thy

Transport_Functions_Galois_Equivalence.thy

Transport_Functions_Galois_Property.thy

Transport_Functions_Galois_Relator.thy

Transport_Functions_Monotone.thy

Transport_Functions_Order_Base.thy

Transport_Functions_Order_Equivalence.thy

Transport_Functions_Relation_Simplifications.thy

Natural_Functors

Transport_Natural_Functors.thy

Transport_Natural_Functors_Base.thy

Transport_Natural_Functors_Galois.thy

Transport_Natural_Functors_Galois_Relator.thy

Transport_Natural_Functors_Order_Base.thy

Transport_Natural_Functors_Order_Equivalence.thy

Transport_Base.thy

Transport_Bijections.thy

Transport_Identity.thy

Transport_Via_Partial_Galois_Connections_Equivalences_Paper.thy

rAFP46cc27ac91e4

thys/ROOTS

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Lattice.thy

thys/Transport/HOL_Basics/Binary_Relations/LBinary_Relations.thy

thys/Transport/HOL_Basics/Binary_Relations/Order/Binary_Relations_Order.thy

thys/Transport/HOL_Basics/Binary_Relations/Order/Binary_Relations_Order_Base.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relation_Properties.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Antisymmetric.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Injective.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Irreflexive.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Left_Total.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Reflexive.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Right_Unique.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Surjective.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Symmetric.thy

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Transitive.thy

thys/Transport/HOL_Basics/Binary_Relations/Restricted_Equality.thy

thys/Transport/HOL_Basics/Functions/Function_Relators.thy

thys/Transport/HOL_Basics/Functions/Functions_Base.thy

thys/Transport/HOL_Basics/Functions/LFunctions.thy

thys/Transport/HOL_Basics/Functions/Properties/Function_Properties.thy

thys/Transport/HOL_Basics/Functions/Properties/Functions_Bijection.thy

thys/Transport/HOL_Basics/Functions/Properties/Functions_Injective.thy

thys/Transport/HOL_Basics/Functions/Properties/Functions_Inverse.thy

thys/Transport/HOL_Basics/Functions/Properties/Functions_Monotone.thy

thys/Transport/HOL_Basics/Functions/Properties/Functions_Surjective.thy

thys/Transport/HOL_Basics/Galois/Galois.thy

thys/Transport/HOL_Basics/Galois/Galois_Base.thy

thys/Transport/HOL_Basics/Galois/Galois_Connections.thy

thys/Transport/HOL_Basics/Galois/Galois_Equivalences.thy

thys/Transport/HOL_Basics/Galois/Galois_Property.thy

thys/Transport/HOL_Basics/Galois/Galois_Relator.thy

thys/Transport/HOL_Basics/Galois/Galois_Relator_Base.thy

thys/Transport/HOL_Basics/Galois/Half_Galois_Property.thy

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Galois.thy

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Orders.thy

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignments.thy

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Binary_Relations.thy

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Functions.thy

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Orders.thy

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignments.thy

thys/Transport/HOL_Basics/HOL_Basics.thy

thys/Transport/HOL_Basics/HOL_Basics_Base.thy

thys/Transport/HOL_Basics/HOL_Mem_Of.thy

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles.thy

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Base.thy

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Functions.thy

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Groups.thy

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Lattices.thy

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Orders.thy

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Relations.thy

thys/Transport/HOL_Basics/Orders/Equivalence_Relations.thy

thys/Transport/HOL_Basics/Orders/Functions/Closure_Operators.thy

thys/Transport/HOL_Basics/Orders/Functions/Order_Functions.thy

thys/Transport/HOL_Basics/Orders/Functions/Order_Functions_Base.thy

thys/Transport/HOL_Basics/Orders/Functors/Order_Equivalences.thy

thys/Transport/HOL_Basics/Orders/Functors/Order_Functors.thy

thys/Transport/HOL_Basics/Orders/Functors/Order_Functors_Base.thy

thys/Transport/HOL_Basics/Orders/Orders.thy

thys/Transport/HOL_Basics/Orders/Partial_Equivalence_Relations.thy

thys/Transport/HOL_Basics/Orders/Partial_Orders.thy

thys/Transport/HOL_Basics/Orders/Preorders.thy

thys/Transport/HOL_Basics/Predicates/Predicates.thy

thys/Transport/HOL_Basics/Predicates/Predicates_Lattice.thy

thys/Transport/HOL_Basics/Predicates/Predicates_Order.thy

thys/Transport/README.md

thys/Transport/ROOT

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree.thy

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Base.thy

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Connection.thy

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Equivalence.thy

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Property.thy

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Relator.thy

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Monotone.thy

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Order_Equivalence.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Base.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Connection.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Equivalence.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Property.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Relator.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Monotone.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Order_Base.thy

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Order_Equivalence.thy

thys/Transport/Transport/Compositions/Transport_Compositions.thy

thys/Transport/Transport/Examples/Prototype/Transport_Prototype.thy

thys/Transport/Transport/Examples/Prototype/Transport_Rel_If.thy

thys/Transport/Transport/Examples/Prototype/transport.ML

thys/Transport/Transport/Examples/Prototype/transport_util.ML

thys/Transport/Transport/Examples/Transport_Dep_Fun_Rel_Examples.thy

thys/Transport/Transport/Examples/Transport_Lists_Sets_Examples.thy

thys/Transport/Transport/Examples/Transport_Partial_Quotient_Types.thy

thys/Transport/Transport/Examples/Transport_Syntax.thy

thys/Transport/Transport/Examples/Typedef/Transport_Typedef.thy

thys/Transport/Transport/Examples/Typedef/Transport_Typedef_Base.thy

thys/Transport/Transport/Functions/Monotone_Function_Relator.thy

thys/Transport/Transport/Functions/Reflexive_Relator.thy

thys/Transport/Transport/Functions/Transport_Functions.thy

thys/Transport/Transport/Functions/Transport_Functions_Base.thy

thys/Transport/Transport/Functions/Transport_Functions_Galois_Connection.thy

thys/Transport/Transport/Functions/Transport_Functions_Galois_Equivalence.thy

thys/Transport/Transport/Functions/Transport_Functions_Galois_Property.thy

thys/Transport/Transport/Functions/Transport_Functions_Galois_Relator.thy

thys/Transport/Transport/Functions/Transport_Functions_Monotone.thy

thys/Transport/Transport/Functions/Transport_Functions_Order_Base.thy

thys/Transport/Transport/Functions/Transport_Functions_Order_Equivalence.thy

thys/Transport/Transport/Functions/Transport_Functions_Relation_Simplifications.thy

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors.thy

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Base.thy

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Galois.thy

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Galois_Relator.thy

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Base.thy

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Equivalence.thy

thys/Transport/Transport/Transport.thy

thys/Transport/Transport/Transport_Base.thy

thys/Transport/Transport/Transport_Bijections.thy

thys/Transport/Transport/Transport_Identity.thy

thys/Transport/Transport/Transport_Via_Partial_Galois_Connections_Equivalences_Paper.thy

thys/Transport/document/root.bib

thys/Transport/document/root.tex