(* Author: Tobias Nipkow *)

theory Leftist_Heap_List
imports
  Leftist_Heap
  Complex_Main
begin

subsection "Converting a list into a leftist heap"

fun merge_adj :: "('a::ord) lheap list → 'a lheap list" where
"merge_adj [] = []" |
"merge_adj [t] = [t]" |
"merge_adj (t1 # t2 # ts) = merge t1 t2 # merge_adj ts"

text ‹For the termination proof of ‹merge_all› below.›
lemma length_merge_adjacent[termination_simp]: "length (merge_adj ts) = (length ts + 1) div 2"
by (induction ts rule: merge_adj.induct) auto

fun merge_all :: "('a::ord) lheap list → 'a lheap" where
"merge_all [] = Leaf" |
"merge_all [t] = t" |
"merge_all ts = merge_all (merge_adj ts)"


subsubsection ‹Functional correctness›

lemma heap_merge_adj: "∀t ∈ set ts. heap t ==> ∀t ∈ set (merge_adj ts). heap t"
by(induction ts rule: merge_adj.induct) (auto simp: heap_merge)

lemma ltree_merge_adj: "∀t ∈ set ts. ltree t ==> ∀t ∈ set (merge_adj ts). ltree t"
by(induction ts rule: merge_adj.induct) (auto simp: ltree_merge)

lemma heap_merge_all: "∀t ∈ set ts. heap t ==> heap (merge_all ts)"
apply(induction ts rule: merge_all.induct)
using [[simp_depth_limit=3]] by (auto simp add: heap_merge_adj)

lemma ltree_merge_all: "∀t ∈ set ts. ltree t ==> ltree (merge_all ts)"
apply(induction ts rule: merge_all.induct)
using [[simp_depth_limit=3]] by (auto simp add: ltree_merge_adj)

lemma mset_merge_adj:
  "∑_# (image_mset mset_tree (mset (merge_adj ts))) =
   ∑_# (image_mset mset_tree (mset ts))"
by(induction ts rule: merge_adj.induct) (auto simp: mset_merge)

lemma mset_merge_all:
  "mset_tree (merge_all ts) = ∑_# (mset (map mset_tree ts))"
by(induction ts rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)

fun lheap_list :: "'a::ord list → 'a lheap" where
"lheap_list xs = merge_all (map (λx. Node Leaf (x,1) Leaf) xs)"

lemma mset_lheap_list: "mset_tree (lheap_list xs) = mset xs"
by (simp add: mset_merge_all o_def)

lemma ltree_lheap_list: "ltree (lheap_list ts)"
by(simp add: ltree_merge_all)

lemma heap_lheap_list: "heap (lheap_list ts)"
by(simp add: heap_merge_all)

lemma size_merge: "size(merge t1 t2) = size t1 + size t2"
by(induction t1 t2 rule: merge.induct) (auto simp: node_def)


subsubsection ‹Running time›

text ‹Not defined automatically because we only count the time for @{const merge}.›

fun T_merge_adj :: "('a::ord) lheap list → nat" where
"T_merge_adj [] = 0" |
"T_merge_adj [t] = 0" |
"T_merge_adj (t1 # t2 # ts) = T_merge t1 t2 + T_merge_adj ts"

fun T_merge_all :: "('a::ord) lheap list → nat" where
"T_merge_all [] = 0" |
"T_merge_all [t] = 0" |
"T_merge_all ts = T_merge_adj ts + T_merge_all (merge_adj ts)"

fun T_lheap_list :: "'a::ord list → nat" where
"T_lheap_list xs = T_merge_all (map (λx. Node Leaf (x,1) Leaf) xs)"

abbreviation Tm where
"Tm n == 2 * log 2 (n+1) + 1"

lemma T_merge_adj: "[ ∀t ∈ set ts. ltree t; ∀t ∈ set ts. size t = n ]
  ==> T_merge_adj ts ≤ (length ts div 2) * Tm n"
proof(induction ts rule: T_merge_adj.induct)
  case 1 thus ?case by simp
next
  case 2 thus ?case by simp
next
  case (3 t1 t2) thus ?case using T_merge_log[of t1 t2] by (simp add: algebra_simps size1_size)
qed

lemma size_merge_adj:
  "[ even(length ts); ∀t ∈ set ts. ltree t; ∀t ∈ set ts. size t = n ]
   ==> ∀t ∈ set (merge_adj ts). size t = 2*n"
by(induction ts rule: merge_adj.induct) (auto simp: size_merge)

lemma T_merge_all:
 "[ ∀t ∈ set ts. ltree t; ∀t ∈ set ts. size t = n; length ts = 2^k ]
  ==> T_merge_all ts ≤ (∑i=1..k. 2^(k-i) * Tm(2 ^ (i-1) * n))"
