diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,725 +1,726 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod AOT Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory Balog_Szemeredi_Gowers BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel Cook_Levin CRYSTALS-Kyber CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport CHERI-C_Memory_Model Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Maximum_Segment_Sum Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Padic_Field Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma SCC_Bloemen_Sequential Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code +StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Turans_Graph_Theorem Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/StrictOmegaCategories/Globular_Set.thy b/thys/StrictOmegaCategories/Globular_Set.thy new file mode 100644 --- /dev/null +++ b/thys/StrictOmegaCategories/Globular_Set.thy @@ -0,0 +1,357 @@ +theory Globular_Set + +imports "HOL-Library.FuncSet" + +begin + +section \Background material on extensional functions\ + +lemma PiE_imp_Pi: "f \ A \\<^sub>E B \ f \ A \ B" by fast + +lemma PiE_iff': "f \ A \\<^sub>E B = (f \ A \ B \ f \ extensional A)" + by (simp add: PiE_iff Pi_iff) + +abbreviation composing ("_ \ _ \ _" [60,0,60]59) + where "g \ f \ D \ compose D g f" + +lemma compose_PiE: "f \ A \ B \ g \ B \ C \ g \ f \ A \ A \\<^sub>E C" + by (metis funcset_compose compose_extensional PiE_iff') + +lemma compose_eq_iff: "(g \ f \ A = k \ h \ A) = (\x \ A. g (f x) = k (h x))" +proof (safe) + fix x assume "g \ f \ A = k \ h \ A" "x \ A" + then show "g (f x) = k (h x)" by (metis compose_eq) +next + assume "\x \ A. g (f x) = k (h x)" + hence "\x. x \ A \ (g \ f \ A) x = (k \ h \ A) x" by (metis compose_eq) + then show "g \ f \ A = k \ h \ A" by (metis extensionalityI compose_extensional) +qed + +lemma compose_eq_if: "(\x. x \ A \ g (f x) = k (h x)) \ g \ f \ A = k \ h \ A" + using compose_eq_iff by blast + +lemma compose_compose_eq_iff2: "(h \ (g \ f \ A) \ A = h' \ (g' \ f' \ A) \ A) = + (\x \ A. h (g (f x)) = h' (g' (f' x)))" + by (simp add: compose_eq compose_eq_iff) + +lemma compose_compose_eq_iff1: assumes "f \ A \ B" "f' \ A \ B" + shows "((h \ g \ B) \ f \ A = (h' \ g' \ B) \ f' \ A) = (\x \ A. h (g (f x)) = h' (g' (f' x)))" +proof - + have "(h \ g \ B) \ f \ A = h \ (g \ f \ A) \ A" by (metis assms(1) compose_assoc) + moreover have "(h' \ g' \ B) \ f' \ A = h' \ (g' \ f' \ A) \ A" by (metis assms(2) compose_assoc) + ultimately have h: "((h \ g \ B) \ f \ A = (h' \ g' \ B) \ f' \ A) = + (h \ (g \ f \ A) \ A = h' \ (g' \ f' \ A) \ A)" by presburger + then show ?thesis by (simp only: h compose_compose_eq_iff2) +qed + +lemma compose_compose_eq_if1: "\f \ A \ B; f' \ A \ B; \x \ A. h (g (f x)) = h' (g' (f' x))\ \ + (h \ g \ B) \ f \ A = (h' \ g' \ B) \ f' \ A" + using compose_compose_eq_iff1 by blast + +lemma compose_compose_eq_if2: "\x \ A. h (g (f x)) = h' (g' (f' x)) \ + h \ (g \ f \ A) \ A = h' \ (g' \ f' \ A) \ A" + using compose_compose_eq_iff2 by blast + +lemma compose_restrict_eq1: "f \ A \ B \ restrict g B \ f \ A = g \ f \ A" + by (smt (verit) PiE compose_eq_iff restrict_apply') + +lemma compose_restrict_eq2: "g \ (restrict f A) \ A = g \ f \ A" + by (metis (mono_tags, lifting) compose_eq_if restrict_apply') + +lemma compose_Id_eq_restrict: "g \ (\x \ A. x) \ A = restrict g A" + by (smt (verit) compose_restrict_eq1 compose_def restrict_apply' restrict_ext) + +section \Globular sets\ + +subsection \Globular sets\ + +text \ + We define a locale \globular_set\ that encodes the cell data of a strict $\omega$-category + \cite[Def 1.4.5]{Leinster2004}. The elements of \X n\ are the \n\-cells, and the maps \s\ + and \t\ give the source and target of a cell, respectively. +\ + +locale globular_set = + fixes X :: "nat \ 'a set" and s :: "nat \ 'a \ 'a" and t :: "nat \ 'a \ 'a" + assumes s_fun: "s n \ X (Suc n) \ X n" + and t_fun: "t n \ X (Suc n) \ X n" + and s_comp: "x \ X (Suc (Suc n)) \ s n (t (Suc n) x) = s n (s (Suc n) x)" + and t_comp: "x \ X (Suc (Suc n)) \ t n (s (Suc n) x) = t n (t (Suc n) x)" +begin + +lemma s_comp': "s n \ t (Suc n) \ X (Suc (Suc n)) = s n \ s (Suc n) \ X (Suc (Suc n))" + by (metis (full_types) compose_eq_if s_comp) + +lemma t_comp': "t n \ s (Suc n) \ X (Suc (Suc n)) = t n \ t (Suc n) \ X (Suc (Suc n))" + by (metis (full_types) compose_eq_if t_comp) + +text \These are the generalised source and target maps. The arguments are the dimension of the +input and output, respectively. They allow notation similar to \s\<^sup>m\<^sup>-\<^sup>p\ in \cite{Leinster2004}.\ + +fun s' :: "nat \ nat \ 'a \ 'a" where +"s' 0 0 = id" | +"s' 0 (Suc n) = undefined" | +"s' (Suc m) n = (if Suc m < n then undefined + else if Suc m = n then id + else s' m n \ s m)" + +fun t' :: "nat \ nat \ 'a \ 'a" where +"t' 0 0 = id" | +"t' 0 (Suc n) = undefined" | +"t' (Suc m) n = (if Suc m < n then undefined + else if Suc m = n then id + else t' m n \ t m)" + +lemma s'_n_n [simp]: "s' n n = id" + by (cases n, simp_all) + +lemma s'_Suc_n_n [simp]: "s' (Suc n) n = s n" + by simp + +lemma s'_Suc_Suc_n_n [simp]: "s' (Suc (Suc n)) n = s n \ s (Suc n)" + by simp + +lemma s'_Suc [simp]: "n \ m \ s' (Suc m) n = s' m n \ s m" + by simp + +lemma s'_Suc': "n < m \ s' m n = s n \ s' m (Suc n)" +proof (induction m arbitrary: n) + case 0 + then show ?case by blast +next + case (Suc m) + hence "n \ m" by fastforce + show ?case proof (cases "n = m", simp) + assume "n \ m" + then show "s' (Suc m) n = s n \ s' (Suc m) (Suc n)" using Suc by fastforce + qed +qed + +lemma t'_n_n [simp]: "t' n n = id" + by (cases n, simp_all) + +lemma t'_Suc_n_n [simp]: "t' (Suc n) n = t n" + by simp + +lemma t'_Suc_Suc_n_n [simp]: "t' (Suc (Suc n)) n = t n \ t (Suc n)" + by simp + +lemma t'_Suc [simp]: "n \ m \ t' (Suc m) n = t' m n \ t m" + by simp + +lemma t'_Suc': "n < m \ t' m n = t n \ t' m (Suc n)" +proof (induction m arbitrary: n) + case 0 + then show ?case by blast +next + case (Suc m) + hence "n \ m" by fastforce + show ?case proof (cases "n = m", simp) + assume "n \ m" + then show "t' (Suc m) n = t n \ t' (Suc m) (Suc n)" using Suc by fastforce + qed +qed + +lemma s'_fun: "n \ m \ s' m n \ X m \ X n" +proof (induction m arbitrary: n) + case 0 + thus ?case by force +next + case (Suc m) + thus ?case proof (cases "n = Suc m") + case True + then show ?thesis by auto + next + case False + hence "n \ m" using `n \ Suc m` by force + thus ?thesis using Suc.IH s_fun s'_Suc by auto + qed +qed + +lemma t'_fun: "n \ m \ t' m n \ X m \ X n" +proof (induction m arbitrary: n) + case 0 + thus ?case by force +next + case (Suc m) + thus ?case proof (cases "n = Suc m") + case True + then show ?thesis by auto + next + case False + hence "n \ m" using `n \ Suc m` by force + thus ?thesis using Suc.IH t_fun t'_Suc by auto + qed +qed + +lemma s'_comp: "\ n < m; x \ X m \ \ s n (t' m (Suc n) x) = s' m n x" +proof (induction "m - n" arbitrary: n) + case 0 + then show ?case by force +next + case IH: (Suc k) + show ?case proof (cases k) + case 0 + with IH(2) have "m = Suc n" by fastforce + then show ?thesis using s'_Suc' by auto + next + case (Suc k') + with \Suc k = m - n\ have hle: "Suc (Suc n) \ m" by simp + hence "Suc n < m" by force + hence "Suc (Suc n) \ m" by fastforce + have "s n (t' m (Suc n) x) + = s n (t (Suc n) (t' m (Suc (Suc n)) x))" using t'_Suc' \Suc n < m\ by simp + also have "\ = s n (s (Suc n) (t' m (Suc (Suc n)) x))" + using t'_fun \Suc (Suc n) \ m\ s_comp IH(4) by blast + also have "\ = s n (s' m (Suc n) x)" + using IH Suc_diff_Suc Suc_inject \Suc n < m\ by presburger + finally show ?thesis using \n < m\ s'_Suc' by simp + qed +qed + +lemma t'_comp: "\ n < m; x \ X m \ \ t n (s' m (Suc n) x) = t' m n x" +proof (induction "m - n" arbitrary: n) + case 0 + then show ?case by force +next + case IH: (Suc k) + show ?case proof (cases k) + case 0 + with IH(2) have "m = Suc n" by fastforce + then show ?thesis using IH.prems(1) by auto + next + case (Suc k') + with \Suc k = m - n\ have hle: "Suc (Suc n) \ m" by simp + hence "Suc n < m" by force + hence "Suc (Suc n) \ m" by fastforce + have "t n (s' m (Suc n) x) + = t n (s (Suc n) (s' m (Suc (Suc n)) x))" using s'_Suc' \Suc n < m\ by simp + also have "\ = t n (t (Suc n) (s' m (Suc (Suc n)) x))" + using s'_fun \Suc (Suc n) \ m\ t_comp IH(4) by blast + also have "\ = t n (t' m (Suc n) x)" + using IH Suc_diff_Suc Suc_inject \Suc n < m\ by presburger + finally show ?thesis using \n < m\ t'_Suc' by simp + qed +qed + +text \The following predicates and sets are needed to define composition in an $\omega$-category.\ + +definition is_parallel_pair :: "nat \ nat \ 'a \ 'a \ bool" where +"is_parallel_pair m n x y \ n \ m \ x \ X m \ y \ X m \ s' m n x = s' m n y \ t' m n x = t' m n y" + +text \\cite[p. 44]{Leinster2004}\ +definition is_composable_pair :: "nat \ nat \ 'a \ 'a \ bool" where +"is_composable_pair m n y x \ n < m \ y \ X m \ x \ X m \ t' m n x = s' m n y" + +definition composable_pairs :: "nat \ nat \ ('a \ 'a) set" where +"composable_pairs m n = {(y, x). is_composable_pair m n y x}" + +lemma composable_pairs_empty: "m \ n \ composable_pairs m n = {}" + using is_composable_pair_def composable_pairs_def by simp + +end + +subsection \Maps between globular sets\ + +text \We define maps between globular sets to be natural transformations of the corresponding +functors \cite[Def 1.4.5]{Leinster2004}.\ + +locale globular_map = source: globular_set X s\<^sub>X t\<^sub>X + target: globular_set Y s\<^sub>Y t\<^sub>Y + for X s\<^sub>X t\<^sub>X Y s\<^sub>Y t\<^sub>Y + + fixes \ :: "nat \ 'a \ 'b" + assumes map_fun: "\ m \ X m \ Y m" + and is_natural_wrt_s: "x \ X (Suc m) \ \ m (s\<^sub>X m x) = s\<^sub>Y m (\ (Suc m) x)" + and is_natural_wrt_t: "x \ X (Suc m) \ \ m (t\<^sub>X m x) = t\<^sub>Y m (\ (Suc m) x)" +begin + +lemma is_natural_wrt_s': "\ n \ m; x \ X m \ \ \ n (source.s' m n x) = target.s' m n (\ m x)" +proof (induction "m - n" arbitrary: n) + case 0 + hence "m = n" by simp + then show ?case by fastforce +next + case (Suc k) + hence "n < m" by force + hence "Suc n \ m" by auto + have "\ n (source.s' m n x) = \ n (s\<^sub>X n (source.s' m (Suc n) x))" + using source.s'_Suc' \n < m\ by simp + also have "\ = s\<^sub>Y n (\ (Suc n) (source.s' m (Suc n) x))" + using source.s'_fun \Suc n \ m\ Suc(1) Suc(4) is_natural_wrt_s by blast + also have "\ = s\<^sub>Y n (target.s' m (Suc n) (\ m x))" + using Suc \Suc n \ m\ Suc_diff_Suc Suc_inject \n < m\ by presburger + finally show ?case using target.s'_Suc' \n < m\ by simp +qed + +lemma is_natural_wrt_t': "\ n \ m; x \ X m \ \ \ n (source.t' m n x) = target.t' m n (\ m x)" +proof (induction "m - n" arbitrary: n) + case 0 + hence "m = n" by simp + then show ?case by fastforce +next + case (Suc k) + hence "n < m" by force + hence "Suc n \ m" by auto + have "\ n (source.t' m n x) = \ n (t\<^sub>X n (source.t' m (Suc n) x))" + using source.t'_Suc' \n < m\ by simp + also have "\ = t\<^sub>Y n (\ (Suc n) (source.t' m (Suc n) x))" + using source.t'_fun \Suc n \ m\ Suc(1) Suc(4) is_natural_wrt_t by blast + also have "\ = t\<^sub>Y n (target.t' m (Suc n) (\ m x))" + using Suc \Suc n \ m\ Suc_diff_Suc Suc_inject \n < m\ by presburger + finally show ?case using target.t'_Suc' \n < m\ by simp +qed + +end + +text \The composition of two globular maps is itself a globular map. This intermediate + locale gathers the data needed for such a statement.\ +locale two_globular_maps = fst: globular_map X s\<^sub>X t\<^sub>X Y s\<^sub>Y t\<^sub>Y \ + snd: globular_map Y s\<^sub>Y t\<^sub>Y Z s\<^sub>Z t\<^sub>Z \ + for X s\<^sub>X t\<^sub>X Y s\<^sub>Y t\<^sub>Y Z s\<^sub>Z t\<^sub>Z \ \ + +sublocale two_globular_maps \ comp: globular_map X s\<^sub>X t\<^sub>X Z s\<^sub>Z t\<^sub>Z "\m. \ m \ \ m" +proof (unfold_locales) + fix m + show "\ m \ \ m \ X m \ Z m" using fst.map_fun snd.map_fun by fastforce +next + fix x m assume "x \ X (Suc m)" + then show "(\ m \ \ m) (s\<^sub>X m x) = s\<^sub>Z m ((\ (Suc m) \ \ (Suc m)) x)" + using fst.is_natural_wrt_s snd.is_natural_wrt_s comp_apply fst.map_fun by fastforce +next + fix x m assume "x \ X (Suc m)" + then show "(\ m \ \ m) (t\<^sub>X m x) = t\<^sub>Z m ((\ (Suc m) \ \ (Suc m)) x)" + using fst.is_natural_wrt_t snd.is_natural_wrt_t comp_apply fst.map_fun by fastforce +qed + +sublocale two_globular_maps \ compose: globular_map X s\<^sub>X t\<^sub>X Z s\<^sub>Z t\<^sub>Z "\m. \ m \ \ m \ X m" +proof (unfold_locales) + fix m + show "\ m \ \ m \ X m \ X m \ Z m" using funcset_compose fst.map_fun snd.map_fun by fast +next + fix x m assume "x \ X (Suc m)" + then show "(\ m \ \ m \ X m) (s\<^sub>X m x) = s\<^sub>Z m ((\ (Suc m) \ \ (Suc m) \ X (Suc m)) x)" + by (metis PiE fst.is_natural_wrt_s snd.is_natural_wrt_s fst.map_fun compose_eq fst.source.s_fun) +next + fix x m assume "x \ X (Suc m)" + then show "(\ m \ \ m \ X m) (t\<^sub>X m x) = t\<^sub>Z m ((\ (Suc m) \ \ (Suc m) \ X (Suc m)) x)" + by (metis PiE fst.is_natural_wrt_t snd.is_natural_wrt_t fst.map_fun compose_eq fst.source.t_fun) +qed + +subsection \The terminal globular set\ + +text \The terminal globular set, with a unique m-cell for each m \cite[p. 264]{Leinster2004}.\ + +interpretation final_glob: globular_set "\m. {()}" "\m. id" "\m. id" + by (unfold_locales, auto) + +context globular_set +begin + +text \\cite[p. 272]{Leinster2004}\ + +interpretation map_to_final_glob: globular_map X s t + "\m. {()}" "\m. id" "\m. id" + "\m. (\x. ())" + by (unfold_locales, simp_all) + +end + +end \ No newline at end of file diff --git a/thys/StrictOmegaCategories/Pasting_Diagram.thy b/thys/StrictOmegaCategories/Pasting_Diagram.thy new file mode 100644 --- /dev/null +++ b/thys/StrictOmegaCategories/Pasting_Diagram.thy @@ -0,0 +1,825 @@ +theory Pasting_Diagram +imports Strict_Omega_Category + +begin + +section \The category of pasting diagrams\ + +text \We define the strict $\omega$-category of pasting diagrams, 'pd'. We encode its cells as rooted + trees. First we develop some basic theory of trees.\ + +subsection \Rooted trees\ + +datatype tree = Node (subtrees: "tree list") \ \\cite[p. 268]{Leinster2004}\ + +abbreviation Leaf :: tree where +"Leaf \ Node []" + +fun subtree :: "tree \ nat list \ tree" ("_ !t _" [59,60]59) where +"t !t [] = t" | +"t !t (i#xs) = subtrees (t !t xs) ! i" + +value "Leaf !t []" (* Leaf *) +value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [0]" (* Node [Leaf, Leaf, Leaf] *) +value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [2,0]" (* Leaf *) +value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [1]" (* Leaf *) +value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [0,2]" (* Leaf *) + +lemma subtrees_Leaf: "(t = Leaf) = (subtrees t = [])" + by (metis tree.collapse tree.sel) + +fun is_subtree_index :: "tree \ nat list \ bool" where +"is_subtree_index t [] = True" | +"is_subtree_index t (i#xs) = (is_subtree_index t xs \ i < length (subtrees (t !t xs)))" + +lemma subtree_append: "ts ! i !t xs = Node ts !t xs @ [i]" + by (induction xs, auto) + +lemma is_subtree_index_append [iff]: "is_subtree_index (Node ts) (xs @ [i]) = + (i < length ts \ is_subtree_index (ts!i) xs)" +proof + show "is_subtree_index (Node ts) (xs @ [i]) \ i < length ts \ is_subtree_index (ts ! i) xs" + by (induction xs, auto simp: subtree_append) +next + show "i < length ts \ is_subtree_index (ts ! i) xs \ is_subtree_index (Node ts) (xs @ [i])" + by (induction xs, auto simp: subtree_append) +qed + +lemma is_subtree_index_append' [iff]: "is_subtree_index t (xs @ [i]) = + (is_subtree_index t [i] \ is_subtree_index (t !t [i]) xs)" + by (metis is_subtree_index_append is_subtree_index.simps subtree.simps tree.collapse) + +lemma max_set_upt [simp]: "Max {0.. []" + shows "length (subtrees (t !t xs)) = Suc (Max {i. is_subtree_index t (i # xs)})" +proof - + have "\i. is_subtree_index t (i # xs) = (i < length (subtrees (t !t xs)))" using assms(1) by simp + hence "{i. is_subtree_index t (i # xs)} = {0.. 0" using assms(2) by simp + ultimately show "length (subtrees (t !t xs)) = Suc (Max {i. is_subtree_index t (i # xs)})" + by (metis max_set_upt gr0_implies_Suc) +qed + +lemma tree_eq_iff_subtree_eq: "(t = u) = (length (subtrees t) = length (subtrees u) \ + (\i < length (subtrees t). t !t [i] = u !t [i]))" + by (cases t, cases u, auto simp add: list_eq_iff_nth_eq) + +text \We define the height of a rooted tree. A tree with only one node has height 0. The trees of +height at most n encode the n-cells in 'pd'.\ +fun height :: "tree \ nat" where +"height Leaf = 0" | +"height (Node ts) = Suc (fold (max \ height) ts 0)" + +value "height Leaf" (* 0 *) +value "height (Node [Leaf, Leaf])" (* 1 *) +value "height (Node [Node [Leaf, Leaf], Leaf])" (* 2 *) +value "height (Node [Node [Leaf, Node [Leaf]]])" (* 3 *) + +lemma height_Node [simp]: "ts \ [] \ height (Node ts) = Suc (fold (max \ height) ts 0)" + by (metis height.simps(2) neq_Nil_conv) + +lemma fold_eq_Max [simp]: "ts \ [] \ fold (max \ height) ts 0 = Max (set (map height ts))" + using Max.set_eq_fold fold_map list.exhaust + by (metis (no_types, lifting) fold_simps(2) map_is_Nil_conv max_nat.right_neutral) + +lemma height_Node_Max: "ts \ [] \ height (Node ts) = Suc (Max (set (map height ts)))" + by simp + +lemma height_Node_pos : "ts \ [] \ 0 < height (Node ts)" +proof (induction "Node ts" rule: height.induct) + case 1 + then show ?case by blast +next + case (2 t ts') + then show ?case by fastforce +qed + +lemma height_exists: + assumes "height (Node ts) = Suc n" + shows "\t. t \ set ts \ height t = n" +proof (cases "ts = []") + case True + then show ?thesis using assms by simp +next + case False + hence "n = Max (set (map height ts))" using assms height_Node_Max by force + hence "n \ set (map height ts)" using Max_in `ts \ []` by auto + then show ?thesis by auto +qed + +lemma height_lt: assumes "t \ set ts" shows "height t < height (Node ts)" +proof - + from assms have nemp: "ts \ []" by fastforce + have "height t \ Max (set (map height ts))" using assms by fastforce + also have "\ = fold (max \ height) ts 0" using nemp fold_eq_Max by simp + finally show ?thesis using nemp by simp +qed + +lemma height_le_imp_le_Suc: + assumes "\t \ set ts. height t \ n" + shows "height (Node ts) \ Suc n" +proof (cases "ts = []") + case True + then show ?thesis by simp +next + case False + hence "height (Node ts) = Suc (Max (set (map height ts)))" using height_Node_Max by blast + also have "\ \ Suc (Max (height ` set ts))" using set_map by fastforce + finally show ?thesis using `ts \ []` assms by simp +qed + +lemma height_zero [simp]: "height t = 0 \ t = Leaf" + by (metis height.cases height_Node_pos less_nat_zero_code) + +lemma is_subtree_index_length_le: "is_subtree_index t xs \ length xs \ height t" +proof (induction xs arbitrary: t rule: rev_induct) + case Nil + then show ?case by force +next + case (snoc i xs) + hence hi: "i < length (subtrees t)" by (metis is_subtree_index_append tree.exhaust_sel) + hence "length xs \ height (subtrees t ! i)" + by (metis snoc is_subtree_index_append tree.exhaust_sel) + moreover have "subtrees t ! i \ set (subtrees t)" using hi by simp + ultimately show ?case using height_lt by fastforce +qed + +lemma height_subtree: "is_subtree_index t xs \ height (t !t xs) \ height t - length xs" +proof (induction xs arbitrary: t rule: rev_induct) + case Nil + then show ?case by simp +next + case (snoc i xs) + hence "is_subtree_index (t !t [i]) xs" using is_subtree_index_append' by fastforce + hence "height (t !t [i] !t xs) \ height (t !t [i]) - length xs" using snoc.IH by blast + moreover have "height (t !t [i]) < height t" + by (metis height_lt is_subtree_index.simps(2) is_subtree_index_append' nth_mem snoc.prems + subtree.simps tree.collapse) + moreover have "t !t [i] !t xs = t !t xs @ [i]" using subtree_append by simp + ultimately show ?case by auto +qed + +lemma height_induct: "(\t. \u. height u < height t \ P u \ P t) \ P t" + by (metis Nat.measure_induct) + +lemma subtree_index_induct [case_names Index Step]: + assumes + "is_subtree_index t xs" + "\xs. \is_subtree_index t xs; \i < length (subtrees (t !t xs)). P (i#xs)\ \ P xs" + shows "P xs" +proof - + have hl: "length xs \ height t" by (simp add: assms(1) is_subtree_index_length_le) + then show "P xs" using assms + proof (induction "height t - length xs" arbitrary: xs) + case 0 + hence "height (t !t xs) = 0" using height_subtree by fastforce + hence "\i < length (subtrees (t !t xs)). P (i # xs)" + by (metis height_zero length_0_conv less_nat_zero_code tree.sel) + then show ?case using "0.prems" by blast + next + case (Suc n) + have "\i < length (subtrees (t !t xs)). P (i # xs)" + proof (safe) + fix i assume "i < length (subtrees (t !t xs))" + hence "is_subtree_index t (i # xs)" using Suc(4) by simp + moreover hence "length (i # xs) \ height t" using is_subtree_index_length_le by blast + moreover have "n = height t - length (i # xs)" using Suc(2) by simp + ultimately show "P (i # xs)" using Suc(1) Suc(5) by blast + qed + then show ?case using Suc.prems by blast + qed +qed + +text \The function \trim\ keeps the first n layers of a tree and removes the remaining ones.\ +fun trim :: "nat \ tree \ tree" where +"trim 0 t = Leaf" | +"trim (Suc n) (Node ts) = Node (map (trim n) ts)" + +lemma trim_Leaf [simp]: "trim n Leaf = Leaf" + by (metis list.simps(8) trim.elims trim.simps(2)) + +lemma height_trim_le: "height (trim n t) \ n" +proof (induction n t rule: trim.induct) + case (1 t) + then show ?case by auto +next + case (2 n ts) + hence "\t' \ set (map (trim n) ts). height t' \ n" by auto + then show ?case using height_le_imp_le_Suc trim.simps(2) by presburger +qed + +lemma trim_const: "height t \ n \ trim n t = t" +proof (induction n t rule: trim.induct) + case (1 t) + then show ?case using height_zero trim_Leaf by blast +next + case (2 n ts) + hence "\t. t \ set ts \ trim n t = t" using height_lt by fastforce + hence "map (trim n) ts = ts" using map_idI by blast + then show ?case by fastforce +qed + +lemma height_trim_le': "n \ height t \ height (trim n t) = n" +proof (induction n t rule: trim.induct) + case (1 t) + then show ?case by fastforce +next + case (2 n ts) + hence "\m. height (Node ts) = Suc m" by presburger + then obtain m where hm: "height (Node ts) = Suc m" by presburger + then obtain t where ht: "t \ set ts \ height t = m" using height_exists by meson + have "n \ m" using 2 hm by fastforce + hence hn: "height (trim n t) = n" using 2 ht by blast + have "trim n t \ set (subtrees (trim (Suc n) (Node ts)))" using ht by simp + then show ?case using hn height_lt by (metis height_trim_le leD le_SucE tree.collapse) +qed + +lemma height_trim: "height (trim n t) = (if n \ height t then n else height t)" + using height_trim_le' trim_const by auto + +value "trim 1 Leaf" +value "trim 1 (Node [Leaf, Leaf])" +value "trim 2 (Node [Node [Leaf, Leaf], Leaf])" +value "trim 1 (Node [Node [Leaf, Node [Leaf]], Node [Leaf]])" + +lemma trim_trim' [simp]: "trim n \ trim n = trim n" +proof (induction n) + case 0 + then show ?case by simp +next + case (Suc n) + then show ?case apply (simp add: fun_eq_iff) proof + fix t + show "trim (Suc n) (trim (Suc n) t) = trim (Suc n) t" + using Suc by (metis list.map_comp tree.exhaust trim.simps(2)) + qed +qed + +lemma trim_trim_Suc [simp]: "trim n \ trim (Suc n) = trim n" +proof (induction n) + case 0 + then show ?case by simp +next + case (Suc n) + then show ?case apply (simp add: fun_eq_iff) proof + fix t + show "trim (Suc n) (trim (Suc (Suc n)) t) = trim (Suc n) t" + using Suc by (metis list.map_comp tree.exhaust trim.simps(2)) + qed +qed + +lemma trim_trim [simp]: "n \ m \ trim n \ trim m = trim n" +proof (induction m arbitrary: n) + case 0 + then show ?case by force +next + case (Suc m) + then show ?case proof (cases "n = Suc m") + case True + then show ?thesis by auto + next + case False + hence "n \ m" using Suc.prems by auto + hence ih: "trim n = trim n \ trim m" using Suc by presburger + hence "trim n \ trim (Suc m) = (trim n \ trim m) \ trim (Suc m)" by simp + also have "\ = trim n \ trim m" by (metis fun.map_comp trim_trim_Suc) + finally show ?thesis using ih by auto + qed +qed + +lemma trim_eq_imp_trim_eq [simp]: "\n \ m; trim m t = trim m u\ \ trim n t = trim n u" + by (metis trim_trim comp_apply) + +lemma trim_1_eq: assumes "trim 1 (Node ts) = trim 1 (Node us)" shows "length ts = length us" +proof - + have "\vs. trim 1 (Node vs) = Node (map (\x. Leaf) vs)" by force + then show ?thesis using assms map_eq_imp_length_eq by auto +qed + +lemma length_subtrees_trim_Suc: "length (subtrees (trim (Suc n) t)) = length (subtrees t)" + by (induction t, simp) + +lemma trim_eq_Leaf: "trim n t = Leaf \ n = 0 \ t = Leaf" + by (induction n t rule: trim.induct, simp_all) + +lemma map_eq_imp_pairs_eq: "map f xs = map g ys \ (\x y. (x, y) \ set (zip xs ys) \ f x = g y)" + by (metis fst_eqD in_set_zip nth_map snd_eqD) + +lemma trim_eq_subtree_eq: + assumes "trim (Suc n) (Node ts) = trim (Suc n) (Node us)" + shows "\t u. (t, u) \ set (zip ts us) \ trim n t = trim n u" +proof - + fix t u assume "(t, u) \ set (zip ts us)" + moreover from assms have "map (trim n) ts = map (trim n) us" by fastforce + ultimately show "trim n t = trim n u" using map_eq_imp_pairs_eq by fast +qed + +lemma pairs_eq_imp_map_eq: + assumes "length xs = length ys" "\(x, y) \ set (zip xs ys). f x = g y" + shows "map f xs = map g ys" +proof - + have "\x y. (x, y) \ set (zip (map f xs) (map g ys)) \ x = y" proof - + fix x y assume h: "(x, y) \ set (zip (map f xs) (map g ys))" + hence "\n. (map f xs)!n = x \ (map g ys)!n = y \ n < length xs \ n < length ys" + by (metis in_set_zip fst_conv length_map snd_conv) + then obtain n where hn: "(map f xs)!n = x" "(map g ys)!n = y" "n < length xs" "n < length ys" + by blast + hence "(xs!n, ys!n) \ set (zip xs ys)" using in_set_zip by fastforce + with hn assms(2) show "x = y" by auto + qed + hence "\(x, y) \ set (zip (map f xs) (map g ys)). x = y" by force + with assms(1) list_eq_iff_zip_eq show "map f xs = map g ys" by fastforce +qed + +lemma map_eq_iff_pairs_eq: "(map f xs = map g ys) = + (length xs = length ys \ (\(x, y) \ set (zip xs ys). f x = g y))" +proof - + have "map f xs = map g ys \ \(x, y) \ set (zip xs ys). f x = g y" using map_eq_imp_pairs_eq + by fast + thus ?thesis by (metis pairs_eq_imp_map_eq length_map) +qed + +lemma subtree_eq_trim_eq: + assumes "length ts = length us" "\(t, u) \ set (zip ts us). trim n t = trim n u" + shows "trim (Suc n) (Node ts) = trim (Suc n) (Node us)" + by (auto simp add: assms map_eq_iff_pairs_eq) + +lemma subtree_trim_1: "is_subtree_index t [i] \ trim (Suc n) t !t [i] = trim n (t !t [i])" + by (smt (verit) Suc_inject is_subtree_index.simps(2) list.distinct(1) nat.distinct(1) nth_map + subtree.elims subtree.simps(2) tree.sel trim.elims) + +lemma is_subtree_index_trim: + "is_subtree_index (trim n t) xs = (is_subtree_index t xs \ length xs \ n)" +proof (induction n t arbitrary: xs rule: trim.induct) + case (1 t) + then show ?case using is_subtree_index_length_le by fastforce +next + case (2 n ts) + then show ?case proof (induction xs rule: rev_induct) + case Nil + then show ?case by auto + next + case (snoc x xs) + then show ?case by fastforce + qed +qed + +lemma subtree_trim: "\is_subtree_index t xs; length xs \ n\ \ + trim n t !t xs = trim (n - length xs) (t !t xs)" +proof (induction n t arbitrary: xs rule: trim.induct) + case (1 t) + then show ?case by simp +next + case (2 n ts) + then show ?case proof (cases "length xs = Suc n") + case True + hence "is_subtree_index (trim (Suc n) (Node ts)) xs" using is_subtree_index_trim 2 by blast + hence "height (trim (Suc n) (Node ts) !t xs) \ 0" + by (metis height_subtree height_trim_le True diff_is_0_eq') + then show ?thesis using True height_zero by fastforce + next + case False + then show ?thesis proof (cases xs rule: rev_cases) + case Nil + then show ?thesis by simp + next + case (snoc ys i) + have hi: "ts ! i \ set ts" "is_subtree_index (ts ! i) ys" using snoc 2(2) by simp_all + have hl: "length ys \ n" using snoc 2(3) by simp + have "Node (map (trim n) ts) !t ys @ [i] = trim n (ts ! i) !t ys" + by (metis "2.prems"(1) is_subtree_index_append nth_map snoc subtree_append) + also have "\ = trim (n - length ys) (ts ! i !t ys)" using 2(1) hi hl by blast + finally show "trim (Suc n) (Node ts) !t xs = trim (Suc n - length xs) (Node ts !t xs)" + by (simp add: snoc subtree_append) + qed + qed +qed + +lemma length_subtrees_trim: "\is_subtree_index t xs; length xs < n\ \ + length (subtrees (trim n t !t xs)) = length (subtrees (t !t xs))" + by (metis subtree_trim length_subtrees_trim_Suc Suc_diff_Suc less_imp_le_nat) + +lemma subtree_trim_Leaf: assumes "is_subtree_index (trim n t) xs" "t !t xs = Leaf" + shows "trim n t !t xs = Leaf" +proof (cases "length xs < n") + case True + then show ?thesis + using length_subtrees_trim assms is_subtree_index_trim subtrees_Leaf by fastforce +next + case False + hence "length xs = n" using assms(1) by (simp add: is_subtree_index_trim) + then show ?thesis using assms(1) is_subtree_index_trim subtree_trim by auto +qed + +subsection \The strict $\omega$-category of pasting diagrams\ + +text \The function \\\ acts as both the source and target map in the globular set of pasting +diagrams. It is denoted $\partial$ in Leinster \cite[p. 264]{Leinster2004}.\ +abbreviation \ where +"\ \ trim" + +value "\ 1 (Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]])" (* Leinster2004: (8.1), p. 264 *) +value "\ 2 (Node [Node [Node [Leaf, Leaf]], Node [Leaf, Leaf]])" (* Leinster2004: (8.3), p. 265 *) + +abbreviation PD :: "nat \ tree set" where +"PD n \ {t. height t \ n}" + +interpretation pd: globular_set PD \ \ + by (unfold_locales, auto simp add: height_trim_le) + +text \The generalised source and target maps have simple interpretations in terms of \trim\.\ + +lemma s'_eq_trim: assumes "n \ m" "height t \ m" shows "pd.s' m n t = trim n t" + using assms +proof (induction m arbitrary: t) + case 0 + moreover hence "n = 0" by force + ultimately show ?case using pd.s'_n_n trim_const by simp +next + case (Suc m) + then show ?case proof (cases "n = Suc m") + case True + then show ?thesis using pd.s'_n_n Suc(3) trim_const by simp + next + case False + with Suc(2) have "n \ m" by simp + hence "pd.s' (Suc m) n t = pd.s' m n (\ m t)" using Suc(3) by force + also have "\ = \ n (\ m t)" using Suc.IH height_trim_le \n \ m\ by blast + finally show ?thesis by (metis trim_trim \n \ m\ comp_apply) + qed +qed + +lemma s'_eq_t': "pd.s' = pd.t'" +proof (clarsimp simp add: fun_eq_iff) + fix m n t + show "pd.s' m n t = pd.t' m n t" proof (induction m arbitrary: n t) + case 0 + then show ?case + using pd.s'_n_n pd.t'_n_n pd.s'.simps(2) pd.t'.simps(2) by (cases n, presburger+) + next + case (Suc m) + then show ?case by (cases "Suc m" rule: linorder_cases, simp_all) + qed +qed + +lemma t'_eq_trim: assumes "n \ m" "height t \ m" shows "pd.t' m n t = trim n t" + by (metis (mono_tags, lifting) assms s'_eq_trim s'_eq_t') + +text \Next we define identities and composition \cite[p. 266]{Leinster2004}. The identity of a tree with height at most \n\ is + the same tree seen as a tree of height at most \n + 1\.\ + +fun tree_comp :: "nat \ tree \ tree \ tree" where +"tree_comp 0 (Node ts) (Node us) = Node (ts @ us)" | +"tree_comp (Suc n) (Node ts) (Node us) = Node (map2 (tree_comp n) ts us)" + +value "tree_comp 1 + (Node [Node [Leaf, Leaf], Leaf, Node [Leaf]]) + (Node [Leaf, Leaf, Node [Leaf, Leaf]])" + (* Node [Node [Leaf, Leaf], Leaf, Node [Leaf, Leaf, Leaf]] *) + (* Leinster2001: p. 39 *) + +value "tree_comp 0 + (Node [Node [Node [Leaf, Leaf]]]) + (Node [Node [Leaf, Leaf]])" + (* Node [Node [Node [Leaf, Leaf]], Node [Leaf, Leaf]] *) + (* Leinster2001: p. 39 *) + +value "tree_comp 0 + (tree_comp 0 + (tree_comp 1 + (Node [Leaf, Leaf]) + (Node [Node [Leaf], Node [Leaf, Leaf, Leaf]])) + (Node [Leaf, Node [Leaf, Leaf]])) + (Node [Leaf, Leaf, Leaf])" + (* Node [ + Node [Leaf], + Node [Leaf, Leaf, Leaf], + Leaf, + Node [Leaf, Leaf], + Leaf, + Leaf, + Leaf]*) + (* Leinster2001: p. 40 *) + +lemma tree_comp_0_Leaf1 [simp]: "tree_comp 0 Leaf t = t" + by (metis eq_Nil_appendI tree.exhaust tree_comp.simps(1)) + +lemma tree_comp_0_Leaf2 [simp]: "tree_comp 0 t Leaf = t" + by (metis append_Nil2 tree.exhaust tree_comp.simps(1)) + +lemma tree_comp_Suc_Leaf1 [simp]: "tree_comp (Suc n) Leaf t = Leaf" + by (cases t, simp) + +lemma tree_comp_Suc_Leaf2 [simp]: "tree_comp (Suc n) t Leaf = Leaf" + by (cases t, simp) + +lemma height_tree_comp_0 [simp]: "height (tree_comp 0 t u) = max (height t) (height u)" +proof (cases "t = Leaf \ u = Leaf") + case True + then show ?thesis by auto +next + case False + hence nempt: "subtrees t \ [] \ subtrees u \ []" by (metis tree.exhaust_sel) + have "height (tree_comp 0 t u) = height (Node (subtrees t @ subtrees u))" + by (metis tree.collapse tree_comp.simps(1)) + also have "\ = Suc (Max (set (map height (subtrees t @ subtrees u))))" + using nempt height_Node_Max by blast + also have "\ = Suc (Max (set (map height (subtrees t)) \ set (map height (subtrees u))))" + by simp + also have "\ = Suc (max (Max (set (map height (subtrees t)))) + (Max (set (map height (subtrees u)))))" + using nempt Max_Un by (metis List.finite_set map_is_Nil_conv set_empty2) + also have "\ = max (Suc (Max (set (map height (subtrees t))))) + (Suc (Max (set (map height (subtrees u)))))" + by linarith + finally show "height (tree_comp 0 t u) = max (height t) (height u)" + using nempt height_Node_Max by (metis tree.collapse) +qed + +text \An alternative description of being composable for trees. Defined so that +\tree_comp n t u\ is defined if and only if \composable_tree n t u\.\ +fun composable_tree :: "nat \ tree \ tree \ bool" where +"composable_tree 0 (Node ts) (Node us) = True" | +"composable_tree (Suc n) (Node ts) (Node us) = (length ts = length us \ + (\i < length ts. composable_tree n (ts!i) (us!i)))" + +lemma sym_composable_tree: "composable_tree n t u = composable_tree n u t" + by (induction n t u rule: composable_tree.induct, simp, fastforce) + +lemma is_composable_pair_imp_composable_tree: "pd.is_composable_pair m n t u \ + composable_tree n t u" +proof (induction n t u rule: composable_tree.induct) + case (1 ts us) + then show ?case by fastforce +next + case (2 n ts us) + with pd.is_composable_pair_def have h: "Suc n < m" "height (Node ts) \ m" "height (Node us) \ m" + "pd.t' m (Suc n) (Node us) = pd.s' m (Suc n) (Node ts)" by blast+ + moreover hence "Suc n \ m" by linarith + ultimately have htrim: "trim (Suc n) (Node ts) = trim (Suc n) (Node us)" + by (metis (mono_tags, lifting) s'_eq_trim t'_eq_trim) + hence "trim 1 (Node ts) = trim 1 (Node us)" + by (metis One_nat_def Suc_le_mono le0 trim_eq_imp_trim_eq) + with trim_1_eq have hl: "length ts = length us" by blast + moreover have "\i < length ts. composable_tree n (ts!i) (us!i)" proof (safe) + fix i assume hi: "i < length ts" + hence "height (ts!i) \ m" using h(2) height_lt nth_mem by fastforce + moreover have "height (us!i) \ m" using hi h(3) height_lt nth_mem hl by fastforce + moreover have "n < m" using h(1) by simp + moreover have "trim n (ts!i) = trim n (us!i)" proof - + have "map (trim n) ts = map (trim n) us" using htrim by auto + thus "trim n (ts!i) = trim n (us!i)" using nth_map hi hl by metis + qed + ultimately have "pd.t' m n (us!i) = pd.s' m n (ts!i)" + using s'_eq_trim t'_eq_trim order_less_imp_le[of n m] by presburger + hence "pd.is_composable_pair m n (ts!i) (us!i)" + using pd.is_composable_pair_def \n < m\ \height (ts!i) \ m\ \height (us!i) \ m\ by blast + with 2(1) hi show "composable_tree n (ts!i) (us!i)" by fast + qed + ultimately show ?case by fastforce +qed + +lemma composable_tree_imp_trim_eq: "composable_tree n t u \ trim n t = trim n u" +proof (induction n t u rule: composable_tree.induct) + case (1 ts us) + then show ?case by simp +next + case (2 n ts us) + then show ?case + by (metis (mono_tags, lifting) nth_map trim.simps(2) length_map nth_equalityI + composable_tree.simps(2)) +qed + +lemma composable_tree_imp_is_composable_pair: + assumes "n < m" "height t \ m" "height u \ m" "composable_tree n t u" + shows "pd.is_composable_pair m n t u" + using assms +proof (induction m arbitrary: n t u) + case 0 + then show ?case by blast +next + case (Suc m) + hence "trim n u = trim n t" using composable_tree_imp_trim_eq by presburger + hence "pd.t' (Suc m) n u = pd.s' (Suc m) n t" + using Suc(2-4) s'_eq_trim t'_eq_trim less_imp_le_nat by presburger + with Suc(2-4) pd.is_composable_pair_def show ?case by blast +qed + +lemma is_composable_pair_iff_composable_tree: "pd.is_composable_pair m n t u = + (n < m \ height t \ m \ height u \ m \ composable_tree n t u)" + by (metis (mono_tags, lifting) composable_tree_imp_is_composable_pair + is_composable_pair_imp_composable_tree mem_Collect_eq pd.is_composable_pair_def) + +lemma composable_tree_imp_composable_tree_subtrees: + "composable_tree (Suc n) (Node ts) (Node us) \ \(t, u) \ set (zip ts us). composable_tree n t u" + by (metis in_set_zip case_prod_beta composable_tree.simps(2)) + +lemma composable_tree_nth_subtrees: + "\composable_tree (Suc n) (Node ts) (Node us); i < length ts\ \ composable_tree n (ts!i) (us!i)" + by fastforce + +lemma is_composable_pair_imp_is_composable_pair_subtrees: + assumes "pd.is_composable_pair (Suc m) (Suc n) (Node ts) (Node us)" + shows "\(t, u) \ set (zip ts us). pd.is_composable_pair m n t u" +proof + have "pd.is_composable_pair m n (fst p) (snd p)" if hp: "p \ set (zip ts us)" for p proof - + have "composable_tree (Suc n) (Node ts) (Node us)" + using is_composable_pair_iff_composable_tree assms by blast + hence h: "composable_tree n (fst p) (snd p)" + using hp composable_tree_imp_composable_tree_subtrees by fastforce + have "fst p \ set ts" "snd p \ set us" by (metis hp in_set_zipE prod.exhaust_sel)+ + hence "height (fst p) \ m" "height (snd p) \ m" + by (meson hp height_lt assms less_Suc_eq_le order_less_le_trans + is_composable_pair_iff_composable_tree)+ + with h is_composable_pair_iff_composable_tree assms + show "pd.is_composable_pair m n (fst p) (snd p)" by force + qed + then show "\x. x \ set (zip ts us) \ case x of (t, u) \ pd.is_composable_pair m n t u" + by force +qed + +lemma in_set_map2: "(z \ set (map2 f xs ys)) = (\(x, y) \ set (zip xs ys). z = f x y)" + by auto + +lemma height_tree_comp_le: "\height t \ m; height u \ m\ \ height (tree_comp n t u) \ m" +proof (induction n t u arbitrary: m rule: tree_comp.induct) + case (1 ts us) + then show ?case using height_tree_comp_0 by presburger +next + case (2 n ts us) + show ?case proof (cases "ts \ [] \ us \ []") + case True + hence "\m'. m = Suc m'" using height_zero "2.prems"(1) not0_implies_Suc by auto + then obtain m' where "m = Suc m'" by blast + hence "\t \ set ts. height t \ m'" "\u \ set us. height u \ m'" + using True "2.prems" by simp+ + hence "\(t, u) \ set (zip ts us). height (tree_comp n t u) \ m'" + by (metis (no_types, lifting) "2.IH" case_prodI2 set_zip_leftD set_zip_rightD) + then show ?thesis using True \m = Suc m'\ by auto + next + case False + then show ?thesis by force + qed +qed + +lemma nth_map2 [simp]: "\n < length xs; n < length ys\ \ map2 f xs ys ! n = f (xs ! n) (ys ! n)" + by fastforce + +lemma trim_tree_comp1: "composable_tree n t u \ trim n (tree_comp n t u) = trim n t" +proof (induction n t u rule: composable_tree.induct) + case (1 ts us) + then show ?case by fastforce +next + case (2 n ts us) + then show ?case by (simp add: list_eq_iff_nth_eq) +qed + +lemma trim_tree_comp2: "composable_tree n t u \ trim n (tree_comp n t u) = trim n u" + using trim_tree_comp1 composable_tree_imp_trim_eq by presburger + +lemma map2_map_map': "map2 f (map g xs) (map h ys) = map (\(x, y). f (g x) (h y)) (zip xs ys)" +proof (induction xs arbitrary: ys) + case Nil + then show ?case by simp +next + case (Cons a xs) + then show ?case proof (induction ys) + case Nil + then show ?case by simp + next + case (Cons a ys) + then show ?case by auto + qed +qed + +lemma trim_tree_comp_commute: "trim m (tree_comp n t u) = tree_comp n (trim m t) (trim m u)" +proof (induction m arbitrary: n t u) + case 0 + then show ?case by (cases n, simp_all) +next + case (Suc m) + then show ?case + by (induction n t u rule: composable_tree.induct, simp_all add: list_eq_iff_nth_eq) +qed + +interpretation pd_pre_cat: pre_strict_omega_category PD \ \ "\ m. tree_comp" "\ n. id" +proof (unfold_locales) + fix m n x' x assume "pd.is_composable_pair m n x' x" + then show "tree_comp n x' x \ PD m" + using is_composable_pair_iff_composable_tree height_tree_comp_le by auto +next + fix n show "id \ PD n \ PD (Suc n)" by simp +next + fix m x' x assume "pd.is_composable_pair (Suc m) m x' x" + then show "\ m (tree_comp m x' x) = \ m x" + by (simp add: is_composable_pair_iff_composable_tree trim_tree_comp2 height_tree_comp_le) +next + fix m x' x assume "pd.is_composable_pair (Suc m) m x' x" + then show "\ m (tree_comp m x' x) = \ m x'" + by (simp add: is_composable_pair_iff_composable_tree trim_tree_comp1 height_tree_comp_le) +next + fix m n x' x assume "pd.is_composable_pair (Suc m) n x' x" "n < m" + then show "\ m (tree_comp n x' x) = tree_comp n (\ m x') (\ m x)" + by (simp add: is_composable_pair_iff_composable_tree trim_tree_comp_commute height_tree_comp_le) +next + fix x n assume "x \ PD n" + then show "\ n (id x) = x" using trim_const by auto +qed + +lemma tree_comp_assoc: "tree_comp n (tree_comp n t u) v = tree_comp n t (tree_comp n u v)" +proof (induction n t u arbitrary: v rule: composable_tree.induct) + case (1 ts us) + then show ?case by (metis append_assoc tree_comp.simps(1) tree.exhaust) +next + case (2 n ts us) + define vs where "vs = subtrees v" hence hv: "v = Node vs" by force + let ?k = "min (length ts) (min (length us) (length vs))" + have "\i < ?k. tree_comp n (tree_comp n (ts!i) (us!i)) (vs!i) = + tree_comp n (ts!i) (tree_comp n (us!i) (vs!i))" using "2.IH" by auto + hence "map2 (tree_comp n) (map2 (tree_comp n) ts us) vs = + map2 (tree_comp n) ts (map2 (tree_comp n) us vs)" by (simp add: list_eq_iff_nth_eq) + then show ?case using hv by auto +qed + +lemma i'_eq_id: "n \ m \ pd_pre_cat.i' m n = id" +proof (induction m) + case 0 + then show ?case using pd_pre_cat.i'.simps(1) by blast +next + case (Suc m) + then show ?case by (metis pd_pre_cat.i'_Suc id_comp le_Suc_eq pd_pre_cat.i'_n_n) +qed + +lemma composable_tree_trim1: "n \ m \ composable_tree n (trim m t) t" +proof (induction n t arbitrary: m rule: trim.induct) + case (1 t) + then show ?case by (metis composable_tree.simps(1) tree.exhaust) +next + case (2 n ts) + hence "\m'. m = Suc m'" by presburger + then obtain m' where hm: "m = Suc m'" "n \ m'" using 2(2) by blast + moreover hence "\i < length ts. composable_tree n (\ m' (ts!i)) (ts!i)" using 2(1) by simp + ultimately show ?case by force +qed + +lemma composable_tree_trim2: "n \ m \ composable_tree n t (trim m t)" + using sym_composable_tree composable_tree_trim1 by presburger + +lemma tree_comp_trim1: "tree_comp n (trim n t) t = t" + by (induction n t rule: trim.induct, simp add: tree.exhaust, simp add: list_eq_iff_nth_eq) + +lemma tree_comp_trim2: "tree_comp n t (trim n t) = t" + by (induction n t rule: trim.induct, simp add: tree.exhaust, simp add: list_eq_iff_nth_eq) + +lemma tree_comp_exchange: + "\q < p; composable_tree p y' y; composable_tree p x' x; + composable_tree q y' x'; composable_tree q y x\ \ + tree_comp q (tree_comp p y' y) (tree_comp p x' x) = + tree_comp p (tree_comp q y' x') (tree_comp q y x)" +proof (induction p y' y arbitrary: q x' x rule: composable_tree.induct) + case (1 ys' ys) + then show ?case proof (induction q x' x rule: composable_tree.induct) + case (1 xs' xs) + then show ?case by blast + next + case (2 q xs' xs) + then show ?case by force + qed +next + case (2 p ys' ys) + then show ?case proof (induction q x' x rule: composable_tree.induct) + case (1 ts us) + then show ?case by force + next + case (2 n ts us) + then show ?case by (simp add: list_eq_iff_nth_eq) + qed +qed + +interpretation pd_cat': strict_omega_category PD \ \ "\ m. tree_comp" "\ n. id" +proof (unfold_locales) + fix m n x' x x'' assume "pd.is_composable_pair m n x' x" "pd.is_composable_pair m n x'' x'" + then show "tree_comp n (tree_comp n x'' x') x = tree_comp n x'' (tree_comp n x' x)" + using tree_comp_assoc is_composable_pair_iff_composable_tree by force +next + fix n m x assume "n < m" "x \ PD m" + moreover hence "height x \ m" by simp + ultimately show "tree_comp n (pd_pre_cat.i' m n (pd.t' m n x)) x = x" + by (metis (no_types, lifting) i'_eq_id t'_eq_trim tree_comp_trim1 id_apply nat_less_le) +next + fix n m x assume "n < m" "x \ PD m" + moreover hence "height x \ m" by simp + ultimately show "tree_comp n x (pd_pre_cat.i' m n (pd.s' m n x)) = x" + by (metis (no_types, lifting) i'_eq_id s'_eq_trim tree_comp_trim2 id_apply nat_less_le) +next + fix q p m y' y x' x assume "q < p" "p < m" + "pd.is_composable_pair m p y' y" "pd.is_composable_pair m p x' x" + "pd.is_composable_pair m q y' x'" "pd.is_composable_pair m q y x" + then show "tree_comp q (tree_comp p y' y) (tree_comp p x' x) = + tree_comp p (tree_comp q y' x') (tree_comp q y x)" + using is_composable_pair_iff_composable_tree tree_comp_exchange by meson +qed (simp) + +end \ No newline at end of file diff --git a/thys/StrictOmegaCategories/ROOT b/thys/StrictOmegaCategories/ROOT new file mode 100644 --- /dev/null +++ b/thys/StrictOmegaCategories/ROOT @@ -0,0 +1,14 @@ +chapter AFP + +session "StrictOmegaCategories" (AFP) = HOL + + options [timeout = 600] + sessions + "HOL-Library" + theories + Globular_Set + Pasting_Diagram + Strict_Omega_Category + document_files + "root.bib" + "root.tex" + \ No newline at end of file diff --git a/thys/StrictOmegaCategories/Strict_Omega_Category.thy b/thys/StrictOmegaCategories/Strict_Omega_Category.thy new file mode 100644 --- /dev/null +++ b/thys/StrictOmegaCategories/Strict_Omega_Category.thy @@ -0,0 +1,100 @@ +theory Strict_Omega_Category +imports Globular_Set + +begin + +section \Strict $\omega$-categories\ + +text \ + First, we define a locale \pre_strict_omega_category\ that holds the data of a strict + $\omega$-category without the associativity, unity and exchange axioms + \cite[Def 1.4.8 (a) - (b)]{Leinster2004}. We do this in order to set up convenient notation + before we state the remaining axioms. +\ + +locale pre_strict_omega_category = globular_set + + fixes comp :: "nat \ nat \ 'a \ 'a \ 'a" + and i :: "nat \ 'a \ 'a" + assumes comp_fun: "is_composable_pair m n x' x \ comp m n x' x \ X m" + and i_fun: "i n \ X n \ X (Suc n)" + and s_comp_Suc: "is_composable_pair (Suc m) m x' x \ s m (comp (Suc m) m x' x) = s m x" + and t_comp_Suc: "is_composable_pair (Suc m) m x' x \ t m (comp (Suc m) m x' x) = t m x'" + and s_comp: "\is_composable_pair (Suc m) n x' x; n < m\ \ + s m (comp (Suc m) n x' x) = comp m n (s m x') (s m x)" + and t_comp: "\is_composable_pair (Suc m) n x' x; n < m\ \ + t m (comp (Suc m) n x' x) = comp m n (t m x') (s m x)" + and s_i: "x \ X n \ s n (i n x) = x" + and t_i: "x \ X n \ t n (i n x) = x" +begin + +text \Similar to the generalised source and target maps in \globular_set\, we defined a generalised +identity map. The first argument gives the dimension of the resulting identity cell, while the +second gives the dimension of the input cell.\ + +fun i' :: "nat \ nat \ 'a \ 'a" where +"i' 0 0 = id" | +"i' 0 (Suc n) = undefined" | +"i' (Suc m) n = (if Suc m < n then undefined + else if Suc m = n then id + else i m \ i' m n)" + +lemma i'_n_n [simp]: "i' n n = id" + by (metis i'.elims i'.simps(1) less_irrefl_nat) + +lemma i'_Suc_n_n [simp]: "i' (Suc n) n = i n" + by simp + +lemma i'_Suc [simp]: "n \ m \ i' (Suc m) n = i m \ i' m n" + by fastforce + +lemma i'_Suc': "n < m \ i' m n = i' m (Suc n) \ i n" +proof (induction m arbitrary: n) + case 0 + then show ?case by blast +next + case (Suc m) + then show ?case by force +qed + +lemma i'_fun: "n \ m \ i' m n \ X n \ X m" +proof (induction m arbitrary: n) + case 0 + then show ?case by fastforce +next + case (Suc m) + thus ?case proof (cases "n = Suc m") + case True + then show ?thesis by auto + next + case False + hence "n \ m" using `n \ Suc m` by force + thus ?thesis using Suc.IH i_fun by auto + qed +qed + +end + +text \Now we may define a strict $\omega$-category including the composition, unity and exchange + axioms \cite[Def 1.4.8 (c) - (f)]{Leinster2004}.\ + +locale strict_omega_category = pre_strict_omega_category + + assumes comp_assoc: "\is_composable_pair m n x' x; is_composable_pair m n x'' x'\ \ + comp m n (comp m n x'' x') x = comp m n x'' (comp m n x' x)" + and i_comp: "\n < m; x \ X m\ \ comp m n (i' m n (t' m n x)) x = x" + and comp_i: "\n < m; x \ X m\ \ comp m n x (i' m n (s' m n x)) = x" + and bin_interchange: "\q < p; p < m; + is_composable_pair m p y' y; is_composable_pair m p x' x; + is_composable_pair m q y' x'; is_composable_pair m q y x\ \ + comp m q (comp m p y' y) (comp m p x' x) = comp m p (comp m q y' x') (comp m q y x)" + and null_interchange: "\q < p; is_composable_pair p q x' x\ \ + comp (Suc p) q (i p x') (i p x) = i p (comp p q x' x)" + +locale strict_omega_functor = globular_map + + source: strict_omega_category X s\<^sub>X t\<^sub>X comp\<^sub>X i\<^sub>X + + target: strict_omega_category Y s\<^sub>Y t\<^sub>Y comp\<^sub>Y i\<^sub>Y + for comp\<^sub>X i\<^sub>X comp\<^sub>Y i\<^sub>Y + + assumes commute_with_comp: "is_composable_pair m n x' x \ + \ m (comp\<^sub>X m n x' x) = comp\<^sub>Y m n (\ m x') (\ m x)" + and commute_with_id: "x \ X n \ \ (Suc n) (i\<^sub>X n x) = i\<^sub>Y n (\ n x)" + +end \ No newline at end of file diff --git a/thys/StrictOmegaCategories/document/root.bib b/thys/StrictOmegaCategories/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/StrictOmegaCategories/document/root.bib @@ -0,0 +1,14 @@ +@book{Leinster2004, + title={Higher operads, higher categories}, + author={Leinster, Tom}, + number={298}, + year={2004}, + publisher={Cambridge University Press} +} + +@article{Leinster2001, + title={Structures in higher-dimensional category theory}, + author={Leinster, Tom}, + journal={arXiv preprint math/0109021}, + year={2001} +} \ No newline at end of file diff --git a/thys/StrictOmegaCategories/document/root.tex b/thys/StrictOmegaCategories/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/StrictOmegaCategories/document/root.tex @@ -0,0 +1,33 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{Strict Omega Categories} +\author{Anthony Bordg \and Adrián Doña Mateo} +\maketitle + +\begin{abstract} + This theory formalises a definition of strict $\omega$-categories and the strict $\omega$-category + of pasting diagrams, following \cite{Leinster2004}. It is the first step towards a formalisation + of weak infinity categories à la Batanin--Leinster. +\end{abstract} + +\tableofcontents + +% include generated text of all theories +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} \ No newline at end of file