# Theory PQ_Implementation

Up to index of Isabelle/HOL/Binomial-Queues

theory PQ_Implementation
imports Binomial_Queue
(* Authors:  René Neumann and Florian Haftmann, TU Muenchen *)header {* Relating Functional Binomial Queues To The Abstract Priority Queues *}theory PQ_Implementationimports PQ Binomial_Queue beginnotation  "PQ.values" ("|(_)|")  and "PQ.priorities" ("\<parallel>(_)\<parallel>")text {*  \noindent Naming convention: prefix @{text "bt_"} for bintrees, @{text "bts_"} for bintree lists,  no prefix for binqueues.*}primrec bt_dfs :: "(('a::linorder, 'b) bintree => 'c) => ('a, 'b) bintree => 'c list"  and bts_dfs :: "(('a::linorder, 'b) bintree => 'c) => ('a, 'b) bintree list  => 'c list" where  "bt_dfs f (Node a v ts) = f (Node a v ts) # bts_dfs f ts"| "bts_dfs f [] = []"| "bts_dfs f (t # ts) = bt_dfs f t @ bts_dfs f ts"lemma bt_dfs_simp:  "bt_dfs f t = f t # bts_dfs f (children t)"  by (cases t) simp_alllemma bts_dfs_append [simp]:  "bts_dfs f (ts @ rs) = bts_dfs f ts @ bts_dfs f rs"  by (induct ts) simp_alllemma set_bts_dfs_rev:  "set (bts_dfs f (rev ts)) = set (bts_dfs f ts)"  by (induct ts) autolemma bts_dfs_rev_distinct:  "distinct (bts_dfs f ts) ==> distinct (bts_dfs f (rev ts))"  by (induct ts) (auto simp add: set_bts_dfs_rev)lemma bt_dfs_comp:  "bt_dfs (f o g) t = map f (bt_dfs g t)"  "bts_dfs (f o g) ts = map f (bts_dfs g ts)"  by (induct t and ts) simp_alllemma bt_dfs_comp_distinct:  "distinct (bt_dfs (f o g) t) ==> distinct (bt_dfs g t)"  "distinct (bts_dfs (f o g) ts) ==> distinct (bts_dfs g ts)"  by (simp_all add: bt_dfs_comp distinct_map [of f])lemma bt_dfs_distinct_children:  "distinct (bt_dfs f x) ==> distinct (bts_dfs f (children x))"  by (cases x) simpfun dfs :: "(('a::linorder, 'b) bintree => 'c) => ('a, 'b) binqueue => 'c list" where  "dfs f [] = []"| "dfs f (None # xs) = dfs f xs"| "dfs f (Some t # xs) = bt_dfs f t @ dfs f xs"lemma dfs_append:  "dfs f (xs @ ys) = (dfs f xs) @ (dfs f ys)"  by (induct xs) simp_alllemma set_dfs_rev:  "set (dfs f (rev xs)) = set (dfs f xs)"  by (induct xs) (auto simp add: dfs_append)lemma set_dfs_Cons:  "set (dfs f (x # xs)) = set (dfs f xs) ∪ set (dfs f [x])"proof -  have "set (dfs f (x # xs)) = set (dfs f (rev xs @ [x]))"    using set_dfs_rev[of f "rev xs @ [x]"] by simp  thus ?thesis by (simp add: dfs_append set_dfs_rev)qedlemma dfs_comp:  "dfs (f o g) xs = map f (dfs g xs)"  by (induct xs) (simp_all add: bt_dfs_comp del: o_apply)lemma dfs_comp_distinct:  "distinct (dfs (f o g) xs) ==> distinct (dfs g xs)"  by (simp add: dfs_comp distinct_map[of f])lemma dfs_distinct_member:  "distinct (dfs f xs) ==>    Some x ∈ set xs ==>    distinct (bt_dfs f x)"proof (induct xs arbitrary: x)  case (Some r xs t) then show ?case by (cases "t = r") simp_allqed simp_alllemma dfs_map_Some_idem:  "dfs f (map Some xs) = bts_dfs f xs"  by (induct xs) simp_allprimrec alist :: "('a, 'b) bintree => ('b × 'a)" where  "alist (Node a v _) = (v, a)"lemma alist_split_pre:  "val t = (fst o alist) t"  "priority t = (snd o alist) t"  by (cases t, simp)+lemma alist_split:  "val = fst o alist"  "priority = snd o alist"  by (auto intro!: ext simp add: alist_split_pre)lemma alist_split_set:  "set (dfs val xs) = fst  set (dfs alist xs)"  "set (dfs priority xs) = snd  set (dfs alist xs)"  by (auto simp add: dfs_comp alist_split)lemma in_set_in_alist:  assumes "Some t ∈ set xs"  shows "(val t, priority t) ∈ set (dfs alist xs)"using assmsproof (induct xs)  case (Some x xs) then show ?case  proof (cases "Some t ∈ set xs")    case False with Some show ?thesis by (cases t) (auto simp add: bt_dfs_simp)  qed simpqed simp_allabbreviation vals where "vals ≡ dfs val"abbreviation prios where "prios ≡ dfs priority"abbreviation elements where "elements ≡ dfs alist"primrec  bt_augment :: "('a::linorder, 'b) bintree => ('b, 'a) PQ.pq => ('b, 'a) PQ.pq"and  bts_augment :: "('a::linorder, 'b) bintree list => ('b, 'a) PQ.pq => ('b, 'a) PQ.pq"where  "bt_augment (Node a v ts) q = PQ.push v a (bts_augment ts q)"| "bts_augment [] q = q"| "bts_augment (t # ts) q = bts_augment ts (bt_augment t q)"lemma bts_augment [simp]:  "bts_augment = fold bt_augment"proof (rule ext)  fix ts :: "('a, 'b) bintree list"  show "bts_augment ts = fold bt_augment ts"    by (induct ts) simp_allqedlemma bt_augment_Node [simp]:  "bt_augment (Node a v ts) q = PQ.push v a (fold bt_augment ts q)"  by (simp add: bts_augment)lemma bt_augment_simp:  "bt_augment t q = PQ.push (val t) (priority t) (fold bt_augment (children t) q)"  by (cases t) (simp_all add: bts_augment)declare bt_augment_bts_augment.simps [simp del]fun pqueue :: "('a::linorder, 'b) binqueue => ('b, 'a) PQ.pq" where  Empty: "pqueue [] = PQ.empty"| None: "pqueue (None # xs) = pqueue xs"| Some: "pqueue (Some t # xs) = bt_augment t (pqueue xs)"lemma bt_augment_v_subset:  "set |q| ⊆ set |bt_augment t q|"  "set |q| ⊆ set |bts_augment ts q|"  by (induct t and ts arbitrary: q and q) autolemma bt_augment_v_in:  "v ∈ set |q| ==> v ∈ set |bt_augment t q|"  "v ∈ set |q| ==> v ∈ set |bts_augment ts q|"  using bt_augment_v_subset[of q] by autolemma bt_augment_v_union:  "set |bt_augment t (bt_augment r q)| =    set |bt_augment t q| ∪ set |bt_augment r q|"  "set |bts_augment ts (bt_augment r q)| =    set |bts_augment ts q| ∪ set |bt_augment r q|"proof (induct t and ts arbitrary: q r and q r)  case Nil_bintree    from bt_augment_v_subset[of q] show ?case by autoqed autolemma bt_val_augment:  shows "set (bt_dfs val t) ∪ set |q| = set |bt_augment t q|"  and   "set (bts_dfs val ts) ∪ set |q| = set |bts_augment ts q|"proof (induct t and ts)  case (Cons_bintree r rs)  have "set |bts_augment rs (bt_augment r q)| =    set |bts_augment rs q| ∪ set |bt_augment r q|"     by (simp only: bt_augment_v_union)    with bt_augment_v_subset[of q]    have "set |bts_augment rs (bt_augment r q)| =      set |bts_augment rs q| ∪ set |bt_augment r q| ∪ set |q|"     by auto  with Cons_bintree show ?case by autoqed autolemma vals_pqueue:  "set (vals xs) = set |pqueue xs|"  by (induct xs) (simp_all add: bt_val_augment)lemma bt_augment_v_push:  "set |bt_augment t (PQ.push v a q)| = set |bt_augment t q| ∪ {v}"  "set |bts_augment ts (PQ.push v a q)| = set |bts_augment ts q| ∪ {v}"  using bt_val_augment[where q = "PQ.push v a q"] by (simp_all add: bt_val_augment)lemma bt_augment_v_push_commute:  "set |bt_augment t (PQ.push v a q)| = set |PQ.push v a (bt_augment t q)|"  "set |bts_augment ts (PQ.push v a q)| = set |PQ.push v a (bts_augment ts q)|"  by (simp_all add: bt_augment_v_push del: bts_augment)lemma bts_augment_v_union:  "set |bt_augment t (bts_augment rs q)| =    set |bt_augment t q| ∪ set |bts_augment rs q|"  "set |bts_augment ts (bts_augment rs q)| =    set |bts_augment ts q| ∪ set |bts_augment rs q|"proof (induct t and ts arbitrary: q rs and q rs)  case Nil_bintree  from bt_augment_v_subset[of q] show ?case by auto  next   case (Cons_bintree x xs)  let ?L = "set |bts_augment xs (bt_augment x (bts_augment rs q))|"    from bt_augment_v_union    have *: "!! q. set |bts_augment xs (bt_augment x q)| =      set |bts_augment xs q| ∪ set |bt_augment x q|" by simp    with Cons_bintree    have "?L =      set |bts_augment xs q| ∪ set |bts_augment rs q| ∪ set |bt_augment x q|"      by auto  with * show ?case by autoqed simplemma bt_augment_v_commute:  "set |bt_augment t (bt_augment r q)| = set |bt_augment r (bt_augment t q)|"  "set |bt_augment t (bts_augment rs q)| = set |bts_augment rs (bt_augment t q)|"  "set |bts_augment ts (bts_augment rs q)| =    set |bts_augment rs (bts_augment ts q)|"  unfolding bts_augment_v_union bt_augment_v_union by auto  lemma bt_augment_v_merge:  "set |bt_augment (merge t r) q| = set |bt_augment t (bt_augment r q)|"  by (simp add: bt_augment_simp [symmetric] bt_augment_v_push    bt_augment_v_commute merge_def)lemma vals_merge [simp]:  "set (bt_dfs val (merge t r)) = set (bt_dfs val t) ∪ set (bt_dfs val r)"  by (auto simp add: bt_dfs_simp merge_def)lemma vals_merge_distinct:  "distinct (bt_dfs val t) ==> distinct (bt_dfs val r) ==>   set (bt_dfs val t) ∩ set (bt_dfs val r) = {} ==>    distinct (bt_dfs val (merge t r))"  by (auto simp add: bt_dfs_simp merge_def)lemma vals_add_Cons:  "set (vals (add x xs)) = set (vals (x # xs))"proof (cases x)  case (Some t) then show ?thesis    by (induct xs arbitrary: x t) autoqed simplemma vals_add_distinct:  assumes "distinct (vals xs)"  and "distinct (dfs val [x])"  and "set (vals xs) ∩ set (dfs val [x]) = {}"  shows "distinct (vals (add x xs))"using assmsproof (cases x)  case (Some t) with assms show ?thesis  proof (induct xs arbitrary: x t)    case (Some r xs)    then have "set (bt_dfs val t) ∩ set (bt_dfs val r) = {}" by auto    with Some have "distinct (bt_dfs val (merge t r))" by (simp add: vals_merge_distinct)    moreover    with Some have "set (vals xs) ∩ set (bt_dfs val (merge t r)) = {}" by auto    moreover note Some    ultimately show ?case by simp  qed autoqed simp    lemma vals_insert [simp]:  "set (vals (insert a v xs)) = set (vals xs) ∪ {v}"  by (simp add: insert_def vals_add_Cons)lemma insert_v_push:  "set (vals (insert a v xs)) = set |PQ.push v a (pqueue xs)|"  by (simp add: vals_pqueue[symmetric])lemma vals_meld:  "set (dfs val (meld xs ys)) = set (dfs val xs) ∪ set (dfs val ys)"proof (induct xs ys rule: meld.induct)  case (3 xs y ys) then show ?case  using set_dfs_Cons[of val y "meld xs ys"] using set_dfs_Cons[of val y ys] by autonext  case (4 x xs ys) then show ?case  using set_dfs_Cons[of val x "meld xs ys"] using set_dfs_Cons[of val x xs] by autonext  case (5 x xs y ys) then show ?case by (auto simp add: vals_add_Cons)qed simp_alllemma vals_meld_distinct:  "distinct (dfs val xs) ==> distinct (dfs val ys) ==>   set (dfs val xs) ∩ set (dfs val ys) = {} ==>   distinct (dfs val (meld xs ys))"proof (induct xs ys rule: meld.induct)  case (3 xs y ys) then show ?case  proof (cases y)    case None with "3" show ?thesis by simp  next    case (Some t)    from "3" have A: "set (vals xs) ∩ set (vals ys) = {}"      using set_dfs_Cons[of val y ys] by auto     moreover    from Some "3" have "set (bt_dfs val t) ∩ set (vals xs) = {}" by auto    moreover    from Some "3" have "set (bt_dfs val t) ∩ set (vals ys) = {}" by simp    ultimately have "set (bt_dfs val t) ∩ set (vals (meld xs ys)) = {}"      by (auto simp add: vals_meld)    with "3" Some show ?thesis by auto  qednext  case (4 x xs ys) then show ?case  proof (cases x)    case None with "4" show ?thesis by simp  next    case (Some t)    from "4" have "set (vals xs) ∩ set (vals ys) = {}"      using set_dfs_Cons[of val x xs] by auto     moreover    from Some "4" have "set (bt_dfs val t) ∩ set (vals xs) = {}" by simp    moreover    from Some "4" have "set (bt_dfs val t) ∩ set (vals ys) = {}" by auto    ultimately have "set (bt_dfs val t) ∩ set (vals (meld xs ys)) = {}"      by (auto simp add: vals_meld)    with "4" Some show ?thesis by auto  qednext  case (5 x xs y ys) then  have "set (vals xs) ∩ set (vals ys) = {}" by (auto simp add: set_dfs_Cons)  with "5" have "distinct (vals (meld xs ys))" by simp  moreover  from "5" have "set (bt_dfs val x) ∩ set (bt_dfs val y) = {}" by auto  with "5" have "distinct (bt_dfs val (merge x y))"    by (simp add: vals_merge_distinct)  moreover  from "5" have "set (vals (meld xs ys)) ∩ set (bt_dfs val (merge x y)) = {}"    by (auto simp add: vals_meld)  ultimately show ?case by (simp add: vals_add_distinct)qed simp_alllemma bt_augment_alist_subset:  "set (PQ.alist_of q) ⊆ set (PQ.alist_of (bt_augment t q))"  "set (PQ.alist_of q) ⊆ set (PQ.alist_of (bts_augment ts q))"proof (induct t and ts arbitrary: q and q)  case (Node a v rs)  show ?case using Node[of q] by (auto simp add: bt_augment_simp set_insort)qed autolemma bt_augment_alist_in:  "(v,a) ∈ set (PQ.alist_of q) ==> (v,a) ∈ set (PQ.alist_of (bt_augment t q))"  "(v,a) ∈ set (PQ.alist_of q) ==> (v,a) ∈ set (PQ.alist_of (bts_augment ts q))"  using bt_augment_alist_subset[of q] by autolemma bt_augment_alist_union:  "distinct (bts_dfs val (r # [t])) ==>    set (bts_dfs val (r # [t])) ∩ set |q| = {} ==>    set (PQ.alist_of (bt_augment t (bt_augment r q))) =     set (PQ.alist_of (bt_augment t q)) ∪ set (PQ.alist_of (bt_augment r q))"    "distinct (bts_dfs val (r # ts)) ==>    set (bts_dfs val (r # ts)) ∩ set |q| = {} ==>    set (PQ.alist_of (bts_augment ts (bt_augment r q))) =     set (PQ.alist_of (bts_augment ts q)) ∪ set (PQ.alist_of (bt_augment r q))"proof (induct t and ts arbitrary: q r and q r)  case Nil_bintree   from bt_augment_alist_subset[of q] show ?case by autonext  case (Node a v rs) then  have    "set (PQ.alist_of (bts_augment rs (bt_augment r q))) =     set (PQ.alist_of (bts_augment rs q)) ∪ set (PQ.alist_of (bt_augment r q))"     by simp  moreover  from Node.prems have *: "v ∉ set |bts_augment rs q| ∪ set |bt_augment r q|" unfolding bt_val_augment[symmetric] by simp  hence "v ∉ set |bts_augment rs (bt_augment r q)|" by (unfold bt_augment_v_union)  moreover  from * have "v ∉ set |bts_augment rs q|" by simp  ultimately show ?case by (simp add: set_insort)next  case (Cons_bintree x xs) then  have -- "FIXME: ugly... and slow"    "distinct (bts_dfs val (x # xs))" and    "distinct (bts_dfs val (r # xs))" and    "distinct (bts_dfs val [r,x])" and    "set (bts_dfs val (x # xs)) ∩ set |bt_augment r q| = {}" and    "set (bts_dfs val (x # xs)) ∩ set |q| = {}" and    "set (bts_dfs val [r, x]) ∩ set |q| = {}" and    "set (bts_dfs val (r # xs)) ∩ set |q| = {}"    unfolding bt_val_augment[symmetric] by auto  with Cons_bintree.hyps show ?case by autoqedlemma bt_alist_augment:  "distinct (bt_dfs val t) ==>    set (bt_dfs val t) ∩ set |q| = {} ==>    set (bt_dfs alist t) ∪ set (PQ.alist_of q) = set (PQ.alist_of (bt_augment t q))"    "distinct (bts_dfs val ts) ==>    set (bts_dfs val ts) ∩ set |q| = {} ==>    set (bts_dfs alist ts) ∪ set (PQ.alist_of q) =     set (PQ.alist_of (bts_augment ts q))"proof (induct t and ts)  case Nil_bintree then show ?case by simpnext  case (Node a v rs)  hence "v ∉ set |bts_augment rs q|"    unfolding bt_val_augment[symmetric] by simp  with Node show ?case by (simp add: set_insort)next  case (Cons_bintree r rs) then  have "set (PQ.alist_of (bts_augment (r # rs) q)) =    set (PQ.alist_of (bts_augment rs q)) ∪ set (PQ.alist_of (bt_augment r q))"    using bt_augment_alist_union by simp  with Cons_bintree bt_augment_alist_subset show ?case by autoqedlemma alist_pqueue:  "distinct (vals xs) ==> set (dfs alist xs) = set (PQ.alist_of (pqueue xs))"  by (induct xs) (simp_all add: vals_pqueue bt_alist_augment)lemma alist_pqueue_priority:  "distinct (vals xs) ==> (v, a) ∈ set (dfs alist xs)    ==> PQ.priority (pqueue xs) v = Some a"  by (simp add: alist_pqueue PQ.priority_def)lemma prios_pqueue:  "distinct (vals xs) ==> set (prios xs) = set \<parallel>pqueue xs\<parallel>"  by (auto simp add: alist_pqueue priorities_set alist_split_set)lemma alist_merge [simp]:  "distinct (bt_dfs val t) ==> distinct (bt_dfs val r) ==>   set (bt_dfs val t) ∩ set (bt_dfs val r) = {} ==>    set (bt_dfs alist (merge t r)) = set (bt_dfs alist t) ∪ set (bt_dfs alist r)"  by (auto simp add: bt_dfs_simp merge_def alist_split)lemma alist_add_Cons:  assumes "distinct (vals (x#xs))"  shows "set (dfs alist (add x xs)) = set (dfs alist (x # xs))"using assms proof (induct xs arbitrary: x)  case Empty then show ?case by (cases x) simp_allnext  case None then show ?case by (cases x) simp_allnext  case (Some y ys) then  show ?case   proof (cases x)    case (Some t)    note prem = Some.prems Some        from prem have "distinct (bt_dfs val (merge t y))"      by (auto simp add: bt_dfs_simp merge_def)    with prem have "distinct (vals (Some (merge t y) # ys))" by auto    with prem Some.hyps      have "set (dfs alist (add (Some (merge t y)) ys)) =        set (dfs alist (Some (merge t y) # ys))" by simp    moreover    from prem have "set (bt_dfs val t) ∩ set (bt_dfs val y) = {}" by auto    with prem      have "set (bt_dfs alist (merge t y)) =        set (bt_dfs alist t) ∪ set (bt_dfs alist y)"      by simp    moreover note prem and Un_assoc          ultimately    show ?thesis by simp  qed simpqedlemma alist_insert [simp]:  "distinct (vals xs) ==>    v ∉ set (vals xs) ==>   set (dfs alist (insert a v xs)) = set (dfs alist xs) ∪ {(v,a)}"  by (simp add: insert_def alist_add_Cons)lemma insert_push:  "distinct (vals xs) ==>   v ∉ set (vals xs) ==>   set (dfs alist (insert a v xs)) = set (PQ.alist_of (PQ.push v a (pqueue xs)))"  by (simp add: alist_pqueue vals_pqueue set_insort)lemma insert_p_push:  assumes "distinct (vals xs)"  and "v ∉ set (vals xs)"  shows "set (prios (insert a v xs)) = set \<parallel>PQ.push v a (pqueue xs)\<parallel>"proof -  from assms    have "set (dfs alist (insert a v xs)) =      set (PQ.alist_of (PQ.push v a (pqueue xs)))"    by (rule insert_push)  thus ?thesis by (simp add: alist_split_set priorities_set)qedlemma empty_empty:  "normalized xs ==> xs = empty <-> PQ.is_empty (pqueue xs)"proof (rule iffI)  assume "xs = []" then show "PQ.is_empty (pqueue xs)" by simpnext  assume N: "normalized xs" and E: "PQ.is_empty (pqueue xs)"  show "xs = []"  proof (rule ccontr)    assume "xs ≠ []"    with N have "set (vals xs) ≠ {}"      by (induct xs) (simp_all add: bt_dfs_simp dfs_append)    hence "set |pqueue xs| ≠ {}" by (simp add: vals_pqueue)    moreover    from E have "set |pqueue xs| = {}" by (simp add: is_empty_empty)        ultimately show False by simp  qedqed  lemma bt_dfs_Min_priority:  assumes "is_heap t"  shows "priority t = Min (set (bt_dfs priority t))"using assmsproof (induct "priority t" "children t" arbitrary: t)  case is_heap_list_Nil then show ?case by (simp add: bt_dfs_simp)next  case (is_heap_list_Cons rs r t) note cons = this  let ?M = "Min (set (bt_dfs priority t))"    obtain t' where "t' = Node (priority t) (val t) rs" by auto  hence ot: "rs = children t'" "priority t' = priority t" by simp_all  with is_heap_list_Cons have "priority t = Min (set (bt_dfs priority t'))"    by simp  with ot    have "priority t = Min (Set.insert (priority t) (set (bts_dfs priority rs)))"    by (simp add: bt_dfs_simp)  moreover  from cons have "priority r = Min (set (bt_dfs priority r))" by simp  moreover  from cons have "children t = r # rs" by simp  then have "bts_dfs priority (children t) =    (bt_dfs priority r) @ (bts_dfs priority rs)" by simp  hence "bt_dfs priority t =    priority t # (bt_dfs priority r @ bts_dfs priority rs)"    by (simp add: bt_dfs_simp)  hence A: "?M = Min    (Set.insert (priority t) (set (bt_dfs priority r) ∪ set (bts_dfs priority rs)))"    by simp    have "Set.insert (priority t) (set (bt_dfs priority r)    ∪ set (bts_dfs priority rs)) =    Set.insert (priority t) (set (bts_dfs priority rs)) ∪ set (bt_dfs priority r)"    by auto  with A have "?M = Min    (Set.insert (priority t) (set (bts_dfs priority rs)) ∪ set (bt_dfs priority r))"    by simp    with Min_Un    [of "Set.insert (priority t) (set (bts_dfs priority rs))" "set (bt_dfs priority r)"]   have "?M =    ord_class.min (Min (Set.insert (priority t) (set (bts_dfs priority rs))))      (Min (set (bt_dfs priority r)))"     by (auto simp add: bt_dfs_simp)  ultimately   have "?M = ord_class.min (priority t) (priority r)" by simp  with priority t ≤ priority r show ?case by (auto simp add: ord_class.min_def)qedlemma is_binqueue_min_Min_prios:  assumes "is_binqueue l xs"  and "normalized xs"  and "xs ≠ []"  shows "min xs = Some (Min (set (prios xs)))"using assmsproof (induct xs)  case (Some l xs x) then show ?case  proof (cases "xs ≠ []")    case False with Some show ?thesis      using bt_dfs_Min_priority[of x] by (simp add: min_single)  next    case True note T = this Some        from T have "normalized xs" by simp    with xs ≠ [] have "prios xs ≠ []" by (induct xs) (simp_all add: bt_dfs_simp)    with T show ?thesis      using Min_Un[of "set (bt_dfs priority x)" "set (prios xs)"]      using bt_dfs_Min_priority[of x]      by (auto simp add: bt_dfs_simp ord_class.min_def)  qedqed simp_all  lemma min_p_min:  assumes "is_binqueue l xs"  and "xs ≠ []"  and "normalized xs"  and "distinct (vals xs)"  and "distinct (prios xs)"  shows "min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))"proof -  from xs ≠ [] normalized xs have "¬ PQ.is_empty (pqueue xs)"    by (simp add: empty_empty)  moreover  from assms have "min xs = Some (Min (set (prios xs)))"    by (simp add: is_binqueue_min_Min_prios)  with distinct (vals xs) have "min xs = Some (Min (set \<parallel>pqueue xs\<parallel> ))"    by (simp add: prios_pqueue)  ultimately show ?thesis   by (simp add: priority_Min_priorities [where q = "pqueue xs"] )qedlemma find_min_p_min:  assumes "is_binqueue l xs"  and "xs ≠ []"  and "normalized xs"  and "distinct (vals xs)"  and "distinct (prios xs)"  shows "priority (the (find_min xs)) =    the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))"proof -  from assms have "min xs ≠ None" by (simp add: normalized_min_not_None)  from assms have "min xs = PQ.priority (pqueue xs) (PQ.min (pqueue xs))"    by (simp add: min_p_min)  with min xs ≠ None show ?thesis by (auto simp add: min_eq_find_min_Some)qedlemma find_min_v_min:  assumes "is_binqueue l xs"  and "xs ≠ []"  and "normalized xs"  and "distinct (vals xs)"  and "distinct (prios xs)"  shows "val (the (find_min xs)) = PQ.min (pqueue xs)"proof -  from assms have "min xs ≠ None" by (simp add: normalized_min_not_None)  then obtain a where oa: "Some a = min xs" by auto  then obtain t where ot: "find_min xs = Some t" "priority t = a"    using min_eq_find_min_Some [of xs a] by auto      hence *: "(val t, a) ∈ set (dfs alist xs)"    by (auto simp add: find_min_exist in_set_in_alist)  have "PQ.min (pqueue xs) = val t"  proof (rule ccontr)        assume A: "PQ.min (pqueue xs) ≠ val t"    then obtain t' where ot':"PQ.min (pqueue xs) = t'" by simp    with A have NE: "val t ≠ t'" by simp        from ot' oa assms have "(t', a) ∈ set (dfs alist xs)"      by (simp add: alist_pqueue PQ.priority_def min_p_min)    with * NE have "¬ distinct (prios xs)"       unfolding alist_split(2)       unfolding dfs_comp       by (induct ("dfs alist xs")) (auto simp add: rev_image_eqI)    with distinct (prios xs) show False by simp  qed  with ot show ?thesis by autoqedlemma alist_normalize_idem:  "dfs alist (normalize xs) = dfs alist xs"unfolding normalize_defproof (induct xs rule: rev_induct)  case (snoc x xs) then show ?case by (cases x) (simp_all add: dfs_append)qed simplemma dfs_match_not_in:  "(∀ t. Some t ∈ set xs --> priority t ≠ a) ==>    set (dfs f (map (match a) xs)) = set (dfs f xs)"by (induct xs) simp_alllemma dfs_match_subset:  "set (dfs f (map (match a) xs)) ⊆ set (dfs f xs)"proof (induct xs rule: list.induct)  case (Cons x xs) then show ?case by (cases x) autoqed simplemma dfs_match_distinct:  "distinct (dfs f xs) ==> distinct (dfs f (map (match a) xs))"proof (induct xs rule: list.induct)  case (Cons x xs) then show ?case    using dfs_match_subset[of f a xs]    by (cases x, auto)qed simplemma dfs_match:  "distinct (prios xs) ==>    distinct (dfs f xs) ==>   Some t ∈ set xs ==>    priority t = a ==>    set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)"proof (induct xs arbitrary: t)  case (Some r xs t) then show ?case   proof (cases "t = r")    case True     from Some have "priority r ∉ set (prios xs)" by (auto simp add: bt_dfs_simp)    with Some True have "a ∉ set (prios xs)" by simp    hence "∀ s. Some s ∈ set xs --> priority s ≠ a"      by (induct xs) (auto simp add: bt_dfs_simp)    hence "set (dfs f (map (match a) xs)) = set (dfs f xs)"      by (simp add: dfs_match_not_in)    with True Some show ?thesis by auto  next    case False    with Some.prems have "Some t ∈ set xs" by simp    with priority t = a have "a ∈ set (prios xs)"    proof (induct xs)      case (Some x xs) then show ?case        by (cases "t = x") (simp_all add: bt_dfs_simp)    qed simp_all    with False Some have "priority r ≠ a" by (auto simp add: bt_dfs_simp)    moreover     from Some False      have "set (dfs f (map (match a) xs)) = set (dfs f xs) - set (bt_dfs f t)"      by simp    moreover    from Some.prems False have "set (bt_dfs f t) ∩ set (bt_dfs f r) = {}"      by (induct xs) auto    hence "set (bt_dfs f r) - set (bt_dfs f t) = set (bt_dfs f r)" by auto        ultimately show ?thesis by auto  qedqed simp_alllemma alist_meld:  "distinct (dfs val xs) ==> distinct (dfs val ys) ==>   set (dfs val xs) ∩ set (dfs val ys) = {} ==>   set (dfs alist (meld xs ys)) = set (dfs alist xs) ∪ set (dfs alist ys)"proof (induct xs ys rule: meld.induct)  case (3 xs y ys)  have "set (dfs alist (y # meld xs ys)) =    set (dfs alist xs) ∪ set (dfs alist (y # ys))"  proof -    note assms = "3"    from assms have "set (vals xs) ∩ set (vals ys) = {}"      using set_dfs_Cons[of val y ys] by auto    moreover    from assms have "distinct (vals ys)" by (cases y) simp_all    moreover    from assms have "distinct (vals xs)" by simp    moreover note assms    ultimately have "set (dfs alist (meld xs ys)) =      set (dfs alist xs) ∪ set (dfs alist ys)" by simp        hence "set (dfs alist (y # meld xs ys)) =      set (dfs alist [y]) ∪ set (dfs alist xs) ∪ set (dfs alist ys)"      using set_dfs_Cons[of alist y "meld xs ys"] by auto    then show ?thesis using set_dfs_Cons[of alist y ys] by auto  qed  thus ?case by simpnext  case (4 x xs ys)  have "set (dfs alist (x # meld xs ys)) =    set (dfs alist (x # xs)) ∪ set (dfs alist ys)"  proof - (* this is the same as for 3 minus some renaming *)    note assms = "4"    from assms have "set (vals xs) ∩ set (vals ys) = {}"      using set_dfs_Cons[of val x xs] by auto    moreover    from assms have "distinct (vals xs)" by (cases x) simp_all    moreover    from assms have "distinct (vals ys)" by simp    moreover note assms    ultimately have "set (dfs alist (meld xs ys)) =      set (dfs alist xs) ∪ set (dfs alist ys)" by simp        hence "set (dfs alist (x # meld xs ys)) =      set (dfs alist [x]) ∪ set (dfs alist xs) ∪ set (dfs alist ys)"      using set_dfs_Cons[of alist x "meld xs ys"] by auto    then show ?thesis using set_dfs_Cons[of alist x xs] by auto  qed  thus ?case by simpnext  case (5 x xs y ys)  have "set (dfs alist (add (Some (merge x y)) (meld xs ys))) =    set (bt_dfs alist x) ∪ set (dfs alist xs)    ∪ set (bt_dfs alist y) ∪ set (dfs alist ys)"  proof -    note assms = "5"        from assms have "distinct (bt_dfs val x)" "distinct (bt_dfs val y)" by simp_all    moreover from assms have xyint:      "set (bt_dfs val x) ∩ set (bt_dfs val y) = {}" by (auto simp add: set_dfs_Cons)    ultimately have *: "set (dfs alist [Some (merge x y)]) =      set (bt_dfs alist x) ∪ set (bt_dfs alist y)" by auto    moreover    from assms      have **: "set (dfs alist (meld xs ys)) = set (dfs alist xs) ∪ set (dfs alist ys)"      by (auto simp add: set_dfs_Cons)    moreover    from assms have "distinct (vals (Some (merge x y) # meld xs ys))"    proof -      from assms xyint have "distinct (bt_dfs val (merge x y))"        by (simp add: vals_merge_distinct)      moreover      from assms have         "distinct (vals xs)"         and "distinct (vals ys)"         and "set (vals xs) ∩ set (vals ys) = {}"        by (auto simp add: set_dfs_Cons)      hence "distinct (vals (meld xs ys))" by (rule vals_meld_distinct)      moreover      from assms        have "set (bt_dfs val (merge x y)) ∩ set (vals (meld xs ys)) = {}"        by (auto simp add: vals_meld)      ultimately show ?thesis by simp    qed       ultimately show ?thesis by (auto simp add: alist_add_Cons)  qed  thus ?case by autoqed simp_alllemma alist_delete_min:  assumes "distinct (vals xs)"  and "distinct (prios xs)"  and "find_min xs = Some (Node a v ts)"  shows "set (dfs alist (delete_min xs)) = set (dfs alist xs) - {(v, a)}"proof -  from distinct (vals xs) have d: "distinct (dfs alist xs)"    using dfs_comp_distinct[of fst alist "xs"]    by (simp only: alist_split)  from assms have IN: "Some (Node a v ts) ∈ set xs"    by (simp add: find_min_exist)  hence sub: "set (bts_dfs alist ts) ⊆ set (dfs alist xs)"    by (induct xs) (auto simp add: bt_dfs_simp)  from d IN have "(v,a) ∉ set (bts_dfs alist ts)"    using dfs_distinct_member[of alist xs "Node a v ts"] by simp  with sub have "set (bts_dfs alist ts) ⊆ set (dfs alist xs) - {(v,a)}" by blast  hence nu: "set (bts_dfs alist ts) ∪ (set (dfs alist xs) - {(v,a)}) =    set (dfs alist xs) - {(v,a)}" by auto  from assms have "distinct (vals (map (match a) xs))"    by (simp add: dfs_match_distinct)   moreover    from IN assms have "distinct (bts_dfs val ts)"    using dfs_distinct_member[of val xs "Node a v ts"]    by (simp add: bt_dfs_distinct_children)  hence "distinct (vals (map Some (rev ts)))"    by (simp add: bts_dfs_rev_distinct dfs_map_Some_idem)  moreover  from assms IN have "set (dfs val (map (match a) xs)) =    set (dfs val xs) - set (bt_dfs val (Node a v ts))"    by (simp add: dfs_match)  hence "set (vals (map (match a) xs)) ∩ set (vals (map Some (rev ts))) = {}"    by (auto simp add: dfs_map_Some_idem set_bts_dfs_rev)  ultimately  have "set (dfs alist (meld (map Some (rev ts)) (map (match a) xs))) =    set (dfs alist (map Some (rev ts))) ∪ set (dfs alist (map (match a) xs))"    using alist_meld by auto  with assms d IN nu show ?thesis    by (simp add: delete_min_def alist_normalize_idem set_bts_dfs_rev dfs_map_Some_idem     dfs_match Diff_insert2 [of "set (dfs alist xs)" "(v,a)" "set (bts_dfs alist ts)"])qedlemma alist_remove_min:  assumes "is_binqueue l xs"  and "distinct (vals xs)"  and "distinct (prios xs)"  and "normalized xs"  and "xs ≠ []"  shows "set (dfs alist (delete_min xs)) =  set (PQ.alist_of (PQ.remove_min (pqueue xs)))"proof -  from assms obtain t where ot: "find_min xs = Some t"    using normalized_find_min_exists by auto  with assms show ?thesis  proof (cases t)    case (Node a v ys)    from assms have "¬ PQ.is_empty (pqueue xs)" by (simp add: empty_empty)    hence "set (PQ.alist_of (PQ.remove_min (pqueue xs))) =      set (PQ.alist_of (pqueue xs)) - {(PQ.min (pqueue xs),        the (PQ.priority (pqueue xs) (PQ.min (pqueue xs))))}"      by (simp add: set_alist_of_remove_min[of "pqueue xs"] del: alist_of_remove_min)        moreover    from assms ot Node    have "set (dfs alist (delete_min xs)) = set (dfs alist xs) - {(v, a)}"      using alist_delete_min[of xs] by simp    moreover    from Node ot have "priority (the (find_min xs)) = a" by simp    with assms have "a = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))"      by (simp add: find_min_p_min)    moreover    from Node ot have "val (the (find_min xs)) = v" by simp    with assms have "v = PQ.min (pqueue xs)" by (simp add: find_min_v_min)        moreover note distinct (vals xs)    ultimately show ?thesis by (simp add: alist_pqueue)  qedqedno_notation  "PQ.values" ("|(_)|")  and "PQ.priorities" ("\<parallel>(_)\<parallel>")end