proof (induction ts arbitrary: k n rule: merge_all.induct)
  case 1 thus ?case by simp
next
  case 2 thus ?case by simp
next
  case (3 t1 t2 ts)
  let ?ts = "t1 # t2 # ts"
  let ?ts2 = "merge_adj ?ts"
  obtain k' where k': "k = Suc k'" using "3.prems"(3)
    by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust)
  have 1: "∀x ∈ set(merge_adj ?ts). ltree x"
    by(rule ltree_merge_adj[OF "3.prems"(1)])
  have "even (length ts)" using "3.prems"(3) even_Suc_Suc_iff by fastforce
  from "3.prems"(2) size_merge_adj[OF this] "3.prems"(1)
  have 2: "∀x ∈ set(merge_adj ?ts). size x = 2*n" by(auto simp: size_merge)
  have 3: "length ?ts2 = 2 ^ k'" using "3.prems"(3) k' by (simp add: length_merge_adjacent)
  have 4: "length ?ts div 2 = 2 ^ k'"
    using "3.prems"(3) k' by(simp add: power_eq_if[of 2 k] split: if_splits)
  have "T_merge_all ?ts = T_merge_adj ?ts + T_merge_all ?ts2" by simp
  also have "… ≤ 2^k' * Tm n + T_merge_all ?ts2"
    using 4 T_merge_adj[OF "3.prems"(1,2)] by auto
  also have "… ≤ 2^k' * Tm n + (∑i=1..k'. 2^(k'-i) * Tm(2 ^ (i-1) * (2*n)))"
    using "3.IH"[OF 1 2 3] by simp
  also have "… = 2^k' * Tm n + (∑i=1..k'. 2^(k'-i) * Tm(2 ^ (Suc(i-1)) * n))"
    by (simp add: mult_ac cong del: sum.cong)
  also have "… = 2^k' * Tm n + (∑i=1..k'. 2^(k'-i) * Tm(2 ^ i * n))"
     by (simp)
  also have "… = (∑i=1..k. 2^(k-i) * Tm(2 ^ (i-1) * real n))"
    by(simp add: sum.atLeast_Suc_atMost[of "Suc 0" "Suc k'"] sum.atLeast_Suc_atMost_Suc_shift[of _ "Suc 0"] k'
        del: sum.cl_ivl_Suc)
  finally show ?case .
qed

lemma summation: "(∑i=1..k. 2^(k-i) * ((2::real)*i+1)) = 5*2^k - (2::real)*k - 5"
proof (induction k)
  case 0 thus ?case by simp
next
  case (Suc k)
  have "(∑i=1..Suc k. 2^(Suc k - i) * ((2::real)*i+1))
    = (∑i=1..k. 2^(k+1-i) * ((2::real)*i+1)) + 2*k+3"
    by(simp)
  also have "… = (∑i=1..k. (2::real)*(2^(k-i) * ((2::real)*i+1))) + 2*k+3"
    by (simp add: Suc_diff_le mult.assoc)
  also have "… = 2*(∑i=1..k. 2^(k-i) * ((2::real)*i+1)) + 2*k+3"
    by(simp add: sum_distrib_left)
  also have "… = (2::real)*(5*2^k - (2::real)*k - 5) + 2*k+3"
    using Suc.IH by simp
  also have "… = 5*2^(Suc k) - (2::real)*(Suc k) - 5"
    by simp
  finally show ?case .
qed

lemma T_lheap_list: assumes "length xs = 2 ^ k"
shows "T_lheap_list xs ≤ 5 * length xs - 2 * log 2 (length xs)"
proof -
  let ?ts = "map (λx. Node Leaf (x,1) Leaf) xs"
  have "T_lheap_list xs = T_merge_all ?ts" by simp
  also have "… ≤ (∑i = 1..k. 2^(k-i) * (2 * log 2 (2^(i-1) + 1) + 1))"
    using T_merge_all[of ?ts 1 k] assms by (simp)
  also have "… ≤ (∑i = 1..k. 2^(k-i) * (2 * log 2 (2*2^(i-1)) + 1))"
    apply(rule sum_mono)
    using zero_le_power[of "2::real"] by (simp add: add_pos_nonneg)
  also have "… = (∑i = 1..k. 2^(k-i) * (2 * log 2 (2^(1+(i-1))) + 1))"
    by (simp del: Suc_pred)
  also have "… = (∑i = 1..k. 2^(k-i) * (2 * log 2 (2^i) + 1))"
    by (simp)
  also have "… = (∑i = 1..k. 2^(k-i) * ((2::real)*i+1))"
    by (simp add:log_nat_power algebra_simps)
  also have "… = 5*(2::real)^k - (2::real)*k - 5"
    using summation by (simp)
  finally show ?thesis
    using assms of_nat_le_iff by simp
qed

end