theory Union_Find_Time imports "../../SepLog_Automatic" "../../Refine_Imperative_HOL/Sepref_Additional" Collections.Partial_Equivalence_Relation "HOL-Library.Code_Target_Numeral" "SepLogicTime_RBTreeBasic.Asymptotics_1D" UnionFind_Impl begin notation timeCredit_assn ("$") text {* We implement a simple union-find data-structure based on an array. It uses path compression and a size-based union heuristics. *} subsection {* Abstract Union-Find on Lists *} text {* We first formulate union-find structures on lists, and later implement them using Imperative/HOL. This is a separation of proof concerns between proving the algorithmic idea correct and generating the verification conditions. *} subsubsection {* Representatives *} text {* We define a function that searches for the representative of an element. This function is only partially defined, as it does not terminate on all lists. We use the domain of this function to characterize valid union-find lists. *} function (domintros) rep_of where "rep_of l i = (if l!i = i then i else rep_of l (l!i))" by pat_completeness auto text {* A valid union-find structure only contains valid indexes, and the @{text "rep_of"} function terminates for all indexes. *} definition "ufa_invar l ≡ ∀i<length l. rep_of_dom (l,i) ∧ l!i<length l" lemma ufa_invarD: "⟦ufa_invar l; i<length l⟧ ⟹ rep_of_dom (l,i)" "⟦ufa_invar l; i<length l⟧ ⟹ l!i<length l" unfolding ufa_invar_def by auto text {* We derive the following equations for the @{text "rep-of"} function. *} lemma rep_of_refl: "l!i=i ⟹ rep_of l i = i" apply (subst rep_of.psimps) apply (rule rep_of.domintros) apply (auto) done lemma rep_of_step: "⟦ufa_invar l; i<length l; l!i≠i⟧ ⟹ rep_of l i = rep_of l (l!i)" apply (subst rep_of.psimps) apply (auto dest: ufa_invarD) done lemmas rep_of_simps = rep_of_refl rep_of_step lemma rep_of_iff: "⟦ufa_invar l; i<length l⟧ ⟹ rep_of l i = (if l!i=i then i else rep_of l (l!i))" by (simp add: rep_of_simps) text {* We derive a custom induction rule, that is more suited to our purposes. *} lemma rep_of_induct[case_names base step, consumes 2]: assumes I: "ufa_invar l" assumes L: "i<length l" assumes BASE: "⋀i. ⟦ ufa_invar l; i<length l; l!i=i ⟧ ⟹ P l i" assumes STEP: "⋀i. ⟦ ufa_invar l; i<length l; l!i≠i; P l (l!i) ⟧ ⟹ P l i" shows "P l i" proof - from ufa_invarD[OF I L] have "ufa_invar l ∧ i<length l ⟶ P l i" apply (induct l≡l i rule: rep_of.pinduct) apply (auto intro: STEP BASE dest: ufa_invarD) done thus ?thesis using I L by simp qed text {* In the following, we define various properties of @{text "rep_of"}. *} lemma rep_of_min: "⟦ ufa_invar l; i<length l ⟧ ⟹ l!(rep_of l i) = rep_of l i" proof - have "⟦rep_of_dom (l,i) ⟧ ⟹ l!(rep_of l i) = rep_of l i" apply (induct arbitrary: rule: rep_of.pinduct) apply (subst rep_of.psimps, assumption) apply (subst (2) rep_of.psimps, assumption) apply auto done thus "⟦ ufa_invar l; i<length l ⟧ ⟹ l!(rep_of l i) = rep_of l i" by (metis ufa_invarD(1)) qed lemma rep_of_bound: "⟦ ufa_invar l; i<length l ⟧ ⟹ rep_of l i < length l" apply (induct rule: rep_of_induct) apply (auto simp: rep_of_iff) done lemma rep_of_idem: "⟦ ufa_invar l; i<length l ⟧ ⟹ rep_of l (rep_of l i) = rep_of l i" by (auto simp: rep_of_min rep_of_refl) lemma rep_of_min_upd: "⟦ ufa_invar l; x<length l; i<length l ⟧ ⟹ rep_of (l[rep_of l x := rep_of l x]) i = rep_of l i" by (metis list_update_id rep_of_min) lemma rep_of_idx: "⟦ufa_invar l; i<length l⟧ ⟹ rep_of l (l!i) = rep_of l i" by (metis rep_of_step) subsubsection {* Abstraction to Partial Equivalence Relation *} definition ufa_α :: "nat list ⇒ (nat×nat) set" where "ufa_α l ≡ {(x,y). x<length l ∧ y<length l ∧ rep_of l x = rep_of l y}" lemma ufa_α_equiv[simp, intro!]: "part_equiv (ufa_α l)" apply rule unfolding ufa_α_def apply (rule symI) apply auto apply (rule transI) apply auto done lemma ufa_α_lenD: "(x,y)∈ufa_α l ⟹ x<length l" "(x,y)∈ufa_α l ⟹ y<length l" unfolding ufa_α_def by auto lemma ufa_α_dom[simp]: "Domain (ufa_α l) = {0..<length l}" unfolding ufa_α_def by auto lemma ufa_α_refl[simp]: "(i,i)∈ufa_α l ⟷ i<length l" unfolding ufa_α_def by simp lemma ufa_α_len_eq: assumes "ufa_α l = ufa_α l'" shows "length l = length l'" by (metis assms le_antisym less_not_refl linorder_le_less_linear ufa_α_refl) subsubsection {* Operations *} lemma ufa_init_invar: "ufa_invar [0..<n]" unfolding ufa_invar_def by (auto intro: rep_of.domintros) lemma ufa_init_correct: "ufa_α [0..<n] = {(x,x) | x. x<n}" unfolding ufa_α_def using ufa_init_invar[of n] apply (auto simp: rep_of_refl) done lemma ufa_find_correct: "⟦ufa_invar l; x<length l; y<length l⟧ ⟹ rep_of l x = rep_of l y ⟷ (x,y)∈ufa_α l" unfolding ufa_α_def by auto abbreviation "ufa_union l x y ≡ l[rep_of l x := rep_of l y]" lemma ufa_union_invar: assumes I: "ufa_invar l" assumes L: "x<length l" "y<length l" shows "ufa_invar (ufa_union l x y)" unfolding ufa_invar_def proof (intro allI impI, simp only: length_list_update) fix i assume A: "i<length l" with I have "rep_of_dom (l,i)" by (auto dest: ufa_invarD) have "ufa_union l x y ! i < length l" using I L A apply (cases "i=rep_of l x") apply (auto simp: rep_of_bound dest: ufa_invarD) done moreover have "rep_of_dom (ufa_union l x y, i)" using I A L proof (induct rule: rep_of_induct) case (base i) thus ?case apply - apply (rule rep_of.domintros) apply (cases "i=rep_of l x") apply auto apply (rule rep_of.domintros) apply (auto simp: rep_of_min) done next case (step i) from step.prems `ufa_invar l` `i<length l` `l!i≠i` have [simp]: "ufa_union l x y ! i = l!i" apply (auto simp: rep_of_min rep_of_bound nth_list_update) done from step show ?case apply - apply (rule rep_of.domintros) apply simp done qed ultimately show "rep_of_dom (ufa_union l x y, i) ∧ ufa_union l x y ! i < length l" by blast qed lemma ufa_union_aux: assumes I: "ufa_invar l" assumes L: "x<length l" "y<length l" assumes IL: "i<length l" shows "rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)" using I IL proof (induct rule: rep_of_induct) case (base i) have [simp]: "rep_of l i = i" using `l!i=i` by (simp add: rep_of_refl) note [simp] = `ufa_invar l` `i<length l` show ?case proof (cases) assume A[simp]: "rep_of l x = i" have [simp]: "l[i := rep_of l y] ! i = rep_of l y" by (auto simp: rep_of_bound) show ?thesis proof (cases) assume [simp]: "rep_of l y = i" show ?thesis by (simp add: rep_of_refl) next assume A: "rep_of l y ≠ i" have [simp]: "rep_of (l[i := rep_of l y]) i = rep_of l y" apply (subst rep_of_step[OF ufa_union_invar[OF I L], simplified]) using A apply simp_all apply (subst rep_of_refl[where i="rep_of l y"]) using I L apply (simp_all add: rep_of_min) done show ?thesis by (simp add: rep_of_refl) qed next assume A: "rep_of l x ≠ i" hence "ufa_union l x y ! i = l!i" by (auto) also note `l!i=i` finally have "rep_of (ufa_union l x y) i = i" by (simp add: rep_of_refl) thus ?thesis using A by auto qed next case (step i) note [simp] = I L `i<length l` have "rep_of l x ≠ i" by (metis I L(1) rep_of_min `l!i≠i`) hence [simp]: "ufa_union l x y ! i = l!i" by (auto simp add: nth_list_update rep_of_bound `l!i≠i`) [] have "rep_of (ufa_union l x y) i = rep_of (ufa_union l x y) (l!i)" by (auto simp add: rep_of_iff[OF ufa_union_invar[OF I L]]) also note step.hyps(4) finally show ?case by (auto simp: rep_of_idx) qed lemma ufa_union_correct: "⟦ ufa_invar l; x<length l; y<length l ⟧ ⟹ ufa_α (ufa_union l x y) = per_union (ufa_α l) x y" unfolding ufa_α_def per_union_def by (auto simp: ufa_union_aux split: if_split_asm ) lemma ufa_compress_aux: assumes I: "ufa_invar l" assumes L[simp]: "x<length l" shows "ufa_invar (l[x := rep_of l x])" and "∀i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i" proof - { fix i assume "i<length (l[x := rep_of l x])" hence IL: "i<length l" by simp have G1: "l[x := rep_of l x] ! i < length (l[x := rep_of l x])" using I IL by (auto dest: ufa_invarD[OF I] simp: nth_list_update rep_of_bound) from I IL have G2: "rep_of (l[x := rep_of l x]) i = rep_of l i ∧ rep_of_dom (l[x := rep_of l x], i)" proof (induct rule: rep_of_induct) case (base i) thus ?case apply (cases "x=i") apply (auto intro: rep_of.domintros simp: rep_of_refl) done next case (step i) hence D: "rep_of_dom (l[x := rep_of l x], i)" apply - apply (rule rep_of.domintros) apply (cases "x=i") apply (auto intro: rep_of.domintros simp: rep_of_min) done thus ?case apply simp using step apply - apply (subst rep_of.psimps[OF D]) apply (cases "x=i") apply (auto simp: rep_of_min rep_of_idx) apply (subst rep_of.psimps[where i="rep_of l i"]) apply (auto intro: rep_of.domintros simp: rep_of_min) done qed note G1 G2 } note G=this thus "∀i<length l. rep_of (l[x := rep_of l x]) i = rep_of l i" by auto from G show "ufa_invar (l[x := rep_of l x])" by (auto simp: ufa_invar_def) qed lemma ufa_compress_invar: assumes I: "ufa_invar l" assumes L[simp]: "x<length l" shows "ufa_invar (l[x := rep_of l x])" using assms by (rule ufa_compress_aux) lemma ufa_compress_correct: assumes I: "ufa_invar l" assumes L[simp]: "x<length l" shows "ufa_α (l[x := rep_of l x]) = ufa_α l" by (auto simp: ufa_α_def ufa_compress_aux[OF I]) subsubsection ‹stuff about the height (by Max Haslbeck)› function (domintros) height_of where "height_of l i = (if l!i = i then 0::nat else 1 + height_of l (l!i))" by pat_completeness auto print_theorems lemma height_of_dom_rep_of_dom[simp]: "height_of_dom (l, i) = rep_of_dom (l, i)" apply(rule) subgoal apply (induct arbitrary: rule: height_of.pinduct) apply (rule rep_of.domintros) by simp subgoal apply (induct arbitrary: rule: rep_of.pinduct) apply (rule height_of.domintros) by simp done lemma height_of_step: "ufa_invar l ⟹ i < length l ⟹ l ! i ≠ i ⟹ height_of l i = Suc (height_of l (l ! i))" by (simp add: height_of.psimps ufa_invarD(1)) definition "h_of l i = Max {height_of l j|j. j<length l ∧ rep_of l j = i}" definition invar where "invar l sl = (length l = length sl ∧ sum (λi. if l!i=i then sl !i else 0) {0..<length l} = length l ∧ (∀i<length l. l!i=i ⟶ (2::nat) ^ h_of l i ≤ sl ! i))" lemma invar_sli_le_l: assumes "invar l sl" "ufa_invar l" "i<length l" shows "sl ! (rep_of l i) ≤ length l" proof - from assms(1) have a: "sum (λi. if l!i=i then sl !i else 0) {0..<length l} = length l" and len: "length sl = length l" by(auto simp: invar_def) let ?r = "(rep_of l i)" from assms have "?r<length l" by(auto simp: rep_of_bound) then have f: "{0..<length l} = {?r} ∪ ({0..<length l}-{?r})" by auto have "sl ! (?r) ≤ sum (λi. if l!i=i then sl !i else 0) ({0..<length l}-{?r}) + (if l!?r=?r then sl !?r else 0)" using assms by (auto simp: rep_of_min) also have "… = sum (λi. if l!i=i then sl !i else 0) {0..<length l}" apply(subst (2) f) apply(subst sum_Un_nat) by simp_all also have "… = length l" using a by simp finally show "sl ! (rep_of l i) ≤ length l" . qed lemma h_rep: "ufa_invar l ⟹ y<length l⟹ height_of l (rep_of l y) = 0" apply (subst height_of.psimps) subgoal by (simp add: rep_of_bound ufa_invarD(1) ufa_union_invar ) by (simp add: rep_of_min) lemma ufa_compress_compresses: "⟦ufa_invar l; i<length l; j<length l⟧ ⟹ height_of (l[j:=rep_of l j]) i ≤ height_of l i" proof (induct rule: rep_of_induct) case (base i) then show ?case apply(subst height_of.psimps) subgoal apply simp apply(rule ufa_invarD(1)) by(auto simp add: ufa_compress_invar) apply (auto simp add: rep_of_refl) by (metis nth_list_update' rep_of_iff) next case (step i) show ?case apply(subst height_of.psimps) subgoal using step by (simp add: ufa_invarD(1) ufa_compress_invar ) apply auto apply(subst (2) height_of.psimps) subgoal using step by (simp add: rep_of_bound ufa_invarD(1) ufa_compress_invar ) using step(1-3) apply auto apply(cases "i=j") subgoal apply simp apply(subst height_of.psimps) subgoal by (simp add: rep_of_bound ufa_compress_invar ufa_invarD(1)) using rep_of_min by auto subgoal apply simp apply(rule step(4)) using step by auto done qed lemma ufa_union_on_path_only_increases_by_one: "⟦ufa_invar l; i<length l; x<length l; y<length l; rep_of l i = rep_of l x⟧ ⟹ height_of (ufa_union l x y) i ≤ Suc (height_of l i)" proof (induct rule: rep_of_induct) case (base i) then show ?case apply(cases "i=rep_of l x") subgoal apply(subst height_of.psimps) subgoal by (simp add: ufa_invarD(1) ufa_union_invar ) apply simp apply (auto simp add: )[] apply(subst height_of.psimps) subgoal by (simp add: rep_of_bound ufa_invarD(1) ufa_union_invar) apply (auto simp: h_rep)[] by(simp add: rep_of_min) subgoal apply(subst height_of.psimps) subgoal apply simp by (simp add: ufa_invarD(1) ufa_union_invar) by simp done next case (step i) then have not: "i≠rep_of l x" using rep_of_min by blast show ?case apply(subst height_of.psimps) subgoal using step by (simp add: ufa_invarD(1) ufa_union_invar ) using not apply simp apply(subst (2) height_of.psimps) subgoal using step by (simp add: rep_of_bound ufa_invarD(1) ufa_union_invar ) apply simp apply safe apply(rule step(4)) using step by (auto simp add: rep_of_idx) qed lemma ufa_union_not_on_path_stays: "⟦ufa_invar l; i<length l; x<length l; y<length l; rep_of l i ≠ rep_of l x⟧ ⟹ height_of (ufa_union l x y) i = height_of l i" proof (induct rule: rep_of_induct) case (base i) then show ?case apply(cases "i=rep_of l x") subgoal by (auto simp add: h_rep rep_of_iff) subgoal apply(subst height_of.psimps) subgoal apply simp by (simp add: ufa_invarD(1) ufa_union_invar) apply auto apply(subst height_of.psimps) subgoal apply simp by (simp add: ufa_invarD(1) ufa_union_invar) by simp done next case (step i) then have not: "i≠rep_of l x" using rep_of_min by blast show ?case apply(subst height_of.psimps) subgoal using step by (simp add: ufa_invarD(1) ufa_union_invar ) using not step(1-3) apply auto apply(subst (2) height_of.psimps) subgoal using step by (simp add: rep_of_bound ufa_invarD(1) ufa_union_invar ) apply simp apply(rule step(4)) using step by (auto simp add: rep_of_idx) qed lemma ufa_union_on_path: "⟦ufa_invar l; i<length l; x<length l; y<length l⟧ ⟹ height_of (ufa_union l x y) i ≤ Suc (height_of l i)" proof (induct rule: rep_of_induct) case (base i) then show ?case apply(cases "i=rep_of l x") subgoal apply(subst height_of.psimps) subgoal by (simp add: ufa_invarD(1) ufa_union_invar ) apply (auto simp add: )[] apply(subst height_of.psimps) subgoal by (simp add: rep_of_bound ufa_invarD(1) ufa_union_invar) apply auto[] by(simp add: rep_of_min) subgoal apply(subst height_of.psimps) subgoal apply simp by (simp add: ufa_invarD(1) ufa_union_invar) by simp done next case (step i) then have not: "i≠rep_of l x" using rep_of_min by blast show ?case apply(subst height_of.psimps) subgoal using step by (simp add: ufa_invarD(1) ufa_union_invar ) using not apply simp apply(subst (2) height_of.psimps) subgoal using step by (simp add: rep_of_bound ufa_invarD(1) ufa_union_invar ) apply simp apply safe apply(rule step(4)) using step by auto qed lemma hel: "(⋀x. x∈A ⟹ f x ≤ g x) ⟹ finite A ⟹ MAXIMUM A f ≤ MAXIMUM A g" by (smt Max_ge_iff Max_in finite_imageI imageE image_eqI image_is_empty order_refl) lemma MAXIMUM_mono: "(⋀x. x∈A ⟹ f x ≤ g x) ⟹ finite A ⟹ A = B ⟹ MAXIMUM A f ≤ MAXIMUM B g" using hel by blast lemma MAXIMUM_eq: "(⋀x. x∈A ⟹ f x = g x) ⟹ finite A ⟹ A = B ⟹ MAXIMUM A f = MAXIMUM B g" apply(rule antisym) by (auto intro: MAXIMUM_mono) lemma h_of_alt: "h_of l i = MAXIMUM {j|j. j<length l ∧ rep_of l j = i} (height_of l)" unfolding h_of_def by (simp add: setcompr_eq_image) lemma h_of_compress: "ufa_invar l ⟹ j < length l ⟹ h_of (l[j:=rep_of l j]) i ≤ h_of l i" unfolding h_of_alt apply(rule MAXIMUM_mono) subgoal apply(rule ufa_compress_compresses) by auto by (auto simp add: ufa_compress_aux(2)) lemma h_of_uf_union_untouched: "ufa_invar l ⟹ x < length l ⟹ y < length l ⟹ i < length l ⟹ l!i = i ⟹ i ≠ rep_of l x ⟹ i ≠ rep_of l y ⟹ h_of (ufa_union l x y) i = h_of l i" unfolding h_of_alt apply(rule MAXIMUM_eq) subgoal apply(rule ufa_union_not_on_path_stays) using ufa_union_aux by auto using ufa_union_aux by auto lemma Suc_h_of: assumes a: "i < length l " "rep_of l i = i" shows "Suc (h_of l i) = MAXIMUM {j|j. j<length l ∧ rep_of l j = i} (λj. Suc (height_of l j))" unfolding h_of_alt apply(subst mono_Max_commute[where f=Suc]) subgoal by (simp add: mono_Suc) subgoal by simp subgoal using a by auto by (simp add: image_image) lemma MAXIMUM_Un: "finite A ⟹ finite B ⟹ A ≠ {} ⟹ B ≠ {} ⟹ MAXIMUM (A ∪ B) f = max (MAXIMUM A f) (MAXIMUM B f)" apply(simp add: image_Un) apply(subst Max_Un) by auto lemma fixes A::nat shows "A≤A' ⟹ B≤B' ⟹ max A B ≤ max A' B'" by auto lemma h_of_uf_union_id: assumes "ufa_invar l "" x < length l "" y < length l "" i < length l " " rep_of l i = i" "i = rep_of l y" and neq: "rep_of l y = rep_of l x" shows "h_of (ufa_union l x y) i = h_of l i" using neq apply simp using assms by (metis list_update_id rep_of_min) lemma h_of_uf_union_touched: assumes "ufa_invar l "" x < length l "" y < length l "" i < length l " " rep_of l i = i" "i = rep_of l y" and neq: "rep_of l y ≠ rep_of l x" shows "h_of (ufa_union l x y) i ≤ max (h_of l (rep_of l y)) (Suc (h_of l (rep_of l x)))" proof - have *: "{j|j. j<length (ufa_union l x y) ∧ rep_of (ufa_union l x y) j = i} = {j|j. j<length (ufa_union l x y) ∧ rep_of (ufa_union l x y) j = i ∧ rep_of l j = rep_of l y} ∪ {j|j. j<length (ufa_union l x y) ∧ rep_of (ufa_union l x y) j = i ∧ rep_of l j = rep_of l x}" (is "_ = ?A ∪ ?B") apply auto using assms by (simp add: ufa_union_aux) have A: "?A = {j |j. j < length l ∧ rep_of l j = rep_of l y}" using ufa_union_aux assms by auto have B: "?B = {j |j. j < length l ∧ rep_of l j = rep_of l x}" using ufa_union_aux assms by auto have "h_of (ufa_union l x y) i = MAXIMUM {j|j. j<length (ufa_union l x y) ∧ rep_of (ufa_union l x y) j = i} (height_of (ufa_union l x y))" unfolding h_of_alt by simp also have "… = MAXIMUM (?A ∪ ?B) (height_of (ufa_union l x y))" unfolding * by simp also have "… = max (MAXIMUM ?A (height_of (ufa_union l x y))) (MAXIMUM ?B (height_of (ufa_union l x y)))" apply(subst MAXIMUM_Un) apply simp_all subgoal apply(rule exI[where x=y]) using assms by (simp add: ufa_union_aux) subgoal apply(rule exI[where x=x]) using assms by (simp add: ufa_union_aux) done also have "… ≤ max (MAXIMUM ?A (height_of l)) (MAXIMUM ?B (λj. Suc (height_of l j)))" apply(rule max.mono) subgoal apply(rule MAXIMUM_mono) subgoal apply(rule order_eq_refl) apply(rule ufa_union_not_on_path_stays) using assms by auto by simp_all subgoal apply(rule MAXIMUM_mono) subgoal apply(rule ufa_union_on_path) using assms by auto apply simp by simp done also have "… ≤ max (h_of l (rep_of l y)) (Suc (h_of l (rep_of l x)))" apply(rule max.mono) subgoal unfolding h_of_alt A by simp subgoal apply(subst Suc_h_of) subgoal using assms by (auto simp: rep_of_min rep_of_bound rep_of_refl) subgoal using assms by (auto simp: rep_of_min rep_of_bound rep_of_refl) unfolding B by simp done finally show ?thesis . qed lemma height_of_le_h_of: "i < length l ⟹ height_of l i ≤ h_of l (rep_of l i)" unfolding h_of_def apply(rule Max.coboundedI) apply simp apply(subst setcompr_eq_image) apply(rule imageI) by auto lemma height_of_ub: assumes "invar l sl" "ufa_invar l" "i<length l" shows "2 ^ (height_of l i) ≤ length l" proof - from assms(1) have "length l = length sl " and 2: "sum (λi. if l!i=i then sl !i else 0) {0..<length l} = length l" and 3: "⋀i. i<length l ⟹ l!i=i ⟹ (2::nat) ^ h_of l i ≤ sl ! i" unfolding invar_def by auto have *: "height_of l i ≤ h_of l (rep_of l i)" using assms by (auto intro: height_of_le_h_of) have "(2::nat) ^ (height_of l i) ≤ 2 ^ (h_of l (rep_of l i))" apply(rule power_increasing) apply(rule *) by simp also have "… ≤ sl ! (rep_of l i)" using 3 assms by(auto simp add: rep_of_bound rep_of_min ) also have "… ≤ length l" using assms by (auto simp: rep_of_bound intro: invar_sli_le_l) finally show ?thesis . qed subsection {* Implementation with Imperative/HOL *} text {* In this section, we implement the union-find data-structure with two arrays, one holding the next-pointers, and another one holding the size information. Note that we do not prove that the array for the size information contains any reasonable values, as the correctness of the algorithm is not affected by this. We leave it future work to also estimate the complexity of the algorithm. *} type_synonym uf = "nat array × nat array" definition is_uf :: "(nat×nat) set ⇒ uf ⇒ assn" where "is_uf R u ≡ case u of (s,p) ⇒ ∃⇩Al szl. p↦⇩al * s↦⇩aszl * ↑(ufa_invar l ∧ ufa_α l = R ∧ length szl = length l ∧ invar l szl)" definition uf_init :: "nat ⇒ uf Heap" where "uf_init n ≡ do { l ← Array.of_list [0..<n]; szl ← Array.new n (1::nat); return (szl,l) }" lemma of_list_rule': "<$ (1 + n)> Array.of_list [0..<n] <λr. r ↦⇩a [0..<n]>" using of_list_rule[of "[0..<n]"] by auto lemma height_of_init: "j<n ⟹ height_of [0..<n] j = 0" by (simp add: height_of.psimps ufa_init_invar ufa_invarD(1)) lemma h_of_init: "i < n ⟹ h_of [0..<n] i = 0" unfolding h_of_def apply auto apply(rule antisym) subgoal apply(rule Max.boundedI) apply simp using ufa_init_invar apply auto apply(rule exI[where x=i]) apply simp subgoal by (simp add: rep_of_refl) apply(rule height_of_init) by simp by simp lemma ufa_init_invar': "invar [0..<n] (replicate n (Suc 0))" unfolding invar_def apply auto using h_of_init by auto definition uf_init_time :: "nat ⇒ nat" where "uf_init_time n == (2*n+3)" lemma uf_init_bound[asym_bound]: "uf_init_time ∈ Θ(λn. n)" unfolding uf_init_time_def by auto2 lemma uf_init_rule: "<$(uf_init_time n)> uf_init n <is_uf {(i,i) |i. i<n}>⇩t" unfolding uf_init_time_def uf_init_def is_uf_def[abs_def] by (sep_auto simp: ufa_init_correct ufa_init_invar ufa_init_invar' zero_time heap: of_list_rule') partial_function (heap) uf_rep_of :: "nat array ⇒ nat ⇒ nat Heap" where [code]: "uf_rep_of p i = do { n ← Array.nth p i; if n=i then return i else uf_rep_of p n }" lemma uf_rep_of_rule: "⟦ufa_invar l; i<length l⟧ ⟹ <p↦⇩al * $(height_of l i + 2)> uf_rep_of p i <λr. p↦⇩al * ↑(r=rep_of l i)>⇩t" apply (induct rule: rep_of_induct) apply (subst uf_rep_of.simps) apply (sep_auto simp: rep_of_refl) apply (subst uf_rep_of.simps) apply (sep_auto simp: rep_of_step height_of_step) done text {* We chose a non tail-recursive version here, as it is easier to prove. *} partial_function (heap) uf_compress :: "nat ⇒ nat ⇒ nat array ⇒ unit Heap" where [code]: "uf_compress i ci p = ( if i=ci then return () else do { ni←Array.nth p i; uf_compress ni ci p; Array.upd i ci p; return () })" lemma compress_invar: assumes "invar l szl" "ufa_invar l" "i<length l" shows "invar (l[i := rep_of l i]) szl" using assms unfolding invar_def apply safe subgoal by simp subgoal apply simp by (smt nth_list_update_eq nth_list_update_neq rep_of_iff rep_of_min sum.ivl_cong) subgoal for i apply(rule order.trans) apply(rule power_increasing[where N="h_of l i"]) subgoal apply(rule h_of_compress) by auto apply simp apply simp by (metis nth_list_update_eq nth_list_update_neq rep_of_min) done lemma uf_compress_rule: "⟦ ufa_invar l; i<length l; ci=rep_of l i; invar l szl ⟧ ⟹ <p↦⇩al * $(1+height_of l i*3)> uf_compress i ci p <λ_. (∃⇩Al'. p↦⇩al' * ↑(invar l' szl ∧ ufa_invar l' ∧ length l' = length l ∧ (∀i<length l. rep_of l' i = rep_of l i)))>⇩t" proof (induction rule: rep_of_induct) case (base i) thus ?case apply (subst uf_compress.simps) apply (sep_auto simp: rep_of_refl) done next case (step i) note SS = `ufa_invar l` `i<length l` `l!i≠i` `ci = rep_of l i` `invar l szl` have IH': "<p ↦⇩a l * $ (1 + height_of l (l ! i) *3)> uf_compress (l ! i) (rep_of l i) p <λ_. (∃⇩Al'. p ↦⇩a l' * ↑ (invar l' szl ∧ufa_invar l' ∧ length l' = length l ∧ (∀i<length l'. rep_of l i = rep_of l' i))) >⇩t" apply(rule pre_rule[OF _ post_rule[OF step.IH[simplified SS rep_of_idx] ]] ) by (sep_auto simp add: rep_of_idx SS)+ show ?case apply (subst uf_compress.simps) apply (sep_auto simp: SS height_of_step heap: ) apply(sep_auto heap: IH') using SS apply (sep_auto ) subgoal using compress_invar by simp subgoal using ufa_compress_invar by fastforce subgoal by simp subgoal using ufa_compress_aux(2) by fastforce done qed definition uf_rep_of_c :: "nat array ⇒ nat ⇒ nat Heap" where "uf_rep_of_c p i ≡ do { ci←uf_rep_of p i; uf_compress i ci p; return ci }" lemma uf_rep_of_c_rule: "⟦ufa_invar l; i<length l; invar l szl⟧ ⟹ <p↦⇩al * $(4+height_of l i*4)> uf_rep_of_c p i <λr. (∃⇩Al'. p↦⇩al' * ↑(r=rep_of l i ∧ ufa_invar l' ∧ invar l' szl ∧ length l' = length l ∧ (∀i<length l. rep_of l' i = rep_of l i)))>⇩t" unfolding uf_rep_of_c_def by (sep_auto heap: uf_compress_rule uf_rep_of_rule) thm height_of_ub definition height_ub :: "nat ⇒ nat" where "height_ub n = nat (ceiling (log 2 n))" lemma height_ub_bound[asym_bound]: "height_ub ∈ Θ(λn. ln n)" unfolding height_ub_def using abcd_lnx[of 0 1 1 0] by auto lemma height_ub: assumes "invar l sl" "ufa_invar l" "i<length l" shows "height_of l i ≤ height_ub (length l)" proof - from height_of_ub[OF assms] have "2 ^ height_of l i ≤ length l" . from le_log2_of_power[OF this] show ?thesis unfolding height_ub_def by linarith qed lemma uf_rep_of_c_rule_ub: assumes "ufa_invar l" "i<length l" "invar l szl" shows "<p↦⇩al * $(4+ height_ub (length l)*4)> uf_rep_of_c p i <λr. (∃⇩Al'. p↦⇩al' * ↑(r=rep_of l i ∧ ufa_invar l' ∧ invar l' szl ∧ length l' = length l ∧ (∀i<length l. rep_of l' i = rep_of l i))) >⇩t" proof - from assms height_ub have "height_of l i ≤ height_ub (length l)" by auto then obtain x where p: "height_ub (length l) = height_of l i + x" using le_Suc_ex by blast show ?thesis unfolding p using assms by(sep_auto heap: uf_rep_of_c_rule) qed definition uf_cmp :: "uf ⇒ nat ⇒ nat ⇒ bool Heap" where "uf_cmp u i j ≡ do { let (s,p)=u; n←Array.len p; if (i≥n ∨ j≥n) then return False else do { ci←uf_rep_of_c p i; cj←uf_rep_of_c p j; return (ci=cj) } }" lemma cnv_to_ufa_α_eq: "⟦(∀i<length l. rep_of l' i = rep_of l i); length l = length l'⟧ ⟹ (ufa_α l = ufa_α l')" unfolding ufa_α_def by auto lemma " card (Domain (ufa_α l)) = length l" by simp definition uf_cmp_time :: "nat ⇒ nat" where "uf_cmp_time n = 10+ height_ub n*8" lemma uf_cmp_time_bound[asym_bound]: "uf_cmp_time ∈ Θ(λn. ln n)" unfolding uf_cmp_time_def by auto2 lemma uf_cmp_rule: "<is_uf R u * $(uf_cmp_time (card (Domain R)))> uf_cmp u i j <λr. is_uf R u * ↑(r⟷(i,j)∈R)>⇩t" unfolding uf_cmp_def is_uf_def uf_cmp_time_def apply (sep_auto heap: uf_rep_of_c_rule_ub length_rule dest: ufa_α_lenD simp: not_le split: prod.split) apply(rule fi_rule[OF uf_rep_of_c_rule_ub]) defer defer defer apply(simp only: mult.assoc) apply(rule match_first) apply sep_auto apply(timeframeinf) defer apply simp apply simp apply simp apply(sep_auto) apply (drule cnv_to_ufa_α_eq, simp_all) apply (drule cnv_to_ufa_α_eq, simp_all) apply (drule cnv_to_ufa_α_eq, simp_all) apply (drule cnv_to_ufa_α_eq, simp_all) apply (drule cnv_to_ufa_α_eq, simp_all) apply (drule cnv_to_ufa_α_eq, simp_all) apply (subst ufa_find_correct) apply (auto simp add: ) done definition uf_union :: "uf ⇒ nat ⇒ nat ⇒ uf Heap" where "uf_union u i j ≡ do { let (s,p)=u; ci ← uf_rep_of p i; cj ← uf_rep_of p j; if (ci=cj) then return (s,p) else do { si ← Array.nth s ci; sj ← Array.nth s cj; if si<sj then do { Array.upd ci cj p; Array.upd cj (si+sj) s; return (s,p) } else do { Array.upd cj ci p; Array.upd ci (si+sj) s; return (s,p) } } }" lemma uf_rep_of_rule_ub: assumes "ufa_invar l" "i<length l" "invar l szl" shows "<p↦⇩al * $(height_ub (length l) + 2)> uf_rep_of p i <λr. p↦⇩al * ↑(r=rep_of l i)>⇩t" proof - from assms height_ub have "height_of l i ≤ height_ub (length l)" by auto then obtain x where p: "height_ub (length l) = height_of l i + x" using le_Suc_ex by blast show ?thesis unfolding p using assms by(sep_auto heap: uf_rep_of_rule) qed lemma 12: assumes "i < length l " "j < length l" "ufa_invar l " "(i, j) ∉ ufa_α l " and size: "szl ! rep_of l i < szl ! rep_of l j " and i: "invar l szl " shows "invar (ufa_union l i j) (szl[rep_of l j := szl ! rep_of l i + szl ! rep_of l j])" proof - let ?upd = "ufa_union l i j" from i have [simp]: "length szl = length l" unfolding invar_def by auto { fix a b and f :: "'a⇒nat" have r: "a≠b ⟹ sum f {a,b} = f a + f b" by simp } note ff=this have *: "{0..<length l} = ({0..<length l}-{rep_of l j}) ∪ {rep_of l j}" using assms rep_of_bound by auto have **:"{0..<length l} = ({0..<length l}-{rep_of l i,rep_of l j}) ∪ {rep_of l i,rep_of l j}" using assms rep_of_bound by auto have ss: "(({0..<length l} - {rep_of l j}) ∩ {ia. ?upd ! ia = ia}) = ({0..<length l}-{rep_of l i,rep_of l j}) ∩ {ia. l ! ia = ia}" using assms by (auto simp: nth_list_update') have "(∑ia = 0..<length l. if ?upd ! ia = ia then szl[rep_of l j := szl ! rep_of l i + szl ! rep_of l j] ! ia else 0) = sum (λia. if ?upd ! ia = ia then szl[rep_of l j := szl ! rep_of l i + szl ! rep_of l j] ! ia else 0) ({0..<length l}-{rep_of l j}) + (szl ! rep_of l i + szl ! rep_of l j)" (is "?A = _") apply(subst *) apply(subst sum_Un_nat) apply simp apply simp apply simp apply safe subgoal using assms rep_of_bound using invar_def by fastforce subgoal using assms by (simp add: rep_of_min ufa_find_correct) subgoal using assms by (simp add: rep_of_min ufa_find_correct) done also have "… = sum (λi. if l ! i = i then szl ! i else 0) ({0..<length l}-{rep_of l i,rep_of l j}) + (szl ! rep_of l i + szl ! rep_of l j)" (is "?L + _ = ?R + _") proof - have "?L = sum (λia. szl[rep_of l j := szl ! rep_of l i + szl ! rep_of l j] ! ia) (({0..<length l}-{rep_of l j})∩{ia. ?upd ! ia = ia})" apply(subst sum.inter_restrict) by simp_all also have "… = sum (λia. szl[rep_of l j := szl ! rep_of l i + szl ! rep_of l j] ! ia) (({0..<length l}-{rep_of l i,rep_of l j}) ∩ {ia. l ! ia = ia})" unfolding ss by simp also have "… = ?R" apply(subst sum.inter_restrict) apply simp apply auto apply(rule sum.cong) apply simp using assms by auto finally have "?L = ?R" . then show ?thesis by simp qed also have "… = (∑i = 0..<length l. if l ! i = i then szl ! i else 0)" apply(subst (2) **) apply(subst sum_Un_nat) apply simp apply simp apply simp apply(subst ff) using assms apply (auto simp: rep_of_min) done also from i have "… = length l" unfolding invar_def by auto finally have A: "?A = length l" . have max_distrib: "⋀a b :: nat. (2::nat) ^ max a b = max (2 ^ a) (2 ^ b)" by (simp add: max_def) { assume a: "rep_of l j < length szl" "?upd ! rep_of l j = rep_of l j" from i have g: "⋀i. i<length l ⟹ l ! i = i ⟹ 2 ^ h_of l i ≤ szl ! i" unfolding invar_def by metis have "(2::nat) ^ (max (h_of l (rep_of l j)) (Suc (h_of l (rep_of l i)))) ≤ max ( (szl ! (rep_of l j))) (2 * (szl ! (rep_of l i)))" apply(subst max_distrib) apply(rule max.mono) subgoal apply(rule g) using assms a by (auto simp: rep_of_min) subgoal apply(simp only: power.power_Suc) apply(rule mult_left_mono) apply(rule g) using assms a by (auto simp: rep_of_refl rep_of_min rep_of_bound) done also have "… ≤ szl ! rep_of l i + szl ! rep_of l j" using size by auto finally have "2 ^ max (h_of l (rep_of l j)) (Suc (h_of l (rep_of l i))) ≤ szl ! rep_of l i + szl ! rep_of l j" . } note absch = this show ?thesis unfolding invar_def apply safe subgoal using i[unfolded invar_def] by simp subgoal apply simp using A by simp subgoal for i apply(cases "i=rep_of l j") subgoal apply simp apply(rule order.trans) apply(rule power_increasing[OF h_of_uf_union_touched]) prefer 9 subgoal using absch by simp using assms by (auto simp: rep_of_idem) subgoal apply simp apply(subst h_of_uf_union_untouched) prefer 8 subgoal using i unfolding invar_def by (metis nth_list_update') using assms apply (auto simp: rep_of_idem ) by (metis nth_list_update') done done qed lemma 21: assumes "i < length l "" j < length l "" ufa_invar l " "(i, j) ∉ ufa_α l " and size: "¬ szl ! rep_of l i < szl ! rep_of l j " and i: "invar l szl " shows "invar (ufa_union l j i) (szl[rep_of l i := szl ! rep_of l i + szl ! rep_of l j])" proof - let ?upd = "ufa_union l j i" from i have [simp]: "length szl = length l" unfolding invar_def by auto { fix a b and f :: "'a⇒nat" have r: "a≠b ⟹ sum f {a,b} = f a + f b" by simp } note ff=this have *: "{0..<length l} = ({0..<length l}-{rep_of l i}) ∪ {rep_of l i}" using assms rep_of_bound by auto have **:"{0..<length l} = ({0..<length l}-{rep_of l i,rep_of l j}) ∪ {rep_of l i,rep_of l j}" using assms rep_of_bound by auto have ss: "(({0..<length l} - {rep_of l i}) ∩ {ia. ?upd ! ia = ia}) = ({0..<length l}-{rep_of l i,rep_of l j}) ∩ {ia. l ! ia = ia}" using assms by (auto simp: nth_list_update') have "(∑ia = 0..<length l. if ?upd ! ia = ia then szl[rep_of l i := szl ! rep_of l i + szl ! rep_of l j] ! ia else 0) = sum (λia. if ?upd ! ia = ia then szl[rep_of l i := szl ! rep_of l i + szl ! rep_of l j] ! ia else 0) ({0..<length l}-{rep_of l i}) + (szl ! rep_of l i + szl ! rep_of l j)" (is "?A = _") apply(subst *) apply(subst sum_Un_nat) apply simp apply simp apply simp apply safe subgoal using assms rep_of_bound using invar_def by fastforce subgoal using assms using rep_of_min ufa_find_correct by fastforce subgoal using assms using rep_of_min ufa_find_correct by fastforce done also have "… = sum (λi. if l ! i = i then szl ! i else 0) ({0..<length l}-{rep_of l i,rep_of l j}) + (szl ! rep_of l i + szl ! rep_of l j)" (is "?L + _ = ?R + _") proof - have "?L = sum (λia. szl[rep_of l i := szl ! rep_of l i + szl ! rep_of l j] ! ia) (({0..<length l}-{rep_of l i})∩{ia. ?upd ! ia = ia})" apply(subst sum.inter_restrict) by simp_all also have "… = sum (λia. szl[rep_of l i := szl ! rep_of l i + szl ! rep_of l j] ! ia) (({0..<length l}-{rep_of l i,rep_of l j}) ∩ {ia. l ! ia = ia})" unfolding ss by simp also have "… = ?R" apply(subst sum.inter_restrict) apply simp apply auto apply(rule sum.cong) apply simp using assms by auto finally have "?L = ?R" . then show ?thesis by simp qed also have "… = (∑i = 0..<length l. if l ! i = i then szl ! i else 0)" apply(subst (2) **) apply(subst sum_Un_nat) apply simp apply simp apply simp apply(subst ff) using assms apply (auto simp: rep_of_min) using ufa_find_correct by blast also from i have "… = length l" unfolding invar_def by auto finally have A: "?A = length l" . have max_distrib: "⋀a b :: nat. (2::nat) ^ max a b = max (2 ^ a) (2 ^ b)" by (simp add: max_def) { assume a: "rep_of l i < length szl" "?upd ! rep_of l i = rep_of l i" from i have g: "⋀i. i<length l ⟹ l ! i = i ⟹ 2 ^ h_of l i ≤ szl ! i" unfolding invar_def by metis have "(2::nat) ^ (max (h_of l (rep_of l i)) (Suc (h_of l (rep_of l j)))) ≤ max ( (szl ! (rep_of l i))) (2 * (szl ! (rep_of l j)))" apply(subst max_distrib) apply(rule max.mono) subgoal apply(rule g) using assms a by (auto simp: rep_of_min) subgoal apply(simp only: power.power_Suc) apply(rule mult_left_mono) apply(rule g) using assms a by (auto simp: rep_of_refl rep_of_min rep_of_bound) done also have "… ≤ szl ! rep_of l i + szl ! rep_of l j" using size by auto finally have "2 ^ max (h_of l (rep_of l i)) (Suc (h_of l (rep_of l j))) ≤ szl ! rep_of l i + szl ! rep_of l j" . } note absch = this show ?thesis unfolding invar_def apply safe subgoal using i[unfolded invar_def] by simp subgoal apply simp using A by simp subgoal for e apply(cases "e=rep_of l i") subgoal apply simp apply(rule order.trans) apply(rule power_increasing[OF h_of_uf_union_touched]) prefer 9 subgoal using absch by simp using assms by (auto simp: rep_of_idem ufa_find_correct) subgoal apply simp apply(subst h_of_uf_union_untouched) prefer 8 subgoal using i unfolding invar_def by (metis nth_list_update') using assms apply (auto simp: rep_of_idem ) by (metis nth_list_update') done done qed lemma uf_union_rule': "⟦i∈Domain R; j∈ Domain R⟧ ⟹ <is_uf R u * $(11+ height_ub (card (Domain R))*2)> uf_union u i j <is_uf (per_union R i j)>⇩t" unfolding uf_union_def apply (cases u) apply (simp add: is_uf_def[abs_def]) apply(sep_auto heap: uf_rep_of_rule_ub) apply(simp add: ufa_α_lenD) apply simp apply(sep_auto heap: uf_rep_of_rule_ub) apply(simp add: ufa_α_lenD) apply simp apply (sep_auto simp: per_union_cmp ufa_α_lenD ufa_find_correct rep_of_bound ufa_union_invar ufa_union_correct ) subgoal apply(drule ufa_α_lenD) apply(drule ufa_α_lenD) using 12 by blast apply (sep_auto simp: per_union_cmp ufa_α_lenD ufa_find_correct rep_of_bound ufa_union_invar ufa_union_correct ) subgoal apply(drule ufa_α_lenD) apply(drule ufa_α_lenD) using 21 by blast done definition "uf_union_time n = 11+ height_ub n*2" lemma uf_union_time_bound[asym_bound]: "uf_union_time ∈ Θ(λn. ln n)" unfolding uf_union_time_def by auto2 lemma uf_union_rule: "⟦i∈Domain R; j∈ Domain R⟧ ⟹ <is_uf R u * $(uf_union_time (card (Domain R)))> uf_union u i j <is_uf (per_union R i j)>⇩t" unfolding uf_union_time_def using uf_union_rule' by auto interpretation UnionFind_Impl is_uf uf_init uf_init_time uf_cmp uf_cmp_time uf_union uf_union_time proof (unfold_locales, goal_cases) case (1 t x' x) show ?case unfolding PR_CONST_def mop_per_init_def apply simp apply(rule extract_cost_otherway'[OF _ uf_init_rule, where Cost_lb="uf_init_time x"]) apply (sep_auto simp: per_init'_def hn_ctxt_def pure_def)+ using 1 by simp next case (2 t R' R a' a b' b) show ?case unfolding PR_CONST_def mop_per_compare_def apply simp apply(rule extract_cost_otherway'[OF _ uf_cmp_rule, where Cost_lb="(uf_cmp_time (card (Domain R')))"]) apply (sep_auto simp: per_init'_def hn_ctxt_def pure_def)+ using 2 by simp next case (3 t R' R a' a b' b) show ?case unfolding PR_CONST_def mop_per_union_def apply simp apply(rule extract_cost_otherway'[OF _ uf_union_rule, where Cost_lb="(uf_union_time (card (Domain R')))"]) apply (sep_auto simp: per_init'_def hn_ctxt_def pure_def)+ subgoal using 3 by simp apply (sep_auto simp: per_init'_def hn_ctxt_def pure_def)+ subgoal using 3 by simp apply (sep_auto simp: per_init'_def hn_ctxt_def pure_def invalid_assn_def)+ using 3 by simp qed end