diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,550 +1,551 @@ ADS_Functor AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod 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 BDD BNF_CC BNF_Operations Banach_Steinhaus Bell_Numbers_Spivey Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK 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 Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC 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 Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interval_Arithmetic_Word32 Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Isabelle_C Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra 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 Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option 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 Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mersenne_Primes MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference 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 Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PCF PLM POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate 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 Projective_Geometry Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions 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 Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic +Relational_Disjoint_Set_Forests Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching 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 Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares SuperCalc Surprise_Paradox Symmetric_Polynomials Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation VectorSpace VeriComp Verified-Prover VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy b/thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy new file mode 100644 --- /dev/null +++ b/thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy @@ -0,0 +1,1746 @@ +(* Title: Disjoint-Set Forests + Author: Walter Guttmann + Maintainer: Walter Guttmann +*) + +theory Disjoint_Set_Forests + +imports + Aggregation_Algebras.Hoare_Logic + Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras +begin + +no_notation + trancl ("(_\<^sup>+)" [1000] 999) + +context stone_relation_algebra +begin + +text \ +We start with a few basic properties of arcs, points and rectangles. + +An arc in a Stone relation algebra corresponds to an atom in a relation algebra and represents a single edge in a graph. +A point represents a set of nodes. +A rectangle represents the Cartesian product of two sets of nodes \cite{BerghammerStruth2010}. +\ + +lemma points_arc: + "point x \ point y \ arc (x * y\<^sup>T)" + by (metis comp_associative conv_dist_comp conv_involutive equivalence_top_closed) + +lemma point_arc: + "point x \ arc (x * x\<^sup>T)" + by (simp add: points_arc) + +lemma injective_codomain: + assumes "injective x" + shows "x * (x \ 1) = x \ 1" +proof (rule antisym) + show "x * (x \ 1) \ x \ 1" + by (metis assms comp_right_one dual_order.trans inf.boundedI inf.cobounded1 inf.sup_monoid.add_commute mult_right_isotone one_inf_conv) +next + show "x \ 1 \ x * (x \ 1)" + by (metis coreflexive_idempotent inf.cobounded1 inf.cobounded2 mult_left_isotone) +qed + +abbreviation rectangle :: "'a \ bool" + where "rectangle x \ x * top * x = x" + +lemma arc_rectangle: + "arc x \ rectangle x" + using arc_top_arc by blast + +section \Relation-Algebraic Semantics of Associative Array Access\ + +text \ +The following two operations model updating array $x$ at index $y$ to value $z$, +and reading the content of array $x$ at index $y$, respectively. +The read operation uses double brackets to avoid ambiguity with list syntax. +The remainder of this section shows basic properties of these operations. +\ + +abbreviation rel_update :: "'a \ 'a \ 'a \ 'a" ("(_[_\_])" [70, 65, 65] 61) + where "x[y\z] \ (y \ z\<^sup>T) \ (-y \ x)" + +abbreviation rel_access :: "'a \ 'a \ 'a" ("(2_[[_]])" [70, 65] 65) + where "x[[y]] \ x\<^sup>T * y" + +text \Theorem 1.1\ + +lemma update_univalent: + assumes "univalent x" + and "vector y" + and "injective z" + shows "univalent (x[y\z])" +proof - + have 1: "univalent (y \ z\<^sup>T)" + using assms(3) inf_commute univalent_inf_closed by force + have "(y \ z\<^sup>T)\<^sup>T * (-y \ x) = (y\<^sup>T \ z) * (-y \ x)" + by (simp add: conv_dist_inf) + also have "... = z * (y \ -y \ x)" + by (metis assms(2) covector_inf_comp_3 inf.sup_monoid.add_assoc inf.sup_monoid.add_commute) + finally have 2: "(y \ z\<^sup>T)\<^sup>T * (-y \ x) = bot" + by simp + have 3: "vector (-y)" + using assms(2) vector_complement_closed by simp + have "(-y \ x)\<^sup>T * (y \ z\<^sup>T) = (-y\<^sup>T \ x\<^sup>T) * (y \ z\<^sup>T)" + by (simp add: conv_complement conv_dist_inf) + also have "... = x\<^sup>T * (-y \ y \ z\<^sup>T)" + using 3 by (metis (mono_tags, hide_lams) conv_complement covector_inf_comp_3 inf.sup_monoid.add_assoc inf.sup_monoid.add_commute) + finally have 4: "(-y \ x)\<^sup>T * (y \ z\<^sup>T) = bot" + by simp + have 5: "univalent (-y \ x)" + using assms(1) inf_commute univalent_inf_closed by fastforce + have "(x[y\z])\<^sup>T * (x[y\z]) = (y \ z\<^sup>T)\<^sup>T * (x[y\z]) \ (-y \ x)\<^sup>T * (x[y\z])" + by (simp add: conv_dist_sup mult_right_dist_sup) + also have "... = (y \ z\<^sup>T)\<^sup>T * (y \ z\<^sup>T) \ (y \ z\<^sup>T)\<^sup>T * (-y \ x) \ (-y \ x)\<^sup>T * (y \ z\<^sup>T) \ (-y \ x)\<^sup>T * (-y \ x)" + by (simp add: mult_left_dist_sup sup_assoc) + finally show ?thesis + using 1 2 4 5 by simp +qed + +text \Theorem 1.2\ + +lemma update_total: + assumes "total x" + and "vector y" + and "regular y" + and "surjective z" + shows "total (x[y\z])" +proof - + have "(x[y\z]) * top = x*top[y\top*z]" + by (simp add: assms(2) semiring.distrib_right vector_complement_closed vector_inf_comp conv_dist_comp) + also have "... = top[y\top]" + using assms(1) assms(4) by simp + also have "... = top" + using assms(3) regular_complement_top by auto + finally show ?thesis + by simp +qed + +text \Theorem 1.3\ + +lemma update_mapping: + assumes "mapping x" + and "vector y" + and "regular y" + and "bijective z" + shows "mapping (x[y\z])" + using assms update_univalent update_total by simp + +text \Theorem 1.4\ + +lemma read_injective: + assumes "injective y" + and "univalent x" + shows "injective (x[[y]])" + using assms injective_mult_closed univalent_conv_injective by blast + +text \Theorem 1.5\ + +lemma read_surjective: + assumes "surjective y" + and "total x" + shows "surjective (x[[y]])" + using assms surjective_mult_closed total_conv_surjective by blast + +text \Theorem 1.6\ + +lemma read_bijective: + assumes "bijective y" + and "mapping x" + shows "bijective (x[[y]])" + by (simp add: assms read_injective read_surjective) + +text \Theorem 1.7\ + +lemma read_point: + assumes "point p" + and "mapping x" + shows "point (x[[p]])" + using assms comp_associative read_injective read_surjective by auto + +text \Theorem 1.8\ + +lemma update_postcondition: + assumes "point x" "point y" + shows "x \ p = x * y\<^sup>T \ p[[x]] = y" + apply (rule iffI) + subgoal by (metis assms comp_associative conv_dist_comp conv_involutive covector_inf_comp_3 equivalence_top_closed vector_covector) + subgoal + apply (rule antisym) + subgoal by (metis assms conv_dist_comp conv_involutive inf.boundedI inf.cobounded1 vector_covector vector_restrict_comp_conv) + subgoal by (smt assms comp_associative conv_dist_comp conv_involutive covector_restrict_comp_conv dense_conv_closed equivalence_top_closed inf.boundedI shunt_mapping vector_covector preorder_idempotent) + done + done + +text \Back and von Wright's array independence requirements \cite{BackWright1998}, + later also lens laws \cite{FosterGreenwaldMoorePierceSchmitt2007}\ + +lemma put_get: + assumes "vector y" "surjective y" "vector z" + shows "(x[y\z])[[y]] = z" +proof - + have "(x[y\z])[[y]] = (y\<^sup>T \ z) * y \ (-y\<^sup>T \ x\<^sup>T) * y" + by (simp add: conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup) + also have "... = z * y" + proof - + have "(-y\<^sup>T \ x\<^sup>T) * y = bot" + by (metis assms(1) covector_inf_comp_3 inf_commute conv_complement mult_right_zero p_inf vector_complement_closed) + thus ?thesis + by (simp add: assms covector_inf_comp_3 inf_commute) + qed + also have "... = z" + by (metis assms(2,3) mult_assoc) + finally show ?thesis + . +qed + +lemma put_put: + "(x[y\z])[y\w] = x[y\w]" + by (metis inf_absorb2 inf_commute inf_le1 inf_sup_distrib1 maddux_3_13 sup_inf_absorb) + +lemma get_put: + assumes "point y" + shows "x[y\x[[y]]] = x" +proof - + have "x[y\x[[y]]] = (y \ y\<^sup>T * x) \ (-y \ x)" + by (simp add: conv_dist_comp) + also have "... = (y \ x) \ (-y \ x)" + proof - + have "y \ y\<^sup>T * x = y \ x" + proof (rule antisym) + have "y \ y\<^sup>T * x = (y \ y\<^sup>T) * x" + by (simp add: assms vector_inf_comp) + also have "(y \ y\<^sup>T) * x = y * y\<^sup>T * x" + by (simp add: assms vector_covector) + also have "... \ x" + using assms comp_isotone by fastforce + finally show "y \ y\<^sup>T * x \ y \ x" + by simp + have "y \ x \ y\<^sup>T * x" + by (simp add: assms vector_restrict_comp_conv) + thus "y \ x \ y \ y\<^sup>T * x" + by simp + qed + thus ?thesis + by simp + qed + also have "... = x" + proof - + have "regular y" + using assms bijective_regular by blast + thus ?thesis + by (metis inf.sup_monoid.add_commute maddux_3_11_pp) + qed + finally show ?thesis + . +qed + +end + +section \Relation-Algebraic Semantics of Disjoint-Set Forests\ + +text \ +A disjoint-set forest represents a partition of a set into equivalence classes. +We take the represented equivalence relation as the semantics of a forest. +It is obtained by operation \fc\ below. +Additionally, operation \wcc\ giving the weakly connected components of a graph will be used for the semantics of the union of two disjoint sets. +Finally, operation \root\ yields the root of a component tree, that is, the representative of a set containing a given element. +This section defines these operations and derives their properties. +\ + +context stone_kleene_relation_algebra +begin + +lemma equivalence_star_closed: + "equivalence x \ equivalence (x\<^sup>\)" + by (simp add: conv_star_commute star.circ_reflexive star.circ_transitive_equal) + +lemma equivalence_plus_closed: + "equivalence x \ equivalence (x\<^sup>+)" + by (simp add: conv_star_commute star.circ_reflexive star.circ_sup_one_left_unfold star.circ_transitive_equal) + +lemma reachable_without_loops: + "x\<^sup>\ = (x \ -1)\<^sup>\" +proof (rule antisym) + have "x * (x \ -1)\<^sup>\ = (x \ 1) * (x \ -1)\<^sup>\ \ (x \ -1) * (x \ -1)\<^sup>\" + by (metis maddux_3_11_pp mult_right_dist_sup regular_one_closed) + also have "... \ (x \ -1)\<^sup>\" + by (metis inf.cobounded2 le_supI mult_left_isotone star.circ_circ_mult star.left_plus_below_circ star_involutive star_one) + finally show "x\<^sup>\ \ (x \ -1)\<^sup>\" + by (metis inf.cobounded2 maddux_3_11_pp regular_one_closed star.circ_circ_mult star.circ_sup_2 star_involutive star_sub_one) +next + show "(x \ -1)\<^sup>\ \ x\<^sup>\" + by (simp add: star_isotone) +qed + +lemma star_plus_loops: + "x\<^sup>\ \ 1 = x\<^sup>+ \ 1" + using star.circ_plus_one star_left_unfold_equal sup_commute by auto + +lemma star_plus_without_loops: + "x\<^sup>\ \ -1 = x\<^sup>+ \ -1" + by (metis maddux_3_13 star_left_unfold_equal) + +text \Theorem 4.2\ + +lemma omit_redundant_points: + assumes "point p" + shows "p \ x\<^sup>\ = (p \ 1) \ (p \ x) * (-p \ x)\<^sup>\" +proof (rule antisym) + let ?p = "p \ 1" + have "?p * x * (-p \ x)\<^sup>\ * ?p \ ?p * top * ?p" + by (metis comp_associative mult_left_isotone mult_right_isotone top.extremum) + also have "... \ ?p" + by (simp add: assms injective_codomain vector_inf_one_comp) + finally have "?p * x * (-p \ x)\<^sup>\ * ?p * x \ ?p * x" + using mult_left_isotone by blast + hence "?p * x * (-p \ x)\<^sup>\ * (p \ x) \ ?p * x" + by (simp add: assms comp_associative vector_inf_one_comp) + also have 1: "... \ ?p * x * (-p \ x)\<^sup>\" + using mult_right_isotone star.circ_reflexive by fastforce + finally have "?p * x * (-p \ x)\<^sup>\ * (p \ x) \ ?p * x * (-p \ x)\<^sup>\ * (-p \ x) \ ?p * x * (-p \ x)\<^sup>\" + by (simp add: mult_right_isotone star.circ_plus_same star.left_plus_below_circ mult_assoc) + hence "?p * x * (-p \ x)\<^sup>\ * ((p \ -p) \ x) \ ?p * x * (-p \ x)\<^sup>\" + by (simp add: comp_inf.mult_right_dist_sup mult_left_dist_sup) + hence "?p * x * (-p \ x)\<^sup>\ * x \ ?p * x * (-p \ x)\<^sup>\" + by (metis assms bijective_regular inf.absorb2 inf.cobounded1 inf.sup_monoid.add_commute shunting_p) + hence "?p * x * (-p \ x)\<^sup>\ * x \ ?p * x \ ?p * x * (-p \ x)\<^sup>\" + using 1 by simp + hence "?p * (1 \ x * (-p \ x)\<^sup>\) * x \ ?p * x * (-p \ x)\<^sup>\" + by (simp add: comp_associative mult_left_dist_sup mult_right_dist_sup) + also have "... \ ?p * (1 \ x * (-p \ x)\<^sup>\)" + by (simp add: comp_associative mult_right_isotone) + finally have "?p * x\<^sup>\ \ ?p * (1 \ x * (-p \ x)\<^sup>\)" + using star_right_induct by (meson dual_order.trans le_supI mult_left_sub_dist_sup_left mult_sub_right_one) + also have "... = ?p \ ?p * x * (-p \ x)\<^sup>\" + by (simp add: comp_associative semiring.distrib_left) + finally show "p \ x\<^sup>\ \ ?p \ (p \ x) * (-p \ x)\<^sup>\" + by (simp add: assms vector_inf_one_comp) + show "?p \ (p \ x) * (-p \ x)\<^sup>\ \ p \ x\<^sup>\" + by (metis assms comp_isotone inf.boundedI inf.cobounded1 inf.coboundedI2 inf.sup_monoid.add_commute le_supI star.circ_increasing star.circ_transitive_equal star_isotone star_left_unfold_equal sup.cobounded1 vector_export_comp) +qed + +text \Weakly connected components\ + +abbreviation "wcc x \ (x \ x\<^sup>T)\<^sup>\" + +text \Theorem 5.1\ + +lemma wcc_equivalence: + "equivalence (wcc x)" + apply (intro conjI) + subgoal by (simp add: star.circ_reflexive) + subgoal by (simp add: star.circ_transitive_equal) + subgoal by (simp add: conv_dist_sup conv_star_commute sup_commute) + done + +text \Theorem 5.2\ + +lemma wcc_increasing: + "x \ wcc x" + by (simp add: star.circ_sub_dist_1) + +lemma wcc_isotone: + "x \ y \ wcc x \ wcc y" + using conv_isotone star_isotone sup_mono by blast + +lemma wcc_idempotent: + "wcc (wcc x) = wcc x" + using star_involutive wcc_equivalence by auto + +text \Theorem 5.3\ + +lemma wcc_below_wcc: + "x \ wcc y \ wcc x \ wcc y" + using wcc_idempotent wcc_isotone by fastforce + +text \Theorem 5.4\ + +lemma wcc_bot: + "wcc bot = 1" + by (simp add: star.circ_zero) + +lemma wcc_one: + "wcc 1 = 1" + by (simp add: star_one) + +text \Theorem 5.5\ + +lemma wcc_top: + "wcc top = top" + by (simp add: star.circ_top) + +text \Theorem 5.6\ + +lemma wcc_with_loops: + "wcc x = wcc (x \ 1)" + by (metis conv_dist_sup star_decompose_1 star_sup_one sup_commute symmetric_one_closed) + +lemma wcc_without_loops: + "wcc x = wcc (x \ -1)" + by (metis conv_star_commute star_sum reachable_without_loops) + +lemma forest_components_wcc: + "injective x \ wcc x = forest_components x" + by (simp add: cancel_separate_1) + +text \Components of a forest, which is represented using edges directed towards the roots\ + +abbreviation "fc x \ x\<^sup>\ * x\<^sup>T\<^sup>\" + +text \Theorem 2.1\ + +lemma fc_equivalence: + "univalent x \ equivalence (fc x)" + apply (intro conjI) + subgoal by (simp add: reflexive_mult_closed star.circ_reflexive) + subgoal by (metis cancel_separate_1 eq_iff star.circ_transitive_equal) + subgoal by (simp add: conv_dist_comp conv_star_commute) + done + +text \Theorem 2.2\ + +lemma fc_increasing: + "x \ fc x" + by (metis le_supE mult_left_isotone star.circ_back_loop_fixpoint star.circ_increasing) + +text \Theorem 2.3\ + +lemma fc_isotone: + "x \ y \ fc x \ fc y" + by (simp add: comp_isotone conv_isotone star_isotone) + +text \Theorem 2.4\ + +lemma fc_idempotent: + "univalent x \ fc (fc x) = fc x" + by (metis fc_equivalence cancel_separate_1 star.circ_transitive_equal star_involutive) + +text \Theorem 2.5\ + +lemma fc_star: + "univalent x \ (fc x)\<^sup>\ = fc x" + using fc_equivalence fc_idempotent star.circ_transitive_equal by simp + +lemma fc_plus: + "univalent x \ (fc x)\<^sup>+ = fc x" + by (metis fc_star star.circ_decompose_9) + +text \Theorem 2.6\ + +lemma fc_bot: + "fc bot = 1" + by (simp add: star.circ_zero) + +lemma fc_one: + "fc 1 = 1" + by (simp add: star_one) + +text \Theorem 2.7\ + +lemma fc_top: + "fc top = top" + by (simp add: star.circ_top) + +text \Theorem 5.7\ + +lemma fc_wcc: + "univalent x \ wcc x = fc x" + by (simp add: fc_star star_decompose_1) + +text \Theorem 4.1\ + +lemma update_acyclic_1: + assumes "acyclic (p \ -1)" + and "point y" + and "point w" + and "y \ p\<^sup>T\<^sup>\ * w" + shows "acyclic ((p[w\y]) \ -1)" +proof - + let ?p = "p[w\y]" + have "w \ p\<^sup>\ * y" + using assms(2-4) by (metis (no_types, lifting) bijective_reverse conv_star_commute) + hence "w * y\<^sup>T \ p\<^sup>\" + using assms(2) shunt_bijective by blast + hence "w * y\<^sup>T \ (p \ -1)\<^sup>\" + using reachable_without_loops by auto + hence "w * y\<^sup>T \ -1 \ (p \ -1)\<^sup>\ \ -1" + by (simp add: inf.coboundedI2 inf.sup_monoid.add_commute) + also have "... \ (p \ -1)\<^sup>+" + by (simp add: star_plus_without_loops) + finally have 1: "w \ y\<^sup>T \ -1 \ (p \ -1)\<^sup>+" + using assms(2,3) vector_covector by auto + have "?p \ -1 = (w \ y\<^sup>T \ -1) \ (-w \ p \ -1)" + by (simp add: inf_sup_distrib2) + also have "... \ (p \ -1)\<^sup>+ \ (-w \ p \ -1)" + using 1 sup_left_isotone by blast + also have "... \ (p \ -1)\<^sup>+ \ (p \ -1)" + using comp_inf.mult_semi_associative sup_right_isotone by auto + also have "... = (p \ -1)\<^sup>+" + by (metis star.circ_back_loop_fixpoint sup.right_idem) + finally have "(?p \ -1)\<^sup>+ \ (p \ -1)\<^sup>+" + by (metis comp_associative comp_isotone star.circ_transitive_equal star.left_plus_circ star_isotone) + also have "... \ -1" + using assms(1) by blast + finally show ?thesis + by simp +qed + +lemma rectangle_star_rectangle: + "rectangle a \ a * x\<^sup>\ * a \ a" + by (metis mult_left_isotone mult_right_isotone top.extremum) + +lemma arc_star_arc: + "arc a \ a * x\<^sup>\ * a \ a" + using arc_top_arc rectangle_star_rectangle by blast + +lemma star_rectangle_decompose: + assumes "rectangle a" + shows "(a \ x)\<^sup>\ = x\<^sup>\ \ x\<^sup>\ * a * x\<^sup>\" +proof (rule antisym) + have 1: "1 \ x\<^sup>\ \ x\<^sup>\ * a * x\<^sup>\" + by (simp add: star.circ_reflexive sup.coboundedI1) + have "(a \ x) * (x\<^sup>\ \ x\<^sup>\ * a * x\<^sup>\) = a * x\<^sup>\ \ a * x\<^sup>\ * a * x\<^sup>\ \ x\<^sup>+ \ x\<^sup>+ * a * x\<^sup>\" + by (metis comp_associative semiring.combine_common_factor semiring.distrib_left sup_commute) + also have "... = a * x\<^sup>\ \ x\<^sup>+ \ x\<^sup>+ * a * x\<^sup>\" + using assms rectangle_star_rectangle by (simp add: mult_left_isotone sup_absorb1) + also have "... = x\<^sup>+ \ x\<^sup>\ * a * x\<^sup>\" + by (metis comp_associative star.circ_loop_fixpoint sup_assoc sup_commute) + also have "... \ x\<^sup>\ \ x\<^sup>\ * a * x\<^sup>\" + using star.left_plus_below_circ sup_left_isotone by auto + finally show "(a \ x)\<^sup>\ \ x\<^sup>\ \ x\<^sup>\ * a * x\<^sup>\" + using 1 by (metis comp_right_one le_supI star_left_induct) +next + show "x\<^sup>\ \ x\<^sup>\ * a * x\<^sup>\ \ (a \ x)\<^sup>\" + by (metis comp_isotone le_supE le_supI star.circ_increasing star.circ_transitive_equal star_isotone sup_ge2) +qed + +lemma star_arc_decompose: + "arc a \ (a \ x)\<^sup>\ = x\<^sup>\ \ x\<^sup>\ * a * x\<^sup>\" + using arc_top_arc star_rectangle_decompose by blast + +lemma plus_rectangle_decompose: + assumes "rectangle a" + shows "(a \ x)\<^sup>+ = x\<^sup>+ \ x\<^sup>\ * a * x\<^sup>\" +proof - + have "(a \ x)\<^sup>+ = (a \ x) * (x\<^sup>\ \ x\<^sup>\ * a * x\<^sup>\)" + by (simp add: assms star_rectangle_decompose) + also have "... = a * x\<^sup>\ \ a * x\<^sup>\ * a * x\<^sup>\ \ x\<^sup>+ \ x\<^sup>+ * a * x\<^sup>\" + by (metis comp_associative semiring.combine_common_factor semiring.distrib_left sup_commute) + also have "... = a * x\<^sup>\ \ x\<^sup>+ \ x\<^sup>+ * a * x\<^sup>\" + using assms rectangle_star_rectangle by (simp add: mult_left_isotone sup_absorb1) + also have "... = x\<^sup>+ \ x\<^sup>\ * a * x\<^sup>\" + by (metis comp_associative star.circ_loop_fixpoint sup_assoc sup_commute) + finally show ?thesis + by simp +qed + +text \Theorem 6.1\ + +lemma plus_arc_decompose: + "arc a \ (a \ x)\<^sup>+ = x\<^sup>+ \ x\<^sup>\ * a * x\<^sup>\" + using arc_top_arc plus_rectangle_decompose by blast + +text \Theorem 6.2\ + +lemma update_acyclic_2: + assumes "acyclic (p \ -1)" + and "point y" + and "point w" + and "y \ p\<^sup>\ * w = bot" + shows "acyclic ((p[w\y]) \ -1)" +proof - + let ?p = "p[w\y]" + have "y\<^sup>T * p\<^sup>\ * w \ -1" + using assms(4) comp_associative pseudo_complement schroeder_3_p by auto + hence 1: "p\<^sup>\ * w * y\<^sup>T * p\<^sup>\ \ -1" + by (metis comp_associative comp_commute_below_diversity star.circ_transitive_equal) + have "?p \ -1 \ (w \ y\<^sup>T) \ (p \ -1)" + by (metis comp_inf.mult_right_dist_sup dual_order.trans inf.cobounded1 inf.coboundedI2 inf.sup_monoid.add_assoc le_supI sup.cobounded1 sup_ge2) + also have "... = w * y\<^sup>T \ (p \ -1)" + using assms(2,3) by (simp add: vector_covector) + finally have "(?p \ -1)\<^sup>+ \ (w * y\<^sup>T \ (p \ -1))\<^sup>+" + by (simp add: comp_isotone star_isotone) + also have "... = (p \ -1)\<^sup>+ \ (p \ -1)\<^sup>\ * w * y\<^sup>T * (p \ -1)\<^sup>\" + using assms(2,3) plus_arc_decompose points_arc by (simp add: comp_associative) + also have "... \ (p \ -1)\<^sup>+ \ p\<^sup>\ * w * y\<^sup>T * p\<^sup>\" + using reachable_without_loops by auto + also have "... \ -1" + using 1 assms(1) by simp + finally show ?thesis + by simp +qed + +lemma acyclic_down_closed: + "x \ y \ acyclic y \ acyclic x" + using comp_isotone star_isotone by fastforce + +text \Theorem 6.3\ + +lemma update_acyclic_3: + assumes "acyclic (p \ -1)" + and "point w" + shows "acyclic ((p[w\w]) \ -1)" +proof - + let ?p = "p[w\w]" + have "?p \ -1 \ (w \ w\<^sup>T \ -1) \ (p \ -1)" + by (metis comp_inf.mult_right_dist_sup inf.cobounded2 inf.sup_monoid.add_assoc sup_right_isotone) + also have "... = p \ -1" + using assms(2) by (metis comp_inf.covector_complement_closed equivalence_top_closed inf_top.right_neutral maddux_3_13 pseudo_complement regular_closed_top regular_one_closed vector_covector vector_top_closed) + finally show ?thesis + using assms(1) acyclic_down_closed by blast +qed + +text \Root of the tree containing point $x$ in the disjoint-set forest $p$\ + +abbreviation "root p x \ p\<^sup>T\<^sup>\ * x \ (p \ 1) * top" + +text \Theorem 3.1\ + +lemma root_var: + "root p x = (p \ 1) * p\<^sup>T\<^sup>\ * x" + by (simp add: coreflexive_comp_top_inf inf_commute mult_assoc) + +text \Theorem 3.2\ + +lemma root_successor_loop: + "univalent p \ root p x = p[[root p x]]" + by (metis root_var injective_codomain comp_associative conv_dist_inf coreflexive_symmetric equivalence_one_closed inf.cobounded2 univalent_conv_injective) + +lemma root_transitive_successor_loop: + "univalent p \ root p x = p\<^sup>T\<^sup>\ * (root p x)" + by (metis mult_1_right star_one star_simulation_right_equal root_successor_loop) + +end + +context stone_relation_algebra_tarski +begin + +text \Two basic results about points using the Tarski rule of relation algebras\ + +lemma point_in_vector_partition: + assumes "point x" + and "vector y" + shows "x \ -y \ x \ --y" +proof (cases "x * x\<^sup>T \ -y") + case True + have "x \ x * x\<^sup>T * x" + by (simp add: ex231c) + also have "... \ -y * x" + by (simp add: True mult_left_isotone) + also have "... \ -y" + by (metis assms(2) mult_right_isotone top.extremum vector_complement_closed) + finally show ?thesis + by simp +next + case False + have "x \ x * x\<^sup>T * x" + by (simp add: ex231c) + also have "... \ --y * x" + using False assms(1) arc_in_partition mult_left_isotone point_arc by blast + also have "... \ --y" + by (metis assms(2) mult_right_isotone top.extremum vector_complement_closed) + finally show ?thesis + by simp +qed + +lemma point_atomic_vector: + assumes "point x" + and "vector y" + and "regular y" + and "y \ x" + shows "y = x \ y = bot" +proof (cases "x \ -y") + case True + thus ?thesis + using assms(4) inf.absorb2 pseudo_complement by force +next + case False + thus ?thesis + using assms point_in_vector_partition by fastforce +qed + +text \Theorem 4.3\ + +lemma distinct_points: + assumes "point x" + and "point y" + and "x \ y" + shows "x \ y = bot" + by (metis assms antisym comp_bijective_complement inf.sup_monoid.add_commute mult_left_one pseudo_complement regular_one_closed point_in_vector_partition) + +text \Back and von Wright's array independence requirements \cite{BackWright1998}\ + +lemma put_get_different: + assumes "point y" "point w" "w \ y" + shows "(x[y\z])[[w]] = x[[w]]" +proof - + have "(x[y\z])[[w]] = (y\<^sup>T \ z) * w \ (-y\<^sup>T \ x\<^sup>T) * w" + by (simp add: conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup) + also have "... = z * (w \ y) \ x\<^sup>T * (w \ -y)" + by (metis assms(1) conv_complement covector_inf_comp_3 inf_commute vector_complement_closed) + also have "... = x\<^sup>T * w" + proof - + have 1: "w \ y = bot" + using assms distinct_points by simp + hence "w \ -y" + using pseudo_complement by simp + thus ?thesis + using 1 by (simp add: inf.absorb1) + qed + finally show ?thesis + . +qed + +lemma put_put_different: + assumes "point y" "point v" "v \ y" + shows "(x[y\z])[v\w] = (x[v\w])[y\z]" +proof - + have "(x[y\z])[v\w] = (v \ w\<^sup>T) \ (-v \ y \ z\<^sup>T) \ (-v \ -y \ x)" + by (simp add: comp_inf.semiring.distrib_left inf_assoc sup_assoc) + also have "... = (v \ w\<^sup>T) \ (y \ z\<^sup>T) \ (-v \ -y \ x)" + using assms distinct_points pseudo_complement inf.absorb2 by simp + also have "... = (y \ z\<^sup>T) \ (v \ w\<^sup>T) \ (-y \ -v \ x)" + by (simp add: inf_commute sup_commute) + also have "... = (y \ z\<^sup>T) \ (-y \ v \ w\<^sup>T) \ (-y \ -v \ x)" + using assms distinct_points pseudo_complement inf.absorb2 by simp + also have "... = (x[v\w])[y\z]" + by (simp add: comp_inf.semiring.distrib_left inf_assoc sup_assoc) + finally show ?thesis + . +qed + +end + +section \Verifying Operations on Disjoint-Set Forests\ + +text \ +In this section we verify the make-set, find-set and union-sets operations of disjoint-set forests. +We start by introducing syntax for updating arrays in programs. +Updating the value at a given array index means updating the whole array. +\ + +syntax + "_rel_update" :: "idt \ 'a \ 'a \ 'b com" ("(2_[_] :=/ _)" [70, 65, 65] 61) + +translations + "x[y] := z" => "(x := (y \ z\<^sup>T) \ (CONST uminus y \ x))" + +text \ +The finiteness requirement in the following class is used for proving that the operations terminate. +\ + +class finite_regular_p_algebra = p_algebra + + assumes finite_regular: "finite { x . regular x }" + +class stone_kleene_relation_algebra_tarski = stone_kleene_relation_algebra + stone_relation_algebra_tarski + +class stone_kleene_relation_algebra_tarski_finite_regular = stone_kleene_relation_algebra_tarski + finite_regular_p_algebra +begin + +subsection \Make-Set\ + +text \ +We prove two correctness results about make-set. +The first shows that the forest changes only to the extent of making one node the root of a tree. +The second result adds that only singleton sets are created. +\ + +definition "make_set_postcondition p x p0 \ x \ p = x * x\<^sup>T \ -x \ p = -x \ p0" + +theorem make_set: + "VARS p + [ point x \ p0 = p ] + p[x] := x + [ make_set_postcondition p x p0 ]" + apply vcg_tc_simp + by (simp add: make_set_postcondition_def inf_sup_distrib1 inf_assoc[THEN sym] vector_covector[THEN sym]) + +theorem make_set_2: + "VARS p + [ point x \ p0 = p \ p \ 1 ] + p[x] := x + [ make_set_postcondition p x p0 \ p \ 1 ]" +proof vcg_tc + fix p + assume 1: "point x \ p0 = p \ p \ 1" + show "make_set_postcondition (p[x\x]) x p0 \ p[x\x] \ 1" + proof (rule conjI) + show "make_set_postcondition (p[x\x]) x p0" + using 1 by (simp add: make_set_postcondition_def inf_sup_distrib1 inf_assoc[THEN sym] vector_covector[THEN sym]) + show "p[x\x] \ 1" + using 1 by (metis coreflexive_sup_closed dual_order.trans inf.cobounded2 vector_covector) + qed +qed + +text \ +The above total-correctness proof allows us to extract a function, which can be used in other implementations below. +This is a technique of \cite{Guttmann2018c}. +\ + +lemma make_set_exists: + "point x \ \p' . make_set_postcondition p' x p" + using tc_extract_function make_set by blast + +definition "make_set p x \ (SOME p' . make_set_postcondition p' x p)" + +lemma make_set_function: + assumes "point x" + and "p' = make_set p x" + shows "make_set_postcondition p' x p" +proof - + let ?P = "\p' . make_set_postcondition p' x p" + have "?P (SOME z . ?P z)" + using assms(1) make_set_exists by (meson someI) + thus ?thesis + using assms(2) make_set_def by auto +qed + +subsection \Find-Set\ + +text \ +Disjoint-set forests are represented by their parent mapping. +It is a forest except each root of a component tree points to itself. + +We prove that find-set returns the root of the component tree of the given node. +\ + +abbreviation "disjoint_set_forest p \ mapping p \ acyclic (p \ -1)" + +definition "find_set_precondition p x \ disjoint_set_forest p \ point x" +definition "find_set_invariant p x y \ find_set_precondition p x \ point y \ y \ p\<^sup>T\<^sup>\ * x" +definition "find_set_postcondition p x y \ point y \ y = root p x" + +lemma find_set_1: + "find_set_precondition p x \ find_set_invariant p x x" + apply (unfold find_set_invariant_def) + using mult_left_isotone star.circ_reflexive find_set_precondition_def by fastforce + +lemma find_set_2: + "find_set_invariant p x y \ y \ p[[y]] \ card { z . regular z \ z \ p\<^sup>T\<^sup>\ * y } = n \ find_set_invariant p x (p[[y]]) \ card { z . regular z \ z \ p\<^sup>T\<^sup>\ * (p[[y]]) } < n" +proof - + let ?s = "{ z . regular z \ z \ p\<^sup>T\<^sup>\ * y }" + let ?t = "{ z . regular z \ z \ p\<^sup>T\<^sup>\ * (p[[y]]) }" + assume 1: "find_set_invariant p x y \ y \ p[[y]] \ card ?s = n" + hence 2: "point (p[[y]])" + using read_point find_set_invariant_def find_set_precondition_def by simp + show "find_set_invariant p x (p[[y]]) \ card ?t < n" + proof (unfold find_set_invariant_def, intro conjI) + show "find_set_precondition p x" + using 1 find_set_invariant_def by simp + show "vector (p[[y]])" + using 2 by simp + show "injective (p[[y]])" + using 2 by simp + show "surjective (p[[y]])" + using 2 by simp + show "p[[y]] \ p\<^sup>T\<^sup>\ * x" + using 1 by (metis (hide_lams) find_set_invariant_def comp_associative comp_isotone star.circ_increasing star.circ_transitive_equal) + show "card ?t < n" + proof - + have 3: "(p\<^sup>T \ -1) * (p\<^sup>T \ -1)\<^sup>+ * y \ (p\<^sup>T \ -1)\<^sup>+ * y" + by (simp add: mult_left_isotone mult_right_isotone star.left_plus_below_circ) + have "p[[y]] = (p\<^sup>T \ 1) * y \ (p\<^sup>T \ -1) * y" + by (metis maddux_3_11_pp mult_right_dist_sup regular_one_closed) + also have "... \ ((p[[y]]) \ y) \ (p\<^sup>T \ -1) * y" + by (metis comp_left_subdist_inf mult_1_left semiring.add_right_mono) + also have "... = (p\<^sup>T \ -1) * y" + using 1 2 find_set_invariant_def distinct_points by auto + finally have 4: "(p\<^sup>T \ -1)\<^sup>\ * (p[[y]]) \ (p\<^sup>T \ -1)\<^sup>+ * y" + using 3 by (metis inf.antisym_conv inf.eq_refl inf_le1 mult_left_isotone star_plus mult_assoc) + hence "p\<^sup>T\<^sup>\ * (p[[y]]) \ p\<^sup>T\<^sup>\ * y" + by (metis mult_isotone order_refl star.left_plus_below_circ star_plus mult_assoc) + hence 5: "?t \ ?s" + using order_trans by auto + have 6: "y \ ?s" + using 1 find_set_invariant_def bijective_regular mult_left_isotone star.circ_reflexive by fastforce + have 7: "\ y \ ?t" + proof + assume "y \ ?t" + hence "y \ (p\<^sup>T \ -1)\<^sup>+ * y" + using 4 by (metis reachable_without_loops mem_Collect_eq order_trans) + hence "y * y\<^sup>T \ (p\<^sup>T \ -1)\<^sup>+" + using 1 find_set_invariant_def shunt_bijective by simp + also have "... \ -1" + using 1 by (metis (mono_tags, lifting) find_set_invariant_def find_set_precondition_def conv_dist_comp conv_dist_inf conv_isotone conv_star_commute equivalence_one_closed star.circ_plus_same symmetric_complement_closed) + finally have "y \ -y" + using schroeder_4_p by auto + thus False + using 1 by (metis find_set_invariant_def comp_inf.coreflexive_idempotent conv_complement covector_vector_comp inf.absorb1 inf.sup_monoid.add_commute pseudo_complement surjective_conv_total top.extremum vector_top_closed regular_closed_top) + qed + have "card ?t < card ?s" + apply (rule psubset_card_mono) + subgoal using finite_regular by simp + subgoal using 5 6 7 by auto + done + thus ?thesis + using 1 by simp + qed + qed +qed + +lemma find_set_3: + "find_set_invariant p x y \ y = p[[y]] \ find_set_postcondition p x y" +proof - + assume 1: "find_set_invariant p x y \ y = p[[y]]" + show "find_set_postcondition p x y" + proof (unfold find_set_postcondition_def, rule conjI) + show "point y" + using 1 find_set_invariant_def by simp + show "y = root p x" + proof (rule antisym) + have "y * y\<^sup>T \ p" + using 1 by (metis find_set_invariant_def find_set_precondition_def shunt_bijective shunt_mapping top_right_mult_increasing) + hence "y * y\<^sup>T \ p \ 1" + using 1 find_set_invariant_def le_infI by blast + hence "y \ (p \ 1) * top" + using 1 by (metis find_set_invariant_def order_lesseq_imp shunt_bijective top_right_mult_increasing mult_assoc) + thus "y \ root p x" + using 1 find_set_invariant_def by simp + next + have 2: "x \ p\<^sup>\ * y" + using 1 find_set_invariant_def find_set_precondition_def bijective_reverse conv_star_commute by auto + have "p\<^sup>T * p\<^sup>\ * y = p\<^sup>T * p * p\<^sup>\ * y \ (p[[y]])" + by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint) + also have "... \ p\<^sup>\ * y \ y" + using 1 by (metis find_set_invariant_def find_set_precondition_def comp_isotone mult_left_sub_dist_sup semiring.add_right_mono star.circ_back_loop_fixpoint star.circ_circ_mult star.circ_top star.circ_transitive_equal star_involutive star_one) + also have "... = p\<^sup>\ * y" + by (metis star.circ_loop_fixpoint sup.left_idem sup_commute) + finally have 3: "p\<^sup>T\<^sup>\ * x \ p\<^sup>\ * y" + using 2 by (simp add: comp_associative star_left_induct) + have "p * y \ (p \ 1) * top = (p \ 1) * p * y" + using comp_associative coreflexive_comp_top_inf inf_commute by auto + also have "... \ p\<^sup>T * p * y" + by (metis inf.cobounded2 inf.sup_monoid.add_commute mult_left_isotone one_inf_conv) + also have "... \ y" + using 1 find_set_invariant_def find_set_precondition_def mult_left_isotone by fastforce + finally have 4: "p * y \ y \ -((p \ 1) * top)" + using 1 by (metis find_set_invariant_def shunting_p bijective_regular) + have "p\<^sup>T * (p \ 1) \ p\<^sup>T \ 1" + using 1 by (metis find_set_invariant_def find_set_precondition_def N_top comp_isotone coreflexive_idempotent inf.cobounded2 inf.sup_monoid.add_commute inf_assoc one_inf_conv shunt_mapping) + hence "p\<^sup>T * (p \ 1) * top \ (p \ 1) * top" + using inf_commute mult_isotone one_inf_conv by auto + hence "p * -((p \ 1) * top) \ -((p \ 1) * top)" + by (metis comp_associative inf.sup_monoid.add_commute p_antitone p_antitone_iff schroeder_3_p) + hence "p * y \ p * -((p \ 1) * top) \ y \ -((p \ 1) * top)" + using 4 dual_order.trans le_supI sup_ge2 by blast + hence "p * (y \ -((p \ 1) * top)) \ y \ -((p \ 1) * top)" + by (simp add: mult_left_dist_sup) + hence "p\<^sup>\ * y \ y \ -((p \ 1) * top)" + by (simp add: star_left_induct) + hence "p\<^sup>T\<^sup>\ * x \ y \ -((p \ 1) * top)" + using 3 dual_order.trans by blast + thus "root p x \ y" + using 1 by (metis find_set_invariant_def shunting_p bijective_regular) + qed + qed +qed + +theorem find_set: + "VARS y + [ find_set_precondition p x ] + y := x; + WHILE y \ p[[y]] + INV { find_set_invariant p x y } + VAR { card { z . regular z \ z \ p\<^sup>T\<^sup>\ * y } } + DO y := p[[y]] + OD + [ find_set_postcondition p x y ]" + apply vcg_tc_simp + apply (fact find_set_1) + apply (fact find_set_2) + by (fact find_set_3) + +lemma find_set_exists: + "find_set_precondition p x \ \y . find_set_postcondition p x y" + using tc_extract_function find_set by blast + +text \ +The root of a component tree is a point, that is, represents a singleton set of nodes. +This could be proved from the definitions using Kleene-relation algebraic calculations. +But they can be avoided because the property directly follows from the postcondition of the previous correctness proof. +The corresponding algorithm shows how to obtain the root. +We therefore have an essentially constructive proof of the following result. +\ + +text \Theorem 3.3\ + +lemma root_point: + "disjoint_set_forest p \ point x \ point (root p x)" + using find_set_exists find_set_precondition_def find_set_postcondition_def by simp + +definition "find_set p x \ (SOME y . find_set_postcondition p x y)" + +lemma find_set_function: + assumes "find_set_precondition p x" + and "y = find_set p x" + shows "find_set_postcondition p x y" + by (metis assms find_set_def find_set_exists someI) + +subsection \Path Compression\ + +text \ +The path-compression technique is frequently implemented in recursive implementations of find-set +modifying the tree on the way out from recursive calls. Here we implement it using a second while-loop, +which iterates over the same path to the root and changes edges to point to the root of the component, +which is known after the while-loop in find-set completes. We prove that path compression preserves +the equivalence-relational semantics of the disjoint-set forest and also preserves the roots of the +component trees. +\ + +definition "path_compression_precondition p x y \ disjoint_set_forest p \ point x \ point y \ y = root p x" +definition "path_compression_invariant p x y p0 w \ + path_compression_precondition p x y \ point w \ y \ p\<^sup>T\<^sup>\ * w \ + (w \ x \ p[[x]] = y \ y \ x \ p\<^sup>T\<^sup>+ * w \ -x) \ p \ 1 = p0 \ 1 \ fc p = fc p0" +definition "path_compression_postcondition p x y p0 \ + path_compression_precondition p x y \ p \ 1 = p0 \ 1 \ fc p = fc p0" + +lemma path_compression_1: + "path_compression_precondition p x y \ p0 = p \ path_compression_invariant p x y p x" + using path_compression_invariant_def path_compression_precondition_def by auto + +lemma path_compression_2: + "path_compression_invariant p x y p0 w \ y \ p[[w]] \ card { z . regular z \ z \ p\<^sup>T\<^sup>\ * w } = n + \ path_compression_invariant (p[w\y]) x y p0 (p[[w]]) \ card { z . regular z \ z \ (p[w\y])\<^sup>T\<^sup>\ * (p[[w]]) } < n" +proof - + let ?p = "p[w\y]" + let ?s = "{ z . regular z \ z \ p\<^sup>T\<^sup>\ * w }" + let ?t = "{ z . regular z \ z \ ?p\<^sup>T\<^sup>\ * (p[[w]]) }" + assume 1: "path_compression_invariant p x y p0 w \ y \ p[[w]] \ card ?s = n" + hence 2: "point (p[[w]])" + by (simp add: path_compression_invariant_def path_compression_precondition_def read_point) + show "path_compression_invariant ?p x y p0 (p[[w]]) \ card ?t < n" + proof (unfold path_compression_invariant_def, intro conjI) + have 3: "mapping ?p" + using 1 by (meson path_compression_invariant_def path_compression_precondition_def update_mapping bijective_regular) + have 4: "w \ y" + using 1 by (metis (no_types, hide_lams) path_compression_invariant_def path_compression_precondition_def root_successor_loop) + hence 5: "w \ y = bot" + using 1 distinct_points path_compression_invariant_def path_compression_precondition_def by auto + hence "y * w\<^sup>T \ -1" + using pseudo_complement schroeder_4_p by auto + hence "y * w\<^sup>T \ p\<^sup>T\<^sup>\ \ -1" + using 1 shunt_bijective path_compression_invariant_def by auto + also have "... \ p\<^sup>T\<^sup>+" + by (simp add: star_plus_without_loops) + finally have 6: "y \ p\<^sup>T\<^sup>+ * w" + using 1 shunt_bijective path_compression_invariant_def by blast + have 7: "w * w\<^sup>T \ -p\<^sup>T\<^sup>+" + proof (rule ccontr) + assume "\ w * w\<^sup>T \ -p\<^sup>T\<^sup>+" + hence "w * w\<^sup>T \ --p\<^sup>T\<^sup>+" + using 1 path_compression_invariant_def point_arc arc_in_partition by blast + hence "w * w\<^sup>T \ p\<^sup>T\<^sup>+ \ 1" + using 1 path_compression_invariant_def path_compression_precondition_def mapping_regular regular_conv_closed regular_closed_star regular_mult_closed by simp + also have "... = ((p\<^sup>T \ 1) * p\<^sup>T\<^sup>\ \ 1) \ ((p\<^sup>T \ -1) * p\<^sup>T\<^sup>\ \ 1)" + by (metis comp_inf.mult_right_dist_sup maddux_3_11_pp mult_right_dist_sup regular_one_closed) + also have "... = ((p\<^sup>T \ 1) * p\<^sup>T\<^sup>\ \ 1) \ ((p \ -1)\<^sup>+ \ 1)\<^sup>T" + by (metis conv_complement conv_dist_inf conv_plus_commute equivalence_one_closed reachable_without_loops) + also have "... \ ((p\<^sup>T \ 1) * p\<^sup>T\<^sup>\ \ 1) \ (-1 \ 1)\<^sup>T" + using 1 by (metis (no_types, hide_lams) path_compression_invariant_def path_compression_precondition_def sup_right_isotone inf.sup_left_isotone conv_isotone) + also have "... = (p\<^sup>T \ 1) * p\<^sup>T\<^sup>\ \ 1" + by simp + also have "... \ (p\<^sup>T \ 1) * top \ 1" + by (metis comp_inf.comp_isotone coreflexive_comp_top_inf equivalence_one_closed inf.cobounded1 inf.cobounded2) + also have "... \ p\<^sup>T" + by (simp add: coreflexive_comp_top_inf_one) + finally have "w * w\<^sup>T \ p\<^sup>T" + by simp + hence "w \ p[[w]]" + using 1 path_compression_invariant_def shunt_bijective by blast + hence "w = p[[w]]" + using 1 2 path_compression_invariant_def epm_3 by fastforce + hence "w = p\<^sup>T\<^sup>+ * w" + using 2 by (metis comp_associative star.circ_top star_simulation_right_equal) + thus False + using 1 4 6 epm_3 path_compression_invariant_def path_compression_precondition_def by fastforce + qed + hence 8: "w \ p\<^sup>T\<^sup>+ * w = bot" + using p_antitone_iff pseudo_complement schroeder_4_p by blast + show "y \ ?p\<^sup>T\<^sup>\ * (p[[w]])" + proof - + have "(w \ y\<^sup>T)\<^sup>T * (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w \ w\<^sup>T * (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (simp add: conv_isotone mult_left_isotone) + also have "... \ w\<^sup>T * p\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (simp add: conv_isotone mult_left_isotone star_isotone mult_right_isotone) + also have "... = w\<^sup>T * p\<^sup>T\<^sup>+ * w" + by (simp add: star_plus mult_assoc) + also have "... = bot" + using 1 8 by (metis (no_types, hide_lams) path_compression_invariant_def covector_inf_comp_3 mult_assoc conv_dist_comp conv_star_commute covector_bot_closed equivalence_top_closed inf.le_iff_sup mult_left_isotone) + finally have "((w \ y\<^sup>T)\<^sup>T \ (-w \ p)\<^sup>T) * (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w \ (-w \ p)\<^sup>T * (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (simp add: bot_unique mult_right_dist_sup) + also have "... \ (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (simp add: mult_left_isotone star.left_plus_below_circ) + finally have "?p\<^sup>T * (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w \ (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (simp add: conv_dist_sup) + hence "?p\<^sup>T\<^sup>\ * p\<^sup>T * w \ (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (metis comp_associative star.circ_loop_fixpoint star_left_induct sup_commute sup_least sup_left_divisibility) + hence "w \ ?p\<^sup>T\<^sup>\ * p\<^sup>T * w \ w \ (-w \ p)\<^sup>T\<^sup>\ * p\<^sup>T * w" + using inf.sup_right_isotone by blast + also have "... \ w \ p\<^sup>T\<^sup>\ * p\<^sup>T * w" + using conv_isotone mult_left_isotone star_isotone inf.sup_right_isotone by simp + also have "... = bot" + using 8 by (simp add: star_plus) + finally have 9: "w\<^sup>T * ?p\<^sup>T\<^sup>\ * p\<^sup>T * w = bot" + using 1 by (metis (no_types, hide_lams) path_compression_invariant_def covector_inf_comp_3 mult_assoc conv_dist_comp covector_bot_closed equivalence_top_closed inf.le_iff_sup mult_left_isotone bot_least inf.absorb1) + have "p\<^sup>T * ?p\<^sup>T\<^sup>\ * p\<^sup>T * w = ((w \ p)\<^sup>T \ (-w \ p)\<^sup>T) * ?p\<^sup>T\<^sup>\ * p\<^sup>T * w" + using 1 by (metis (no_types, lifting) bijective_regular conv_dist_sup inf_commute maddux_3_11_pp path_compression_invariant_def) + also have "... = (w \ p)\<^sup>T * ?p\<^sup>T\<^sup>\ * p\<^sup>T * w \ (-w \ p)\<^sup>T * ?p\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (simp add: mult_right_dist_sup) + also have "... \ w\<^sup>T * ?p\<^sup>T\<^sup>\ * p\<^sup>T * w \ (-w \ p)\<^sup>T * ?p\<^sup>T\<^sup>\ * p\<^sup>T * w" + using semiring.add_right_mono comp_isotone conv_isotone by auto + also have "... = (-w \ p)\<^sup>T * ?p\<^sup>T\<^sup>\ * p\<^sup>T * w" + using 9 by simp + also have "... \ ?p\<^sup>T\<^sup>+ * p\<^sup>T * w" + by (simp add: conv_isotone mult_left_isotone) + also have "... \ ?p\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (simp add: comp_isotone star.left_plus_below_circ) + finally have "p\<^sup>T\<^sup>\ * p\<^sup>T * w \ ?p\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (metis comp_associative star.circ_loop_fixpoint star_left_induct sup_commute sup_least sup_left_divisibility) + thus "y \ ?p\<^sup>T\<^sup>\ * (p[[w]])" + using 6 by (simp add: star_simulation_right_equal mult_assoc) + qed + have 10: "acyclic (?p \ -1)" + using 1 update_acyclic_1 path_compression_invariant_def path_compression_precondition_def by auto + have "?p[[p\<^sup>T\<^sup>+ * w]] \ p\<^sup>T\<^sup>+ * w" + proof - + have "(w\<^sup>T \ y) * p\<^sup>T\<^sup>+ * w = y \ w\<^sup>T * p\<^sup>T\<^sup>+ * w" + using 1 by (metis (no_types, hide_lams) path_compression_invariant_def path_compression_precondition_def inf_commute vector_inf_comp) + hence "?p[[p\<^sup>T\<^sup>+ * w]] = (y \ w\<^sup>T * p\<^sup>T\<^sup>+ * w) \ (-w\<^sup>T \ p\<^sup>T) * p\<^sup>T\<^sup>+ * w" + by (simp add: comp_associative conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup) + also have "... \ y \ (-w\<^sup>T \ p\<^sup>T) * p\<^sup>T\<^sup>+ * w" + using sup_left_isotone by auto + also have "... \ y \ p\<^sup>T * p\<^sup>T\<^sup>+ * w" + using mult_left_isotone sup_right_isotone by auto + also have "... \ y \ p\<^sup>T\<^sup>+ * w" + using semiring.add_left_mono mult_left_isotone mult_right_isotone star.left_plus_below_circ by auto + also have "... = p\<^sup>T\<^sup>+ * w" + using 6 by (simp add: sup_absorb2) + finally show ?thesis + by simp + qed + hence 11: "?p\<^sup>T\<^sup>\ * (p[[w]]) \ p\<^sup>T\<^sup>+ * w" + using star_left_induct by (simp add: mult_left_isotone star.circ_mult_increasing) + hence 12: "?p\<^sup>T\<^sup>+ * (p[[w]]) \ p\<^sup>T\<^sup>+ * w" + using dual_order.trans mult_left_isotone star.left_plus_below_circ by blast + have 13: "?p[[x]] = y \ y \ x \ ?p\<^sup>T\<^sup>+ * (p[[w]]) \ -x" + proof (cases "w = x") + case True + hence "?p[[x]] = (w\<^sup>T \ y) * w \ (-w\<^sup>T \ p\<^sup>T) * w" + by (simp add: conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup) + also have "... = (w\<^sup>T \ y) * w \ p\<^sup>T * (-w \ w)" + using 1 by (metis (no_types, lifting) conv_complement inf.sup_monoid.add_commute path_compression_invariant_def covector_inf_comp_3 vector_complement_closed) + also have "... = (w\<^sup>T \ y) * w" + by simp + also have "... = y * w" + using 1 inf.sup_monoid.add_commute path_compression_invariant_def covector_inf_comp_3 by simp + also have "... = y" + using 1 by (metis comp_associative path_compression_precondition_def path_compression_invariant_def) + finally show ?thesis + using 4 8 12 True pseudo_complement inf.sup_monoid.add_commute order.trans by blast + next + case False + have "?p[[x]] = (w\<^sup>T \ y) * x \ (-w\<^sup>T \ p\<^sup>T) * x" + by (simp add: conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup) + also have "... = y * (w \ x) \ p\<^sup>T * (-w \ x)" + using 1 by (metis (no_types, lifting) conv_complement inf.sup_monoid.add_commute path_compression_invariant_def covector_inf_comp_3 vector_complement_closed) + also have "... = p\<^sup>T * (-w \ x)" + using 1 False path_compression_invariant_def path_compression_precondition_def distinct_points by auto + also have "... = y" + using 1 False path_compression_invariant_def path_compression_precondition_def distinct_points inf.absorb2 pseudo_complement by auto + finally show ?thesis + using 1 12 False path_compression_invariant_def by auto + qed + thus "p[[w]] \ x \ ?p[[x]] = y \ y \ x \ ?p\<^sup>T\<^sup>+ * (p[[w]]) \ -x" + by simp + have 14: "?p\<^sup>T\<^sup>\ * x = x \ y" + proof (rule antisym) + have "?p\<^sup>T * (x \ y) = y \ ?p\<^sup>T * y" + using 13 by (simp add: mult_left_dist_sup) + also have "... = y \ (w\<^sup>T \ y) * y \ (-w\<^sup>T \ p\<^sup>T) * y" + by (simp add: conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup sup_assoc) + also have "... \ y \ (w\<^sup>T \ y) * y \ p\<^sup>T * y" + using mult_left_isotone sup_right_isotone by auto + also have "... = y \ (w\<^sup>T \ y) * y" + using 1 by (smt sup.cobounded1 sup_absorb1 path_compression_invariant_def path_compression_precondition_def root_successor_loop) + also have "... \ y \ y * y" + using mult_left_isotone sup_right_isotone by auto + also have "... = y" + using 1 by (metis mult_semi_associative sup_absorb1 path_compression_invariant_def path_compression_precondition_def) + also have "... \ x \ y" + by simp + finally show "?p\<^sup>T\<^sup>\ * x \ x \ y" + by (simp add: star_left_induct) + next + show "x \ y \ ?p\<^sup>T\<^sup>\ * x" + using 13 by (metis mult_left_isotone star.circ_increasing star.circ_loop_fixpoint sup.boundedI sup_ge2) + qed + have 15: "y = root ?p x" + proof - + have "(p \ 1) * y = (p \ 1) * (p \ 1) * p\<^sup>T\<^sup>\ * x" + using 1 path_compression_invariant_def path_compression_precondition_def root_var mult_assoc by auto + also have "... = (p \ 1) * p\<^sup>T\<^sup>\ * x" + using coreflexive_idempotent by auto + finally have 16: "(p \ 1) * y = y" + using 1 path_compression_invariant_def path_compression_precondition_def root_var by auto + have 17: "(p \ 1) * x \ y" + using 1 by (metis (no_types, lifting) comp_right_one mult_left_isotone mult_right_isotone star.circ_reflexive path_compression_invariant_def path_compression_precondition_def root_var) + have "root ?p x = (?p \ 1) * (x \ y)" + using 14 by (metis mult_assoc root_var) + also have "... = (w \ y\<^sup>T \ 1) * (x \ y) \ (-w \ p \ 1) * (x \ y)" + by (simp add: inf_sup_distrib2 semiring.distrib_right) + also have "... = (w \ 1 \ y\<^sup>T) * (x \ y) \ (-w \ p \ 1) * (x \ y)" + by (simp add: inf.left_commute inf.sup_monoid.add_commute) + also have "... = (w \ 1) * (y \ (x \ y)) \ (-w \ p \ 1) * (x \ y)" + using 1 by (metis (no_types, lifting) path_compression_invariant_def path_compression_precondition_def covector_inf_comp_3) + also have "... = (w \ 1) * y \ (-w \ p \ 1) * (x \ y)" + by (simp add: inf.absorb1) + also have "... = (w \ 1 * y) \ (-w \ (p \ 1) * (x \ y))" + using 1 by (metis (no_types, lifting) inf_assoc vector_complement_closed path_compression_invariant_def vector_inf_comp) + also have "... = (w \ y) \ (-w \ ((p \ 1) * x \ y))" + using 16 by (simp add: mult_left_dist_sup) + also have "... = (w \ y) \ (-w \ y)" + using 17 by (simp add: sup.absorb2) + also have "... = y" + using 1 by (metis id_apply bijective_regular comp_inf.mult_right_dist_sup comp_inf.vector_conv_covector inf_top.right_neutral regular_complement_top path_compression_invariant_def) + finally show ?thesis + by simp + qed + show "path_compression_precondition ?p x y" + using 1 3 10 15 path_compression_invariant_def path_compression_precondition_def by auto + show "vector (p[[w]])" + using 2 by simp + show "injective (p[[w]])" + using 2 by simp + show "surjective (p[[w]])" + using 2 by simp + have "w \ p \ 1 \ w \ w\<^sup>T \ p" + by (metis inf.boundedE inf.boundedI inf.cobounded1 inf.cobounded2 one_inf_conv) + also have "... = w * w\<^sup>T \ p" + using 1 vector_covector path_compression_invariant_def by auto + also have "... \ -p\<^sup>T\<^sup>+ \ p" + using 7 by (simp add: inf.coboundedI2 inf.sup_monoid.add_commute) + finally have "w \ p \ 1 = bot" + by (metis (no_types, hide_lams) conv_dist_inf coreflexive_symmetric inf.absorb1 inf.boundedE inf.cobounded2 pseudo_complement star.circ_mult_increasing) + also have "w \ y\<^sup>T \ 1 = bot" + using 5 antisymmetric_bot_closed asymmetric_bot_closed comp_inf.schroeder_2 inf.absorb1 one_inf_conv by fastforce + finally have "w \ p \ 1 = w \ y\<^sup>T \ 1" + by simp + thus "?p \ 1 = p0 \ 1" + using 1 by (metis bijective_regular comp_inf.semiring.distrib_left inf.sup_monoid.add_commute maddux_3_11_pp path_compression_invariant_def) + show "fc ?p = fc p0" + proof - + have "p[[w]] = p\<^sup>T * (w \ p\<^sup>\ * y)" + using 1 by (metis (no_types, lifting) bijective_reverse conv_star_commute inf.absorb1 path_compression_invariant_def path_compression_precondition_def) + also have "... = p\<^sup>T * (w \ p\<^sup>\) * y" + using 1 vector_inf_comp path_compression_invariant_def mult_assoc by auto + also have "... = p\<^sup>T * ((w \ 1) \ (w \ p) * (-w \ p)\<^sup>\) * y" + using 1 omit_redundant_points path_compression_invariant_def by auto + also have "... = p\<^sup>T * (w \ 1) * y \ p\<^sup>T * (w \ p) * (-w \ p)\<^sup>\ * y" + by (simp add: comp_associative mult_left_dist_sup mult_right_dist_sup) + also have "... \ p\<^sup>T * y \ p\<^sup>T * (w \ p) * (-w \ p)\<^sup>\ * y" + by (metis semiring.add_right_mono comp_isotone eq_iff inf.cobounded1 inf.sup_monoid.add_commute mult_1_right) + also have "... = y \ p\<^sup>T * (w \ p) * (-w \ p)\<^sup>\ * y" + using 1 path_compression_invariant_def path_compression_precondition_def root_successor_loop by fastforce + also have "... \ y \ p\<^sup>T * p * (-w \ p)\<^sup>\ * y" + using comp_isotone sup_right_isotone by auto + also have "... \ y \ (-w \ p)\<^sup>\ * y" + using 1 by (metis (no_types, lifting) mult_left_isotone star.circ_circ_mult star_involutive star_one sup_right_isotone path_compression_invariant_def path_compression_precondition_def) + also have "... = (-w \ p)\<^sup>\ * y" + by (metis star.circ_loop_fixpoint sup.left_idem sup_commute) + finally have 18: "p[[w]] \ (-w \ p)\<^sup>\ * y" + by simp + have "p\<^sup>T * (-w \ p)\<^sup>\ * y = p\<^sup>T * y \ p\<^sup>T * (-w \ p) * (-w \ p)\<^sup>\ * y" + by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint sup_commute) + also have "... = y \ p\<^sup>T * (-w \ p) * (-w \ p)\<^sup>\ * y" + using 1 path_compression_invariant_def path_compression_precondition_def root_successor_loop by fastforce + also have "... \ y \ p\<^sup>T * p * (-w \ p)\<^sup>\ * y" + using comp_isotone sup_right_isotone by auto + also have "... \ y \ (-w \ p)\<^sup>\ * y" + using 1 by (metis (no_types, lifting) mult_left_isotone star.circ_circ_mult star_involutive star_one sup_right_isotone path_compression_invariant_def path_compression_precondition_def) + also have "... = (-w \ p)\<^sup>\ * y" + by (metis star.circ_loop_fixpoint sup.left_idem sup_commute) + finally have 19: "p\<^sup>T\<^sup>\ * p\<^sup>T * w \ (-w \ p)\<^sup>\ * y" + using 18 by (simp add: comp_associative star_left_induct) + have "w\<^sup>T \ p\<^sup>T = p\<^sup>T * (w\<^sup>T \ 1)" + using 1 by (metis conv_dist_comp conv_dist_inf equivalence_one_closed vector_inf_one_comp path_compression_invariant_def) + also have "... \ p[[w]]" + by (metis comp_right_subdist_inf inf.boundedE inf.sup_monoid.add_commute one_inf_conv) + also have "... \ p\<^sup>T\<^sup>\ * p\<^sup>T * w" + by (simp add: mult_left_isotone star.circ_mult_increasing_2) + also have "... \ (-w \ p)\<^sup>\ * y" + using 19 by simp + finally have "w \ p \ y\<^sup>T * (-w \ p)\<^sup>T\<^sup>\" + by (metis conv_dist_comp conv_dist_inf conv_involutive conv_isotone conv_star_commute) + hence "w \ p \ (w \ y\<^sup>T) * (-w \ p)\<^sup>T\<^sup>\" + using 1 by (metis inf.absorb1 inf.left_commute inf.left_idem inf.orderI vector_inf_comp path_compression_invariant_def) + also have "... \ (w \ y\<^sup>T) * ?p\<^sup>T\<^sup>\" + by (simp add: conv_isotone mult_right_isotone star_isotone) + also have "... \ ?p * ?p\<^sup>T\<^sup>\" + by (simp add: mult_left_isotone) + also have "... \ fc ?p" + by (simp add: mult_left_isotone star.circ_increasing) + finally have 20: "w \ p \ fc ?p" + by simp + have "-w \ p \ ?p" + by simp + also have "... \ fc ?p" + by (simp add: fc_increasing) + finally have "(w \ -w) \ p \ fc ?p" + using 20 by (simp add: comp_inf.semiring.distrib_left inf.sup_monoid.add_commute) + hence "p \ fc ?p" + using 1 by (metis (no_types, hide_lams) bijective_regular comp_inf.semiring.distrib_left inf.sup_monoid.add_commute maddux_3_11_pp path_compression_invariant_def) + hence 21: "fc p \ fc ?p" + using 3 fc_idempotent fc_isotone by fastforce + have "?p \ (w \ y\<^sup>T) \ p" + using sup_right_isotone by auto + also have "... = w * y\<^sup>T \ p" + using 1 path_compression_invariant_def path_compression_precondition_def vector_covector by auto + also have "... \ p\<^sup>\ \ p" + using 1 by (metis (no_types, lifting) conv_dist_comp conv_involutive conv_isotone conv_star_commute le_supI shunt_bijective star.circ_increasing sup_absorb1 path_compression_invariant_def) + also have "... \ fc p" + using fc_increasing star.circ_back_loop_prefixpoint by auto + finally have "fc ?p \ fc p" + using 1 by (metis (no_types, lifting) path_compression_invariant_def path_compression_precondition_def fc_idempotent fc_isotone) + thus ?thesis + using 1 21 path_compression_invariant_def by simp + qed + show "card ?t < n" + proof - + have "?p\<^sup>T * p\<^sup>T\<^sup>\ * w = (w\<^sup>T \ y) * p\<^sup>T\<^sup>\ * w \ (-w\<^sup>T \ p\<^sup>T) * p\<^sup>T\<^sup>\ * w" + by (simp add: conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup) + also have "... \ (w\<^sup>T \ y) * p\<^sup>T\<^sup>\ * w \ p\<^sup>T * p\<^sup>T\<^sup>\ * w" + using mult_left_isotone sup_right_isotone by auto + also have "... \ (w\<^sup>T \ y) * p\<^sup>T\<^sup>\ * w \ p\<^sup>T\<^sup>\ * w" + using mult_left_isotone star.left_plus_below_circ sup_right_isotone by blast + also have "... \ y * p\<^sup>T\<^sup>\ * w \ p\<^sup>T\<^sup>\ * w" + using semiring.add_right_mono mult_left_isotone by auto + also have "... \ y * top \ p\<^sup>T\<^sup>\ * w" + by (simp add: comp_associative le_supI1 mult_right_isotone) + also have "... = p\<^sup>T\<^sup>\ * w" + using 1 path_compression_invariant_def path_compression_precondition_def sup_absorb2 by auto + finally have "?p\<^sup>T\<^sup>\ * p\<^sup>T * w \ p\<^sup>T\<^sup>\ * w" + using 11 by (metis dual_order.trans star.circ_loop_fixpoint sup_commute sup_ge2 mult_assoc) + hence 22: "?t \ ?s" + using order_lesseq_imp mult_assoc by auto + have 23: "w \ ?s" + using 1 bijective_regular path_compression_invariant_def eq_iff star.circ_loop_fixpoint by auto + have 24: "\ w \ ?t" + proof + assume "w \ ?t" + hence 25: "w \ (?p\<^sup>T \ -1)\<^sup>\ * (p[[w]])" + using reachable_without_loops by auto + hence "p[[w]] \ (?p \ -1)\<^sup>\ * w" + using 1 2 by (metis (no_types, hide_lams) bijective_reverse conv_star_commute reachable_without_loops path_compression_invariant_def) + also have "... \ p\<^sup>\ * w" + proof - + have "p\<^sup>T\<^sup>\ * y = y" + using 1 path_compression_invariant_def path_compression_precondition_def root_transitive_successor_loop by fastforce + hence "y\<^sup>T * p\<^sup>\ * w = y\<^sup>T * w" + by (metis conv_dist_comp conv_involutive conv_star_commute) + also have "... = bot" + using 1 5 by (metis (no_types, hide_lams) conv_dist_comp conv_dist_inf equivalence_top_closed inf_top.right_neutral schroeder_2 symmetric_bot_closed path_compression_invariant_def) + finally have 26: "y\<^sup>T * p\<^sup>\ * w = bot" + by simp + have "(?p \ -1) * p\<^sup>\ * w = (w \ y\<^sup>T \ -1) * p\<^sup>\ * w \ (-w \ p \ -1) * p\<^sup>\ * w" + by (simp add: comp_inf.mult_right_dist_sup mult_right_dist_sup) + also have "... \ (w \ y\<^sup>T \ -1) * p\<^sup>\ * w \ p * p\<^sup>\ * w" + by (meson inf_le1 inf_le2 mult_left_isotone order_trans sup_right_isotone) + also have "... \ (w \ y\<^sup>T \ -1) * p\<^sup>\ * w \ p\<^sup>\ * w" + using mult_left_isotone star.left_plus_below_circ sup_right_isotone by blast + also have "... \ y\<^sup>T * p\<^sup>\ * w \ p\<^sup>\ * w" + by (meson inf_le1 inf_le2 mult_left_isotone order_trans sup_left_isotone) + also have "... = p\<^sup>\ * w" + using 26 by simp + finally show ?thesis + by (metis comp_associative le_supI star.circ_loop_fixpoint sup_ge2 star_left_induct) + qed + finally have "w \ p\<^sup>T\<^sup>\ * p\<^sup>T * w" + using 11 25 reachable_without_loops star_plus by auto + thus False + using 1 7 by (metis inf.le_iff_sup le_bot pseudo_complement schroeder_4_p semiring.mult_zero_right star.circ_plus_same path_compression_invariant_def) + qed + have "card ?t < card ?s" + apply (rule psubset_card_mono) + subgoal using finite_regular by simp + subgoal using 22 23 24 by auto + done + thus ?thesis + using 1 by simp + qed + qed +qed + +lemma path_compression_3: + "path_compression_invariant p x y p0 w \ y = p[[w]] \ path_compression_postcondition p x (p[[w]]) p0" + using path_compression_invariant_def path_compression_postcondition_def path_compression_precondition_def by auto + +theorem path_compression: + "VARS p t w + [ path_compression_precondition p x y \ p0 = p ] + w := x; + WHILE y \ p[[w]] + INV { path_compression_invariant p x y p0 w } + VAR { card { z . regular z \ z \ p\<^sup>T\<^sup>\ * w } } + DO t := w; + w := p[[w]]; + p[t] := y + OD + [ path_compression_postcondition p x y p0 ]" + apply vcg_tc_simp + apply (fact path_compression_1) + apply (fact path_compression_2) + by (fact path_compression_3) + +lemma path_compression_exists: + "path_compression_precondition p x y \ \p' . path_compression_postcondition p' x y p" + using tc_extract_function path_compression by blast + +definition "path_compression p x y \ (SOME p' . path_compression_postcondition p' x y p)" + +lemma path_compression_function: + assumes "path_compression_precondition p x y" + and "p' = path_compression p x y" + shows "path_compression_postcondition p' x y p" + by (metis assms path_compression_def path_compression_exists someI) + +subsection \Find-Set with Path Compression\ + +text \ +We sequentially combine find-set and path compression. +We consider implementations which use the previously derived functions and implementations which unfold their definitions. +\ + +theorem find_set_path_compression: + "VARS p y + [ find_set_precondition p x \ p0 = p ] + y := find_set p x; + p := path_compression p x y + [ path_compression_postcondition p x y p0 ]" + apply vcg_tc_simp + using find_set_function find_set_postcondition_def find_set_precondition_def path_compression_function path_compression_precondition_def by fastforce + +theorem find_set_path_compression_1: + "VARS p t w y + [ find_set_precondition p x \ p0 = p ] + y := find_set p x; + w := x; + WHILE y \ p[[w]] + INV { path_compression_invariant p x y p0 w } + VAR { card { z . regular z \ z \ p\<^sup>T\<^sup>\ * w } } + DO t := w; + w := p[[w]]; + p[t] := y + OD + [ path_compression_postcondition p x y p0 ]" + apply vcg_tc_simp + using find_set_function find_set_postcondition_def find_set_precondition_def path_compression_1 path_compression_precondition_def + apply fastforce + apply (fact path_compression_2) + by (fact path_compression_3) + +theorem find_set_path_compression_2: + "VARS p y + [ find_set_precondition p x \ p0 = p ] + y := x; + WHILE y \ p[[y]] + INV { find_set_invariant p x y \ p0 = p } + VAR { card { z . regular z \ z \ p\<^sup>T\<^sup>\ * y } } + DO y := p[[y]] + OD; + p := path_compression p x y + [ path_compression_postcondition p x y p0 ]" + apply vcg_tc_simp + apply (simp add: find_set_1) + using find_set_2 apply blast + by (smt find_set_3 find_set_invariant_def find_set_postcondition_def find_set_precondition_def path_compression_function path_compression_precondition_def) + +theorem find_set_path_compression_3: + "VARS p t w y + [ find_set_precondition p x \ p0 = p ] + y := x; + WHILE y \ p[[y]] + INV { find_set_invariant p x y \ p0 = p } + VAR { card { z . regular z \ z \ p\<^sup>T\<^sup>\ * y } } + DO y := p[[y]] + OD; + w := x; + WHILE y \ p[[w]] + INV { path_compression_invariant p x y p0 w } + VAR { card { z . regular z \ z \ p\<^sup>T\<^sup>\ * w } } + DO t := w; + w := p[[w]]; + p[t] := y + OD + [ path_compression_postcondition p x y p0 ]" + apply vcg_tc_simp + apply (simp add: find_set_1) + using find_set_2 apply blast + using find_set_3 find_set_invariant_def find_set_postcondition_def find_set_precondition_def path_compression_invariant_def path_compression_precondition_def apply blast + apply (fact path_compression_2) + by (fact path_compression_3) + +text \ +Find-set with path compression returns two results: the representative of the tree and the modified disjoint-set forest. +\ + +lemma find_set_path_compression_exists: + "find_set_precondition p x \ \p' y . path_compression_postcondition p' x y p" + using tc_extract_function find_set_path_compression by blast + +definition "find_set_path_compression p x \ (SOME (p',y) . path_compression_postcondition p' x y p)" + +lemma find_set_path_compression_function: + assumes "find_set_precondition p x" + and "(p',y) = find_set_path_compression p x" + shows "path_compression_postcondition p' x y p" +proof - + let ?P = "\(p',y) . path_compression_postcondition p' x y p" + have "?P (SOME z . ?P z)" + apply (unfold some_eq_ex) + using assms(1) find_set_path_compression_exists by simp + thus ?thesis + using assms(2) find_set_path_compression_def by auto +qed + +subsection \Union-Sets\ + +text \ +We only consider a naive union-sets operation (without ranks). +The semantics is the equivalence closure obtained after adding the link between the two given nodes, +which requires those two elements to be in the same set. +The implementation uses temporary variable \t\ to store the two results returned by find-set with path compression. +The disjoint-set forest, which keeps being updated, is threaded through the sequence of operations. +\ + +definition "union_sets_precondition p x y \ disjoint_set_forest p \ point x \ point y" +definition "union_sets_postcondition p x y p0 \ union_sets_precondition p x y \ fc p = wcc (p0 \ x * y\<^sup>T)" + +theorem union_sets: + "VARS p r s t + [ union_sets_precondition p x y \ p0 = p ] + t := find_set_path_compression p x; + p := fst t; + r := snd t; + t := find_set_path_compression p y; + p := fst t; + s := snd t; + p[r] := s + [ union_sets_postcondition p x y p0 ]" +proof vcg_tc_simp + fix p + let ?t1 = "find_set_path_compression p x" + let ?p1 = "fst ?t1" + let ?r = "snd ?t1" + let ?t2 = "find_set_path_compression ?p1 y" + let ?p2 = "fst ?t2" + let ?s = "snd ?t2" + let ?p = "?p2[?r\?s]" + assume 1: "union_sets_precondition p x y \ p0 = p" + show "union_sets_postcondition ?p x y p" + proof (unfold union_sets_postcondition_def union_sets_precondition_def, intro conjI) + have "path_compression_postcondition ?p1 x ?r p" + using 1 by (simp add: find_set_precondition_def union_sets_precondition_def find_set_path_compression_function) + hence 2: "disjoint_set_forest ?p1 \ point ?r \ ?r = root ?p1 x \ ?p1 \ 1 = p \ 1 \ fc ?p1 = fc p" + using path_compression_precondition_def path_compression_postcondition_def by auto + hence "path_compression_postcondition ?p2 y ?s ?p1" + using 1 by (simp add: find_set_precondition_def union_sets_precondition_def find_set_path_compression_function) + hence 3: "disjoint_set_forest ?p2 \ point ?s \ ?s = root ?p2 y \ ?p2 \ 1 = ?p1 \ 1 \ fc ?p2 = fc ?p1" + using path_compression_precondition_def path_compression_postcondition_def by auto + hence 4: "fc ?p2 = fc p" + using 2 by simp + show 5: "univalent ?p" + using 2 3 update_univalent by blast + show "total ?p" + using 2 3 bijective_regular update_total by blast + show "acyclic (?p \ -1)" + proof (cases "?r = ?s") + case True + thus ?thesis + using 3 update_acyclic_3 by fastforce + next + case False + hence "bot = ?r \ ?s" + using 2 3 distinct_points by blast + also have "... = ?r \ ?p2\<^sup>T\<^sup>\ * ?s" + using 3 root_transitive_successor_loop by force + finally have "?s \ ?p2\<^sup>\ * ?r = bot" + using schroeder_1 conv_star_commute inf.sup_monoid.add_commute by fastforce + thus ?thesis + using 2 3 update_acyclic_2 by blast + qed + show "vector x" + using 1 by (simp add: union_sets_precondition_def) + show "injective x" + using 1 by (simp add: union_sets_precondition_def) + show "surjective x" + using 1 by (simp add: union_sets_precondition_def) + show "vector y" + using 1 by (simp add: union_sets_precondition_def) + show "injective y" + using 1 by (simp add: union_sets_precondition_def) + show "surjective y" + using 1 by (simp add: union_sets_precondition_def) + show "fc ?p = wcc (p \ x * y\<^sup>T)" + proof (rule antisym) + have "?r = ?p1[[?r]]" + using 2 root_successor_loop by force + hence "?r * ?r\<^sup>T \ ?p1\<^sup>T" + using 2 eq_refl shunt_bijective by blast + hence "?r * ?r\<^sup>T \ ?p1" + using 2 conv_order coreflexive_symmetric by fastforce + hence "?r * ?r\<^sup>T \ ?p1 \ 1" + using 2 inf.boundedI by blast + also have "... = ?p2 \ 1" + using 3 by simp + finally have "?r * ?r\<^sup>T \ ?p2" + by simp + hence "?r \ ?p2 * ?r" + using 2 shunt_bijective by blast + hence 6: "?p2[[?r]] \ ?r" + using 3 shunt_mapping by blast + have "?r \ ?p2 \ ?r * (top \ ?r\<^sup>T * ?p2)" + using 2 by (metis dedekind_1) + also have "... = ?r * ?r\<^sup>T * ?p2" + by (simp add: mult_assoc) + also have "... \ ?r * ?r\<^sup>T" + using 6 by (metis comp_associative conv_dist_comp conv_involutive conv_order mult_right_isotone) + also have "... \ 1" + using 2 by blast + finally have 7: "?r \ ?p2 \ 1" + by simp + have "p \ wcc p" + by (simp add: star.circ_sub_dist_1) + also have "... = wcc ?p2" + using 4 by (simp add: star_decompose_1) + also have 8: "... \ wcc ?p" + proof - + have "wcc ?p2 = wcc ((-?r \ ?p2) \ (?r \ ?p2))" + using 2 by (metis bijective_regular inf.sup_monoid.add_commute maddux_3_11_pp) + also have "... \ wcc ((-?r \ ?p2) \ 1)" + using 7 wcc_isotone sup_right_isotone by simp + also have "... = wcc (-?r \ ?p2)" + using wcc_with_loops by simp + also have "... \ wcc ?p" + using wcc_isotone sup_ge2 by blast + finally show ?thesis + by simp + qed + finally have 9: "p \ wcc ?p" + by force + have "?r \ ?p1\<^sup>T\<^sup>\ * x" + using 2 by simp + hence 10: "?r * x\<^sup>T \ ?p1\<^sup>T\<^sup>\" + using 1 shunt_bijective union_sets_precondition_def by blast + hence "x * ?r\<^sup>T \ ?p1\<^sup>\" + using conv_dist_comp conv_order conv_star_commute by force + also have "... \ wcc ?p1" + by (simp add: star.circ_sub_dist) + also have "... = wcc ?p2" + using 2 3 by (simp add: fc_wcc) + also have "... \ wcc ?p" + using 8 by simp + finally have 11: "x * ?r\<^sup>T \ wcc ?p" + by simp + have 12: "?r * ?s\<^sup>T \ wcc ?p" + using 2 3 star.circ_sub_dist_1 sup_assoc vector_covector by auto + have "?s \ ?p2\<^sup>T\<^sup>\ * y" + using 3 by simp + hence 13: "?s * y\<^sup>T \ ?p2\<^sup>T\<^sup>\" + using 1 shunt_bijective union_sets_precondition_def by blast + also have "... \ wcc ?p2" + using star_isotone sup_ge2 by blast + also have "... \ wcc ?p" + using 8 by simp + finally have 14: "?s * y\<^sup>T \ wcc ?p" + by simp + have "x \ x * ?r\<^sup>T * ?r \ y \ y * ?s\<^sup>T * ?s" + using 2 3 shunt_bijective by blast + hence "x * y\<^sup>T \ x * ?r\<^sup>T * ?r * (y * ?s\<^sup>T * ?s)\<^sup>T" + using comp_isotone conv_isotone by blast + also have "... = x * ?r\<^sup>T * ?r * ?s\<^sup>T * ?s * y\<^sup>T" + by (simp add: comp_associative conv_dist_comp) + also have "... \ wcc ?p * (?r * ?s\<^sup>T) * (?s * y\<^sup>T)" + using 11 by (metis mult_left_isotone mult_assoc) + also have "... \ wcc ?p * wcc ?p * (?s * y\<^sup>T)" + using 12 by (metis mult_left_isotone mult_right_isotone) + also have "... \ wcc ?p * wcc ?p * wcc ?p" + using 14 by (metis mult_right_isotone) + also have "... = wcc ?p" + by (simp add: star.circ_transitive_equal) + finally have "p \ x * y\<^sup>T \ wcc ?p" + using 9 by simp + hence "wcc (p \ x * y\<^sup>T) \ wcc ?p" + using wcc_below_wcc by simp + thus "wcc (p \ x * y\<^sup>T) \ fc ?p" + using 5 fc_wcc by simp + have "-?r \ ?p2 \ wcc ?p2" + by (simp add: inf.coboundedI2 star.circ_sub_dist_1) + also have "... = wcc p" + using 4 by (simp add: star_decompose_1) + also have "... \ wcc (p \ x * y\<^sup>T)" + by (simp add: wcc_isotone) + finally have 15: "-?r \ ?p2 \ wcc (p \ x * y\<^sup>T)" + by simp + have "?r * x\<^sup>T \ wcc ?p1" + using 10 inf.order_trans star.circ_sub_dist sup_commute by fastforce + also have "... = wcc p" + using 2 by (simp add: star_decompose_1) + also have "... \ wcc (p \ x * y\<^sup>T)" + by (simp add: wcc_isotone) + finally have 16: "?r * x\<^sup>T \ wcc (p \ x * y\<^sup>T)" + by simp + have 17: "x * y\<^sup>T \ wcc (p \ x * y\<^sup>T)" + using le_supE star.circ_sub_dist_1 by blast + have "y * ?s\<^sup>T \ ?p2\<^sup>\" + using 13 conv_dist_comp conv_order conv_star_commute by fastforce + also have "... \ wcc ?p2" + using star.circ_sub_dist sup_commute by fastforce + also have "... = wcc p" + using 4 by (simp add: star_decompose_1) + also have "... \ wcc (p \ x * y\<^sup>T)" + by (simp add: wcc_isotone) + finally have 18: "y * ?s\<^sup>T \ wcc (p \ x * y\<^sup>T)" + by simp + have "?r \ ?r * x\<^sup>T * x \ ?s \ ?s * y\<^sup>T * y" + using 1 shunt_bijective union_sets_precondition_def by blast + hence "?r * ?s\<^sup>T \ ?r * x\<^sup>T * x * (?s * y\<^sup>T * y)\<^sup>T" + using comp_isotone conv_isotone by blast + also have "... = ?r * x\<^sup>T * x * y\<^sup>T * y * ?s\<^sup>T" + by (simp add: comp_associative conv_dist_comp) + also have "... \ wcc (p \ x * y\<^sup>T) * (x * y\<^sup>T) * (y * ?s\<^sup>T)" + using 16 by (metis mult_left_isotone mult_assoc) + also have "... \ wcc (p \ x * y\<^sup>T) * wcc (p \ x * y\<^sup>T) * (y * ?s\<^sup>T)" + using 17 by (metis mult_left_isotone mult_right_isotone) + also have "... \ wcc (p \ x * y\<^sup>T) * wcc (p \ x * y\<^sup>T) * wcc (p \ x * y\<^sup>T)" + using 18 by (metis mult_right_isotone) + also have "... = wcc (p \ x * y\<^sup>T)" + by (simp add: star.circ_transitive_equal) + finally have "?p \ wcc (p \ x * y\<^sup>T)" + using 2 3 15 vector_covector by auto + hence "wcc ?p \ wcc (p \ x * y\<^sup>T)" + using wcc_below_wcc by blast + thus "fc ?p \ wcc (p \ x * y\<^sup>T)" + using 5 fc_wcc by simp + qed + qed +qed + +lemma union_sets_exists: + "union_sets_precondition p x y \ \p' . union_sets_postcondition p' x y p" + using tc_extract_function union_sets by blast + +definition "union_sets p x y \ (SOME p' . union_sets_postcondition p' x y p)" + +lemma union_sets_function: + assumes "union_sets_precondition p x y" + and "p' = union_sets p x y" + shows "union_sets_postcondition p' x y p" + by (metis assms union_sets_def union_sets_exists someI) + +end + +end + diff --git a/thys/Relational_Disjoint_Set_Forests/ROOT b/thys/Relational_Disjoint_Set_Forests/ROOT new file mode 100644 --- /dev/null +++ b/thys/Relational_Disjoint_Set_Forests/ROOT @@ -0,0 +1,16 @@ +chapter AFP + +session Relational_Disjoint_Set_Forests (AFP) = Stone_Kleene_Relation_Algebras + + + options [timeout = 600] + + sessions + Aggregation_Algebras + + theories + Disjoint_Set_Forests + + document_files + "root.tex" + "root.bib" + diff --git a/thys/Relational_Disjoint_Set_Forests/document/root.bib b/thys/Relational_Disjoint_Set_Forests/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Relational_Disjoint_Set_Forests/document/root.bib @@ -0,0 +1,199 @@ +@STRING{afp = {Archive of Formal Proofs}} +@STRING{fac = {Formal Aspects of Computing}} +@STRING{is = {Information Sciences}} +@STRING{jlamp = {Journal of Logical and Algebraic Methods in Programming}} +@STRING{lncs = {Lecture Notes in Computer Science}} +@STRING{mitp = {MIT Press}} +@STRING{sv = {Springer}} + +@Book{BackWright1998, + author = {Back, R.-J. and von Wright, J.}, + title = {Refinement Calculus}, + publisher = sv, + address = {New York}, + year = 1998, + note = {} +} + +@Article{BackhouseCarre1975, + author = {Backhouse, R. C. and Carr{\'e}, B. A.}, + title = {Regular Algebra Applied to Path-finding Problems}, + journal = {Journal of the Institute of Mathematics and its Applications}, + volume = 15, + number = 2, + pages = {161--186}, + year = 1975, + note = {} +} + +@Article{Berghammer1999, + author = {Berghammer, R.}, + title = {Combining relational calculus and the {Dijkstra--Gries} method for deriving relational programs}, + journal = is, + volume = 119, + number = {3--4}, + pages = {155--171}, + year = 1999, + note = {} +} + +@InProceedings{BerghammerKargerWolf1998, + author = {Berghammer, R. and von Karger, B. and Wolf, A.}, + title = {Relation-Algebraic Derivation of Spanning Tree Algorithms}, + editor = {Jeuring, J.}, + booktitle = {Mathematics of Program Construction (MPC 1998)}, + publisher = sv, + series = lncs, + volume = 1422, + pages = {23--43}, + year = 1998, + note = {} +} + +@InProceedings{BerghammerStruth2010, + author = {Berghammer, R. and Struth, G.}, + title = {On Automated Program Construction and Verification}, + editor = {Bolduc, C. and Desharnais, J. and Ktari, B.}, + booktitle = {Mathematics of Program Construction (MPC 2010)}, + publisher = sv, + series = lncs, + volume = 6120, + pages = {22--41}, + year = 2010, + note = {} +} + +@Book{CormenLeisersonRivest1990, + author = {Cormen, T. H. and Leiserson, C. E. and Rivest, R. L.}, + title = {Introduction to Algorithms}, + publisher = mitp, + year = 1990, + note = {} +} + +@Article{FosterGreenwaldMoorePierceSchmitt2007, + author = {Foster, J. N. and Greenwald, M. B. and Moore, J. T. and Pierce, B. C. and Schmitt, A.}, + title = {Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem}, + journal = toplas, + volume = 29, + number = {3:17}, + pages = {1--65}, + year = 2007, + note = {} +} + +@Article{GallerFisher1964, + author = {Galler, B. A. and Fisher, M. J.}, + title = {An Improved Equivalence Algorithm}, + journal = cacm, + volume = 7, + number = 5, + pages = {301--303}, + year = 1964, + note = {} +} + +@Book{GondranMinoux2008, + author = {Gondran, M. and Minoux, M.}, + title = {Graphs, Dioids and Semirings}, + publisher = sv, + year = 2008, + note = {} +} + +@Article{Guttmann2018c, + author = {Guttmann, W.}, + title = {Verifying Minimum Spanning Tree Algorithms with {Stone} Relation Algebras}, + journal = jlamp, + volume = 101, + pages = {132--150}, + year = 2018, + note = {} +} + +@InProceedings{Guttmann2020b, + author = {Guttmann, W.}, + title = {Verifying the Correctness of Disjoint-Set Forests with {Kleene} Relation Algebras}, + editor = {Fahrenberg, U. and Jipsen, P. and Winter, M.}, + booktitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2020)}, + publisher = sv, + series = lncs, + volume = 12062, + pages = {134--151}, + year = 2020, + note = {} +} + +@Article{HoefnerMoeller2012, + author = {H{\"o}fner, P. and M{\"o}ller, B.}, + title = {Dijkstra, {Floyd} and {Warshall} meet {Kleene}}, + journal = fac, + volume = 24, + number = 4, + pages = {459--476}, + year = 2012, + note = {} +} + +@Article{Kozen1994, + author = {Kozen, D.}, + title = {A completeness theorem for {Kleene} algebras and the algebra of regular events}, + journal = {Information and Computation}, + volume = 110, + number = 2, + pages = {366--390}, + year = 1994, + note = {} +} + +@Article{LammichMeis2012, + author = {Lammich, P. and Meis, R.}, + title = {A Separation Logic Framework for {I}mperative {HOL}}, + journal = afp, + year = 2012, + note = {} +} + +@InProceedings{Moeller1993, + author = {M{\"o}ller, B.}, + title = {Derivation of Graph and Pointer Algorithms}, + editor = {M{\"o}ller, B. and Partsch, H. A. and Schuman, S. A.}, + booktitle = {Formal Program Development}, + publisher = sv, + series = lncs, + volume = 755, + pages = {123--160}, + year = 1993, + note = {} +} + +@Article{Tarjan1975, + author = {Tarjan, R. E.}, + title = {Efficiency of a Good But Not Linear Set Union Algorithm}, + journal = jacm, + volume = 22, + number = 2, + pages = {215--225}, + year = 1975, + note = {} +} + +@Article{Tarski1941, + author = {Tarski, A.}, + title = {On the calculus of relations}, + journal = {The Journal of Symbolic Logic}, + volume = 6, + number = 3, + pages = {73--89}, + year = 1941, + note = {} +} + +@Article{Zhan2018, + author = {Zhan, B.}, + title = {Verifying Imperative Programs using {Auto2}}, + journal = afp, + year = 2018, + note = {} +} + diff --git a/thys/Relational_Disjoint_Set_Forests/document/root.tex b/thys/Relational_Disjoint_Set_Forests/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Relational_Disjoint_Set_Forests/document/root.tex @@ -0,0 +1,61 @@ +\documentclass[11pt,a4paper]{article} + +\usepackage{isabelle,isabellesym} +\usepackage{amssymb,ragged2e} +\usepackage{pdfsetup} + +\isabellestyle{it} +\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\justifying\color{blue}}{\end{isapar}} +\renewcommand\labelitemi{$*$} +%\urlstyle{rm} + +\begin{document} + +\title{Relational Disjoint-Set Forests} +\author{Walter Guttmann} +\maketitle + +\begin{abstract} + We give a simple relation-algebraic semantics of read and write operations on associative arrays. + The array operations seamlessly integrate with assignments in the Hoare-logic library. + Using relation algebras and Kleene algebras we verify the correctness of an array-based implementation of disjoint-set forests with a naive union operation and a find operation with path compression. +\end{abstract} + +\tableofcontents + +\section{Overview} + +Relation algebras and Kleene algebras have previously been used to reason about graphs and graph algorithms \cite{BackhouseCarre1975,Berghammer1999,BerghammerStruth2010,BerghammerKargerWolf1998,GondranMinoux2008,HoefnerMoeller2012,Moeller1993}. +The operations of these algebras manipulate entire graphs, which is useful for specification but not directly intended for implementation. +Low-level array access is a key ingredient for efficient algorithms \cite{CormenLeisersonRivest1990}. +We give a relation-algebraic semantics for such read/write access to associative arrays. +This allows us to extend relation-algebraic verification methods to a lower level of more efficient implementations. + +In this theory we focus on arrays with the same index and value sets, which can be modelled as homogeneous relations and therefore as elements of relation algebras and Kleene algebras \cite{Kozen1994,Tarski1941}. +We implement and verify the correctness of disjoint-set forests with path compression and naive union \cite{CormenLeisersonRivest1990,GallerFisher1964,Tarjan1975}. + +In order to prepare this theory for future applications with weighted graphs, the verification uses Stone relation algebras, which have weaker axioms than relation algebras \cite{Guttmann2018c}. + +Section 2 contains the simple relation-algebraic semantics of associative array read and write and basic properties of these access operations. +In Section 3 we give a Kleene-relation-algebraic semantics of disjoint-set forests. +The make-set, find-set and union-sets operations are implemented and verified in Section 4. + +This Isabelle/HOL theory formally verifies results in \cite{Guttmann2020b}. +Theorem numbers from this paper are mentioned in the theory for reference. +See the paper for further details and related work. + +Several Isabelle/HOL theories are related to disjoint sets. +The theory \texttt{HOL/Library/Disjoint\_Sets.thy} contains results about partitions and sets of disjoint sets and does not consider their implementation. +An implementation of disjoint-set forests with path compression and a size-based heuristic in the Imperative/HOL framework is verified in Archive of Formal Proofs entry \cite{LammichMeis2012}. +Improved automation of this proof is considered in Archive of Formal Proofs entry \cite{Zhan2018}. +These approaches are based on logical specifications whereas the present theory uses relation algebras and Kleene algebras. + +\begin{flushleft} +\input{session} +\end{flushleft} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} +