Diffusion afp-devel 401f381c1542

feat(Transport) major improvement of overloaded properties + new relational…
401f381c1542
Actions

Tags

None

Subscribers

None

Description

feat(Transport) major improvement of overloaded properties + new relational properties

Details

Provenance

Authored on

Parents

rAFP999b71d9f41d: fix(ML_Unification) replace binders before aeconv (avoids lowering)

Branches

Unknown

Tags

Unknown

Event Timeline

kappelmann committed rAFP401f381c1542: feat(Transport) major improvement of overloaded properties + new relational….Mar 25 2024, 10:48 AM

Changes (62)

Path

Size

Binary_Relations

Binary_Relation_Functions.thy

Binary_Relations_Lattice.thy

Order/

Binary_Relations_Order.thy

Binary_Relations_Order_Base.thy

Binary_Relation_Properties.thy

Binary_Relations_Antisymmetric.thy

Binary_Relations_Bi_Total.thy

Binary_Relations_Bi_Unique.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

Reverse_Implies.thy

Function_Relators.thy

Functions_Restrict.thy

Properties/

Functions_Bijection.thy

Functions_Injective.thy

Functions_Inverse.thy

Functions_Monotone.thy

Functions_Surjective.thy

Galois/

Galois_Relator_Base.thy

Half_Galois_Property.thy

HOL_Alignments/

HOL_Algebra_Alignment_Galois.thy

HOL_Alignment_Binary_Relations.thy

HOL_Alignment_Functions.thy

HOL_Alignment_Orders.thy

Orders/

Equivalence_Relations.thy

Functions/

Closure_Operators.thy

Order_Functions_Base.thy

Functors/

Order_Functors_Base.thy

Partial_Equivalence_Relations.thy

Partial_Orders.thy

Transport/

Compositions/

Agree/

Transport_Compositions_Agree_Order_Equivalence.thy

Generic/

Transport_Compositions_Generic_Galois_Connection.thy

Transport_Compositions_Generic_Galois_Property.thy

Examples/

Prototype/

Transport_Prototype.thy

Transport_Rel_If.thy

Transport_Dep_Fun_Rel_Examples.thy

Functions/

Reflexive_Relator.thy

Transport_Functions_Galois_Property.thy

Transport_Functions_Galois_Relator.thy

Transport_Functions_Order_Base.thy

Transport_Functions_Order_Equivalence.thy

Natural_Functors/

Transport_Natural_Functors_Base.thy

Transport_Natural_Functors_Galois_Relator.thy

Transport_Natural_Functors_Order_Base.thy

Transport_Natural_Functors_Order_Equivalence.thy

Transport_Bijections.thy

rAFP401f381c1542

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Lattice.thy

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Restricted_Equality.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Reverse_Implies.thy

Loading...

thys/Transport/HOL_Basics/Functions/Function_Relators.thy

Loading...

thys/Transport/HOL_Basics/Functions/Functions_Restrict.thy

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

thys/Transport/HOL_Basics/Galois/Galois_Relator_Base.thy

Loading...

thys/Transport/HOL_Basics/Galois/Half_Galois_Property.thy

Loading...

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Galois.thy

Loading...

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Binary_Relations.thy

Loading...

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Functions.thy

Loading...

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Orders.thy

Loading...

thys/Transport/HOL_Basics/HOL_Mem_Of.thy

Loading...

thys/Transport/HOL_Basics/Orders/Equivalence_Relations.thy

Loading...

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

Loading...

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

Loading...

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

Loading...

thys/Transport/HOL_Basics/Orders/Partial_Equivalence_Relations.thy

Loading...

thys/Transport/HOL_Basics/Orders/Partial_Orders.thy

Loading...

thys/Transport/HOL_Basics/Orders/Preorders.thy

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

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

Loading...

thys/Transport/Transport/Examples/Transport_Dep_Fun_Rel_Examples.thy

Loading...

thys/Transport/Transport/Functions/Reflexive_Relator.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Galois_Property.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Galois_Relator.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Order_Base.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Order_Equivalence.thy

Loading...

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Base.thy

Loading...

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Galois_Relator.thy

Loading...

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Base.thy

Loading...

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Equivalence.thy

Loading...

thys/Transport/Transport/Transport_Bijections.thy

Loading...