Quelle Leftist_Heap_List.thy Sprache: Isabelle

(* 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 \<open>For the termination proof of \<open>merge_all\<close> below.\<close>
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 \<open>Functional correctness\<close>

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:
  "\\<^sub># (image_mset mset_tree (mset (merge_adj ts))) =
   \<Sum>\<^sub># (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) = \\<^sub># (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 \<open>Running time\<close>

text \<open>Not defined automatically because we only count the time for @{const merge}.\<close>

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 \
  \<Longrightarrow> T_merge_adj ts \<le> (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 \
   \<Longrightarrow> \<forall>t \<in> 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 \
  \<Longrightarrow> T_merge_all ts \<le> (\<Sum>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))
    = (\<Sum>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

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.