HomeIsabelle/Phabricator
Diffusion afp-devel 237996782d80

feat(Transport) functions as binary relations, improved mono notation, make non…
237996782d80
Actions

Description

feat(Transport) functions as binary relations, improved mono notation, make non-dependent relators definitions, generalise some concepts

Details

Provenance
kappelmannAuthored on
Parents
rAFPfe57a84f565f: feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems…
Branches
Unknown
Tags
Unknown

Changes (101)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.
PathSize
Functions/
Properties/
Galois/
Functions/
Functors/
Transport/
Compositions/
Agree/
Generic/
Examples/
Prototype/
Typedef/
Functions/
Natural_Functors/

rAFP237996782d80

View Options

thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Agree.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Extend.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Dependent_Binary_Relations.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Clean_Function.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Base.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Composition.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Evaluation.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Extend.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Lambda.thy

View Options

thys/Transport/HOL_Basics/Binary_Relations/LBinary_Relations.thy

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

thys/Transport/HOL_Basics/Functions/Function_Relators.thy

View Options

thys/Transport/HOL_Basics/Functions/Functions_Base.thy

View Options

thys/Transport/HOL_Basics/Functions/Functions_Restrict.thy

View Options

thys/Transport/HOL_Basics/Functions/LFunctions.thy

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

thys/Transport/HOL_Basics/Galois/Galois.thy

View Options

thys/Transport/HOL_Basics/Galois/Galois_Property.thy

View Options

thys/Transport/HOL_Basics/Galois/Galois_Relator.thy

View Options

thys/Transport/HOL_Basics/Galois/Half_Galois_Property.thy

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Galois.thy

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Orders.thy

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Binary_Relations.thy

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Functions.thy

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Orders.thy

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Predicates.thy

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignments.thy

View Options

thys/Transport/HOL_Basics/HOL_Basics.thy

View Options

thys/Transport/HOL_Basics/HOL_Basics_Base.thy

View Options

thys/Transport/HOL_Basics/HOL_Mem_Of.thy

View Options

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

View Options

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

View Options

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

View Options

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

View Options

thys/Transport/HOL_Basics/Orders/Linear_Orders.thy

View Options

thys/Transport/HOL_Basics/Orders/Orders.thy

View Options

thys/Transport/HOL_Basics/Predicates/Bounded_Definite_Description.thy

View Options

thys/Transport/HOL_Basics/Predicates/Bounded_Quantifiers.thy

View Options

thys/Transport/HOL_Basics/Predicates/Predicate_Functions.thy

View Options

thys/Transport/HOL_Basics/Predicates/Predicates.thy

View Options

thys/Transport/HOL_Basics/Predicates/Predicates_Order.thy

View Options

thys/Transport/ROOT

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

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

View Options

thys/Transport/Transport/Examples/Transport_Dep_Fun_Rel_Examples.thy

View Options

thys/Transport/Transport/Examples/Transport_Lists_Sets_Examples.thy

View Options

thys/Transport/Transport/Examples/Transport_Partial_Quotient_Types.thy

View Options

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

View Options

thys/Transport/Transport/Functions/Monotone_Function_Relator.thy

View Options

thys/Transport/Transport/Functions/Reflexive_Relator.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Base.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Galois_Connection.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Galois_Equivalence.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Galois_Property.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Galois_Relator.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Monotone.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Order_Base.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Order_Equivalence.thy

View Options

thys/Transport/Transport/Functions/Transport_Functions_Relation_Simplifications.thy

View Options

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Base.thy

View Options

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Equivalence.thy